checkpoint

new.exs

@@ -386,6 +386,552 @@ defmodule Tdd.Variable do
   def v_list_tail_pred(nested_pred_var), do: {5, :d_tail, nested_pred_var, nil}
 end
 
+defmodule Tdd.Predicate.Info do
+  @moduledoc "A knowledge base for the properties of TDD predicate variables."
+  alias Tdd.Variable
+
+  @doc "Returns a map of traits for a given predicate variable."
+  @spec get_traits(term()) :: map() | nil
+  def get_traits({0, :is_atom, _, _}), do: %{type: :primary, category: :atom}
+  def get_traits({0, :is_integer, _, _}), do: %{type: :primary, category: :integer}
+  def get_traits({0, :is_list, _, _}), do: %{type: :primary, category: :list}
+  def get_traits({0, :is_tuple, _, _}), do: %{type: :primary, category: :tuple}
+
+  def get_traits({1, :value, _val, _}) do
+    %{type: :atom_value, category: :atom, implies: [{Variable.v_is_atom(), true}]}
+  end
+
+  def get_traits({2, :alt, _, _}),
+    do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]}
+
+  def get_traits({2, :beq, _, _}),
+    do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]}
+
+  def get_traits({2, :cgt, _, _}),
+    do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]}
+
+  def get_traits({4, :a_size, _, _}) do
+    %{type: :tuple_prop, category: :tuple, implies: [{Variable.v_is_tuple(), true}]}
+  end
+
+  def get_traits({4, :b_element, index, _nested_var}) do
+    %{
+      type: :tuple_recursive,
+      category: :tuple,
+      sub_key: {:elem, index},
+      implies: [{Variable.v_is_tuple(), true}]
+    }
+  end
+
+  def get_traits({5, :a_all_elements, element_spec, _}) do
+    %{
+      type: :list_recursive_ambient,
+      category: :list,
+      ambient_constraint_spec: element_spec,
+      implies: [{Variable.v_is_list(), true}]
+    }
+  end
+
+  def get_traits({5, :b_is_empty, _, _}) do
+    %{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]}
+  end
+
+  def get_traits({5, :c_head, _nested_var, _}) do
+    %{
+      type: :list_recursive,
+      category: :list,
+      sub_key: :head,
+      implies: [{Variable.v_is_list(), true}, {Variable.v_list_is_empty(), false}]
+    }
+  end
+
+  def get_traits({5, :d_tail, _nested_var, _}) do
+    %{
+      type: :list_recursive,
+      category: :list,
+      sub_key: :tail,
+      implies: [{Variable.v_is_list(), true}, {Variable.v_list_is_empty(), false}]
+    }
+  end
+
+  # Default case for unknown variables
+  def get_traits(_), do: nil
+end
+
+# in a new file, e.g., lib/tdd/consistency/engine.ex
+defmodule Tdd.Consistency.Engine do
+  @moduledoc """
+    A rule-based engine for checking the semantic consistency of a set of assumptions.
+    Placeholders: The check_atom_consistency and check_integer_consistency functions are placeholders. They would need to be filled in with the logic for checking unique values and valid ranges, respectively.
+
+    The Circular Dependency: The check_recursive_consistency function highlights the deepest challenge. To properly check if a head's assumed type is compatible with a list_of(X) constraint, the consistency engine needs to ask the TDD compiler: "What is the TDD for the type implied by these head assumptions?" and "What is the TDD for X?", and then call is_subtype. This creates a cycle: Algo.simplify -> Engine.check -> Compiler.spec_to_id -> Algo.simplify.
+
+    Breaking the Cycle: The standard way to break this cycle is to pass a "compiler handle" or context down through the calls. Engine.check wouldn't call the top-level compiler, but a recursive version that knows it's already inside a compilation. For now, we will leave this logic incomplete, as fully implementing it is a major task. The key is that we have isolated where this hard problem lives.
+  """
+
+  alias Tdd.Predicate.Info
+
+  @doc "Checks if a map of assumptions is logically consistent."
+  @spec check(map()) :: :consistent | :contradiction
+  def check(assumptions) do
+    with {:ok, expanded} <- expand_with_implications(assumptions),
+         :ok <- check_flat_consistency(expanded),
+         :ok <- check_recursive_consistency(expanded) do
+      :consistent
+    else
+      :error -> :contradiction
+    end
+  end
+
+  # Expands the assumption set by recursively adding all implied truths.
+  defp expand_with_implications(assumptions, new_implications \\ true) do
+    if new_implications == false do
+      {:ok, assumptions}
+    else
+      {next_assumptions, added_new} =
+        Enum.reduce(assumptions, {assumptions, false}, fn
+          {var, true}, {acc, changed} ->
+            case Info.get_traits(var) do
+              %{implies: implies_list} ->
+                Enum.reduce(implies_list, {acc, changed}, fn {implied_var, implied_val},
+                                                             {inner_acc, inner_changed} ->
+                  case Map.get(inner_acc, implied_var) do
+                    nil -> {Map.put(inner_acc, implied_var, implied_val), true}
+                    ^implied_val -> {inner_acc, inner_changed}
+                    # Mark for immediate failure
+                    _ -> {Map.put(inner_acc, :__contradiction__, true), true}
+                  end
+                end)
+
+              _ ->
+                {acc, changed}
+            end
+
+          _other_assumption, acc ->
+            acc
+        end)
+
+      if Map.has_key?(next_assumptions, :__contradiction__) do
+        :error
+      else
+        expand_with_implications(next_assumptions, added_new)
+      end
+    end
+  end
+
+  # Checks for contradictions on a "flat" set of properties for a single entity.
+  defp check_flat_consistency(assumptions) do
+    # Group assumptions by category defined in Predicate.Info
+    by_category =
+      Enum.group_by(assumptions, fn {var, _val} ->
+        case Info.get_traits(var) do
+          %{category: cat} -> cat
+          _ -> :unknown
+        end
+      end)
+
+    # Chain together all the individual checks
+    # Add tuple, etc. checks here
+    with :ok <-
+           check_primary_exclusivity(
+             Map.get(by_category, :atom, []),
+             Map.get(by_category, :integer, []),
+             Map.get(by_category, :list, []),
+             Map.get(by_category, :tuple, [])
+           ),
+         :ok <- check_atom_consistency(Map.get(by_category, :atom, [])),
+         :ok <- check_integer_consistency(Map.get(by_category, :integer, [])),
+         :ok <- check_list_flat_consistency(Map.get(by_category, :list, [])) do
+      :ok
+    else
+      :error -> :error
+    end
+  end
+
+  # Checks that at most one primary type is true.
+  defp check_primary_exclusivity(atom_asm, int_asm, list_asm, tuple_asm) do
+    # Simplified: count how many primary types are constrained to be true
+    true_primary_types =
+      [atom_asm, int_asm, list_asm, tuple_asm]
+      |> Enum.count(fn assumptions_list ->
+        # A primary type is true if its main var is explicitly true,
+        # or if any of its property vars are true.
+        Enum.any?(assumptions_list, fn {_, val} -> val == true end)
+      end)
+
+    if true_primary_types > 1, do: :error, else: :ok
+  end
+
+  # Placeholder for atom-specific checks (e.g., cannot be :foo and :bar)
+  defp check_atom_consistency(_assumptions), do: :ok
+
+  # Placeholder for integer-specific checks (e.g., x < 5 and x > 10)
+  defp check_integer_consistency(_assumptions), do: :ok
+
+  # Checks for flat contradictions on a list, e.g. is_empty and has_head.
+  defp check_list_flat_consistency(assumptions) do
+    is_empty_true =
+      Enum.any?(assumptions, fn {var, val} ->
+        val == true and Info.get_traits(var)[:type] == :list_prop
+      end)
+
+    has_head_or_tail_prop =
+      Enum.any?(assumptions, fn {var, val} ->
+        val == true and Info.get_traits(var)[:type] == :list_recursive
+      end)
+
+    if is_empty_true and has_head_or_tail_prop, do: :error, else: :ok
+  end
+
+  # Handles recursive checks for structured types.
+  defp check_recursive_consistency(assumptions) do
+    # This is still a complex piece of logic, but it's now more structured.
+    # Partition assumptions into sub-problems (head, tail, elements)
+    sub_problems =
+      Enum.reduce(assumptions, %{}, fn {var, val}, acc ->
+        case Info.get_traits(var) do
+          %{type: :list_recursive, sub_key: key} ->
+            # var is e.g. {5, :c_head, {0, :is_atom, nil, nil}, nil}
+            # we want to create a sub-problem for :head with assumption {{0, :is_atom, nil, nil} => val}
+            {_cat, _pred, nested_var, _pad} = var
+            Map.update(acc, key, [{nested_var, val}], &[{nested_var, val} | &1])
+
+          %{type: :tuple_recursive, sub_key: key} ->
+            # Similar logic for tuples
+            {_cat, _pred, _index, nested_var} = var
+            Map.update(acc, key, [{nested_var, val}], &[{nested_var, val} | &1])
+
+          _ ->
+            acc
+        end
+      end)
+
+    # Get ambient constraints (e.g., from `list_of(X)`)
+    ambient_constraints =
+      Enum.reduce(assumptions, %{}, fn {var, true}, acc ->
+        case Info.get_traits(var) do
+          %{type: :list_recursive_ambient, ambient_constraint_spec: spec} ->
+            # This part is tricky. How do we enforce this?
+            # We need to know that the sub-problem's type is a subtype of this spec.
+            # This requires the TDD compiler. This is the main circular dependency.
+            # simplified for now
+            Map.put(acc, :head, spec)
+
+          _ ->
+            acc
+        end
+      end)
+
+    # Recursively check each sub-problem
+    Enum.reduce_while(sub_problems, :ok, fn {sub_key, sub_assumptions_list}, _acc ->
+      sub_assumptions_map = Map.new(sub_assumptions_list)
+      # Here we would also need to check against ambient constraints.
+      # e.g. is_subtype(build_type_from(sub_assumptions_map), ambient_constraints[sub_key])
+      # This logic remains complex.
+
+      case check(sub_assumptions_map) do
+        :consistent -> {:cont, :ok}
+        :contradiction -> {:halt, :error}
+      end
+    end)
+  end
+end
+
+# in a new file, e.g., lib/tdd/algo.ex
+# defmodule Tdd.Algo do
+#   @moduledoc "Implements the core, stateless algorithms for TDD manipulation."
+#   alias Tdd.Store
+#   alias Tdd.Consistency.Engine
+#
+#   # --- Binary Operation: Apply ---
+#   @spec apply(atom, (atom, atom -> atom), non_neg_integer, non_neg_integer) :: non_neg_integer
+#   def apply(op_name, op_lambda, u1_id, u2_id) do
+#     cache_key = {op_name, Enum.sort([u1_id, u2_id])}
+#
+#     case Store.get_op_cache(cache_key) do
+#       {:ok, result_id} ->
+#         result_id
+#
+#       :not_found ->
+#         result_id = do_apply(op_name, op_lambda, u1_id, u2_id)
+#         Store.put_op_cache(cache_key, result_id)
+#         result_id
+#     end
+#   end
+#
+#   defp do_apply(op_name, op_lambda, u1_id, u2_id) do
+#     # This is the classic Shannon Expansion algorithm (ITE - If-Then-Else)
+#     with {:ok, u1_details} <- Store.get_node(u1_id),
+#          {:ok, u2_details} <- Store.get_node(u2_id) do
+#       cond do
+#         # Terminal cases
+#         (u1_details == :true_terminal or u1_details == :false_terminal) and
+#             (u2_details == :true_terminal or u2_details == :false_terminal) ->
+#           res_terminal_symbol = op_lambda.(u1_details, u2_details)
+#
+#           if res_terminal_symbol == :true_terminal,
+#             do: Store.true_node_id(),
+#             else: Store.false_node_id()
+#
+#         # One is terminal, one is not
+#         u1_details == :true_terminal or u1_details == :false_terminal ->
+#           {var2, y2, n2, d2} = u2_details
+#           res_y = apply(op_name, op_lambda, u1_id, y2)
+#           res_n = apply(op_name, op_lambda, u1_id, n2)
+#           res_d = apply(op_name, op_lambda, u1_id, d2)
+#           Store.find_or_create_node(var2, res_y, res_n, res_d)
+#
+#         u2_details == :true_terminal or u2_details == :false_terminal ->
+#           {var1, y1, n1, d1} = u1_details
+#           res_y = apply(op_name, op_lambda, y1, u2_id)
+#           res_n = apply(op_name, op_lambda, n1, u2_id)
+#           res_d = apply(op_name, op_lambda, d1, u2_id)
+#           Store.find_or_create_node(var1, res_y, res_n, res_d)
+#
+#         # Both are non-terminals
+#         true ->
+#           {var1, y1, n1, d1} = u1_details
+#           {var2, y2, n2, d2} = u2_details
+#           # Select top variable based on global order
+#           top_var = Enum.min([var1, var2])
+#
+#           res_y =
+#             apply(
+#               op_name,
+#               op_lambda,
+#               if(var1 == top_var, do: y1, else: u1_id),
+#               if(var2 == top_var, do: y2, else: u2_id)
+#             )
+#
+#           res_n =
+#             apply(
+#               op_name,
+#               op_lambda,
+#               if(var1 == top_var, do: n1, else: u1_id),
+#               if(var2 == top_var, do: n2, else: u2_id)
+#             )
+#
+#           res_d =
+#             apply(
+#               op_name,
+#               op_lambda,
+#               if(var1 == top_var, do: d1, else: u1_id),
+#               if(var2 == top_var, do: d2, else: u2_id)
+#             )
+#
+#           Store.find_or_create_node(top_var, res_y, res_n, res_d)
+#       end
+#     end
+#   end
+#
+#   # --- Unary Operation: Negation ---
+#   @spec negate(non_neg_integer) :: non_neg_integer
+#   def negate(tdd_id) do
+#     cache_key = {:negate, tdd_id}
+#
+#     case Store.get_op_cache(cache_key) do
+#       {:ok, result_id} ->
+#         result_id
+#
+#       :not_found ->
+#         result_id =
+#           case Store.get_node(tdd_id) do
+#             {:ok, :true_terminal} ->
+#               Store.false_node_id()
+#
+#             {:ok, :false_terminal} ->
+#               Store.true_node_id()
+#
+#             {:ok, {var, y, n, d}} ->
+#               res_y = negate(y)
+#               res_n = negate(n)
+#               res_d = negate(d)
+#               Store.find_or_create_node(var, res_y, res_n, res_d)
+#           end
+#
+#         Store.put_op_cache(cache_key, result_id)
+#         result_id
+#     end
+#   end
+#
+#   # --- Unary Operation: Semantic Simplification ---
+#   @spec simplify(non_neg_integer(), map()) :: non_neg_integer()
+#   def simplify(tdd_id, assumptions) do
+#     sorted_assumptions = Enum.sort(assumptions)
+#     cache_key = {:simplify, tdd_id, sorted_assumptions}
+#
+#     case Store.get_op_cache(cache_key) do
+#       {:ok, result_id} ->
+#         result_id
+#
+#       :not_found ->
+#         result_id = do_simplify(tdd_id, assumptions)
+#         Store.put_op_cache(cache_key, result_id)
+#         result_id
+#     end
+#   end
+#
+#   defp do_simplify(tdd_id, assumptions) do
+#     # 1. Check if current path is contradictory.
+#     if Engine.check(assumptions) == :contradiction do
+#       Store.false_node_id()
+#     else
+#       case Store.get_node(tdd_id) do
+#         # 2. Handle terminal nodes.
+#         {:ok, :true_terminal} ->
+#           Store.true_node_id()
+#
+#         {:ok, :false_terminal} ->
+#           Store.false_node_id()
+#
+#         # 3. Handle non-terminal nodes.
+#         {:ok, {var, y, n, d}} ->
+#           # 4. Check if the variable is already constrained.
+#           case Map.get(assumptions, var) do
+#             true ->
+#               simplify(y, assumptions)
+#
+#             false ->
+#               simplify(n, assumptions)
+#
+#             :dc ->
+#               simplify(d, assumptions)
+#
+#             nil ->
+#               # Not constrained, so we check for implied constraints.
+#               # Note: This is an expensive part of the algorithm.
+#               # (As noted, the recursive part of the check is still incomplete)
+#               implies_true = Engine.check(Map.put(assumptions, var, false)) == :contradiction
+#               implies_false = Engine.check(Map.put(assumptions, var, true)) == :contradiction
+#
+#               cond do
+#                 # Should be caught by initial check
+#                 implies_true and implies_false ->
+#                   Store.false_node_id()
+#
+#                 implies_true ->
+#                   simplify(y, assumptions)
+#
+#                 implies_false ->
+#                   simplify(n, assumptions)
+#
+#                 true ->
+#                   # Recurse on all branches with new assumptions
+#                   s_y = simplify(y, Map.put(assumptions, var, true))
+#                   s_n = simplify(n, Map.put(assumptions, var, false))
+#                   s_d = simplify(d, Map.put(assumptions, var, :dc))
+#                   Store.find_or_create_node(var, s_y, s_n, s_d)
+#               end
+#           end
+#       end
+#     end
+#   end
+# end
+defmodule Tdd.TypeReconstructor do
+  @moduledoc """
+  Reconstructs a high-level `TypeSpec` from a low-level assumption map.
+
+  This module performs the inverse operation of the TDD compiler. It takes a
+  set of predicate assumptions (e.g., from a path in a TDD) and synthesizes
+  the most specific `TypeSpec` that satisfies all of those assumptions.
+  """
+  alias Tdd.TypeSpec
+  alias Tdd.Predicate.Info
+  alias Tdd.Variable
+
+  @doc """
+  Takes a map of `{variable, boolean}` assumptions and returns a `TypeSpec`.
+  """
+  @spec spec_from_assumptions(map()) :: TypeSpec.t()
+  def spec_from_assumptions(assumptions) do
+    # 1. Partition assumptions into groups for the top-level entity and its sub-components.
+    partitions =
+      Enum.group_by(assumptions, fn {var, _val} ->
+        case Info.get_traits(var) do
+          %{type: :list_recursive, sub_key: key} -> key # :head or :tail
+          %{type: :tuple_recursive, sub_key: key} -> key # {:elem, index}
+          # All other predicates apply to the top-level entity
+          _ -> :top_level
+        end
+      end)
+
+    # 2. Reconstruct the spec for the top-level entity from its flat assumptions.
+    top_level_assumptions = Map.get(partitions, :top_level, []) |> Map.new()
+    top_level_spec = spec_from_flat_assumptions(top_level_assumptions)
+
+    # 3. Recursively reconstruct specs for all sub-problems (head, tail, elements).
+    sub_problem_specs =
+      partitions
+      |> Map.drop([:top_level])
+      |> Enum.map(fn {sub_key, sub_assumptions_list} ->
+        # Re-map the nested variables back to their base form for the recursive call.
+        # e.g., {{5, :c_head, NESTED_VAR, _}, val} -> {NESTED_VAR, val}
+        remapped_assumptions =
+          sub_assumptions_list
+          |> Map.new(fn {var, val} ->
+            # This pattern matching is a bit simplified for clarity
+            {_cat, _pred, nested_var_or_idx, maybe_nested_var} = var
+            nested_var = if is_nil(maybe_nested_var), do: nested_var_or_idx, else: maybe_nested_var
+            {nested_var, val}
+          end)
+
+        # Recursively build the spec for the sub-problem
+        sub_spec = spec_from_assumptions(remapped_assumptions)
+
+        # Wrap it in a constructor that describes its relationship to the parent
+        case sub_key do
+          :head -> {:cons, sub_spec, :any} # Partial spec: just describes the head
+          :tail -> {:cons, :any, sub_spec} # Partial spec: just describes the tail
+          {:elem, index} ->
+            # Create a sparse tuple spec, e.g., {any, any, <sub_spec>, any}
+            # This is complex, a simpler approach is needed for now.
+            # For now, we'll just return a tuple spec that isn't fully specific.
+            # A full implementation would need to know the tuple's size.
+            {:tuple, [sub_spec]} # This is an oversimplification but works for demo
+        end
+      end)
+
+    # 4. The final spec is the intersection of the top-level spec and all sub-problem specs.
+    final_spec_list = [top_level_spec | sub_problem_specs]
+    TypeSpec.normalize({:intersect, final_spec_list})
+  end
+
+
+  @doc "Handles only the 'flat' (non-recursive) assumptions for a single entity."
+  defp spec_from_flat_assumptions(assumptions) do
+    specs =
+      Enum.map(assumptions, fn {var, bool_val} ->
+        # Convert each assumption into a `TypeSpec`.
+        # A `true` assumption means the type is `X`.
+        # A `false` assumption means the type is `¬X`.
+        spec =
+          case var do
+            {0, :is_atom, _, _} -> :atom
+            {0, :is_integer, _, _} -> :integer
+            {0, :is_list, _, _} -> :list
+            {0, :is_tuple, _, _} -> :tuple
+            {1, :value, val, _} -> {:literal, val}
+            # For integer properties, we create a range spec. This part could be more detailed.
+            {2, :alt, n, _} -> {:integer_range, :neg_inf, n - 1} # x < n
+            {2, :beq, n, _} -> {:literal, n}
+            {2, :cgt, n, _} -> {:integer_range, n + 1, :pos_inf} # x > n
+            {4, :a_size, _, _} -> :tuple # Simplified for now
+            {5, :b_is_empty, _, _} -> {:literal, []}
+            # Ignore recursive and ambient vars at this flat level
+            _ -> :any
+          end
+
+        if bool_val, do: spec, else: {:negation, spec}
+      end)
+
+    # The result is the intersection of all the individual specs.
+    TypeSpec.normalize({:intersect, specs})
+  end
+end
+####
+# xxx
+####
+
 defmodule TddStoreTests do
   def test(name, expected, result) do
     if expected == result do
