From 8b6171283dcd63dcfa59ddb862f06e5fb9d26876 Mon Sep 17 00:00:00 2001
From: Kacper Marzecki <kacper.marzecki@schibsted.com>
Date: Tue, 17 Jun 2025 12:56:04 +0200
Subject: [PATCH] checkpoint

---
 test1.exs | 965 ++++++++++++++++++++++++++----------------------------
 1 file changed, 456 insertions(+), 509 deletions(-)

diff --git a/test1.exs b/test1.exs
index 7f0b30a..3070e57 100644
--- a/test1.exs
+++ b/test1.exs
@@ -216,6 +216,148 @@ This section outlines how various Elixir-like datatypes are (or will be) represe
 This document provides a snapshot of the current TDD system and a roadmap for its extension. The core principle is the combination of structurally canonical ROBDDs (via `make_node_raw` and `apply_raw`) with a semantic simplification layer (`simplify_with_constraints`) that embeds knowledge of the type system's rules.
 """
 
+########################  TDD FOR SET-THEORETIC TYPES (v2 Path Edition)  ########################
+#
+# 0.  High-level summary ­––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
+#
+# • Each decision-node variable is a **path** - a list of **steps** that describe how to
+#   reach a primitive predicate inside a value.
+#
+#     [
+#       {:tag,      :is_tuple},              # primary discriminator
+#       {:field,    0},                      # tuple element 0
+#       {:primitive, {:value_eq, lit(:foo)}} # primitive test on that element
+#     ]
+#
+# • **Global order** is Erlang term ordering on the path list (lexicographic).
+#   Canonicality proofs need no extra machinery.
+#
+# • **Step alphabet (finite):**
+#   {:tag, primary_atom}
+#   {:field, index}                  – tuple element
+#   {:head} | {:tail}                – list
+#   {:key, lit_id} | {:has_key, lit_id} – map predicates
+#   {:primitive, primitive_test}
+#   {:typevar, var_atom}
+#
+# • Literals are interned to small integers via `Tdd.Path.lit/1`.  No runtime node-IDs ever
+#   appear in a variable key.
+#
+# • Everything else (hash-consing, operations, tests) works unchanged.
+#
+# ----------------------------------------------------------------------------------------------
+#
+#
+
+defmodule Tdd.Path do
+  @moduledoc """
+  Helper for building and analysing **path-based predicate keys**.
+
+  A *path* is a list of *steps* (tuples).  Erlang term ordering on the list is
+  the global order required for canonical TDDs.
+  """
+
+  # -- Literal interning -------------------------------------------------------
+
+  @lit_table :tdd_literal_table
+
+  def start_link, do: :ets.new(@lit_table, [:named_table, :set, :public])
+
+  @doc "Return a stable small integer for any literal (atom/int/binary/etc.)"
+  def lit(x) do
+    case :ets.lookup(@lit_table, x) do
+      [{^x, id}] ->
+        id
+
+      [] ->
+        id = :erlang.unique_integer([:positive, :monotonic])
+        :ets.insert(@lit_table, {x, id})
+        id
+    end
+  end
+
+  # -- Step constructors -------------------------------------------------------
+
+  def tag(t), do: [{:tag, t}]
+  def is_atom, do: tag(:is_atom)
+  def is_tuple, do: tag(:is_tuple)
+  def is_integer, do: tag(:is_integer)
+  def is_list, do: tag(:is_list)
+
+  def value_eq(val), do: [{:primitive, {:value_eq, lit(val)}}]
+  def int_interval({lo, hi}), do: [{:primitive, {:interval, :int, {lo, hi}}}]
+
+  def tuple_size_eq(n),
+    do: [{:tag, :is_tuple}, {:primitive, {:length, :tuple, n}}]
+
+  def tuple_field(i, inner_path),
+    do: [{:tag, :is_tuple}, {:field, i} | inner_path]
+
+  def list_is_empty, do: [{:tag, :is_list}, {:primitive, {:length, :list, 0}}]
+  def list_head(inner), do: [{:tag, :is_list}, {:head} | inner]
+  def list_tail(inner), do: [{:tag, :is_list}, {:tail} | inner]
+  def list_all(inner_tid), do: [{:tag, :is_list}, {:primitive, {:all_elements, inner_tid}}]
+
+  # Type variables
+  def typevar(v), do: [{:typevar, v}]
+
+  # -- Path inspection utilities ----------------------------------------------
+
+  def primary_tag([{:tag, t} | _]), do: t
+  def primary_tag(_), do: :unknown
+
+  def primitive([{:primitive, p}]), do: p
+  def primitive([_ | rest]), do: primitive(rest)
+  def primitive(_), do: nil
+
+  def starts_with?(path, prefix), do: Enum.take(path, length(prefix)) == prefix
+
+  def pretty(path) do
+    path
+    |> Enum.map(&step_to_string/1)
+    |> Enum.join("/")
+  end
+
+  defp step_to_string({:tag, t}), do: Atom.to_string(t)
+  defp step_to_string({:field, i}), do: "[#{i}]"
+  defp step_to_string({:head}), do: "head"
+  defp step_to_string({:tail}), do: "tail"
+  defp step_to_string({:typevar, v}), do: "var(#{v})"
+  defp step_to_string({:primitive, p}), do: inspect(p)
+  defp step_to_string(other), do: inspect(other)
+end
+
+defmodule Tdd.Variables do
+  @moduledoc false
+  alias Tdd.Path
+
+  # Primary tags
+  def v_is_atom, do: Path.is_atom()
+  def v_is_tuple, do: Path.is_tuple()
+  def v_is_integer, do: Path.is_integer()
+  def v_is_list, do: Path.is_list()
+
+  # Atom predicates
+  def v_atom_eq(a), do: Path.is_atom() ++ Path.value_eq(a)
+
+  # Integer predicates (encode eq/lt/gt via intervals)
+  def v_int_eq(n), do: Path.is_integer() ++ Path.int_interval({n, n})
+  def v_int_lt(n), do: Path.is_integer() ++ Path.int_interval({:neg_inf, n - 1})
+  def v_int_gt(n), do: Path.is_integer() ++ Path.int_interval({n + 1, :pos_inf})
+
+  # Tuple predicates
+  def v_tuple_size_eq(n), do: Path.tuple_size_eq(n)
+
+  def v_tuple_elem_pred(i, inner_var_path),
+    do: Path.tuple_field(i, inner_var_path)
+
+  # List predicates
+  def v_list_is_empty, do: Path.list_is_empty()
+  def v_list_head_pred(inner), do: Path.list_head(inner)
+  def v_list_tail_pred(inner), do: Path.list_tail(inner)
+  def v_list_all_elements_are(tid), do: Path.list_all(tid)
+end
+
 defmodule Tdd.Core do
   @moduledoc """
   The core, semantically-unaware TDD graph engine.
