some progress with recursive checks

new.exs

@@ -517,6 +517,57 @@ defmodule Tdd.Store do
     Process.put(@op_cache_key, Map.put(cache, cache_key, result))
     :ok
   end
+
+@doc """
+  Creates a unique, temporary placeholder node for a recursive spec.
+  Returns the ID of this placeholder.
+  """
+  @spec create_placeholder(TypeSpec.t()) :: non_neg_integer()
+  def create_placeholder(spec) do
+    # The variable is a unique tuple that won't conflict with real predicates.
+    # The children are meaningless (-1) as they will be replaced.
+    find_or_create_node({:placeholder, spec}, -1, -1, -1)
+  end
+
+  @doc """
+  Updates a node's details directly. This is a special-purpose, mutable-style
+  operation used exclusively by the compiler to "tie the knot" for recursive types.
+  It updates both the forward and reverse lookup tables.
+  """
+  @spec update_node_in_place(
+          non_neg_integer(),
+          new_details ::
+            {:ok,
+             {term(), non_neg_integer(), non_neg_integer(), non_neg_integer()}
+             | :true_terminal
+             | :false_terminal}
+        ) :: :ok
+  def update_node_in_place(id, {:ok, new_details}) do
+    # Get current state
+    nodes = Process.get(@nodes_key)
+    node_by_id = Process.get(@node_by_id_key)
+
+    # 1. Find and remove the old reverse mapping from the `nodes` table.
+    #    The node at `id` is a placeholder, so its details are what we created above.
+    old_details = Map.get(node_by_id, id)
+    nodes = Map.delete(nodes, old_details)
+
+    # 2. Add the new reverse mapping to the `nodes` table.
+    #    But only if the new details correspond to a non-terminal node.
+    nodes =
+      case new_details do
+        {_v, _y, _n, _d} -> Map.put(nodes, new_details, id)
+        _ -> nodes
+      end
+
+    # 3. Update the main `node_by_id` table.
+    node_by_id = Map.put(node_by_id, id, new_details)
+
+    # 4. Save the updated tables.
+    Process.put(@nodes_key, nodes)
+    Process.put(@node_by_id_key, node_by_id)
+    :ok
+  end
 end
 
 defmodule Tdd.Variable do
@@ -1097,10 +1148,9 @@ defmodule Tdd.Algo do
     current_state = {tdd_id, sorted_assumptions}
 
     # Coinductive base case: if we have seen this exact state before in this
-    # call stack, we are in a loop. For a least-fixed-point type (like list_of),
-    # this represents an un-satisfiable recursive constraint, which is `none`.
+    # call stack, we are in a loop. 
     if MapSet.member?(context, current_state) do
-      Store.false_node_id()
+      Store.true_node_id()
     else
       new_context = MapSet.put(context, current_state)
       assumptions = Map.new(sorted_assumptions)
@@ -1169,7 +1219,50 @@ defmodule Tdd.Algo do
       end
     end
   end
+@doc """
+  Recursively traverses a TDD graph from `root_id`, creating a new graph
+  where all references to `from_id` are replaced with `to_id`.
 
+  This is a pure function used to "tie the knot" in recursive type compilation.
+  """
+  @spec substitute(root_id :: non_neg_integer(), from_id :: non_neg_integer(), to_id :: non_neg_integer()) ::
+          non_neg_integer()
+  def substitute(root_id, from_id, to_id) do
+    # Handle the trivial case where the root is the node to be replaced.
+    if root_id == from_id, do: to_id, else: do_substitute(root_id, from_id, to_id)
+  end
+
+  # The private helper uses memoization to avoid re-computing identical sub-graphs.
+  defp do_substitute(root_id, from_id, to_id) do
+    cache_key = {:substitute, root_id, from_id, to_id}
+
+    case Store.get_op_cache(cache_key) do
+      {:ok, result_id} ->
+        result_id
+
+      :not_found ->
+        result_id =
+          case Store.get_node(root_id) do
+            # Terminal nodes are unaffected unless they are the target of substitution.
+            {:ok, :true_terminal} -> Store.true_node_id()
+            {:ok, :false_terminal} -> Store.false_node_id()
+
+            # For internal nodes, recursively substitute in all children.
+            {:ok, {var, y, n, d}} ->
+              new_y = substitute(y, from_id, to_id)
+              new_n = substitute(n, from_id, to_id)
+              new_d = substitute(d, from_id, to_id)
+              Store.find_or_create_node(var, new_y, new_n, new_d)
+
+            # This case should not be hit if the graph is well-formed.
+            {:error, reason} ->
+               raise "substitute encountered an error getting node #{root_id}: #{reason}"
+          end
+
+        Store.put_op_cache(cache_key, result_id)
+        result_id
+    end
+  end
   # defp do_simplify(tdd_id, assumptions) do
   #   IO.inspect([tdd_id, assumptions], label: "do_simplify(tdd_id, assumptions)")
   #   # First, check if the current assumption set is already a contradiction.
