checkpoint

test1.exs

@@ -238,6 +238,9 @@ defmodule Tdd.Core do
   def false_id, do: @false_node_id
   defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id
 
+  def terminal_id?(id) when is_terminal_id(id), do: true
+  def terminal_id?(_), do: false
+
   # --- State Management ---
 
   def init do
@@ -495,26 +498,37 @@ defmodule Tdd.PredicateLogic do
     end
   end
 
+  @doc """
+  A general-purpose reasoner that uses the main `saturate` function.
+  It determines if a predicate is implied true or false by a set of constraints
+  by checking if adding its opposite leads to a contradiction.
+  """
+  defp _reason_by_contradiction(predicate, constraints) do
+    # Is `predicate` implied TRUE? (i.e., is `constraints AND NOT predicate` a contradiction?)
+    cond do
+      saturate(Map.put(constraints, predicate, false)) == :contradiction ->
+        true
+
+      # Is `predicate` implied FALSE? (i.e., is `constraints AND predicate` a contradiction?)
+      saturate(Map.put(constraints, predicate, true)) == :contradiction ->
+        false
+
+      true ->
+        :unknown
+    end
+  end
+
   @doc """
   Checks if a `predicate` is logically implied (or contradicted) by a
   set of `constraints`.
-
-  This is the core of semantic simplification. It uses a recursive dispatch
-  strategy to handle predicates nested within data structures.
-
-  ## Return Values
-  - `true`: The constraints imply the predicate is true.
-           (e.g., `x == 5` implies `x < 10`)
-  - `false`: The constraints imply the predicate is false (i.e., its negation is true).
-            (e.g., `x == 5` implies `x > 10` is false)
-  - `:unknown`: The constraints are insufficient to determine the predicate's truth value.
   """
   def check_implication(predicate, constraints) do
-    # The case statement acts as our master dispatcher.
     case predicate do
-      # -----------------------------------------------------------------
+      # --- NEW HANDLER for primary type predicates ---
-      # --- 1. Base Cases: Handling raw, non-nested predicates
+      {0, _} ->
-      # -----------------------------------------------------------------
+        _reason_by_contradiction(predicate, constraints)
+
+      # --- EXISTING BASE CASES ---
       {1, :value, _} ->
         _atom_implication(predicate, constraints)
 
@@ -524,40 +538,26 @@ defmodule Tdd.PredicateLogic do
       {4, :size, _} ->
         _tuple_size_implication(predicate, constraints)
 
-      # ... add other base cases for list_is_empty, etc., if needed ...
+      # --- EXISTING RECURSIVE CASES ---
-
-      # -----------------------------------------------------------------
-      # --- 2. Recursive Cases: Handling nested predicates
-      # -----------------------------------------------------------------
       {4, :element, index, inner_predicate} ->
-        # Isolate the sub-problem for this specific tuple element.
         element_constraints =
           gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1))
 
-        # Recurse on the sub-problem.
         check_implication(inner_predicate, element_constraints)
 
       {5, :head, inner_predicate} ->
-        # Isolate the sub-problem for the list head.
         head_constraints =
           gather_local_constraints(constraints, &match?({5, :head, _}, &1))
 
-        # Recurse on the sub-problem.
         check_implication(inner_predicate, head_constraints)
 
       {5, :tail, inner_predicate} ->
-        # Isolate the sub-problem for the list tail.
         tail_constraints =
           gather_local_constraints(constraints, &match?({5, :tail, _}, &1))
 
-        # Recurse on the sub-problem.
         check_implication(inner_predicate, tail_constraints)
 
-      # ... add other recursive cases for map_key_value, etc., in the future ...
+      # --- DEFAULT CASE ---
-
-      # -----------------------------------------------------------------
-      # --- 3. Default Case
-      # -----------------------------------------------------------------
       _ ->
         # We don't have specific reasoning logic for this predicate type.
         :unknown
