From 967eb93aa87215e6f497096cc5e8b10ed43e3fba Mon Sep 17 00:00:00 2001
From: Kacper Marzecki <kacper.marzecki@schibsted.com>
Date: Tue, 17 Jun 2025 19:48:50 +0200
Subject: [PATCH] checkpoint

---
 test1.exs | 885 ++++--------------------------------------------------
 tests.exs | 796 ++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 855 insertions(+), 826 deletions(-)
 create mode 100644 tests.exs

diff --git a/test1.exs b/test1.exs
index 3070e57..94abcdf 100644
--- a/test1.exs
+++ b/test1.exs
@@ -429,33 +429,25 @@ defmodule Tdd.Core do
   """
 
   def make_node(variable, yes_id, no_id, dc_id) do
-    # NEW, MORE POWERFUL REDUCTION RULE:
-    # If the 'yes' and 'no' paths lead to the same result, the test on this
-    # variable is redundant. The entire node can be replaced by that result.
-    cond do
-      yes_id == no_id ->
-        yes_id
+    if yes_id == no_id and no_id == dc_id do
+      yes_id
+    else
+      state = get_state()
+      node_tuple = {variable, yes_id, no_id, dc_id}
 
-      yes_id == dc_id && no_id == dc_id ->
-        yes_id
+      if Map.has_key?(state.nodes, node_tuple) do
+        state.nodes[node_tuple]
+      else
+        new_id = state.next_id
 
-      true ->
-        state = get_state()
-        node_tuple = {variable, yes_id, no_id, 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
+        })
 
-        if Map.has_key?(state.nodes, node_tuple) do
-          state.nodes[node_tuple]
-        else
-          new_id = state.next_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
+        new_id
+      end
     end
   end
 
@@ -494,7 +486,7 @@ defmodule Tdd.Core do
               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, d1)
+              make_node(var1, res_y, res_n, res_d)
 
             true ->
               {var1, y1, n1, d1} = u1_details
@@ -662,14 +654,14 @@ defmodule Tdd.PredicateLogic do
 
   # ------------ implication helpers ------------------------------------------
 
-  defp atom_implication(id, constr) do
-    case {Map.get(constr, V.v_atom_eq(id)), find_any_atom_true(constr)} do
-      {true, _} -> true
-      {false, _} -> false
-      {nil, true_id} when true_id != id -> false
-      _ -> :unknown
-    end
+def atom_implication(id, constr) do
+  case {Map.get(constr, V.v_atom_eq(id)), find_any_atom_true(constr)} do
+    {true,  _} -> true
+    {false, _} -> false
+    {nil, nil} -> :unknown                  # <- ⬅️ special-case “no info”
+    {nil, other} when other != id -> false  # <- only different, real atom
   end
+end
 
   defp find_any_atom_true(constr) do
     constr
@@ -762,7 +754,12 @@ defmodule Tdd do
 
   # --- System Init ---
   def init_tdd_system do
-    Tdd.Path.start_link()
+    try do
+      Tdd.Path.start_link()
+    rescue
+      _ -> nil
+    end
+
     Core.init()
     IO.puts("TDD system initialized with new architecture.")
   end
@@ -775,9 +772,17 @@ defmodule Tdd do
   def type_integer, do: Core.make_node(V.v_is_integer(), type_any(), type_none(), type_none())
   def type_list, do: Core.make_node(V.v_is_list(), type_any(), type_none(), type_none())
 
-  def type_atom_literal(a),
-    do:
-      intersect(type_atom(), Core.make_node(V.v_atom_eq(a), type_any(), type_none(), type_none()))
+  def type_atom_literal(a) do
+    id = Core.make_node(V.v_atom_eq(a), type_any(), type_none(), type_none())
+    IO.inspect("BEFORE SIMPLIFICATION")
+    print_tdd(id)
+
+    after_simplification = id |> Tdd.simplify(%{})
+
+    IO.inspect("AFTER SIMPLIFICATION")
+    print_tdd(after_simplification)
+    after_simplification
+  end
 
   def type_int_eq(n),
     do:
@@ -1265,801 +1270,29 @@ defmodule Tdd do
   end
 end
 
-# --- Example Usage ---
 Tdd.init_tdd_system()
-
-# Basic Types
-tdd_foo = Tdd.type_atom_literal(:foo)
-tdd_bar = Tdd.type_atom_literal(:bar)
-tdd_atom = Tdd.type_atom()
-tdd_empty_tuple = Tdd.type_empty_tuple()
-tdd_any = Tdd.type_any()
-tdd_none = Tdd.type_none()
-
-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()
+tdd_foo = Tdd.type_atom_literal(:foo)
+tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
+tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
+intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
+tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
+# Tdd.print_tdd(intersected_complex)
+# Tdd.print_tdd(tdd_foo_or_empty_tuple)
+# !!!!!!!!!!!!!!!!!!
+tdd_foo = Tdd.type_atom_literal(:foo)
+Tdd.print_tdd(tdd_foo)
+# outputs: ID 0: false
+# 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)
+# )
+Code.require_file("./tests.exs")
 
-test_all = fn ->
-  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)
-  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)
-
-  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", false, 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, []))
-end
-
-defmodule IntegerTests do
-  def run(test_fn) do
-    Process.put(:test_failures, [])
-    # Reset for each test group if needed, or once globally
-    Tdd.init_tdd_system()
-
-    # Integer types
-    tdd_int = Tdd.type_integer()
-    tdd_int_5 = Tdd.type_int_eq(5)
-    tdd_int_7 = Tdd.type_int_eq(7)
-    # x < 10
-    tdd_int_lt_10 = Tdd.type_int_lt(10)
-    # x > 3
-    tdd_int_gt_3 = Tdd.type_int_gt(3)
-    # x < 3
-    tdd_int_lt_3 = Tdd.type_int_lt(3)
-    # x > 10
-    tdd_int_gt_10 = Tdd.type_int_gt(10)
-    tdd_atom_foo = Tdd.type_atom_literal(:foo)
-    #
-    # IO.puts("\n--- Integer Type Structures ---")
-    # IO.puts("Integer:")
-    # Tdd.print_tdd(tdd_int)
-    # IO.puts("Int == 5:")
-    # Tdd.print_tdd(tdd_int_5)
-    # IO.puts("Int < 10:")
-    # Tdd.print_tdd(tdd_int_lt_10)
-
-    IO.puts("\n--- Integer Subtyping Tests ---")
-    test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
-    test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5))
-    test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7))
-    test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5))
-    test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo))
-
-    test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int))
-    test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10))
-    # 5 < 10
-    test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10))
-    test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5))
-
-    test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int))
-    # 5 > 3
-    test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3))
-    test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5))
-
-    # x < 3 implies x < 10
-    test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10))
-    # x > 10 implies x > 3
-    test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
-    test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3))
-    test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10))
-
-    IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
-    intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7)
-    test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none())
-    # IO.puts("Structure of int_5 & int_7 (should be ID 0):")
-    # Tdd.print_tdd(intersect_5_7)
-
-    # x < 3 AND x > 10
-    intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10)
-    test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none())
-    # IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
-    # Tdd.print_tdd(intersect_lt3_gt10)
-
-    # x < 10 AND x > 3 (e.g. 4,5..9)
-    intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3)
-    test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none())
-    # IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
-    # Tdd.print_tdd(intersect_lt10_gt3)
-    # Test a value within this intersection
-    test_fn.(
-      "int_5 <: (int_lt_10 & int_gt_3)",
-      true,
-      Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3)
-    )
-
-    # x == 5 AND x < 3
-    intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3)
-    test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none())
-
-    IO.puts("\n--- Integer Union Tests ---")
-    union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7)
-    test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7))
-    test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7))
-    test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7))
-    # IO.puts("Structure of int_5 | int_7:")
-    # Tdd.print_tdd(union_5_7)
-
-    # (int < 3) | (int > 10)
-    union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
-
-    test_fn.(
-      "int_eq(0) <: (int < 3 | int > 10)",
-      true,
-      Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges)
-    )
-
-    test_fn.(
-      "int_eq(5) <: (int < 3 | int > 10)",
-      false,
-      Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges)
-    )
-
-    test_fn.(
-      "int_eq(12) <: (int < 3 | int > 10)",
-      true,
-      Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
-    )
-
-    IO.inspect(Process.get(:test_failures, []))
-  end
-end
-
-defmodule TupleTests do
-  import Tdd
-
-  def run(test_fn) do
-    Process.put(:test_failures, [])
-    # Re-init the system for a clean slate for these tests
-    Tdd.init_tdd_system()
-    IO.puts("\n--- Running TupleTests ---")
-
-    # --- Basic Types for convenience ---
-    t_atom = type_atom()
-    t_int = type_integer()
-    t_foo = type_atom_literal(:foo)
-    t_bar = type_atom_literal(:bar)
-    t_int_5 = type_int_eq(5)
-    t_int_6 = type_int_eq(6)
-    t_int_pos = type_int_gt(0)
-    t_any = type_any()
-    t_none = type_none()
-    # any tuple
-    t_tuple = type_tuple()
-    t_empty_tuple = type_empty_tuple()
-
-    # --- Specific Tuple Types ---
-    # {atom(), integer()}
-    tup_atom_int = type_tuple([t_atom, t_int])
-    # {:foo, 5}
-    tup_foo_5 = type_tuple([t_foo, t_int_5])
-    # {pos_integer(), atom()}
-    tup_pos_atom = type_tuple([t_int_pos, t_atom])
-    # {atom(), any}
-    tup_atom_any = type_tuple([t_atom, t_any])
-    # {any, integer()}
-    tup_any_int = type_tuple([t_any, t_int])
-    # a tuple of size 2, {any, any}
-    tup_s2_any = type_tuple_sized_any(2)
-    # a tuple of size 3, {any, any, any}
-    tup_s3_any = type_tuple_sized_any(3)
-    # {integer(), atom()}
-    tup_int_atom = type_tuple([t_int, t_atom])
-    # {{:foo}}
-    tup_nested_foo = type_tuple([type_tuple([t_foo])])
-    # {{atom()}}
-    tup_nested_atom = type_tuple([type_tuple([t_atom])])
-    # {any, none} -> this should resolve to none
-    tup_with_none = type_tuple([t_any, t_none])
-
-    IO.puts("\n--- Section: Basic Subtyping ---")
-    test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
-    test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
-    test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
-    test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
-    test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
-    test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))
-
-    IO.puts("\n--- Section: Size-related Subtyping ---")
-    test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
-    test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
-    test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
-    test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
-    test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
-    test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))
-
-    IO.puts("\n--- Section: Intersection ---")
-    # {atom, any} & {any, int} -> {atom, int}
-    intersect1 = intersect(tup_atom_any, tup_any_int)
-    test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)
-
-    # {atom, int} & {int, atom} -> none
-    intersect2 = intersect(tup_atom_int, tup_int_atom)
-    test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)
-
-    # tuple_size_2 & tuple_size_3 -> none
-    intersect3 = intersect(tup_s2_any, tup_s3_any)
-    test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)
-
-    # tuple() & {atom, int} -> {atom, int}
-    intersect4 = intersect(t_tuple, tup_atom_int)
-    test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)
-
-    IO.puts("\n--- Section: Union ---")
-    # {:foo, 5} | {pos_int, atom}
-    union1 = sum(tup_foo_5, tup_pos_atom)
-    test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))
-
-    test_fn.(
-      "{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
-      true,
-      is_subtype(tup_pos_atom, union1)
-    )
-
-    test_fn.(
-      "{atom, int} <: ({:foo, 5} | {pos_int, atom})",
-      false,
-      is_subtype(tup_atom_int, union1)
-    )
-
-    # {atom, any} | {any, int} -> a complex type, let's check subtyping against it
-    union2 = sum(tup_atom_any, tup_any_int)
-    # {atom, int} is in both parts of the union.
-    test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
-    # {:foo, :bar} is only in {atom, any}.
-    test_fn.(
-      "{:foo, :bar} <: ({atom,any} | {any,int})",
-      true,
-      is_subtype(type_tuple([t_foo, t_bar]), union2)
-    )
-
-    # {5, 6} is only in {any, int}.
-    test_fn.(
-      "{5, 6} <: ({atom,any} | {any,int})",
-      true,
-      is_subtype(type_tuple([t_int_5, t_int_6]), union2)
-    )
-
-    # {5, :foo} is in neither part of the union.
-    test_fn.(
-      "{5, :foo} <: ({atom,any} | {any,int})",
-      false,
-      is_subtype(type_tuple([t_int_5, t_foo]), union2)
-    )
-
-    IO.puts("\n--- Section: Negation and Type Difference ---")
-    # atom is disjoint from tuple, so atom <: ¬tuple
-    test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))
-
-    # A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
-    test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
-    # {int, atom} is a subtype of ¬{atom, int} because their elements differ
-    test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
-    # tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
-    test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))
-
-    # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
-    diff1 = intersect(tup_s2_any, negate(tup_atom_any))
-
-    # {integer, integer} has a first element that is not an atom, so it should be in the difference.
-    tup_int_int = type_tuple([t_int, t_int])
-    test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
-
-    test_fn.(
-      "{atom, int} <: (tuple_size_2 - {atom, any})",
-      false,
-      is_subtype(tup_atom_int, diff1)
-    )
-
-    IO.puts("\n--- Section: Nested Tuples ---")
-    test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
-    test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
-    # Intersection of disjoint nested types: {{:foo}} & {{:bar}}
-    intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
-    test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
-    # Union of nested types
-    union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
-    test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))
-
-    test_fn.(
-      "{{:bar}} <: ({{:foo}} | {{:bar}})",
-      true,
-      is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
-    )
-
-    test_fn.(
-      "{{atom}} <: ({{:foo}} | {{:bar}})",
-      false,
-      is_subtype(tup_nested_atom, union_nested)
-    )
-
-    IO.puts("\n--- Section: Edge Cases (any, none) ---")
-    # A type `{any, none}` should not be possible. The value `none` cannot exist.
-    # The simplification logic should reduce this to `type_none`.
-    test_fn.("{any, none} == none", true, tup_with_none == t_none)
-
-    # Intersection with a tuple containing none should result in none
-    intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
-    test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)
-
-    # Union with a tuple containing none should be a no-op
-    union_with_none_tuple = sum(tup_atom_int, tup_with_none)
-    test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)
-
-    # --- Original tests from problem description for regression ---
-    IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")
-
-    test_fn.(
-      "{1, :foo} <: {int_gt_0, :foo | :bar}",
-      true,
-      is_subtype(
-        type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
-        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
-      )
-    )
-
-    test_fn.(
-      "{0, :foo} <: {int_gt_0, :foo | :bar}",
-      false,
-      is_subtype(
-        type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
-        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
-      )
-    )
-
-    test_fn.(
-      "{1, :kek} <: {int_gt_0, :foo | :bar}",
-      false,
-      is_subtype(
-        type_tuple([
-          type_int_eq(1),
-          type_atom_literal(:kek)
-        ]),
-        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
-      )
-    )
-
-    IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
-  end
-end
-
-defmodule ListTests do
-  import Tdd
-
-  def run(test_fn) do
-    Process.put(:test_failures, [])
-    Tdd.init_tdd_system()
-    IO.puts("\n--- Running ListTests ---")
-
-    # --- Basic Types ---
-    t_atom = type_atom()
-    t_int = type_integer()
-    t_foo = type_atom_literal(:foo)
-    t_bar = type_atom_literal(:bar)
-    t_any = type_any()
-    t_none = type_none()
-
-    # --- List Types ---
-    t_list = type_list()
-    t_empty_list = type_empty_list()
-    # [atom | list]
-    t_cons_atom_list = type_cons(t_atom, t_list)
-    # [:foo | []]
-    t_cons_foo_empty = type_cons(t_foo, t_empty_list)
-    # [atom | []]
-    t_cons_atom_empty = type_cons(t_atom, t_empty_list)
-    # [any | []]
-    t_cons_any_empty = type_cons(t_any, t_empty_list)
-    # [integer | list]
-    t_cons_int_list = type_cons(t_int, t_list)
-
-    IO.puts("\n--- Section: Basic List Subtyping ---")
-    test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
-    test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
-    test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
-    test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
-    test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
-    test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
-    test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
-    test_fn.("atom <: list", false, is_subtype(t_atom, t_list))
-
-    IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
-    # Head is a subtype
-    test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
-    test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
-    # Tail is a subtype
-    test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
-    test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
-    # Both are subtypes
-    test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
-    # Neither is a subtype
-    test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
-    # A list of length 1 is a subtype of a list of any element of length 1
-    test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))
-
-    IO.puts("\n--- Section: List Intersection ---")
-    # [atom|list] & [integer|list] -> should be none due to head conflict
-    intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
-    test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)
-
-    # [any|[]] & [atom|list] -> should be [atom|[]]
-    intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
-    test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)
-
-    # [] & [atom|list] -> should be none because one is empty and one is not
-    intersect3 = intersect(t_empty_list, t_cons_atom_list)
-    test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)
-
-    IO.puts("\n--- Section: List Union ---")
-    # [] | [atom|[]]
-    union1 = sum(t_empty_list, t_cons_atom_empty)
-    test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
-    test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))
-
-    test_fn.(
-      "[integer|[]] <: ([] | [atom|[]])",
-      false,
-      is_subtype(type_cons(t_int, t_empty_list), union1)
-    )
-
-    # [:foo|[]] | [:bar|[]]
-    union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
-    # This union is a subtype of [atom|[]]
-    test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
-    test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))
-
-    IO.puts("\n--- Section: List Negation ---")
-    # list is a subtype of not(atom)
-    test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
-    # A non-empty list is a subtype of not an empty list
-    test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
-    # [integer|list] is a subtype of not [atom|list]
-    test_fn.(
-      "[integer|list] <: ¬[atom|list]",
-      true,
-      is_subtype(t_cons_int_list, negate(t_cons_atom_list))
-    )
-
-    IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
-  end
-end
-
-defmodule ListOfTests do
-  import Tdd
-
-  def run(test_fn) do
-    Process.put(:test_failures, [])
-    Tdd.init_tdd_system()
-    IO.puts("\n--- Running ListOfTests ---")
-
-    # --- Basic Types ---
-    t_atom = type_atom()
-    t_int = type_integer()
-    t_pos_int = type_int_gt(0)
-    t_int_5 = type_int_eq(5)
-
-    # --- list(X) Types ---
-    t_list_of_int = type_list_of(t_int)
-    t_list_of_pos_int = type_list_of(t_pos_int)
-    t_list_of_atom = type_list_of(t_atom)
-
-    # --- Specific List Types ---
-    t_list = type_list()
-    t_empty_list = type_empty_list()
-    # [5]
-    t_list_one_int = type_cons(t_int_5, t_empty_list)
-    # [:foo]
-    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
-    # [5, :foo]
-    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
-
-    IO.puts("\n--- Section: Basic list(X) Subtyping ---")
-    test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
-    test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
-    test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
-    test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
-    test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
-    test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))
-
-    test_fn.(
-      "[5, :foo] <: list(any)",
-      true,
-      is_subtype(t_list_int_and_atom, type_list_of(type_any()))
-    )
-
-    IO.puts("\n--- Section: Covariance of list(X) ---")
-
-    test_fn.(
-      "list(pos_integer) <: list(integer)",
-      true,
-      is_subtype(t_list_of_pos_int, t_list_of_int)
-    )
-
-    test_fn.(
-      "list(integer) <: list(pos_integer)",
-      false,
-      is_subtype(t_list_of_int, t_list_of_pos_int)
-    )
-
-    IO.puts("\n--- Section: Intersection of list(X) ---")
-    # list(integer) & list(pos_integer) should be list(pos_integer)
-    intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
-
-    test_fn.(
-      "(list(int) & list(pos_int)) == list(pos_int)",
-      true,
-      intersect1 == t_list_of_pos_int
-    )
-
-    # list(integer) & list(atom) should be just [] (empty list is the only common member)
-    # The system simplifies this intersection to a type that only accepts the empty list.
-    intersect2 = intersect(t_list_of_int, t_list_of_atom)
-    test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
-    test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
-    test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
-    # It should be equivalent to `type_empty_list`
-    test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)
-
-    IO.puts("\n--- Section: Intersection of list(X) with cons ---")
-    # list(integer) & [:foo | []] -> should be none
-    intersect3 = intersect(t_list_of_int, t_list_one_atom)
-    test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())
-
-    # list(integer) & [5 | []] -> should be [5 | []]
-    intersect4 = intersect(t_list_of_int, t_list_one_int)
-    test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)
-
-    # list(integer) & [5, :foo] -> should be none
-    intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
-    test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())
-
-    IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
-  end
-end
-
-defmodule AdhocTest do
-  import Tdd
-
-  def run(test_fn) do
-    # --- Basic Types ---
-    t_atom = type_atom()
-    t_int = type_integer()
-    t_pos_int = type_int_gt(0)
-    t_int_5 = type_int_eq(5)
-
-    # --- list(X) Types ---
-    t_list_of_int = type_list_of(t_int)
-    t_list_of_pos_int = type_list_of(t_pos_int)
-    t_list_of_atom = type_list_of(t_atom)
-
-    # --- Specific List Types ---
-    t_list = type_list()
-    t_empty_list = type_empty_list()
-    # [5]
-    t_list_one_int = type_cons(t_int_5, t_empty_list)
-    # [:foo]
-    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
-    # [5, :foo]
-    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
-    intersect4 = intersect(t_list_of_int, t_list_one_int)
-    IO.inspect("first_subtype")
-    a = is_subtype(intersect4, t_list_one_int)
-    IO.inspect("second_subtype")
-    b = is_subtype(t_list_one_int, intersect4)
-    test_fn.("list(integer) & [5] == [5]", true, a == b)
-  end
-end
-
-test_all.()
 # IntegerTests.run(test)
 # TupleTests.run(test)
 # ListTests.run(test)
diff --git a/tests.exs b/tests.exs
new file mode 100644
index 0000000..f254a5a
--- /dev/null
+++ b/tests.exs
@@ -0,0 +1,796 @@
+
+# --- Example Usage ---
+Tdd.init_tdd_system()
+
+# Basic Types
+tdd_foo = Tdd.type_atom_literal(:foo)
+tdd_bar = Tdd.type_atom_literal(:bar)
+tdd_atom = Tdd.type_atom()
+tdd_empty_tuple = Tdd.type_empty_tuple()
+tdd_any = Tdd.type_any()
+tdd_none = Tdd.type_none()
+
+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()
+
+test_all = fn ->
+  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)
+  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)
+
+  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", false, 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, []))
+end
+defmodule IntegerTests do
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    # Reset for each test group if needed, or once globally
+    Tdd.init_tdd_system()
+
+    # Integer types
+    tdd_int = Tdd.type_integer()
+    tdd_int_5 = Tdd.type_int_eq(5)
+    tdd_int_7 = Tdd.type_int_eq(7)
+    # x < 10
+    tdd_int_lt_10 = Tdd.type_int_lt(10)
+    # x > 3
+    tdd_int_gt_3 = Tdd.type_int_gt(3)
+    # x < 3
+    tdd_int_lt_3 = Tdd.type_int_lt(3)
+    # x > 10
+    tdd_int_gt_10 = Tdd.type_int_gt(10)
+    tdd_atom_foo = Tdd.type_atom_literal(:foo)
+    #
+    # IO.puts("\n--- Integer Type Structures ---")
+    # IO.puts("Integer:")
+    # Tdd.print_tdd(tdd_int)
+    # IO.puts("Int == 5:")
+    # Tdd.print_tdd(tdd_int_5)
+    # IO.puts("Int < 10:")
+    # Tdd.print_tdd(tdd_int_lt_10)
+
+    IO.puts("\n--- Integer Subtyping Tests ---")
+    test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
+    test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5))
+    test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7))
+    test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5))
+    test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo))
+
+    test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int))
+    test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10))
+    # 5 < 10
+    test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10))
+    test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5))
+
+    test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int))
+    # 5 > 3
+    test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3))
+    test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5))
+
+    # x < 3 implies x < 10
+    test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10))
+    # x > 10 implies x > 3
+    test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
+    test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3))
+    test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10))
+
+    IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
+    intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7)
+    test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none())
+    # IO.puts("Structure of int_5 & int_7 (should be ID 0):")
+    # Tdd.print_tdd(intersect_5_7)
+
+    # x < 3 AND x > 10
+    intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10)
+    test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none())
+    # IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
+    # Tdd.print_tdd(intersect_lt3_gt10)
+
+    # x < 10 AND x > 3 (e.g. 4,5..9)
+    intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3)
+    test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none())
+    # IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
+    # Tdd.print_tdd(intersect_lt10_gt3)
+    # Test a value within this intersection
+    test_fn.(
+      "int_5 <: (int_lt_10 & int_gt_3)",
+      true,
+      Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3)
+    )
+
+    # x == 5 AND x < 3
+    intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3)
+    test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none())
+
+    IO.puts("\n--- Integer Union Tests ---")
+    union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7)
+    test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7))
+    test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7))
+    test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7))
+    # IO.puts("Structure of int_5 | int_7:")
+    # Tdd.print_tdd(union_5_7)
+
+    # (int < 3) | (int > 10)
+    union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
+
+    test_fn.(
+      "int_eq(0) <: (int < 3 | int > 10)",
+      true,
+      Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges)
+    )
+
+    test_fn.(
+      "int_eq(5) <: (int < 3 | int > 10)",
+      false,
+      Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges)
+    )
+
+    test_fn.(
+      "int_eq(12) <: (int < 3 | int > 10)",
+      true,
+      Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
+    )
+
+    IO.inspect(Process.get(:test_failures, []))
+  end
+end
+
+defmodule TupleTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    # Re-init the system for a clean slate for these tests
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running TupleTests ---")
+
+    # --- Basic Types for convenience ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_foo = type_atom_literal(:foo)
+    t_bar = type_atom_literal(:bar)
+    t_int_5 = type_int_eq(5)
+    t_int_6 = type_int_eq(6)
+    t_int_pos = type_int_gt(0)
+    t_any = type_any()
+    t_none = type_none()
+    # any tuple
+    t_tuple = type_tuple()
+    t_empty_tuple = type_empty_tuple()
+
+    # --- Specific Tuple Types ---
+    # {atom(), integer()}
+    tup_atom_int = type_tuple([t_atom, t_int])
+    # {:foo, 5}
+    tup_foo_5 = type_tuple([t_foo, t_int_5])
+    # {pos_integer(), atom()}
+    tup_pos_atom = type_tuple([t_int_pos, t_atom])
+    # {atom(), any}
+    tup_atom_any = type_tuple([t_atom, t_any])
+    # {any, integer()}
+    tup_any_int = type_tuple([t_any, t_int])
+    # a tuple of size 2, {any, any}
+    tup_s2_any = type_tuple_sized_any(2)
+    # a tuple of size 3, {any, any, any}
+    tup_s3_any = type_tuple_sized_any(3)
+    # {integer(), atom()}
+    tup_int_atom = type_tuple([t_int, t_atom])
+    # {{:foo}}
+    tup_nested_foo = type_tuple([type_tuple([t_foo])])
+    # {{atom()}}
+    tup_nested_atom = type_tuple([type_tuple([t_atom])])
+    # {any, none} -> this should resolve to none
+    tup_with_none = type_tuple([t_any, t_none])
+
+    IO.puts("\n--- Section: Basic Subtyping ---")
+    test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
+    test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
+    test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
+    test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
+    test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
+    test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))
+
+    IO.puts("\n--- Section: Size-related Subtyping ---")
+    test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
+    test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
+    test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
+    test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
+    test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
+    test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))
+
+    IO.puts("\n--- Section: Intersection ---")
+    # {atom, any} & {any, int} -> {atom, int}
+    intersect1 = intersect(tup_atom_any, tup_any_int)
+    test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)
+
+    # {atom, int} & {int, atom} -> none
+    intersect2 = intersect(tup_atom_int, tup_int_atom)
+    test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)
+
+    # tuple_size_2 & tuple_size_3 -> none
+    intersect3 = intersect(tup_s2_any, tup_s3_any)
+    test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)
+
+    # tuple() & {atom, int} -> {atom, int}
+    intersect4 = intersect(t_tuple, tup_atom_int)
+    test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)
+
+    IO.puts("\n--- Section: Union ---")
+    # {:foo, 5} | {pos_int, atom}
+    union1 = sum(tup_foo_5, tup_pos_atom)
+    test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))
+
+    test_fn.(
+      "{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
+      true,
+      is_subtype(tup_pos_atom, union1)
+    )
+
+    test_fn.(
+      "{atom, int} <: ({:foo, 5} | {pos_int, atom})",
+      false,
+      is_subtype(tup_atom_int, union1)
+    )
+
+    # {atom, any} | {any, int} -> a complex type, let's check subtyping against it
+    union2 = sum(tup_atom_any, tup_any_int)
+    # {atom, int} is in both parts of the union.
+    test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
+    # {:foo, :bar} is only in {atom, any}.
+    test_fn.(
+      "{:foo, :bar} <: ({atom,any} | {any,int})",
+      true,
+      is_subtype(type_tuple([t_foo, t_bar]), union2)
+    )
+
+    # {5, 6} is only in {any, int}.
+    test_fn.(
+      "{5, 6} <: ({atom,any} | {any,int})",
+      true,
+      is_subtype(type_tuple([t_int_5, t_int_6]), union2)
+    )
+
+    # {5, :foo} is in neither part of the union.
+    test_fn.(
+      "{5, :foo} <: ({atom,any} | {any,int})",
+      false,
+      is_subtype(type_tuple([t_int_5, t_foo]), union2)
+    )
+
+    IO.puts("\n--- Section: Negation and Type Difference ---")
+    # atom is disjoint from tuple, so atom <: ¬tuple
+    test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))
+
+    # A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
+    test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
+    # {int, atom} is a subtype of ¬{atom, int} because their elements differ
+    test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
+    # tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
+    test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))
+
+    # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
+    diff1 = intersect(tup_s2_any, negate(tup_atom_any))
+
+    # {integer, integer} has a first element that is not an atom, so it should be in the difference.
+    tup_int_int = type_tuple([t_int, t_int])
+    test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
+
+    test_fn.(
+      "{atom, int} <: (tuple_size_2 - {atom, any})",
+      false,
+      is_subtype(tup_atom_int, diff1)
+    )
+
+    IO.puts("\n--- Section: Nested Tuples ---")
+    test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
+    test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
+    # Intersection of disjoint nested types: {{:foo}} & {{:bar}}
+    intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
+    test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
+    # Union of nested types
+    union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
+    test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))
+
+    test_fn.(
+      "{{:bar}} <: ({{:foo}} | {{:bar}})",
+      true,
+      is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
+    )
+
+    test_fn.(
+      "{{atom}} <: ({{:foo}} | {{:bar}})",
+      false,
+      is_subtype(tup_nested_atom, union_nested)
+    )
+
+    IO.puts("\n--- Section: Edge Cases (any, none) ---")
+    # A type `{any, none}` should not be possible. The value `none` cannot exist.
+    # The simplification logic should reduce this to `type_none`.
+    test_fn.("{any, none} == none", true, tup_with_none == t_none)
+
+    # Intersection with a tuple containing none should result in none
+    intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
+    test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)
+
+    # Union with a tuple containing none should be a no-op
+    union_with_none_tuple = sum(tup_atom_int, tup_with_none)
+    test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)
+
+    # --- Original tests from problem description for regression ---
+    IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")
+
+    test_fn.(
+      "{1, :foo} <: {int_gt_0, :foo | :bar}",
+      true,
+      is_subtype(
+        type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
+        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
+      )
+    )
+
+    test_fn.(
+      "{0, :foo} <: {int_gt_0, :foo | :bar}",
+      false,
+      is_subtype(
+        type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
+        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
+      )
+    )
+
+    test_fn.(
+      "{1, :kek} <: {int_gt_0, :foo | :bar}",
+      false,
+      is_subtype(
+        type_tuple([
+          type_int_eq(1),
+          type_atom_literal(:kek)
+        ]),
+        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
+      )
+    )
+
+    IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
+  end
+end
+
+defmodule ListTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running ListTests ---")
+
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_foo = type_atom_literal(:foo)
+    t_bar = type_atom_literal(:bar)
+    t_any = type_any()
+    t_none = type_none()
+
+    # --- List Types ---
+    t_list = type_list()
+    t_empty_list = type_empty_list()
+    # [atom | list]
+    t_cons_atom_list = type_cons(t_atom, t_list)
+    # [:foo | []]
+    t_cons_foo_empty = type_cons(t_foo, t_empty_list)
+    # [atom | []]
+    t_cons_atom_empty = type_cons(t_atom, t_empty_list)
+    # [any | []]
+    t_cons_any_empty = type_cons(t_any, t_empty_list)
+    # [integer | list]
+    t_cons_int_list = type_cons(t_int, t_list)
+
+    IO.puts("\n--- Section: Basic List Subtyping ---")
+    test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
+    test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
+    test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
+    test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
+    test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
+    test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
+    test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
+    test_fn.("atom <: list", false, is_subtype(t_atom, t_list))
+
+    IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
+    # Head is a subtype
+    test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
+    test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
+    # Tail is a subtype
+    test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
+    test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
+    # Both are subtypes
+    test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
+    # Neither is a subtype
+    test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
+    # A list of length 1 is a subtype of a list of any element of length 1
+    test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))
+
+    IO.puts("\n--- Section: List Intersection ---")
+    # [atom|list] & [integer|list] -> should be none due to head conflict
+    intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
+    test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)
+
+    # [any|[]] & [atom|list] -> should be [atom|[]]
+    intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
+    test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)
+
+    # [] & [atom|list] -> should be none because one is empty and one is not
+    intersect3 = intersect(t_empty_list, t_cons_atom_list)
+    test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)
+
+    IO.puts("\n--- Section: List Union ---")
+    # [] | [atom|[]]
+    union1 = sum(t_empty_list, t_cons_atom_empty)
+    test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
+    test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))
+
+    test_fn.(
+      "[integer|[]] <: ([] | [atom|[]])",
+      false,
+      is_subtype(type_cons(t_int, t_empty_list), union1)
+    )
+
+    # [:foo|[]] | [:bar|[]]
+    union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
+    # This union is a subtype of [atom|[]]
+    test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
+    test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))
+
+    IO.puts("\n--- Section: List Negation ---")
+    # list is a subtype of not(atom)
+    test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
+    # A non-empty list is a subtype of not an empty list
+    test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
+    # [integer|list] is a subtype of not [atom|list]
+    test_fn.(
+      "[integer|list] <: ¬[atom|list]",
+      true,
+      is_subtype(t_cons_int_list, negate(t_cons_atom_list))
+    )
+
+    IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
+  end
+end
+
+defmodule ListOfTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running ListOfTests ---")
+
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_pos_int = type_int_gt(0)
+    t_int_5 = type_int_eq(5)
+
+    # --- list(X) Types ---
+    t_list_of_int = type_list_of(t_int)
+    t_list_of_pos_int = type_list_of(t_pos_int)
+    t_list_of_atom = type_list_of(t_atom)
+
+    # --- Specific List Types ---
+    t_list = type_list()
+    t_empty_list = type_empty_list()
+    # [5]
+    t_list_one_int = type_cons(t_int_5, t_empty_list)
+    # [:foo]
+    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
+    # [5, :foo]
+    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
+
+    IO.puts("\n--- Section: Basic list(X) Subtyping ---")
+    test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
+    test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
+    test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
+    test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
+    test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
+    test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))
+
+    test_fn.(
+      "[5, :foo] <: list(any)",
+      true,
+      is_subtype(t_list_int_and_atom, type_list_of(type_any()))
+    )
+
+    IO.puts("\n--- Section: Covariance of list(X) ---")
+
+    test_fn.(
+      "list(pos_integer) <: list(integer)",
+      true,
+      is_subtype(t_list_of_pos_int, t_list_of_int)
+    )
+
+    test_fn.(
+      "list(integer) <: list(pos_integer)",
+      false,
+      is_subtype(t_list_of_int, t_list_of_pos_int)
+    )
+
+    IO.puts("\n--- Section: Intersection of list(X) ---")
+    # list(integer) & list(pos_integer) should be list(pos_integer)
+    intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
+
+    test_fn.(
+      "(list(int) & list(pos_int)) == list(pos_int)",
+      true,
+      intersect1 == t_list_of_pos_int
+    )
+
+    # list(integer) & list(atom) should be just [] (empty list is the only common member)
+    # The system simplifies this intersection to a type that only accepts the empty list.
+    intersect2 = intersect(t_list_of_int, t_list_of_atom)
+    test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
+    test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
+    test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
+    # It should be equivalent to `type_empty_list`
+    test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)
+
+    IO.puts("\n--- Section: Intersection of list(X) with cons ---")
+    # list(integer) & [:foo | []] -> should be none
+    intersect3 = intersect(t_list_of_int, t_list_one_atom)
+    test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())
+
+    # list(integer) & [5 | []] -> should be [5 | []]
+    intersect4 = intersect(t_list_of_int, t_list_one_int)
+    test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)
+
+    # list(integer) & [5, :foo] -> should be none
+    intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
+    test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())
+
+    IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
+  end
+end
+
+defmodule AdhocTest do
+  import Tdd
+
+  def run(test_fn) do
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_pos_int = type_int_gt(0)
+    t_int_5 = type_int_eq(5)
+
+    # --- list(X) Types ---
+    t_list_of_int = type_list_of(t_int)
+    t_list_of_pos_int = type_list_of(t_pos_int)
+    t_list_of_atom = type_list_of(t_atom)
+
+    # --- Specific List Types ---
+    t_list = type_list()
+    t_empty_list = type_empty_list()
+    # [5]
+    t_list_one_int = type_cons(t_int_5, t_empty_list)
+    # [:foo]
+    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
+    # [5, :foo]
+    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
+    intersect4 = intersect(t_list_of_int, t_list_one_int)
+    IO.inspect("first_subtype")
+    a = is_subtype(intersect4, t_list_one_int)
+    IO.inspect("second_subtype")
+    b = is_subtype(t_list_one_int, intersect4)
+    test_fn.("list(integer) & [5] == [5]", true, a == b)
+  end
+end
+
+
+test_all.()