@@ -1364,10 +1457,18 @@ defmodule Tdd.Compiler do
   alias Tdd.Variable
   alias Tdd.Store
   alias Tdd.Algo
-
-  @doc "The main entry point. Takes a spec and returns its TDD ID."
+ @doc """
+  The main public entry point. Takes a spec and returns its TDD ID.
+  This now delegates to a private function with a context for recursion.
+  """
   @spec spec_to_id(TypeSpec.t()) :: non_neg_integer()
   def spec_to_id(spec) do
+    # Start with an empty context map.
+    spec_to_id(spec, %{})
+  end
+ # This is the new core compilation function with a context map.
+  # The context tracks `{spec => placeholder_id}` for in-progress compilations.
+defp spec_to_id(spec, context) do
     normalized_spec = TypeSpec.normalize(spec)
     cache_key = {:spec_to_id, normalized_spec}
 
@@ -1376,54 +1477,107 @@ defmodule Tdd.Compiler do
         id
 
       :not_found ->
-        # Do the raw compilation first.
-        raw_id = do_spec_to_id(normalized_spec)
-        # THEN, do a final semantic simplification pass. This is the fix.
-        id = Algo.simplify(raw_id)
-        Store.put_op_cache(cache_key, id)
-        id
+        # Check if we are in a recursive call for a spec we're already compiling.
+        case Map.get(context, normalized_spec) do
+          placeholder_id when is_integer(placeholder_id) ->
+            placeholder_id
+
+          nil ->
+            # This is a new spec. Decide which compilation path to take.
+            if is_recursive_spec?(normalized_spec) do
+              # Use the full knot-tying logic only for recursive types.
+              compile_recursive_spec(normalized_spec, context)
+            else
+              # Use the simple, direct path for all other types.
+              compile_non_recursive_spec(normalized_spec, context)
             end
         end
+    end
+  end
+ defp is_recursive_spec?({:list_of, _}), do: true
+  defp is_recursive_spec?(_), do: false
+
+ # NEW: The logic for simple, non-recursive types.
+  defp compile_non_recursive_spec(spec, context) do
+    # Just compile the body directly. Pass context in case it contains recursive children.
+    raw_id = do_spec_to_id(spec, context)
+    final_id = Algo.simplify(raw_id)
+
+    # Cache and return.
+    Store.put_op_cache({:spec_to_id, spec}, final_id)
+    final_id
+  end
 
-  # This helper does the raw, structural compilation. It does NOT call simplify.
-  defp do_spec_to_id(spec) do
+  # NEW: The full knot-tying logic, now isolated.
+  defp compile_recursive_spec(spec, context) do
+    # 1. Create a placeholder and update the context.
+    placeholder_id = Store.create_placeholder(spec)
+    new_context = Map.put(context, spec, placeholder_id)
+
+    # 2. Compile the body. It will be built with pointers to the placeholder.
+    body_id = do_spec_to_id(spec, new_context)
+
+    # 3. THIS IS THE CRUCIAL FIX:
+    #    Instead of mutating the store, we create a NEW graph where all
+    #    internal pointers to `placeholder_id` are replaced with `body_id`.
+    #    This makes the graph point to its own root, creating the cycle.
+    final_id = Algo.substitute(body_id, placeholder_id, body_id)
+
+    # 4. Simplify the resulting (now correctly cyclic) graph.
+    simplified_id = Algo.simplify(final_id)
+
+    # 5. Cache the result and return it.
+    Store.put_op_cache({:spec_to_id, spec}, simplified_id)
+    simplified_id
+  end
+  # This helper does the raw, structural compilation.
+  # It now takes and passes down the context.
+  defp do_spec_to_id(spec, context) do
     case spec do
