########################  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
end

# ----------------------------------------------------------------------------------------------
defmodule Tdd.Core do
  @moduledoc """
  Core hash-consed DAG engine (unchanged except it now stores *paths* as variables).
  """

  # … (IDENTICAL to previous Core; unchanged code elided for brevity)
  # Copy your previous `Tdd.Core` implementation here verbatim – it already
  # treats the variable term as opaque, so no edits are required.
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.PredicateLogic do
  @moduledoc false
  alias Tdd.Path
  alias Tdd.Variables, as: V

  # 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}

  # ------------ public API ----------------------------------------------------

  def saturate(facts) do
    with {:ok, s} <- static_exclusions(facts),
         :ok      <- further_checks(s) do
      {:ok, s}
    else
      _ -> :contradiction
    end
  end

  def check_implication(var, constraints) do
    case {Path.primary_tag(var), Path.primitive(var)} do
      {:is_atom, {:value_eq, id}} ->
        atom_implication(id, constraints)

      {: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 path_with_tag(_sample, tag), do: [{:tag, tag}]   # helper

  # ------------ fine-grained checks ------------------------------------------

  defp further_checks(facts) do
    cond do
      atom_val_conflict?(facts)      -> :contradiction
      tuple_size_conflict?(facts)    -> :contradiction
      int_interval_conflict?(facts)  -> :contradiction
      list_structure_conflict?(facts)-> :contradiction
      true                           -> :ok
    end
  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
    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 compare_bounds(:neg_inf,_), do: -1
  defp compare_bounds(_, :pos_inf), do: -1
  defp compare_bounds(a,b), do: a-b

  # list head/tail vs empty
  defp list_structure_conflict?(facts) do
    empty? = Map.get(facts, V.v_list_is_empty()) == true
    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

  # ------------ implication helpers ------------------------------------------

  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
    Enum.find_value(constr, fn
      {p,true} when Path.primary_tag(p)==:is_atom ->
        case Path.primitive(p) do {:value_eq,id}->id; _->nil end
      _->nil
    end)
  end

  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 any_tuple_size_true(constr) do
    Enum.find_value(constr, fn
      {p,true} ->
        case Path.primitive(p) do {:length,:tuple,sz}->sz; _->nil end
      _->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

# ----------------------------------------------------------------------------------------------
#  >>>  PUBLIC API  – same as before but calling new variable builders  <<<

defmodule Tdd do
  @moduledoc """
  Public API (constructors, ops, tests) – rewritten to call **path-based variables**.
  """

  alias Tdd.Core
  alias Tdd.Variables, as: V
  alias Tdd.PredicateLogic

  # …… UNCHANGED operational code (sum/intersect/negate/simplify)…  copy from previous file
  #     only change: every old `{cat,…}` literal replaced with `V.*` helpers

  # -- System init ------------------------------------------------------------
  def init_tdd_system do
    Tdd.Path.start_link()
    Core.init()
  end

  # -- Constructors (use new variable paths) ----------------------------------
  def type_any,     do: Core.true_id()
  def type_none,    do: Core.false_id()

  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())

  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_int_eq(n), do: intersect(type_integer(), Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none()))
  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_gt(n), do: intersect(type_integer(), Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none()))

  def type_empty_tuple,
      do: intersect(type_tuple(), Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none()))

  # … rest of constructors identical, but all variable references changed to V.* …

  # NOTE: The big bodies of intersect/sum/negate/simplify etc. are COPY-PASTED from
  #       the previous file *unchanged* – they already treat variables opaquely.
end

# ----------------------------------------------------------------------------------------------
#  >>>  TEST SUITE  – unchanged behaviour  <<<

# Copy all existing tests exactly – they rely on public API, not internals.
# (Omitted here to save space; paste from original file.)

###############################################################################################