@@ -695,21 +1241,31 @@ defmodule TddVariableTests do
     test("v_is_atom returns correct tuple", {0, :is_atom, nil, nil}, Variable.v_is_atom())
     test("v_atom_eq returns correct tuple", {1, :value, :foo, nil}, Variable.v_atom_eq(:foo))
     test("v_int_lt returns correct tuple", {2, :alt, 10, nil}, Variable.v_int_lt(10))
-    test("v_tuple_size_eq returns correct tuple", {4, :a_size, 2, nil}, Variable.v_tuple_size_eq(2))
+
+    test(
+      "v_tuple_size_eq returns correct tuple",
+      {4, :a_size, 2, nil},
+      Variable.v_tuple_size_eq(2)
+    )
 
     test(
       "v_tuple_elem_pred nests a variable correctly",
-      {4, :b_element, 0, {0, :is_integer, nil, nil  }},
+      {4, :b_element, 0, {0, :is_integer, nil, nil}},
       Variable.v_tuple_elem_pred(0, Variable.v_is_integer())
     )
 
-    test("v_list_is_empty returns correct tuple", {5, :b_is_empty, nil, nil}, Variable.v_list_is_empty())
+    test(
+      "v_list_is_empty returns correct tuple",
+      {5, :b_is_empty, nil, nil},
+      Variable.v_list_is_empty()
+    )
 
     test(
       "v_list_head_pred nests a variable correctly",
       {5, :c_head, {0, :is_atom, nil, nil}, nil},
       Variable.v_list_head_pred(Variable.v_is_atom())
     )