+      # Pass context on all recursive calls to spec_to_id/2
       :any -> Store.true_node_id()
       :none -> Store.false_node_id()
       :atom -> create_base_type_tdd(Variable.v_is_atom())
       :integer -> create_base_type_tdd(Variable.v_is_integer())
       :list -> create_base_type_tdd(Variable.v_is_list())
       :tuple -> create_base_type_tdd(Variable.v_is_tuple())
-      {:literal, val} when is_atom(val) -> compile_value_equality(:atom, Variable.v_atom_eq(val))
-      {:literal, val} when is_integer(val) -> compile_value_equality(:integer, Variable.v_int_eq(val))
-      {:literal, []} -> compile_value_equality(:list, Variable.v_list_is_empty())
-      {:integer_range, min, max} -> compile_integer_range(min, max)
+      {:literal, val} when is_atom(val) -> compile_value_equality(:atom, Variable.v_atom_eq(val), context)
+      {:literal, val} when is_integer(val) -> compile_value_equality(:integer, Variable.v_int_eq(val), context)
+      {:literal, []} -> compile_value_equality(:list, Variable.v_list_is_empty(), context)
+      {:integer_range, min, max} -> compile_integer_range(min, max, context)
 
       {:union, specs} ->
-        Enum.map(specs, &spec_to_id/1)
+        Enum.map(specs, &spec_to_id(&1, context))
         |> Enum.reduce(Store.false_node_id(), fn id, acc ->
           Algo.apply(:sum, &op_union_terminals/2, id, acc)
         end)
 
       {:intersect, specs} ->
-        Enum.map(specs, &spec_to_id/1)
+        Enum.map(specs, &spec_to_id(&1, context))
         |> Enum.reduce(Store.true_node_id(), fn id, acc ->
           Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
         end)
 
       {:negation, sub_spec} ->
-        Algo.negate(spec_to_id(sub_spec))
+        Algo.negate(spec_to_id(sub_spec, context))
 
       {:cons, head_spec, tail_spec} ->
-        id_head = spec_to_id(head_spec)
-        id_tail = spec_to_id(tail_spec)
-        compile_cons_from_ids(id_head, id_tail)
+        id_head = spec_to_id(head_spec, context)
+        id_tail = spec_to_id(tail_spec, context)
+        compile_cons_from_ids(id_head, id_tail, context)
 
       {:tuple, elements} ->
-        compile_tuple(elements)
+        compile_tuple(elements, context)
 
-      {:list_of, element_spec} ->
-        compile_list_of(element_spec)
+      # --- REMOVE THE SPECIAL CASE ---
+      # The main `spec_to_id/2` logic now handles ALL recursive types.
+      {:list_of, _element_spec} ->
+        # We need to compile the logical definition: [] | cons(E, list_of(E))
+        # The TypeSpec normalizer doesn't do this expansion, so we do it here.
+        {:ok, {:list_of, element_spec}} = {:ok, spec}
+        recursive_def = {:union, [{:literal, []}, {:cons, element_spec, spec}]}
+        # Now compile this definition. The main `spec_to_id/2` will handle the knot-tying.
+        spec_to_id(recursive_def, context)
 
       _ ->
         raise "Tdd.Compiler: Cannot compile unknown spec: #{inspect(spec)}"
