366 lines
13 KiB
Plaintext
366 lines
13 KiB
Plaintext
|
||
######################## 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.)
|
||
|
||
###############################################################################################
|
||
|