@@ -393,395 +535,216 @@ defmodule Tdd.Core do
 end
 
 defmodule Tdd.PredicateLogic do
-  @moduledoc "..."
+  @moduledoc false
+  alias Tdd.Path
   alias Tdd.Variables, as: V
 
-  @primary_types [:is_atom, :is_tuple, :is_integer, :is_list]
-  @primary_type_exclusivity_rules (for type <- @primary_types, into: %{} do
-                                     antecedent = {{0, type}, true}
+  # 1. Mutual exclusivity of primary tags
+  @primary [:is_atom, :is_tuple, :is_integer, :is_list]
+  @primary_pairs for a <- @primary, b <- @primary, a < b, do: {a, b}
 
-                                     consequents =
-                                       for other_type <- @primary_types,
-                                           other_type != type,
-                                           do: {{{0, other_type}, false}}
+  # ------------ public API ----------------------------------------------------
 
-                                     {antecedent, consequents}
-                                   end)
-  @rules @primary_type_exclusivity_rules
-
-  def saturate(assumptions) do
-    case apply_static_rules(assumptions) do
-      {:ok, saturated_facts} -> final_check(saturated_facts)
-      :contradiction -> :contradiction
-      {:contradiction, _} -> :contradiction
+  def saturate(facts) do
+    with {:ok, s} <- static_exclusions(facts),
+         :ok <- further_checks(s) do
+      {:ok, s}
+    else
+      _ -> :contradiction
     end
   end
 