@@ -1434,15 +1588,14 @@ defmodule Tdd.Compiler do
 
   defp create_base_type_tdd(var), do: Store.find_or_create_node(var, Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
 
-  defp compile_value_equality(base_type_spec, value_var) do
+ defp compile_value_equality(base_type_spec, value_var, context) do
     eq_node = create_base_type_tdd(value_var)
-    # Note: spec_to_id is safe here because it's on non-recursive base types.
-    base_node_id = spec_to_id(base_type_spec)
+    base_node_id = spec_to_id(base_type_spec, context)
     Algo.apply(:intersect, &op_intersect_terminals/2, base_node_id, eq_node)
   end
 
-  defp compile_integer_range(min, max) do
-    base_id = spec_to_id(:integer)
+  defp compile_integer_range(min, max, context) do
+    base_id = spec_to_id(:integer, context)
     lt_min_tdd = if min != :neg_inf, do: create_base_type_tdd(Variable.v_int_lt(min))
     gte_min_tdd = if lt_min_tdd, do: Algo.negate(lt_min_tdd), else: spec_to_id(:any)
     id_with_min = Algo.apply(:intersect, &op_intersect_terminals/2, base_id, gte_min_tdd)
@@ -1455,15 +1608,15 @@ defmodule Tdd.Compiler do
     end
   end
 
-  defp compile_cons_from_ids(h_id, t_id) do
+defp compile_cons_from_ids(h_id, t_id, context) do # Pass context
     # Build `list & !is_empty` manually and safely.
     id_list = create_base_type_tdd(Variable.v_is_list())
     id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
     id_not_is_empty = Algo.negate(id_is_empty)
     non_empty_list_id = Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
 
-    head_checker = sub_problem(&Variable.v_list_head_pred/1, h_id)
-    tail_checker = sub_problem(&Variable.v_list_tail_pred/1, t_id)
+    head_checker = sub_problem(&Variable.v_list_head_pred/1, h_id, context) # Pass context
+    tail_checker = sub_problem(&Variable.v_list_tail_pred/1, t_id, context) # Pass context
 
     [non_empty_list_id, head_checker, tail_checker]
     |> Enum.reduce(Store.true_node_id(), fn id, acc ->
@@ -1471,9 +1624,9 @@ defmodule Tdd.Compiler do
     end)
   end
 
-  defp compile_tuple(elements) do
+defp compile_tuple(elements, context) do
     size = length(elements)
-    base_id = spec_to_id(:tuple)
+    base_id = spec_to_id(:tuple, context)
     size_tdd = create_base_type_tdd(Variable.v_tuple_size_eq(size))
     initial_id = Algo.apply(:intersect, &op_intersect_terminals/2, base_id, size_tdd)
 
@@ -1482,57 +1635,101 @@ defmodule Tdd.Compiler do
     |> Enum.reduce(initial_id, fn {elem_spec, index}, acc_id ->
       elem_id = spec_to_id(elem_spec)
       elem_key_constructor = &Variable.v_tuple_elem_pred(index, &1)
-      elem_checker = sub_problem(elem_key_constructor, elem_id)
+    elem_checker = sub_problem(elem_key_constructor, elem_id, context) # Pass context
       Algo.apply(:intersect, &op_intersect_terminals/2, acc_id, elem_checker)
     end)
   end
 
-  defp sub_problem(sub_key_constructor, tdd_id) do
+defp do_sub_problem(sub_key_constructor, tdd_id, context) do
+  # The `if` block is now a standard multi-clause `cond` or `case` at the top.
+  # Let's use a `cond` to make the guard explicit.
+  cond do
+    # Guard against invalid IDs from placeholder children.
+    tdd_id < 0 ->
+      Store.false_node_id()
+
+    # If it's a valid ID, proceed with the main logic.
+    true ->
+      case Store.get_node(tdd_id) do
+        {:ok, :true_terminal} ->
+          Store.true_node_id()
+
+        {:ok, :false_terminal} ->
+          Store.false_node_id()
+
+        # Handle placeholders by operating on their spec, not their TDD structure.
+        {:ok, {{:placeholder, spec}, _, _, _}} ->
+          dummy_var = sub_key_constructor.(:dummy)
+
+          case dummy_var do
+            {5, :c_head, :dummy, _} ->
+              {:list_of, element_spec} = spec
+              spec_to_id(element_spec, context)
+
+            {5, :d_tail, :dummy, _} ->
+              tdd_id
+
+            {4, :b_element, index, :dummy} ->
+              {:tuple, elements} = spec
+              spec_to_id(Enum.at(elements, index), context)
+
+            _ ->
+              raise "sub_problem encountered an unhandled recursive predicate on a placeholder: #{inspect(dummy_var)}"
+          end
+
+        # The normal, non-placeholder case
+        {:ok, {var, y, n, d}} ->
+          Store.find_or_create_node(
+            sub_key_constructor.(var),
+            sub_problem(sub_key_constructor, y, context),
+            sub_problem(sub_key_constructor, n, context),
+            sub_problem(sub_key_constructor, d, context)
+          )
+
+        # This case should now be unreachable.
+        {:error, :not_found} ->
+          raise "sub_problem received an unknown tdd_id: #{tdd_id}"
+      end
+  end
+end
+
+ defp sub_problem(sub_key_constructor, tdd_id, context) do
     cache_key = {:sub_problem, sub_key_constructor, tdd_id}
+    # Note: context is not part of the cache key. This is a simplification that
+    # assumes the result of a sub_problem is independent of the wider compilation
+    # context, which is true for our use case.
     case Store.get_op_cache(cache_key) do
-      {:ok, result_id} -> result_id
+      {:ok, result_id} ->
+        result_id
+
       :not_found ->
-        result_id = do_sub_problem(sub_key_constructor, tdd_id)
+        result_id = do_sub_problem(sub_key_constructor, tdd_id, context)
         Store.put_op_cache(cache_key, result_id)
         result_id
     end
   end
 
-  defp do_sub_problem(sub_key_constructor, tdd_id) do
-    case Store.get_node(tdd_id) do
-      {:ok, :true_terminal} -> Store.true_node_id()
-      {:ok, :false_terminal} -> Store.false_node_id()
-      {:ok, {var, y, n, d}} ->
-        Store.find_or_create_node(
-          sub_key_constructor.(var),
-          sub_problem(sub_key_constructor, y),
-          sub_problem(sub_key_constructor, n),
-          sub_problem(sub_key_constructor, d)
-        )
-    end
-  end
-
-  defp compile_list_of(element_spec) do
-    norm_elem_spec = TypeSpec.normalize(element_spec)
-    cache_key = {:compile_list_of, norm_elem_spec}
-    case Store.get_op_cache(cache_key) do
-      {:ok, id} -> id
-      :not_found ->
-        id = do_compile_list_of(norm_elem_spec)
-        Store.put_op_cache(cache_key, id)
-        id
-    end
-  end
-
-  defp do_compile_list_of(element_spec) do
-    id_elem = spec_to_id(element_spec)
-    id_empty_list = spec_to_id({:literal, []})
-    step_function = fn id_x ->
-      id_cons = compile_cons_from_ids(id_elem, id_x)
-      Algo.apply(:sum, &op_union_terminals/2, id_empty_list, id_cons)
-    end
-    loop_until_stable(Store.false_node_id(), step_function)
-  end
+  # defp compile_list_of(element_spec) do
+  #   norm_elem_spec = TypeSpec.normalize(element_spec)
+  #   cache_key = {:compile_list_of, norm_elem_spec}
+  #   case Store.get_op_cache(cache_key) do
+  #     {:ok, id} -> id
+  #     :not_found ->
+  #       id = do_compile_list_of(norm_elem_spec)
+  #       Store.put_op_cache(cache_key, id)
+  #       id
+  #   end
+  # end
+  #
+  # defp do_compile_list_of(element_spec) do
+  #   id_elem = spec_to_id(element_spec)
+  #   id_empty_list = spec_to_id({:literal, []})
+  #   step_function = fn id_x ->
+  #     id_cons = compile_cons_from_ids(id_elem, id_x)
+  #     Algo.apply(:sum, &op_union_terminals/2, id_empty_list, id_cons)
+  #   end
+  #   loop_until_stable(Store.false_node_id(), step_function)
+  # end
 
   # THIS IS THE FINAL, CORRECTED LOOP
 defp loop_until_stable(prev_id, step_function, iteration \\ 0) do