@@ -574,7 +574,7 @@ defmodule Tdd.PredicateLogic do
   Gathers, unwraps, and isolates constraints for a specific component.
   """
   defp gather_local_constraints(all_constraints, filter_fun) do
-    for {{var, bool_val}} <- all_constraints,
+    for {var, bool_val} <- all_constraints,
         filter_fun.(var),
         into: %{} do
       # Unwrap the predicate for the local check.
@@ -954,15 +954,18 @@ defmodule Tdd do
 
   # --- High-Level Operations ---
 
-  def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{})
+  def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{}) |> simplify(%{})
-  def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{})
+  def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) |> simplify(%{})
 
   def negate(u_id) do
     negate_recursive(u_id, %{})
+    |> simplify(%{})
   end
 
   def is_subtype(sub_id, super_id) do
     # A <: B  <=>  A & ~B == none
+    IO.inspect("sub_id in is_subtype")
+    Tdd.print_tdd(sub_id)
     IO.inspect("negate(super_id) in is_subtype")
     Tdd.print_tdd(negate(super_id))
     IO.inspect("intersect(sub_id, negate(super_id)) in is_subtype")
@@ -1029,30 +1032,17 @@ defmodule Tdd do
   end
 
   defp compute_op(op_name, u1_id, u2_id, constraints) do
-    # 1. Saturate constraints to detect contradictions early.
     case PredicateLogic.saturate(constraints) do
       :contradiction ->
-        # This path is impossible given the constraints.
+        # This path is impossible. For an intersection, the result is the empty set.
-        # The meaning of a contradiction depends on the operation.
+        handle_contradiction(op_name)
-        case op_name do
-          :intersect -> type_none()
-          # Placeholder for a more robust sum logic
-          :sum -> if u1_id, do: u2_id, else: u1_id
-          # not(false) -> true
-          :negate -> type_any()
-        end
 
       {:ok, saturated_constraints} ->
-        # Simplify inputs based on saturated constraints before recursing.
+        # REMOVED: No more pre-simplifying inputs here.
-        s1 = simplify(u1_id, saturated_constraints)
+        # We pass the original IDs and the full context to dispatch_op.
-        s2 = if u2_id, do: simplify(u2_id, saturated_constraints), else: nil
+        n1 = Core.get_node(u1_id)
-
+        n2 = Core.get_node(u2_id)
-        # Get node details of the *simplified* inputs.
+        dispatch_op(op_name, u1_id, n1, u2_id, n2, saturated_constraints)
-        n1 = Core.get_node(s1)
-        n2 = if s2, do: Core.get_node(s2), else: nil
-
-        # Dispatch to the actual operation logic.
-        dispatch_op(op_name, s1, n1, s2, n2, saturated_constraints)
     end
   end
 
@@ -1067,7 +1057,22 @@ defmodule Tdd do
   defp handle_contradiction(:sum), do: type_none()
 
   # This is the replacement for the "implied value" check in the old `simplify_with_constraints`.
-  defp simplify(id, constraints) do
+  def simplify(id, constraints) do
+    # Memoization is critical for performance
+    cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()}
+
+    if cached = Core.get_op_cache(cache_key) do
+      cached
+    else
+      # We will call saturate at the beginning of the operation (in compute_op),
+      # so we can assume constraints are consistent here.
+      res = compute_simplify(id, constraints)
+      Core.put_op_cache(cache_key, res)
+      res
+    end
+  end
+
+  defp compute_simplify(id, constraints) do
     case Core.get_node(id) do
       true ->
         type_any()
@@ -1075,8 +1080,8 @@ defmodule Tdd do
       false ->
         type_none()
 
-      {var, y, n, _d} ->
+      {var, y, n, d} ->
-        # Check for direct constraint first.
+        # First, check if the variable is directly constrained
         case Map.get(constraints, var) do
           true ->
             simplify(y, constraints)
@@ -1085,68 +1090,83 @@ defmodule Tdd do
             simplify(n, constraints)
 
           :dc ->
-            # For now, we don't have logic to imply :dc, so we just follow the branch.
+            simplify(d, constraints)
-            # A more advanced system might, but it's not needed for these tests.
-            simplify(_d, constraints)
 
+          # If not directly constrained, check for an *implied* constraint
           nil ->
             case PredicateLogic.check_implication(var, constraints) do
-              true -> simplify(y, constraints)
+              true ->
-              false -> simplify(n, constraints)
+                simplify(y, constraints)
-              # The path is not forced, so the node cannot be simplified away.
+
-              :unknown -> id
+              false ->
+                simplify(n, constraints)
+
+              # If the node cannot be eliminated, we MUST simplify its children
+              # and rebuild the node. This is the key fix.
+              :unknown ->
+                res_y = simplify(y, Map.put(constraints, var, true))
+                res_n = simplify(n, Map.put(constraints, var, false))
+                res_d = simplify(d, Map.put(constraints, var, :dc))
+                Core.make_node(var, res_y, res_n, res_d)
             end
         end
     end
   end
 
-  defp dispatch_op(op_name, s1, n1, s2, n2, constraints) do
+  defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do
-    op_lambda = op_lambda(op_name)
+    # --- Step 1: Simplify the current nodes under the given constraints. ---
+    # This is the crucial change. We simplify first, before doing anything else.
+    s1_id = simplify(u1_id, constraints)
+    s2_id = simplify(u2_id, constraints)
 
-    cond do
+    # If simplification resolved either to a terminal, we can take a shortcut.
-      # Case 1: Both inputs are terminals. This is the base case.
+    if Core.terminal_id?(s1_id) or Core.terminal_id?(s2_id) do
-      (n1 == true or n1 == false) and (n2 == true or n2 == false) ->
+      apply_terminals(op_name, s1_id, s2_id)
-        res = op_lambda.(n1, n2)
+    else
-        if res == true, do: type_any(), else: type_none()
+      # --- Step 2: Get details of the *simplified* nodes and proceed. ---
+      sn1 = Core.get_node(s1_id)
+      sn2 = Core.get_node(s2_id)
 
-      # Case 2: The first input (s1) is a terminal, but s2 is not.
+      {var1, y1, n1_child, d1} = sn1
-      n1 == true or n1 == false ->
+      {var2, y2, n2_child, d2} = sn2
-        {var2, y2, n2_child, d2} = n2
+      top_var = Enum.min([var1, var2])
-        # Recurse on the children of s2, passing s1 down unchanged.
-        res_y = do_op(op_name, s1, y2, Map.put(constraints, var2, true))
-        res_n = do_op(op_name, s1, n2_child, Map.put(constraints, var2, false))
-        res_d = do_op(op_name, s1, d2, Map.put(constraints, var2, :dc))
-        Core.make_node(var2, res_y, res_n, res_d)
 
-      # Case 3: The second input (s2) is a terminal, but s1 is not.
+      # Determine children for the recursive call based on top_var.
-      n2 == true or n2 == false ->
+      call_y1 = if(var1 == top_var, do: y1, else: s1_id)
-        {var1, y1, n1_child, d1} = n1
+      call_y2 = if(var2 == top_var, do: y2, else: s2_id)
-        # Recurse on the children of s1, passing s2 down unchanged.
+      call_n1 = if(var1 == top_var, do: n1_child, else: s1_id)
-        res_y = do_op(op_name, y1, s2, Map.put(constraints, var1, true))
+      call_n2 = if(var2 == top_var, do: n2_child, else: s2_id)
-        res_n = do_op(op_name, n1_child, s2, Map.put(constraints, var1, false))
+      call_d1 = if(var1 == top_var, do: d1, else: s1_id)
-        res_d = do_op(op_name, d1, s2, Map.put(constraints, var1, :dc))
+      call_d2 = if(var2 == top_var, do: d2, else: s2_id)
-        Core.make_node(var1, res_y, res_n, res_d)
 
-      # Case 4: Neither input is a terminal. This is the main recursive step.
+      # --- Step 3: Recurse with the original do_op entry point ---
-      true ->
+      res_y = do_op(op_name, call_y1, call_y2, Map.put(constraints, top_var, true))
-        {var1, y1, n1_child, d1} = n1
+      res_n = do_op(op_name, call_n1, call_n2, Map.put(constraints, top_var, false))
-        {var2, y2, n2_child, d2} = n2
+      res_d = do_op(op_name, call_d1, call_d2, Map.put(constraints, top_var, :dc))
-        top_var = Enum.min([var1, var2])
 
-        # Determine the children for the recursive call based on the top variable.
+      Core.make_node(top_var, res_y, res_n, res_d)
-        # If a node's variable is not the top_var, we pass the node's ID itself.
+    end
-        # If it *is* the top_var, we pass its child's ID.
+  end
-        call_y1 = if(var1 == top_var, do: y1, else: s1)
-        call_y2 = if(var2 == top_var, do: y2, else: s2)
-        call_n1 = if(var1 == top_var, do: n1_child, else: s1)
-        call_n2 = if(var2 == top_var, do: n2_child, else: s2)
-        call_d1 = if(var1 == top_var, do: d1, else: s1)
-        call_d2 = if(var2 == top_var, do: d2, else: s2)
 
-        res_y = do_op(op_name, call_y1, call_y2, Map.put(constraints, top_var, true))
+  defp apply_terminals(op_name, id1, id2) do
-        res_n = do_op(op_name, call_n1, call_n2, Map.put(constraints, top_var, false))
+    lambda = op_lambda(op_name)
-        res_d = do_op(op_name, call_d1, call_d2, Map.put(constraints, top_var, :dc))
+    n1 = Core.get_node(id1)
-        Core.make_node(top_var, res_y, res_n, res_d)
+    n2 = Core.get_node(id2)
+
+    # If both are terminals, just apply the op.
+    if Core.terminal_id?(id1) and Core.terminal_id?(id2) do
+      if lambda.(n1, n2), do: type_any(), else: type_none()
+    else
+      # If only one is a terminal, we must recurse on the other's children.
+      # This ensures correctness for operations like `A & true -> A`.
+      non_terminal_id = if(Core.terminal_id?(id1), do: id2, else: id1)
+      terminal_id = if(Core.terminal_id?(id1), do: id1, else: id2)
+      {var, y, n, d} = Core.get_node(non_terminal_id)
+
+      res_y = apply_terminals(op_name, y, terminal_id)
+      res_n = apply_terminals(op_name, n, terminal_id)
+      res_d = apply_terminals(op_name, d, terminal_id)
+      Core.make_node(var, res_y, res_n, res_d)
     end
   end
 
@@ -1982,227 +2002,24 @@ defmodule ListOfTests do
   end
 end
 
-# test_all.()
+defmodule AdhocTest do
-# IntegerTests.run(test)
+  import Tdd
-# TupleTests.run(test)
-# ListTests.run(test)
-# ListOfTests.run(test)
 
-a = Tdd.type_tuple([Tdd.type_int_eq(1), Tdd.type_atom_literal(:foo)])
+  def run(test_fn) do
+    tup_atom_any = type_tuple([type_atom(), type_any()])
+    tup_s2_any = type_tuple_sized_any(2)
+    # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
+    diff1 = intersect(tup_s2_any, negate(tup_atom_any))
 
-b =
+    # {integer, integer} has a first element that is not an atom, so it should be in the difference.
-  Tdd.type_tuple([
+    tup_int_int = type_tuple([type_integer(), type_integer()])
-    Tdd.type_int_gt(0),
+    test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
-    Tdd.sum(Tdd.type_atom_literal(:foo), Tdd.type_atom_literal(:bar))
+  end
-  ])
+end
 
-IO.inspect("type_tuple([type_int_eq(1), type_atom_literal(:foo)])")
+test_all.()
-a |> Tdd.print_tdd()
+IntegerTests.run(test)
-
+TupleTests.run(test)
-IO.inspect("type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])")
+ListTests.run(test)
-b |> Tdd.print_tdd()
+ListOfTests.run(test)
-
+# AdhocTest.run(test)
-test.(
-  "{1, :foo} <: {int_gt_0, :foo | :bar}",
-  true,
-  Tdd.is_subtype(a, b)
-)
-
-# output: 
-#
-# TDD system initialized with new architecture.
-# "type_tuple([type_int_eq(1), type_atom_literal(:foo)])"
-# ID 26: {{0, :is_tuple}, 25, 0, 0}
-#   Yes ->
-#   ID 25: {{4, :size, 2}, 24, 0, 0}
-#     Yes ->
-#     ID 24: {{4, :element, 0, {0, :is_integer}}, 23, 0, 0}
-#       Yes ->
-#       ID 23: {{4, :element, 0, {2, :beq, 1}}, 22, 0, 0}
-#         Yes ->
-#         ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0}
-#           Yes ->
-#           ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0}
-#             Yes ->
-#             ID 1: true
-#             No  ->
-#             ID 0: false
-#             DC  ->
-#             ID 0: false
-#           No  ->
-#           ID 0: false
-#           DC  ->
-#           ID 0: false
-#         No  ->
-#         ID 0: false
-#         DC  ->
-#         ID 0: false
-#       No  ->
-#       ID 0: false
-#       DC  ->
-#       ID 0: false
-#     No  ->
-#     ID 0: false
-#     DC  ->
-#     ID 0: false
-#   No  ->
-#   ID 0: false
-#   DC  ->
-#   ID 0: false
-# "type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])"
-# ID 40: {{0, :is_tuple}, 39, 0, 0}
-#   Yes ->
-#   ID 39: {{4, :size, 2}, 38, 0, 0}
-#     Yes ->
-#     ID 38: {{4, :element, 0, {0, :is_integer}}, 37, 0, 0}
-#       Yes ->
-#       ID 37: {{4, :element, 0, {2, :cgt, 0}}, 36, 0, 0}
-#         Yes ->
-#         ID 36: {{4, :element, 1, {0, :is_atom}}, 35, 0, 0}
-#           Yes ->
-#           ID 35: {{4, :element, 1, {1, :value, :bar}}, 1, 21, 21}
-#             Yes ->
-#             ID 1: true
-#             No  ->
-#             ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0}
-#               Yes ->
-#               ID 1: true
-#               No  ->
-#               ID 0: false
-#               DC  ->
-#               ID 0: false
-#             DC  ->
-#             ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0}
-#               Yes ->
-#               ID 1: true
-#               No  ->
-#               ID 0: false
-#               DC  ->
-#               ID 0: false
-#           No  ->
-#           ID 0: false
-#           DC  ->
-#           ID 0: false
-#         No  ->
-#         ID 0: false
-#         DC  ->
-#         ID 0: false
-#       No  ->
-#       ID 0: false
-#       DC  ->
-#       ID 0: false
-#     No  ->
-#     ID 0: false
-#     DC  ->
-#     ID 0: false
-#   No  ->
-#   ID 0: false
-#   DC  ->
-#   ID 0: false
-# "negate(super_id) in is_subtype"
-# ID 47: {{0, :is_tuple}, 46, 1, 1}
-#   Yes ->
-#   ID 46: {{4, :size, 2}, 45, 1, 1}
-#     Yes ->
-#     ID 45: {{4, :element, 0, {0, :is_integer}}, 44, 1, 1}
-#       Yes ->
-#       ID 44: {{4, :element, 0, {2, :cgt, 0}}, 43, 1, 1}
-#         Yes ->
-#         ID 43: {{4, :element, 1, {0, :is_atom}}, 42, 1, 1}
-#           Yes ->
-#           ID 42: {{4, :element, 1, {1, :value, :bar}}, 0, 41, 41}
-#             Yes ->
-#             ID 0: false
-#             No  ->
-#             ID 41: {{4, :element, 1, {1, :value, :foo}}, 0, 1, 1}
-#               Yes ->
-#               ID 0: false
-#               No  ->
-#               ID 1: true
-#               DC  ->
-#               ID 1: true
-#             DC  ->
-#             ID 41: {{4, :element, 1, {1, :value, :foo}}, 0, 1, 1}
-#               Yes ->
-#               ID 0: false
-#               No  ->
-#               ID 1: true
-#               DC  ->
-#               ID 1: true
-#           No  ->
-#           ID 1: true
-#           DC  ->
-#           ID 1: true
-#         No  ->
-#         ID 1: true
-#         DC  ->
-#         ID 1: true
-#       No  ->
-#       ID 1: true
-#       DC  ->
-#       ID 1: true
-#     No  ->
-#     ID 1: true
-#     DC  ->
-#     ID 1: true
-#   No  ->
-#   ID 1: true
-#   DC  ->
-#   ID 1: true
-# "intersect(sub_id, negate(super_id)) in is_subtype"
-# ID 52: {{0, :is_tuple}, 51, 0, 0}
-#   Yes ->
-#   ID 51: {{4, :size, 2}, 50, 0, 0}
-#     Yes ->
-#     ID 50: {{4, :element, 0, {0, :is_integer}}, 49, 0, 0}
-#       Yes ->
-#       ID 49: {{4, :element, 0, {2, :beq, 1}}, 48, 0, 0}
-#         Yes ->
-#         ID 48: {{4, :element, 0, {2, :cgt, 0}}, 0, 22, 22}
-#           Yes ->
-#           ID 0: false
-#           No  ->
-#           ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0}
-#             Yes ->
-#             ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0}
-#               Yes ->
-#               ID 1: true
-#               No  ->
-#               ID 0: false
-#               DC  ->
-#               ID 0: false
-#             No  ->
-#             ID 0: false
-#             DC  ->
-#             ID 0: false
-#           DC  ->
-#           ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0}
-#             Yes ->
-#             ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0}
-#               Yes ->
-#               ID 1: true
-#               No  ->
-#               ID 0: false
-#               DC  ->
-#               ID 0: false
-#             No  ->
-#             ID 0: false
-#             DC  ->
-#             ID 0: false
-#         No  ->
-#         ID 0: false
-#         DC  ->
-#         ID 0: false
-#       No  ->
-#       ID 0: false
-#       DC  ->
-#       ID 0: false
-#     No  ->
-#     ID 0: false
-#     DC  ->
-#     ID 0: false
-#   No  ->
-#   ID 0: false
-#   DC  ->
-#   ID 0: false
-# {1, :foo} <: {int_gt_0, :foo | :bar} (Expected: true) -> Result: false - FAILED