-  defp apply_static_rules(facts) do
-    Enum.reduce(facts, {:ok, facts}, fn {var, val}, {status, acc_facts} ->
-      if status == :contradiction do
-        {:contradiction, %{}}
-      else
-        rules_for_fact = Map.get(@rules, {var, val}, [])
+  def check_implication(var, constraints) do
+    case {Path.primary_tag(var), Path.primitive(var)} do
+      {:is_atom, {:value_eq, id}} ->
+        atom_implication(id, constraints)
 
-        # --- THE CORRECTED PATTERN MATCH IS HERE ---
-        # The data is `{{{Var, Val}}}`. We need to match this shape.
-        Enum.reduce_while(rules_for_fact, {:ok, acc_facts}, fn {{consequent_var, consequent_val}},
-                                                               {_st, inner_facts} ->
-          case Map.get(inner_facts, consequent_var) do
-            nil -> {:cont, {:ok, Map.put(inner_facts, consequent_var, consequent_val)}}
-            ^consequent_val -> {:cont, {:ok, inner_facts}}
-            _ -> {:halt, {:contradiction, %{}}}
-          end
-        end)
+      {:is_tuple, {:length, :tuple, n}} ->
+        tuple_size_implication(n, constraints)
+
+      {:is_integer, {:interval, :int, intv}} ->
+        int_implication(intv, constraints)
+
+      _ ->
+        :unknown
+    end
+  end
+
+  # ------------ static exclusions --------------------------------------------
+
+  defp static_exclusions(facts) do
+    Enum.reduce_while(@primary_pairs, {:ok, facts}, fn {a, b}, {:ok, acc} ->
+      v_a = V.v_is_atom() |> path_with_tag(a)
+      v_b = V.v_is_atom() |> path_with_tag(b)
+
+      case {Map.get(acc, v_a), Map.get(acc, v_b)} do
+        {true, true} -> {:halt, :contradiction}
+        _ -> {:cont, {:ok, acc}}
       end
     end)
   end
 
-  defp final_check(facts) do
+  # helper
+  defp path_with_tag(_sample, tag), do: [{:tag, tag}]
+
+  # ------------ fine-grained checks ------------------------------------------
+
+  defp further_checks(facts) do
     cond do
-      check_atom_values(facts) == :contradiction -> :contradiction
-      check_tuple_values(facts) == :contradiction -> :contradiction
-      check_integer_ranges(facts) == :contradiction -> :contradiction
-      check_list_structure(facts) == :contradiction -> :contradiction
-      true -> {:ok, facts}
+      atom_val_conflict?(facts) -> :contradiction
+      tuple_size_conflict?(facts) -> :contradiction
+      int_interval_conflict?(facts) -> :contradiction
+      list_structure_conflict?(facts) -> :contradiction
+      true -> :ok
     end
   end
 
-  defp check_atom_values(facts) do
-    trues =
-      Enum.reduce(facts, MapSet.new(), fn
-        {{1, :value, atom_val}, true}, acc -> MapSet.put(acc, atom_val)
-        _, acc -> acc
-      end)
-
-    if MapSet.size(trues) > 1, do: :contradiction, else: :ok
-  end
-
-  defp check_tuple_values(facts) do
-    trues =
-      Enum.reduce(facts, MapSet.new(), fn
-        {{4, :size, size_val}, true}, acc -> MapSet.put(acc, size_val)
-        _, acc -> acc
-      end)
-
-    if MapSet.size(trues) > 1, do: :contradiction, else: :ok
-  end
-
-  defp check_list_structure(facts) do
-    is_assumed_empty = Map.get(facts, V.v_list_is_empty()) == true
-
-    if is_assumed_empty do
-      has_head_or_tail_pred =
-        Enum.any?(facts, fn {var, _} ->
-          case var do
-            {5, :head, _} -> true
-            {5, :tail, _} -> true
-            _ -> false
-          end
-        end)
-
-      if has_head_or_tail_pred, do: :contradiction, else: :ok
-    else
-      :ok
-    end
-  end
-
-  # --- Integer Logic ---
-
-  # THIS IS THE SINGLE, CORRECT DEFINITION TO USE
-  defp check_integer_ranges(facts) do
-    if facts[V.v_is_integer()] != true do
-      :ok
-    else
-      if calculate_integer_interval(facts) == :contradiction, do: :contradiction, else: :ok
-    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`.
-  """
-  def check_implication(predicate, constraints) do
-    case predicate do
-      # --- NEW HANDLER for primary type predicates ---
-      {0, _} ->
-        _reason_by_contradiction(predicate, constraints)
-
-      # --- EXISTING BASE CASES ---
-      {1, :value, _} ->
-        _atom_implication(predicate, constraints)
-
-      {2, _, _} ->
-        _integer_implication(predicate, constraints)
-
-      {4, :size, _} ->
-        _tuple_size_implication(predicate, constraints)
-
-      # --- EXISTING RECURSIVE CASES ---
-      {4, :element, index, inner_predicate} ->
-        element_constraints =
-          gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1))
-
-        check_implication(inner_predicate, element_constraints)
-
-      {5, :head, inner_predicate} ->
-        head_constraints =
-          gather_local_constraints(constraints, &match?({5, :head, _}, &1))
-
-        check_implication(inner_predicate, head_constraints)
-
-      {5, :tail, inner_predicate} ->
-        tail_constraints =
-          gather_local_constraints(constraints, &match?({5, :tail, _}, &1))
-
-        check_implication(inner_predicate, tail_constraints)
-
-      # --- DEFAULT CASE ---
-      _ ->
-        # We don't have specific reasoning logic for this predicate type.
-        :unknown
-    end
-  end
-
-  # ===================================================================
-  # == PRIVATE HELPERS
-  # ===================================================================
-
-  # --- Constraint Isolation Helper ---
-
-  @doc """
-  Gathers, unwraps, and isolates constraints for a specific component.
-  """
-  defp gather_local_constraints(all_constraints, filter_fun) do
-    for {var, bool_val} <- all_constraints,
-        filter_fun.(var),
-        into: %{} do
-      # Unwrap the predicate for the local check.
-      # e.g., from `{4, :element, 0, {2, :beq, 5}}` we want `{2, :beq, 5}`
-      inner_predicate = elem(var, tuple_size(var) - 1)
-      {inner_predicate, bool_val}
-    end
-  end
-
-  # --- Base Case Reasoners ---
-
-  # Reasoner for integer predicates.
-  # Renamed from `check_integer_implication` to `_integer_implication` to denote it's a private helper.
-  defp _integer_implication(predicate, constraints) do
-    case calculate_integer_interval(constraints) do
-      :contradiction ->
-        # A contradiction implies anything.
-        true
-
-      {min_val, max_val} ->
-        {_p_cat, p_type, p_val} = predicate
-
-        cond do
-          # The current interval [min, max] is a SUBSET of the predicate's interval
-          (p_type == :alt and is_integer(max_val) and max_val < p_val) or
-            (p_type == :cgt and is_integer(min_val) and min_val > p_val) or
-              (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
-            true
-
-          # The current interval [min, max] is DISJOINT from the predicate's interval
-          (p_type == :alt and is_integer(min_val) and min_val >= p_val) or
-            (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
-              (p_type == :beq and
-                 ((is_integer(min_val) and min_val > p_val) or
-                    (is_integer(max_val) and max_val < p_val))) ->
-            false
-
-          true ->
-            :unknown
-        end
-    end
-  end
-
-  # Reasoner for atom predicates using Enum.reduce
-  defp _atom_implication(predicate, constraints) do
-    # The predicate we are testing, e.g., {{1, :value, :foo}, true}
-    {{1, :value, p_val}, _} = {predicate, true}
-
-    # Use Enum.reduce to find all atom values constrained to be true or false.
-    {true_atoms, false_atoms} =
-      Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
-        # Match a constraint that an atom value MUST be true
-        {{1, :value, val}, true}, {true_set, false_set} ->
-          {MapSet.put(true_set, val), false_set}
-
-        # Match a constraint that an atom value MUST be false
-        {{1, :value, val}, false}, {true_set, false_set} ->
-          {true_set, MapSet.put(false_set, val)}
-
-        # Ignore any other kind of constraint
-        _, acc ->
-          acc
-      end)
-
-    cond do
-      # If the predicate's value is explicitly known to be false.
-      p_val in false_atoms ->
-        false
-
-      # If the predicate's value is explicitly known to be true.
-      p_val in true_atoms ->
-        true
-
-      # If we know the value MUST be something else (and it's not our predicate's value).
-      # e.g., constraints say the value is :bar, and we're checking for :foo.
-      not Enum.empty?(true_atoms) and p_val not in true_atoms ->
-        false
-
-      # Otherwise, we don't have enough information.
-      true ->
-        :unknown
-    end
-  end
-
-  # Reasoner for tuple size predicates using Enum.reduce
-  defp _tuple_size_implication(predicate, constraints) do
-    # The predicate we are testing, e.g., {{4, :size, 2}, true}
-    {{4, :size, p_val}, _} = {predicate, true}
-
-    {true_sizes, false_sizes} =
-      Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
-        {{4, :size, val}, true}, {true_set, false_set} ->
-          {MapSet.put(true_set, val), false_set}
-
-        {{4, :size, val}, false}, {true_set, false_set} ->
-          {true_set, MapSet.put(false_set, val)}
-
-        _, acc ->
-          acc
-      end)
-
-    cond do
-      # If the predicate's size is explicitly known to be false.
-      p_val in false_sizes ->
-        false
-
-      # If the predicate's size is explicitly known to be true.
-      p_val in true_sizes ->
-        true
-
-      # If we know the size MUST be something else.
-      not Enum.empty?(true_sizes) and p_val not in true_sizes ->
-        false
-
-      # Otherwise, we don't know.
-      true ->
-        :unknown
-    end
-  end
-
-  defp check_integer_implication(predicate, constraints) do
-    if constraints[V.v_is_integer()] != true do
-      :unknown
-    else
-      case calculate_integer_interval(constraints) do
-        :contradiction ->
-          true
-
-        {min_val, max_val} ->
-          {_p_cat, p_type, p_val} = predicate
-
-          cond do
-            (p_type == :alt and is_integer(max_val) and max_val < p_val) or
-              (p_type == :cgt and is_integer(min_val) and min_val > p_val) or
-                (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
-              true
-
-            (p_type == :alt and is_integer(min_val) and min_val >= p_val) or
-              (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
-                (p_type == :beq and
-                   ((is_integer(min_val) and min_val > p_val) or
-                      (is_integer(max_val) and max_val < p_val))) ->
-              false
-
-            true ->
-              :unknown
-          end
+  # atom value clash
+  defp atom_val_conflict?(facts) do
+    vals =
+      for {path, true} <- facts,
+          Path.primary_tag(path) == :is_atom,
+          {:value_eq, id} <- [Path.primitive(path)] do
+        id
       end
+
+    Enum.uniq(vals) |> length() > 1
+  end
+
+  # tuple size clash
+  defp tuple_size_conflict?(facts) do
+    sizes = for {p, true} <- facts, {:length, :tuple, n} <- [Path.primitive(p)], do: n
+    Enum.uniq(sizes) |> length > 1
+  end
+
+  # integer interval contradiction helper
+  defp int_interval_conflict?(facts) do
+    intervals =
+      for {p, true} <- facts, {:interval, :int, intv} <- [Path.primitive(p)], do: intv
+
+    case intervals do
+      [] ->
+        false
+
+      _ ->
+        Enum.reduce_while(intervals, {:neg_inf, :pos_inf}, fn
+          {:neg_inf, hi}, {:neg_inf, cur_hi} when hi < cur_hi ->
+            {:cont, {:neg_inf, hi}}
+
+          {lo, :pos_inf}, {cur_lo, :pos_inf} when lo > cur_lo ->
+            {:cont, {lo, :pos_inf}}
+
+          {lo1, hi1}, {lo2, hi2} ->
+            lo = max(lo1, lo2)
+            hi = min(hi1, hi2)
+            if compare_bounds(lo, hi) <= 0, do: {:cont, {lo, hi}}, else: {:halt, :conflict}
+        end) == :conflict
     end
   end
 
-  defp calculate_integer_interval(facts) do
-    bounds =
-      Enum.reduce(facts, %{eq: nil, min: nil, max: nil}, fn
-        {var, true}, acc ->
-          case var do
-            {2, :beq, n} ->
-              if(is_nil(acc.eq) or acc.eq == n, do: %{acc | eq: n}, else: %{acc | eq: :conflict})
+  defp compare_bounds(:neg_inf, _), do: -1
+  defp compare_bounds(_, :pos_inf), do: -1
+  defp compare_bounds(a, b), do: a - b
 
-            {2, :alt, n} ->
-              %{acc | max: min_opt(acc.max, n - 1)}
+  # list head/tail vs empty
+  defp list_structure_conflict?(facts) do
+    empty? = Map.get(facts, V.v_list_is_empty()) == true
 
-            {2, :cgt, n} ->
-              %{acc | min: max_opt(acc.min, n + 1)}
-
-            _ ->
-              acc
-          end
-
-        {var, false}, acc ->
-          case var do
-            {2, :alt, n} -> %{acc | min: max_opt(acc.min, n)}
-            {2, :cgt, n} -> %{acc | max: min_opt(acc.max, n)}
-            _ -> acc
-          end
-
-        _, acc ->
-          acc
+    if empty? do
+      Enum.any?(facts, fn {p, _} ->
+        Path.starts_with?(p, Path.list_head([])) or
+          Path.starts_with?(p, Path.list_tail([]))
       end)
+    else
+      false
+    end
+  end
 
-    cond do
-      bounds.eq == :conflict ->
-        :contradiction
+  # ------------ implication helpers ------------------------------------------
 
-      is_integer(bounds.eq) ->
-        if (is_nil(bounds.min) or bounds.eq >= bounds.min) and
-             (is_nil(bounds.max) or bounds.eq <= bounds.max) do
-          {bounds.eq, bounds.eq}
-        else
-          :contradiction
+  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
+  end
+
+  defp find_any_atom_true(constr) do
+    constr
+    |> Enum.map(fn x -> {x, Path.primary_tag(x)} end)
+
+    Enum.find_value(constr, fn
+      {{p, true}, :is_atom} ->
+        case Path.primitive(p) do
+          {:value_eq, id} -> id
+          _ -> nil
         end
 
-      is_integer(bounds.min) and is_integer(bounds.max) and bounds.min > bounds.max ->
-        :contradiction
+      _ ->
+        nil
+    end)
+  end
 
-      true ->
-        {bounds.min, bounds.max}
+  defp tuple_size_implication(n, constr) do
+    case {Map.get(constr, V.v_tuple_size_eq(n)), any_tuple_size_true(constr)} do
+      {true, _} -> true
+      {false, _} -> false
+      {nil, true_n} when true_n != n -> false
+      _ -> :unknown
     end
   end
 
-  defp min_opt(nil, x), do: x
-  defp min_opt(x, nil), do: x
-  defp min_opt(x, y), do: min(x, y)
+  defp any_tuple_size_true(constr) do
+    Enum.find_value(constr, fn
+      {p, true} ->
+        case Path.primitive(p) do
+          {:length, :tuple, sz} -> sz
+          _ -> nil
+        end
 
-  defp max_opt(nil, x), do: x
-  defp max_opt(x, nil), do: x
-  defp max_opt(x, y), do: max(x, y)
+      _ ->
+        nil
+    end)
+  end
+
+  defp int_implication(intv, constr) do
+    # intersect current interval with candidate; if unchanged ⇒ implied
+    with {:ok, {lo, hi}} <- current_int_interval(constr) do
+      if subset?(lo, hi, intv), do: true, else: :unknown
+    else
+      :none -> :unknown
+      :contradiction -> true
+    end
+  end
+
+  defp current_int_interval(constr) do
+    intvs = for {p, true} <- constr, {:interval, :int, iv} = Path.primitive(p), do: iv
+
+    case intvs do
+      [] ->
+        :none
+
+      list ->
+        Enum.reduce_while(list, {:neg_inf, :pos_inf}, fn
+          {:neg_inf, hi}, {:neg_inf, cur_hi} ->
+            {:cont, {:neg_inf, min(hi, cur_hi)}}
+
+          {lo, :pos_inf}, {cur_lo, :pos_inf} ->
+            {:cont, {max(lo, cur_lo), :pos_inf}}
+
+          {lo1, hi1}, {lo2, hi2} ->
+            lo = max(lo1, lo2)
+            hi = min(hi1, hi2)
+            if compare_bounds(lo, hi) <= 0, do: {:cont, {lo, hi}}, else: {:halt, :contradiction}
+        end)
+    end
+  end
+
+  defp subset?(lo, hi, {lo2, hi2}) do
+    compare_bounds(lo2, lo) <= 0 and compare_bounds(hi, hi2) <= 0
+  end
 end
 
 defmodule Tdd do
@@ -799,82 +762,50 @@ defmodule Tdd do
 
   # --- System Init ---
   def init_tdd_system do
+    Tdd.Path.start_link()
     Core.init()
     IO.puts("TDD system initialized with new architecture.")
   end
 
-  # --- Variable Definitions (could be in their own module) ---
-  defmodule Variables do
-    def v_is_atom, do: {0, :is_atom}
-    def v_is_tuple, do: {0, :is_tuple}
-    def v_is_integer, do: {0, :is_integer}
-    def v_is_list, do: {0, :is_list}
-    def v_atom_eq(v), do: {1, :value, v}
-    def v_int_eq(n), do: {2, :beq, n}
-    def v_int_lt(n), do: {2, :alt, n}
-    def v_int_gt(n), do: {2, :cgt, n}
-    def v_tuple_size_eq(n), do: {4, :size, n}
-    def v_tuple_elem_pred(i, v), do: {4, :element, i, v}
-    def v_list_is_empty, do: {5, :is_empty}
-    def v_list_head_pred(v), do: {5, :head, v}
-    def v_list_tail_pred(v), do: {5, :tail, v}
-    def v_list_all_elements_are(id), do: {5, :all_elements, id}
-  end
-
-  # --- Type Constructors (Completed) ---
-
   def type_any, do: Core.true_id()
   def type_none, do: Core.false_id()
 
-  # Base type constructors
   def type_atom, do: Core.make_node(V.v_is_atom(), type_any(), type_none(), type_none())
   def type_tuple, do: Core.make_node(V.v_is_tuple(), type_any(), type_none(), type_none())
   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())
 
-  # --- Atom Constructors ---
+  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(val) do
-    # A specific atom is the intersection of `atom()` and `value == val`.
-    constraint_node = Core.make_node(V.v_atom_eq(val), type_any(), type_none(), type_none())
-    intersect(type_atom(), constraint_node)
-  end
+  def type_int_eq(n),
+    do:
+      intersect(
+        type_integer(),
+        Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none())
+      )
 
-  # --- Integer Constructors ---
+  def type_int_lt(n),
+    do:
+      intersect(
+        type_integer(),
+        Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none())
+      )
 
-  def type_int_eq(n) do
-    # A specific integer is the intersection of `integer()` and `value == n`.
-    constraint_node = Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none())
-    intersect(type_integer(), constraint_node)
-  end
+  def type_int_gt(n),
+    do:
+      intersect(
+        type_integer(),
+        Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none())
+      )
 
-  def type_int_lt(n) do
-    # An integer `< n` is the intersection of `integer()` and `value < n`.
-    constraint_node = Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none())
-    intersect(type_integer(), constraint_node)
-  end
-
-  def type_int_gt(n) do
-    # An integer `> n` is the intersection of `integer()` and `value > n`.
-    constraint_node = Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none())
-    intersect(type_integer(), constraint_node)
-  end
-
-  # --- Tuple Constructors ---
-
-  def type_empty_tuple do
-    # `{}` is the intersection of `tuple()` and `size == 0`.
-    constraint_node = Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none())
-    intersect(type_tuple(), constraint_node)
-  end
-
-  def type_tuple_sized_any(size) do
-    # A tuple of a fixed size is the intersection of `tuple()` and `size == N`.
-    constraint_node =
-      Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none())
-
-    intersect(type_tuple(), constraint_node)
-  end
+  def type_empty_tuple,
+    do:
+      intersect(
+        type_tuple(),
+        Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none())
+      )
 
   def type_tuple(element_type_ids) when is_list(element_type_ids) do
     # This is the most complex tuple constructor. It represents a tuple with
@@ -900,6 +831,13 @@ defmodule Tdd do
     end)
   end
 
+  def type_tuple_sized_any(size),
+    do:
+      intersect(
+        type_tuple(),
+        Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none())
+      )
+
   # --- List Constructors ---
 
   def type_empty_list do
@@ -1081,72 +1019,82 @@ defmodule Tdd do
         type_none()
 
       {var, y, n, d} ->
+        # ----------- detect head / tail predicates in path form ---------------
         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)
+            # list head
+            [{:tag, :is_list}, {:head} | inner] ->
+              all_elements_type(constraints)
+              |> incompatible?(inner)
 
-              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
+            # list tail
+            [{:tag, :is_list}, {:tail} | inner] ->
+              all_elements_type(constraints)
+              |> incompatible_tail?(inner)
 
             _ ->
               false
           end
 
         if contradiction do
-          # The 'yes' branch is impossible. The node simplifies to its 'no' branch.
           simplify(n, constraints)
         else
-          case Map.get(constraints, var) do
-            true ->
-              simplify(y, constraints)
+          follow_or_recurse(var, y, n, d, constraints)
+        end
+    end
+  end
 
-            false ->
-              simplify(n, constraints)
+  # --- small helpers ----------------------------------------------------------
+  defp all_elements_type(constraints) do
+    Enum.find_value(constraints, fn
+      {p, true} ->
+        case Tdd.Path.primitive(p) do
+          {:all_elements, tid} -> tid
+          _ -> nil
+        end
 
-            :dc ->
-              simplify(d, constraints)
+      _ ->
+        nil
+    end)
+  end
 
-            nil ->
-              case PredicateLogic.check_implication(var, constraints) do
-                true ->
-                  simplify(y, constraints)
+  defp incompatible?(nil, _inner), do: false
+  defp incompatible?(tid, inner), do: intersect(predicate_to_tdd(inner), tid) == type_none()
 
-                false ->
-                  simplify(n, constraints)
+  # tail must be a *list* whose elements have the requested type
+  defp incompatible_tail?(nil, _inner), do: false
 
-                :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
+  defp incompatible_tail?(tid, inner) do
+    required_tail = type_list_of(tid)
+
+    intersect(predicate_to_tdd(inner), required_tail) == type_none()
+  end
+
+  # unchanged logic, just factored out
+  defp follow_or_recurse(var, y, n, d, constraints) do
+    case Map.get(constraints, var) do
+      true ->
+        simplify(y, constraints)
+
+      false ->
+        simplify(n, constraints)
+
+      :dc ->
+        simplify(d, constraints)
+
+      nil ->
+        case PredicateLogic.check_implication(var, constraints) do
+          true ->
+            simplify(y, constraints)
+
+          false ->
+            simplify(n, constraints)
+
+          :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
@@ -1248,38 +1196,40 @@ defmodule Tdd do
   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}
+  defp predicate_to_tdd(path) do
+    cache_key = {:predicate_to_tdd, path}
 
     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()
+      # generic “predicate-is-true” node
+      id = Core.make_node(path, type_any(), type_none(), type_none())
+
+      # specialised shorthands for a few common paths
+      id =
+        cond do
+          path == V.v_is_atom() ->
+            type_atom()
+
+          path == V.v_is_tuple() ->
+            type_tuple()
+
+          path == V.v_is_integer() ->
+            type_integer()
+
+          path == V.v_is_list() ->
+            type_list()
+
+          # list(all_elements = T)
+          {:all_elements, tid} = Tdd.Path.primitive(path) ->
+            type_list_of(tid)
+
+          true ->
+            id
         end
 
-      Core.put_op_cache(cache_key, res)
-      res
+      Core.put_op_cache(cache_key, id)
+      id
     end
   end
 
@@ -1289,14 +1239,19 @@ defmodule Tdd do
   """
   def print_tdd(id, indent \\ 0) do
     prefix = String.duplicate("  ", indent)
-    # Use Tdd.Core to get node details
-    details = Core.get_node(id)
+    details = Tdd.Core.get_node(id)
 
-    IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
+    variable =
+      case details do
+        {path, _, _, _} -> "  " <> Tdd.Path.pretty(path)
+        bool when bool in [true, false] -> ""
+        _ -> ""
+      end
+
+    IO.puts("#{prefix}ID #{id}: #{inspect(details)}#{variable}")
 
     case details do
-      # A variable node
-      {_var, y, n, d} ->
+      {_, y, n, d} ->
         IO.puts("#{prefix}  Yes ->")
         print_tdd(y, indent + 1)
         IO.puts("#{prefix}  No  ->")
@@ -1304,16 +1259,8 @@ defmodule Tdd do
         IO.puts("#{prefix}  DC  ->")
         print_tdd(d, indent + 1)
 
-      # Terminal nodes (:true or :false)
-      true ->
+      _ ->
         :ok
-
-      false ->
-        :ok
-
-      # Handle cases where an ID might not be found
-      nil ->
-        IO.puts("#{prefix} Error: Unknown ID #{id}")
     end
   end
 end
@@ -2112,9 +2059,9 @@ defmodule AdhocTest do
   end
 end
 
-# test_all.()
+test_all.()
 # IntegerTests.run(test)
 # TupleTests.run(test)
 # ListTests.run(test)
 # ListOfTests.run(test)
-AdhocTest.run(test)
+# AdhocTest.run(test)