+
     test(
       "v_list_all_elements_are nests a TypeSpec correctly",
       {5, :a_all_elements, {:union, [:atom, :integer]}, nil},
@@ -760,8 +1316,13 @@ defmodule TddVariableTests do
       Variable.v_tuple_elem_pred(0, Variable.v_is_atom()) <
         Variable.v_tuple_elem_pred(0, Variable.v_is_integer())
     )
-IO.inspect(Variable.v_list_all_elements_are(:atom), label: "Variable.v_list_all_elements_are(:atom)")
+
+    IO.inspect(Variable.v_list_all_elements_are(:atom),
+      label: "Variable.v_list_all_elements_are(:atom)"
+    )
+
     IO.inspect(Variable.v_list_is_empty(), label: "Variable.v_list_is_empty()")
+
     test(
       "List :a_all_elements var < List :b_is_empty var",
       true,
@@ -792,7 +1353,351 @@ IO.inspect(Variable.v_list_all_elements_are(:atom), label: "Variable.v_list_all_
   end
 end
 
-# To run the tests, you would call this function:
+
+defmodule ConsistencyEngineTests do
+  alias Tdd.Consistency.Engine
+  alias Tdd.Variable
+
+  defp test(name, expected, assumptions_map) do
+    result = Engine.check(assumptions_map)
+    # ... test reporting logic ...
+    is_ok = (expected == result)
+    status = if is_ok, do: "[PASS]", else: "[FAIL]"
+    IO.puts("#{status} #{name}")
+    unless is_ok do
+      IO.puts("       Expected: #{inspect(expected)}, Got: #{inspect(result)}")
+      Process.put(:test_failures, [name | Process.get(:test_failures, [])])
+    end
+  end
+
+  def run() do
+    IO.puts("\n--- Running Tdd.Consistency.Engine Tests ---")
+    Process.put(:test_failures, [])
+
+    # --- Section: Basic & Implication Tests ---
+    IO.puts("\n--- Section: Basic & Implication Tests ---")
+    test("An empty assumption map is consistent", :consistent, %{})
+    test("A single valid assumption is consistent", :consistent, %{Variable.v_is_atom() => true})
+    test(
+      "An explicit contradiction is caught",
+      :contradiction,
+      %{Variable.v_is_atom() => true, Variable.v_is_atom() => false}
+    )
+    test(
+      "An implied contradiction is caught by expander",
+      :contradiction,
+      %{Variable.v_atom_eq(:foo) => true, Variable.v_is_atom() => false}
+    )
+    test(
+      "Implication creates a consistent set",
+      :consistent,
+      %{Variable.v_atom_eq(:foo) => true} # implies is_atom=true
+    )
+
+    # --- Section: Primary Type Exclusivity ---
+    IO.puts("\n--- Section: Primary Type Exclusivity ---")
+    test(
+      "Two primary types cannot both be true",
+      :contradiction,
+      %{Variable.v_is_atom() => true, Variable.v_is_integer() => true}
+    )
+    test(
+      "Two primary types implied to be true is a contradiction",
+      :contradiction,
+      %{Variable.v_atom_eq(:foo) => true, Variable.v_int_eq(5) => true}
+    )
+    test(
+      "One primary type true and another false is consistent",
+      :consistent,
+      %{Variable.v_is_atom() => true, Variable.v_is_integer() => false}
+    )
+
+
+    # --- Section: Atom Consistency ---
+    IO.puts("\n--- Section: Atom Consistency ---")
+    test(
+      "An atom cannot equal two different values",
+      :contradiction,
+      %{Variable.v_atom_eq(:foo) => true, Variable.v_atom_eq(:bar) => true}
+    )
+    test(
+      "An atom can equal one value",
+      :consistent,
+      %{Variable.v_atom_eq(:foo) => true}
+    )
+
+    # --- Section: List Flat Consistency ---
+    IO.puts("\n--- Section: List Flat Consistency ---")
+    test(
+      "A list cannot be empty and have a head property",
+      :contradiction,
+      %{Variable.v_list_is_empty() => true, Variable.v_list_head_pred(Variable.v_is_atom()) => true}
+    )
+    test(
+      "A non-empty list can have a head property",
+      :consistent,
+      %{Variable.v_list_is_empty() => false, Variable.v_list_head_pred(Variable.v_is_atom()) => true}
+    )
+    test(
+      "A non-empty list is implied by head property",
+      :consistent,
+      %{Variable.v_list_head_pred(Variable.v_is_atom()) => true} # implies is_empty=false
+    )
+
+    # --- Section: Integer Consistency ---
+    IO.puts("\n--- Section: Integer Consistency ---")
+    test("int == 5 is consistent", :consistent, %{Variable.v_int_eq(5) => true})
+    test("int == 5 AND int == 10 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_eq(10) => true})
+    test("int < 10 AND int > 20 is a contradiction", :contradiction, %{Variable.v_int_lt(10) => true, Variable.v_int_gt(20) => true})
+    test("int > 5 AND int < 4 is a contradiction", :contradiction, %{Variable.v_int_gt(5) => true, Variable.v_int_lt(4) => true})
+    test("int > 5 AND int < 7 is consistent", :consistent, %{Variable.v_int_gt(5) => true, Variable.v_int_lt(7) => true}) # 6
+    test("int == 5 AND int < 3 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_lt(3) => true})
+    test("int == 5 AND int > 10 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_gt(10) => true})
+    test("int == 5 AND int > 3 is consistent", :consistent, %{Variable.v_int_eq(5) => true, Variable.v_int_gt(3) => true})
+
+    # --- Final Report ---
+    failures = Process.get(:test_failures, [])
+    if failures == [] do
+      IO.puts("\n✅ All Consistency.Engine tests passed!")
+    else
+      IO.puts("\n❌ Found #{length(failures)} test failures.")
+    end
+  end
+end
+# defmodule TddAlgoTests do
+#   alias Tdd.Store
+#   alias Tdd.Variable
+#   alias Tdd.Algo
+#   alias Tdd.TypeSpec # We need this to create stable variables
+#
+#   # --- Test Helper ---
+#   defp test(name, expected, result) do
+#     # A simple equality test is sufficient here.
+#     if expected == result do
+#       IO.puts("[PASS] #{name}")
+#     else
+#       IO.puts("[FAIL] #{name}")
+#       IO.puts("       Expected: #{inspect(expected)}")
+#       IO.puts("       Got:      #{inspect(result)}")
+#       Process.put(:test_failures, [name | Process.get(:test_failures, [])])
+#     end
+#   end
+#
+#   # Helper to pretty print a TDD for debugging
+#   defp print_tdd(id, indent \\ 0) do
+#     prefix = String.duplicate("  ", indent)
+#     case Store.get_node(id) do
+#       {:ok, details} ->
+#         IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
+#         case details do
+#           {_var, y, n, d} ->
+#             IO.puts("#{prefix}  Yes ->"); print_tdd(y, indent + 1)
+#             IO.puts("#{prefix}  No  ->"); print_tdd(n, indent + 1)
+#             IO.puts("#{prefix}  DC  ->"); print_tdd(d, indent + 1)
+#           _ -> :ok
+#         end
+#       {:error, reason} ->
+#         IO.puts("#{prefix}ID #{id}: Error - #{reason}")
+#     end
+#   end
+#
+#   # --- Test Runner ---
+#   def run() do
+#     IO.puts("\n--- Running Tdd.Algo & Tdd.Consistency.Engine Tests ---")
+#     Process.put(:test_failures, [])
+#
+#     # Setup: Initialize the store and define some basic TDDs using the new modules.
+#     Store.init()
+#     true_id = Store.true_node_id()
+#     false_id = Store.false_node_id()
+#
+#     # --- Manually build some basic type TDDs for testing ---
+#     # t_atom = if is_atom then true else false
+#     t_atom = Store.find_or_create_node(Variable.v_is_atom(), true_id, false_id, false_id)
+#     # t_int = if is_int then true else false
+#     t_int = Store.find_or_create_node(Variable.v_is_integer(), true_id, false_id, false_id)
+#
+#     # t_foo = if is_atom then (if value == :foo then true else false) else false
+#     foo_val_check = Store.find_or_create_node(Variable.v_atom_eq(:foo), true_id, false_id, false_id)
+#     t_foo = Store.find_or_create_node(Variable.v_is_atom(), foo_val_check, false_id, false_id)
+#
+#     # t_bar = if is_atom then (if value == :bar then true else false) else false
+#     bar_val_check = Store.find_or_create_node(Variable.v_atom_eq(:bar), true_id, false_id, false_id)
+#     t_bar = Store.find_or_create_node(Variable.v_is_atom(), bar_val_check, false_id, false_id)
+#
+#     # --- Section: Negate Algorithm ---
+#     IO.puts("\n--- Section: Algo.negate ---")
+#     negated_true = Algo.negate(true_id)
+#     test("negate(true) is false", false_id, negated_true)
+#     negated_false = Algo.negate(false_id)
+#     test("negate(false) is true", true_id, negated_false)
+#     # Double negation should be identity
+#     test("negate(negate(t_atom)) is t_atom", t_atom, Algo.negate(Algo.negate(t_atom)))
+#
+#     # --- Section: Apply Algorithm (Union & Intersection) ---
+#     IO.puts("\n--- Section: Algo.apply (raw structural operations) ---")
+#     op_sum = fn
+#         :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal
+#         t, :false_terminal -> t; :false_terminal, t -> t
+#     end
+#     op_intersect = fn
+#         :false_terminal, _ -> :false_terminal; _, :false_terminal -> :false_terminal
+#         t, :true_terminal -> t; :true_terminal, t -> t
+#     end
+#
+#     # atom | int
+#     sum_atom_int = Algo.apply(:sum, op_sum, t_atom, t_int)
+#     # The result should be a node that checks is_atom, then if false, checks is_int
+#     # We expect a structure like: if is_atom -> true, else -> t_int
+#     is_atom_node = {Variable.v_is_atom(), true_id, t_int, t_int}
+#     expected_sum_structure_id = Store.find_or_create_node(elem(is_atom_node, 0), elem(is_atom_node, 1), elem(is_atom_node, 2), elem(is_atom_node, 3))
+#     test("Structure of 'atom | int' is correct", expected_sum_structure_id, sum_atom_int)
+#
+#     # :foo & :bar (structurally, before simplification)
+#     # It should build a tree that checks is_atom, then value==:foo, then value==:bar
+#     # This will be complex, but the key is that it's NOT the false_id yet.
+#     intersect_foo_bar_raw = Algo.apply(:intersect, op_intersect, t_foo, t_bar)
+#     test(":foo & :bar (raw) is not the false node", false, intersect_foo_bar_raw == false_id)
+#
+#     # --- Section: Simplify Algorithm (Flat Types) ---
+#     IO.puts("\n--- Section: Algo.simplify (with Consistency.Engine) ---")
+#
+#     # An impossible structure: node that requires a value to be an atom AND an integer
+#     # This tests the `check_primary_exclusivity` rule.
+#     contradictory_assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true}
+#     # Simplifying ANYTHING under contradictory assumptions should yield `false`.
+#     simplified_under_contradiction = Algo.simplify(true_id, contradictory_assumptions)
+#     test("Simplifying under contradictory assumptions (atom & int) results in false", false_id, simplified_under_contradiction)
+#
+#     # Test implication: A property implies its primary type
+#     # A value being `:foo` implies it is an atom.
+#     assumptions_with_foo = %{Variable.v_atom_eq(:foo) => true}
+#     # If we simplify t_int under this assumption, it should become false.
+#     # The engine expands to `{is_atom: true, value==:foo: true}`. Then it sees that
+#     # the t_int node's variable `is_integer` must be false (from exclusivity rule).
+#     simplified_int_given_foo = Algo.simplify(t_int, assumptions_with_foo)
+#     test("Simplifying 'integer' given 'value==:foo' results in false", false_id, simplified_int_given_foo)
+#
+#     # Now, let's simplify the raw intersection of :foo and :bar
+#     simplified_foo_bar = Algo.simplify(intersect_foo_bar_raw, %{})
+#     # The simplify algorithm should discover the contradiction that an atom cannot be
+#     # both :foo and :bar at the same time. (This requires `check_atom_consistency` to be implemented).
+#     # For now, we stub it and test the plumbing.
+#     # Let's test a simpler contradiction that we *have* implemented.
+#     intersect_atom_int_raw = Algo.apply(:intersect, op_intersect, t_atom, t_int)
+#     simplified_atom_int = Algo.simplify(intersect_atom_int_raw, %{})
+#     test("Simplifying 'atom & int' results in false", false_id, simplified_atom_int)
+#
+#     # Test path collapsing
+#     # If we simplify 'atom | int' under the assumption 'is_atom == true', it should become `true`.
+#     simplified_sum_given_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => true})
+#     test("Simplifying 'atom | int' given 'is_atom==true' results in true", true_id, simplified_sum_given_atom)
+#     # If we simplify 'atom | int' under the assumption 'is_atom == false', it should become `t_int`.
+#     simplified_sum_given_not_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => false})
+#     test("Simplifying 'atom | int' given 'is_atom==false' results in 'integer'", t_int, simplified_sum_given_not_atom)
+#
+#
+#     # --- Final Report ---
+#     failures = Process.get(:test_failures, [])
+#     if failures == [] do
+#       IO.puts("\n✅ All Tdd.Algo tests passed!")
+#     else
+#       IO.puts("\n❌ Found #{length(failures)} test failures.")
+#       # Optional: print details of failed tests if needed
+#     end
+#   end
+# end
+defmodule TypeReconstructorTests do
+  alias Tdd.TypeReconstructor
+  alias Tdd.Variable
+  alias Tdd.TypeSpec
+
+  defp test(name, expected_spec, assumptions) do
+    # Normalize both expected and result for a canonical comparison
+    expected = TypeSpec.normalize(expected_spec)
+    result = TypeSpec.normalize(TypeReconstructor.spec_from_assumptions(assumptions))
+
+    is_ok = (expected == result)
+    status = if is_ok, do: "[PASS]", else: "[FAIL]"
+    IO.puts("#{status} #{name}")
+    unless is_ok do
+      IO.puts("       Expected: #{inspect(expected)}")
+      IO.puts("       Got:      #{inspect(result)}")
+      Process.put(:test_failures, [name | Process.get(:test_failures, [])])
+    end
+  end
+
+  def run() do
+    IO.puts("\n--- Running Tdd.TypeReconstructor Tests ---")
+    Process.put(:test_failures, [])
+
+    # --- Section: Basic Flat Reconstructions ---
+    IO.puts("\n--- Section: Basic Flat Reconstructions ---")
+    test("is_atom=true -> atom", :atom, %{Variable.v_is_atom() => true})
+    test("is_atom=false -> ¬atom", {:negation, :atom}, %{Variable.v_is_atom() => false})
+    test(
+      "is_atom=true AND value==:foo -> :foo",
+      {:literal, :foo},
+      %{Variable.v_is_atom() => true, Variable.v_atom_eq(:foo) => true}
+    )
+    test(
+      "is_atom=true AND value!=:foo -> atom & ¬:foo",
+      {:intersect, [:atom, {:negation, {:literal, :foo}}]},
+      %{Variable.v_is_atom() => true, Variable.v_atom_eq(:foo) => false}
+    )
+    test(
+      "is_integer=true AND int==5 -> 5",
+      {:literal, 5},
+      %{Variable.v_is_integer() => true, Variable.v_int_eq(5) => true}
+    )
+    test(
+      "is_list=true AND is_empty=true -> []",
+      {:literal, []},
+      %{Variable.v_is_list() => true, Variable.v_list_is_empty() => true}
+    )
+
+    # --- Section: Combined Flat Reconstructions ---
+    IO.puts("\n--- Section: Combined Flat Reconstructions ---")
+    test(
+      "int > 10 AND int < 20",
+      # This is complex. Our simple reconstructor makes two separate ranges.
+      # A more advanced one would combine them into a single {:integer_range, 11, 19}.
+      # For now, we test the current behavior.
+      {:intersect, [
+        :integer,
+        {:integer_range, 11, :pos_inf},
+        {:integer_range, :neg_inf, 19}
+      ]},
+      %{Variable.v_int_gt(10) => true, Variable.v_int_lt(20) => true}
+    )
+
+    # --- Section: Recursive Reconstructions (Simplified) ---
+    IO.puts("\n--- Section: Recursive Reconstructions ---")
+    # This tests the partitioning and recursive call logic.
+    # Our simple implementation of recursive cases means we can only test simple things.
+    test(
+      "head is an atom",
+      {:intersect, [:list, {:cons, :atom, :any}]},
+      # Assumption for `is_list=true` is implied by `v_list_head_pred`
+      %{Variable.v_list_head_pred(Variable.v_is_atom()) => true}
+    )
+
+    # Note: The recursive tests are limited by the simplifications made in the
+    # implementation (e.g., tuple reconstruction). A full implementation would
+    # require more context (like tuple size) to be passed down.
+
+    # --- Final Report ---
+    failures = Process.get(:test_failures, [])
+    if failures == [] do
+      IO.puts("\n✅ All TypeReconstructor tests passed!")
+    else
+      IO.puts("\n❌ Found #{length(failures)} test failures.")
+    end
+  end
+end
 TypeSpecTests.run()
 TddStoreTests.run()
 TddVariableTests.run()
+# TddAlgoTests.run()
+# ConsistencyEngineTests.run()
+TypeReconstructorTests.run()