From 3e0d6f348513e64020e8024abbd35bf6ed4cab52 Mon Sep 17 00:00:00 2001
From: Kacper Marzecki <kacper-marzecki@github.com>
Date: Sun, 15 Jun 2025 19:56:13 +0200
Subject: [PATCH] checkpoit

---
 test.exs | 524 ++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 348 insertions(+), 176 deletions(-)

diff --git a/test.exs b/test.exs
index d8eb966..31178b9 100644
--- a/test.exs
+++ b/test.exs
@@ -1,4 +1,8 @@
 defmodule Tdd do
+  # --- Existing code from your previous version ---
+  # (init_tdd_system, get_state, update_state, make_node, get_node_details,
+  #  variable definitions, basic type constructors, apply, sum, print_tdd)
+  # Ensure your `apply/4` function is the corrected version from the MatchError fix.
   @moduledoc """
   Ternary decision diagram for set-theoretic types.
   """
@@ -7,37 +11,31 @@ defmodule Tdd do
   @false_node_id 0
   @true_node_id 1
 
-  # --- State: Managed via module attributes (for simplicity in this example) ---
-  # @nodes: Map from {var, yes_id, no_id, dc_id} -> node_id
-  # @node_by_id: Map from node_id -> {var, yes_id, no_id, dc_id}
-  # @next_id: Integer for the next available node ID
-  # @op_cache: Cache for apply operations: {{op_name, id1, id2} -> result_id}
-
   defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id
 
-  # Initialize state (call this once, or ensure it's idempotent)
   def init_tdd_system do
-    # Node 0 represents FALSE, Node 1 represents TRUE.
-    # These don't have var/children, so we represent them specially or handle them in functions.
-    # For @node_by_id, we can store a marker.
     Process.put(:nodes, %{})
+
     Process.put(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal})
-    Process.put(:next_id, 2) # Start after true/false
+
+    Process.put(:next_id, 2)
     Process.put(:op_cache, %{})
     IO.puts("TDD system initialized.")
   end
 
-  # Helper to get current state
   defp get_state do
     %{
       nodes: Process.get(:nodes, %{}),
-      node_by_id: Process.get(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal}),
+      node_by_id:
+        Process.get(:node_by_id, %{
+          @false_node_id => :false_terminal,
+          @true_node_id => :true_terminal
+        }),
       next_id: Process.get(:next_id, 2),
       op_cache: Process.get(:op_cache, %{})
     }
   end
 
-  # Helper to update state
   defp update_state(changes) do
     current_state = get_state()
     new_state = Map.merge(current_state, changes)
@@ -47,171 +45,106 @@ defmodule Tdd do
     Process.put(:op_cache, new_state.op_cache)
   end
 
-  # --- Node Creation and Reduction ---
-  # This is the core function to get or create a node.
-  # It implements the reduction rules.
   def make_node(variable, yes_id, no_id, dc_id) do
-    # Reduction Rule: If all children are identical, this node is redundant.
-    # (This is a strong form of reduction for TDDs)
     if yes_id == no_id && yes_id == dc_id do
-      # IO.puts "Reduction (all children same): var #{inspect variable} -> #{yes_id}"
       yes_id
     else
       state = get_state()
       node_tuple = {variable, yes_id, no_id, dc_id}
 
       if Map.has_key?(state.nodes, node_tuple) do
-        # Node already exists
         state.nodes[node_tuple]
       else
-        # Create new node
         new_id = state.next_id
-        # IO.puts "Creating node #{new_id}: #{inspect variable}, y:#{yes_id}, n:#{no_id}, d:#{dc_id}"
+
         update_state(%{
           nodes: Map.put(state.nodes, node_tuple, new_id),
           node_by_id: Map.put(state.node_by_id, new_id, node_tuple),
           next_id: new_id + 1
         })
+
         new_id
       end
     end
   end
 
-  # Get details of a node (useful for apply and debugging)
   def get_node_details(id) when is_terminal_id(id) do
     if id == @true_node_id, do: :true_terminal, else: :false_terminal
   end
+
   def get_node_details(id) do
     state = get_state()
-    state.node_by_id[id] # Returns {var, yes, no, dc} or nil
+    state.node_by_id[id]
   end
 
