checkpoint

test1.exs

@@ -1081,7 +1081,52 @@ defmodule Tdd do
         type_none()
 
       {var, y, n, d} ->
-        # First, check if the variable is directly constrained
+        # --- START OF THE CRUCIAL NEW LOGIC ---
+        # Special check for list head/tail vs. all_elements contradiction.
+        # This logic MUST be here because it requires calling TDD operations (intersect).
+        contradiction =
+          case var do
+            {5, :head, head_predicate} ->
+              all_elements_type_id =
+                Enum.find_value(constraints, fn
+                  {{5, :all_elements, type_id}, true} -> type_id
+                  _ -> nil
+                end)
+
+              if all_elements_type_id do
+                head_type = predicate_to_tdd(head_predicate)
+                # Is the required head type compatible with the element type?
+                intersect(head_type, all_elements_type_id) == type_none()
+              else
+                false
+              end
+
+            {5, :tail, tail_predicate} ->
+              all_elements_type_id =
+                Enum.find_value(constraints, fn
+                  {{5, :all_elements, type_id}, true} -> type_id
+                  _ -> nil
+                end)
+
+              if all_elements_type_id do
+                tail_type = predicate_to_tdd(tail_predicate)
+                # The tail must be a list of the element type.
+                required_tail_type = type_list_of(all_elements_type_id)
+                intersect(tail_type, required_tail_type) == type_none()
+              else
+                false
+              end
+
+            _ ->
+              false
+          end
+
+        if contradiction do
+          # The 'yes' branch is impossible. The node simplifies to its 'no' branch.
+          simplify(n, constraints)
+        else
+          # --- END OF NEW LOGIC ---
+          # Proceed with the original simplification logic.
           case Map.get(constraints, var) do
             true ->
               simplify(y, constraints)
@@ -1092,7 +1137,6 @@ defmodule Tdd do
             :dc ->
               simplify(d, constraints)
 
-          # If not directly constrained, check for an *implied* constraint
             nil ->
               case PredicateLogic.check_implication(var, constraints) do
                 true ->
@@ -1101,8 +1145,6 @@ defmodule Tdd do
                 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))
@@ -1112,6 +1154,7 @@ defmodule Tdd do
           end
         end
     end
+  end
 
   defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do
     # --- Step 1: Simplify the current nodes under the given constraints. ---
@@ -1206,6 +1249,45 @@ defmodule Tdd do
     end
   end
 
+  @doc """
+  Converts a single predicate variable into a full TDD type.
+  This is the key to comparing predicates with other TDD types.
+  """
+  defp predicate_to_tdd(predicate) do
+    # Memoize for performance, as this might be called repeatedly.
+    cache_key = {:predicate_to_tdd, predicate}
+
+    if cached = Core.get_op_cache(cache_key) do
+      cached
+    else
+      res =
+        case predicate do
+          {0, :is_atom} -> type_atom()
+          {0, :is_tuple} -> type_tuple()
+          {0, :is_integer} -> type_integer()
+          {0, :is_list} -> type_list()
+          {1, :value, val} -> type_atom_literal(val)
+          {2, :beq, n} -> type_int_eq(n)
+          {2, :alt, n} -> type_int_lt(n)
+          {2, :cgt, n} -> type_int_gt(n)
+          {4, :size, n} -> type_tuple_sized_any(n)
+          {5, :is_empty} -> type_empty_list()
+          # A head/tail predicate implies the value is a list AND has that head/tail.
+          # The inner predicate is what we care about for the type check.
+          {5, :head, inner_p} -> predicate_to_tdd(inner_p)
+          {5, :tail, inner_p} -> predicate_to_tdd(inner_p)
+          {5, :all_elements, type_id} -> type_list_of(type_id)
+          # A tuple element predicate is about the element, not the tuple itself.
+          {4, :element, _, inner_p} -> predicate_to_tdd(inner_p)
+          # Fallback for unknown/complex predicates: assume they can be anything.
+          _ -> type_any()
+        end
+
+      Core.put_op_cache(cache_key, res)
+      res
+    end
+  end
+
   @doc """
   Prints a human-readable representation of a TDD, starting from the given ID.
   It recursively prints the structure of the graph.
@@ -2006,20 +2088,38 @@ defmodule AdhocTest do
   import Tdd
 
   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))
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_pos_int = type_int_gt(0)
+    t_int_5 = type_int_eq(5)
 
-    # {integer, integer} has a first element that is not an atom, so it should be in the difference.
-    tup_int_int = type_tuple([type_integer(), type_integer()])
-    test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
+    # --- 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)
-ListOfTests.run(test)
-# AdhocTest.run(test)
+# test_all.()
+# IntegerTests.run(test)
+# TupleTests.run(test)
+# ListTests.run(test)
+# ListOfTests.run(test)
+AdhocTest.run(test)