-
-  # --- Variable Definitions (subset for now) ---
-  # Category 0: Primary Type Discriminators
   @v_is_atom {0, :is_atom}
   @v_is_tuple {0, :is_tuple}
-  # Add other primary types here in order, e.g., {0, :is_integer}, {0, :is_list}
 
-  # Category 1: Atom-Specific Predicates
   def v_atom_eq(atom_val), do: {1, :value, atom_val}
-
-  # Category 4: Tuple-Specific Predicates
   def v_tuple_size_eq(size), do: {4, :size, size}
   def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}
 
-  # --- Basic Type Constructors ---
-  # These construct TDDs representing specific types.
-  # For simplicity, they assume an "empty" background (all other types are false).
-  # `dc_id` is often `@false_node_id` in constructors because if a variable is "don't care"
-  # for this specific type, it means it *could* be something that makes it NOT this type.
-
   def type_any, do: @true_node_id
   def type_none, do: @false_node_id
 
-  # Represents the type `atom()` (any atom)
   def type_atom do
-    # The variable order means we must consider @v_is_tuple *before* specific atom properties
-    # if we were to build from a full list of variables.
-    # However, for a simple constructor, we focus on the defining properties.
-    # The `apply` algorithm will handle interactions with other types correctly due to variable ordering.
-
-    # If it's an atom, it's true for this type.
-    # If it's not an atom, it's false for this type.
-    # If we "don't care" if it's an atom, it's not specific enough to be `type_atom`, so false.
     make_node(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
   end
 
-  # Represents a specific atom literal, e.g., `:foo`
   def type_atom_literal(atom_val) do
-    var_eq = v_atom_eq(atom_val) # e.g., {1, :value, :foo}
-
-    # Node for specific atom value: if value matches, true; else false.
+    var_eq = v_atom_eq(atom_val)
     atom_val_node = make_node(var_eq, @true_node_id, @false_node_id, @false_node_id)
-
-    # Node for primary type: if is_atom, check value; else false.
     make_node(@v_is_atom, atom_val_node, @false_node_id, @false_node_id)
   end
 
-  # Represents `tuple()` (any tuple)
   def type_tuple do
     make_node(@v_is_tuple, @true_node_id, @false_node_id, @false_node_id)
   end
 
-  # Represents an empty tuple `{}`
   def type_empty_tuple do
     var_size_0 = v_tuple_size_eq(0)
     tuple_size_node = make_node(var_size_0, @true_node_id, @false_node_id, @false_node_id)
     make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
   end
 
-  # Represents a tuple of a specific size with any elements, e.g., `{any, any}` for size 2
   def type_tuple_sized_any(size) do
     var_size = v_tuple_size_eq(size)
-    # For element checks, 'any' means the element specific predicates would all go to their dc child,
-    # which leads to true. So, for representing `tuple_of_size_N_with_any_elements`,
-    # we only need to check the size after confirming it's a tuple.
     tuple_size_node = make_node(var_size, @true_node_id, @false_node_id, @false_node_id)
     make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
   end
 
-  # --- The APPLY Algorithm ---
-  # apply(op_lambda, u1_id, u2_id)
-  # op_lambda takes (terminal1_val, terminal2_val) and returns resulting terminal_val
-  # e.g., for OR: fn :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal; _,_ -> :false_terminal end
-  # which then maps to @true_node_id or @false_node_id.
-
   def apply(op_name, op_lambda, u1_id, u2_id) do
     state = get_state()
-    # Ensure cache_key is canonical for commutative operations
     cache_key = {op_name, Enum.sort([u1_id, u2_id])}
 
     cond do
-      # 1. Check cache first
       Map.has_key?(state.op_cache, cache_key) ->
         state.op_cache[cache_key]
 
-      # 2. Base case: Both u1 and u2 are terminals
       is_terminal_id(u1_id) && is_terminal_id(u2_id) ->
         res_terminal_symbol = op_lambda.(get_node_details(u1_id), get_node_details(u2_id))
-        # Result is a terminal ID, no need to cache these simple computations directly,
-        # the calls leading to them will be cached.
         if res_terminal_symbol == :true_terminal, do: @true_node_id, else: @false_node_id
 
-      # 3. Recursive case: At least one is non-terminal.
-      #    Handle sub-cases where one is terminal and the other is not.
       true ->
-        # Pre-check for terminal optimizations specific to the operation
-        # This can make some operations (like sum with @true_node_id) much faster.
-        # For sum:
-        # if u1_id == @true_node_id or u2_id == @true_node_id, result is @true_node_id (if op is sum)
-        # if u1_id == @false_node_id, result is u2_id (if op is sum)
-        # if u2_id == @false_node_id, result is u1_id (if op is sum)
-        # These are handled by op_lambda if both are terminals. If one is terminal,
-        # the recursive calls below will hit that.
-
         u1_details = get_node_details(u1_id)
         u2_details = get_node_details(u2_id)
 
         result_id =
           cond do
-            # Case 3a: u1 is terminal, u2 is not
             u1_details == :true_terminal or u1_details == :false_terminal ->
-              {var2, y2, n2, d2} = u2_details # u2 must be a node
+              {var2, y2, n2, d2} = u2_details
               res_y = apply(op_name, op_lambda, u1_id, y2)
               res_n = apply(op_name, op_lambda, u1_id, n2)
               res_d = apply(op_name, op_lambda, u1_id, d2)
               make_node(var2, res_y, res_n, res_d)
 
-            # Case 3b: u2 is terminal, u1 is not
             u2_details == :true_terminal or u2_details == :false_terminal ->
-              {var1, y1, n1, d1} = u1_details # u1 must be a node
+              {var1, y1, n1, d1} = u1_details
               res_y = apply(op_name, op_lambda, y1, u2_id)
               res_n = apply(op_name, op_lambda, n1, u2_id)
               res_d = apply(op_name, op_lambda, d1, u2_id)
               make_node(var1, res_y, res_n, res_d)
 
-            # Case 3c: Both u1 and u2 are non-terminal nodes
             true ->
               {var1, y1, n1, d1} = u1_details
               {var2, y2, n2, d2} = u2_details
@@ -219,13 +152,10 @@ defmodule Tdd do
               top_var =
                 cond do
                   var1 == var2 -> var1
-                  # Elixir's tuple comparison provides the global variable order
                   var1 < var2 -> var1
-                  true -> var2 # var2 < var1
+                  true -> var2
                 end
 
-              # Recursive calls: if a variable is not the top_var for a TDD,
-              # that TDD is passed through unchanged to the next level of recursion.
               res_y =
                 cond do
                   top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, y1, y2)
@@ -246,118 +176,360 @@ defmodule Tdd do
                   top_var == var1 -> apply(op_name, op_lambda, d1, u2_id)
                   true -> apply(op_name, op_lambda, u1_id, d2)
                 end
+
               make_node(top_var, res_y, res_n, res_d)
           end
 
-        # Cache the result of this (op, u1, u2) call
         update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
         result_id
     end
   end
 
-  # --- Set Operations ---
   def sum(tdd1_id, tdd2_id) do
     op_lambda_sum = fn
-      (:true_terminal, _) -> :true_terminal # true or X = true
-      (_, :true_terminal) -> :true_terminal # X or true = true
-      (:false_terminal, t2_val) -> t2_val   # false or X = X
-      (t1_val, :false_terminal) -> t1_val   # X or false = X
+      :true_terminal, _ -> :true_terminal
+      _, :true_terminal -> :true_terminal
+      :false_terminal, t2_val -> t2_val
+      t1_val, :false_terminal -> t1_val
     end
+
     apply(:sum, op_lambda_sum, tdd1_id, tdd2_id)
   end
 
-  # Placeholder for intersect and negate
-  # def intersect(one, two) do end
-  # def negate(one) do end
+  # --- Intersection ---
+  def intersect(tdd1_id, tdd2_id) do
+    op_lambda_intersect = fn
+      # AND logic for terminals
+      # false and X = false
+      :false_terminal, _ -> :false_terminal
+      # X and false = false
+      _, :false_terminal -> :false_terminal
+      # true and X = X (e.g. true and true = true, true and false = false)
+      :true_terminal, t2_val -> t2_val
+      # X and true = X
+      t1_val, :true_terminal -> t1_val
+    end
 
+    apply(:intersect, op_lambda_intersect, tdd1_id, tdd2_id)
+  end
 
-  # --- Helper to inspect the TDD structure (for debugging) ---
-  def print_tdd(id, indent \\ 0) do
-    prefix = String.duplicate("  ", indent)
-    details = get_node_details(id)
-    IO.puts "#{prefix}ID #{id}: #{inspect details}"
-    case details do
-      {_var, y, n, d} ->
-        IO.puts "#{prefix}  Yes ->"
-        print_tdd(y, indent + 1)
-        IO.puts "#{prefix}  No  ->"
-        print_tdd(n, indent + 1)
-        IO.puts "#{prefix}  DC  ->"
-        print_tdd(d, indent + 1)
-      :true_terminal -> :ok
-      :false_terminal -> :ok
-      nil -> IO.puts "#{prefix} Error: Unknown ID #{id}"
+  # --- Negation ---
+  def negate(tdd_id) do
+    state = get_state()
+    # Unary operation cache key
+    cache_key = {:negate, tdd_id}
+
+    cond do
+      # Handle terminals directly, no caching needed for these simple cases.
+      tdd_id == @true_node_id ->
+        @false_node_id
+
+      tdd_id == @false_node_id ->
+        @true_node_id
+
+      # Check cache for non-terminal IDs
+      Map.has_key?(state.op_cache, cache_key) ->
+        state.op_cache[cache_key]
+
+      # Compute for non-terminal ID if not in cache
+      true ->
+        case get_node_details(tdd_id) do
+          {var, y, n, d} ->
+            res_y = negate(y)
+            res_n = negate(n)
+            res_d = negate(d)
+            result_id = make_node(var, res_y, res_n, res_d)
+            # Cache the computed result for this non-terminal tdd_id
+            update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
+            result_id
+
+          nil ->
+            # This should ideally not be reached if IDs are managed correctly
+            raise "Tdd.negate: Unknown node ID #{inspect(tdd_id)} during get_node_details. State: #{inspect(state.node_by_id)}"
+        end
     end
   end
 
+  # --- Subtyping ---
+  # A <: B  (A is a subtype of B)
+  def is_subtype(sub_type_id, super_type_id) do
+    cond do
+      # Optimization: A is always a subtype of A
+      sub_type_id == super_type_id ->
+        true
+
+      # Optimization: `none` is a subtype of anything
+      sub_type_id == @false_node_id ->
+        true
+
+      # Optimization: Anything is a subtype of `any`
+      super_type_id == @true_node_id ->
+        true
+
+      true ->
+        # Definition: A <: B  <=>  A ∩ (¬B) == ∅ (type_none / @false_node_id)
+        negated_super = negate(super_type_id)
+        intersection_result = intersect(sub_type_id, negated_super)
+        intersection_result == @false_node_id
+    end
+  end
+
+  def print_tdd(id, indent \\ 0) do
+    prefix = String.duplicate("  ", indent)
+    details = get_node_details(id)
+    IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
+
+    case details do
+      {_var, y, n, d} ->
+        IO.puts("#{prefix}  Yes ->")
+        print_tdd(y, indent + 1)
+        IO.puts("#{prefix}  No  ->")
+        print_tdd(n, indent + 1)
+        IO.puts("#{prefix}  DC  ->")
+        print_tdd(d, indent + 1)
+
+      :true_terminal ->
+        :ok
+
+      :false_terminal ->
+        :ok
+
+      nil ->
+        IO.puts("#{prefix} Error: Unknown ID #{id}")
+    end
+  end
 end
 
 # --- Example Usage ---
-# Initialize the system (important!)
 Tdd.init_tdd_system()
 
-IO.puts "\n--- TDD for :foo ---"
+# Basic Types
 tdd_foo = Tdd.type_atom_literal(:foo)
-Tdd.print_tdd(tdd_foo)
-# Expected:
-# ID 4: {{0, :is_atom}, 3, 0, 0}
-#   Yes ->
-#   ID 3: {{1, :value, :foo}, 1, 0, 0}
-#     Yes ->
-#     ID 1: :true_terminal
-#     No  ->
-#     ID 0: :false_terminal
-#     DC  ->
-#     ID 0: :false_terminal
-#   No  ->
-#   ID 0: :false_terminal
-#   DC  ->
-#   ID 0: :false_terminal
-
-IO.puts "\n--- TDD for :bar ---"
 tdd_bar = Tdd.type_atom_literal(:bar)
-Tdd.print_tdd(tdd_bar)
-# Similar structure, but with {1, :value, :bar} and different intermediate IDs like 6, 5.
-
-IO.puts "\n--- TDD for :foo or :bar ---"
-tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
-Tdd.print_tdd(tdd_foo_or_bar)
-
-# Expected structure for tdd_foo_or_bar (variable order matters):
-# Top var: {0, :is_atom}
-#   Yes branch: (node for :foo or :bar, given it's an atom)
-#     Top var: {1, :value, :bar} (assuming :bar < :foo lexicographically for sorting example, or however Elixir sorts them)
-#       Yes branch (:bar is true): true_terminal
-#       No branch (:bar is false): (node for checking :foo)
-#         Top var: {1, :value, :foo}
-#           Yes branch (:foo is true): true_terminal
-#           No branch (:foo is false): false_terminal
-#           DC branch: false_terminal
-#       DC branch: false_terminal (if value is don't care, it's not :bar)
-#   No branch: false_terminal (not an atom)
-#   DC branch: false_terminal (is_atom is don't care)
-
-IO.puts "\n--- TDD for empty tuple {} ---"
+tdd_atom = Tdd.type_atom()
 tdd_empty_tuple = Tdd.type_empty_tuple()
-Tdd.print_tdd(tdd_empty_tuple)
-# Expected:
-# ID X: {{0, :is_tuple}, Y, 0, 0}
-#  Yes ->
-#  ID Y: {{4, :size, 0}, 1, 0, 0}
-#    ... leads to true/false ...
-#  No -> ID 0
-#  DC -> ID 0
+tdd_any = Tdd.type_any()
+tdd_none = Tdd.type_none()
 
-IO.puts "\n--- TDD for :foo or {} ---"
+IO.puts("\n--- TDD for :foo ---")
+Tdd.print_tdd(tdd_foo)
+
+IO.puts("\n--- TDD for not :foo ---")
+Tdd.print_tdd(Tdd.negate(tdd_foo))
+
+IO.puts("\n--- TDD for atom ---")
+Tdd.print_tdd(tdd_atom)
+
+IO.puts("\n--- TDD for not atom ---")
+# Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
+# This represents "anything that is not an atom". The DC branch becomes true because if
+# "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
+Tdd.print_tdd(Tdd.negate(tdd_atom))
+
+IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
+tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
+# Expected ID 0: :false_terminal
+Tdd.print_tdd(tdd_foo_and_bar)
+
+IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
+tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
+# Expected to be structurally identical to tdd_foo
+Tdd.print_tdd(tdd_foo_and_atom)
+
+test = fn name, expected, result ->
+  current_failures = Process.get(:test_failures, [])
+
+  if expected != result do
+    Process.put(:test_failures, [name | current_failures])
+  end
+
+  status = if expected == result, do: "PASSED", else: "FAILED"
+  IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
+end
+
+# Basic Types
+tdd_foo = Tdd.type_atom_literal(:foo)
+tdd_bar = Tdd.type_atom_literal(:bar)
+tdd_baz = Tdd.type_atom_literal(:baz)
+tdd_atom = Tdd.type_atom()
+tdd_empty_tuple = Tdd.type_empty_tuple()
+tdd_tuple = Tdd.type_tuple()
+# Tuple of size 2, e.g. {any, any}
+tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
+tdd_any = Tdd.type_any()
+tdd_none = Tdd.type_none()
+
+IO.puts("\n--- Basic Subtyping Tests ---")
+test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
+test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
+test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
+test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
+test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
+test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
+test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
+test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
+test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
+test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))
+
+IO.puts("\n--- Any/None Subtyping Tests ---")
+test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
+test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
+test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
+test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
+test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
+test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
+test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
+test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))
+
+IO.puts("\n--- Union related Subtyping ---")
+tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
+tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)
+
+test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
+test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
+test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
+test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))
+
+test.(
+  "(:foo | :bar) <: (:foo | :bar | :baz)",
+  true,
+  Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
+)
+
+test.(
+  "(:foo | :bar | :baz) <: (:foo | :bar)",
+  false,
+  Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
+)
+
+# Test against a non-member of the union
+test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))
+
+IO.puts("\n--- Intersection related Subtyping ---")
+# Should be equivalent to tdd_foo
+tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
+# Should be tdd_none
+tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
+
+test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
+test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
+test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
+test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
+test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
+# An intersection is a subtype of its components
+test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
+# (none <: atom)
+test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
+# (none <: tuple)
+test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))
+
+IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
+# Reminder: ¬A <: ¬B  is equivalent to B <: A (contrapositive)
+
+# Test 1: ¬atom <: ¬:foo  (Equivalent to :foo <: atom, which is true)
+test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))
+
+# Test 2: ¬:foo <: ¬atom  (Equivalent to atom <: :foo, which is false)
+test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))
+
+# Double negation
+test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
+test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))
+
+# Disjoint types
+test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
+test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
+test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))
+
+IO.puts("\n--- Mixed Types & Complex Subtyping ---")
+tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
 tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
-Tdd.print_tdd(tdd_foo_or_empty_tuple)
-# Expected structure (variable order {0, :is_atom} < {0, :is_tuple}):
-# Top var: {0, :is_atom}
-#  Yes branch: (node for :foo, given it's an atom, and not a tuple)
-#    ... (structure of tdd_foo, but false branch of {0, :is_tuple} might point here)
-#  No branch: (node for {}, given it's not an atom)
-#    ... (structure of tdd_empty_tuple, but false branch of {0, :is_atom} might point here)
-#  DC branch: (complicated, depends on how dc propagates for sum)
-#    For sum, if `is_atom` is dc for foo and for tuple, then result is dc.
-#    Since our constructors use false for dc, `apply(:sum, false_id, false_id)` for dc branches yields `false_id`.
-#    So, the DC branch of the root will be false.
+
+test.(
+  "(:foo | {}) <: (atom | tuple)",
+  true,
+  Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
+)
+
+test.(
+  "(atom | tuple) <: (:foo | {})",
+  false,
+  Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
+)
+
+test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
+test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))
+
+# De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
+# (:foo | :bar) <: ¬(¬:foo & ¬:bar)
+tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))
+
+test.(
+  "(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
+  true,
+  Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
+)
+
+test.(
+  "¬(¬:foo & ¬:bar) <: (:foo | :bar)",
+  true,
+  Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
+)
+
+# Type difference: atom - :foo  (represented as atom & ¬:foo)
+tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
+test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
+test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
+# True if :bar is in (atom - :foo)
+test.("(atom - :foo) <: :bar", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
+test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
+
+# (atom - :foo) | :foo should be atom
+tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo)
+test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom))
+test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom))
+
+# (atom | {}) & (tuple | :foo) must be (:foo | {})
+# Represents `atom() | {}`
+tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
+# Represents `tuple() | :foo`
+tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
+intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
+# Expected result for intersected_complex is tdd_foo_or_empty_tuple
+
+test.(
+  "(atom | {}) & (tuple | :foo) <: (:foo | {})",
+  true,
+  Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple)
+)
+
+test.(
+  "(:foo | {}) <: (atom | {}) & (tuple | :foo)",
+  true,
+  Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex)
+)
+
+# {} | tuple_size_2 should be a subtype of tuple
+tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2)
+test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple))
+
+test.(
+  "({} | tuple_size_2) <: ({} | tuple_size_2)",
+  true,
+  Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2)
+)
+
+test.("({} | tuple_size_2) <: tuple_size_2", false, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2))
+
+IO.puts("\n--- TDD structure for (atom - :foo) ---")
+Tdd.print_tdd(tdd_atom_minus_foo)
+IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
+Tdd.print_tdd(tdd_recombined_atom)
+IO.puts("\n--- TDD structure for 'atom' for comparison ---")
+Tdd.print_tdd(tdd_atom)
+
+IO.inspect(Process.get(:test_failures, []))
+IO.inspect("tdd_atom_and_tuple")
+Tdd.print_tdd(tdd_atom_and_tuple)
+IO.inspect("tdd_none")
+Tdd.print_tdd(tdd_none)