checkpoint before next attempt at recursive types - noice debugging here
This commit is contained in:
Kacper Marzecki
parent
ff557cb221
commit
bcddae26cb
293
new.exs
293
new.exs
@ -575,7 +575,6 @@ defmodule Tdd.Variable do
|
||||
# @spec v_list_all_elements_are(TypeSpec.t()) :: term()
|
||||
# def v_list_all_elements_are(element_spec), do: {5, :a_all_elements, element_spec, nil}
|
||||
|
||||
|
||||
@doc "Predicate: The list is the empty list `[]`."
|
||||
@spec v_list_is_empty() :: term()
|
||||
def v_list_is_empty, do: {5, :b_is_empty, nil, nil}
|
||||
@ -1093,7 +1092,7 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
# The private helper now takes a `context` to detect infinite recursion.
|
||||
# The private helper now takes a `context` to detect infinite recursion.
|
||||
# The private helper now takes a `context` to detect infinite recursion.
|
||||
defp do_simplify(tdd_id, sorted_assumptions, context) do
|
||||
current_state = {tdd_id, sorted_assumptions}
|
||||
|
||||
@ -1369,7 +1368,6 @@ defmodule Tdd.Compiler do
|
||||
@doc "The main entry point. Takes a spec and returns its TDD ID."
|
||||
@spec spec_to_id(TypeSpec.t()) :: non_neg_integer()
|
||||
def spec_to_id(spec) do
|
||||
# Memoization wrapper for the entire compilation process.
|
||||
normalized_spec = TypeSpec.normalize(spec)
|
||||
cache_key = {:spec_to_id, normalized_spec}
|
||||
|
||||
@ -1378,125 +1376,76 @@ defmodule Tdd.Compiler do
|
||||
id
|
||||
|
||||
:not_found ->
|
||||
id = do_spec_to_id(normalized_spec)
|
||||
# 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
|
||||
end
|
||||
end
|
||||
|
||||
# The core compilation logic.
|
||||
# This helper does the raw, structural compilation. It does NOT call simplify.
|
||||
defp do_spec_to_id(spec) do
|
||||
raw_id =
|
||||
case spec do
|
||||
# --- Base Types ---
|
||||
:any ->
|
||||
Store.true_node_id()
|
||||
case spec do
|
||||
: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)
|
||||
|
||||
:none ->
|
||||
Store.false_node_id()
|
||||
{:union, specs} ->
|
||||
Enum.map(specs, &spec_to_id/1)
|
||||
|> Enum.reduce(Store.false_node_id(), fn id, acc ->
|
||||
Algo.apply(:sum, &op_union_terminals/2, id, acc)
|
||||
end)
|
||||
|
||||
:atom ->
|
||||
create_base_type_tdd(Variable.v_is_atom())
|
||||
{:intersect, specs} ->
|
||||
Enum.map(specs, &spec_to_id/1)
|
||||
|> Enum.reduce(Store.true_node_id(), fn id, acc ->
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
|
||||
end)
|
||||
|
||||
:integer ->
|
||||
create_base_type_tdd(Variable.v_is_integer())
|
||||
{:negation, sub_spec} ->
|
||||
Algo.negate(spec_to_id(sub_spec))
|
||||
|
||||
:list ->
|
||||
create_base_type_tdd(Variable.v_is_list())
|
||||
{: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)
|
||||
|
||||
:tuple ->
|
||||
create_base_type_tdd(Variable.v_is_tuple())
|
||||
{:tuple, elements} ->
|
||||
compile_tuple(elements)
|
||||
|
||||
# --- Literal Types ---
|
||||
{:literal, val} when is_atom(val) ->
|
||||
compile_value_equality(:atom, Variable.v_atom_eq(val))
|
||||
{:list_of, element_spec} ->
|
||||
compile_list_of(element_spec)
|
||||
|
||||
{: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 ---
|
||||
{:integer_range, min, max} ->
|
||||
compile_integer_range(min, max)
|
||||
|
||||
# --- Set-Theoretic Combinators ---
|
||||
{:union, specs} ->
|
||||
ids = Enum.map(specs, &spec_to_id/1)
|
||||
|
||||
Enum.reduce(ids, Store.false_node_id(), fn id, acc ->
|
||||
Algo.apply(:sum, &op_union_terminals/2, id, acc)
|
||||
end)
|
||||
|
||||
{:intersect, specs} ->
|
||||
ids = Enum.map(specs, &spec_to_id/1)
|
||||
|
||||
Enum.reduce(ids, 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))
|
||||
|
||||
# --- RECURSIVE TYPES ---
|
||||
#
|
||||
# {:list_of, element_spec} ->
|
||||
# id_list = spec_to_id(:list)
|
||||
# # The element_spec MUST be normalized to be a canonical part of the variable.
|
||||
norm_elem_spec = TypeSpec.normalize(element_spec)
|
||||
var = Variable.v_list_all_elements_are(norm_elem_spec)
|
||||
# id_check = create_base_type_tdd(var)
|
||||
# Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
|
||||
{: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)
|
||||
|
||||
{:tuple, elements} ->
|
||||
compile_tuple(elements)
|
||||
|
||||
|
||||
# --- Default ---
|
||||
_ ->
|
||||
raise "Tdd.Compiler: Cannot compile unknown spec: #{inspect(spec)}"
|
||||
end
|
||||
|
||||
# CRUCIAL: Every constructed TDD must be passed through simplify
|
||||
# to ensure it's in its canonical, semantically-reduced form.
|
||||
Algo.simplify(raw_id)
|
||||
_ ->
|
||||
raise "Tdd.Compiler: Cannot compile unknown spec: #{inspect(spec)}"
|
||||
end
|
||||
end
|
||||
|
||||
# ------------------------------------------------------------------
|
||||
# Private Compilation Helpers
|
||||
# ------------------------------------------------------------------
|
||||
# --- Private Helpers ---
|
||||
|
||||
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()
|
||||
)
|
||||
end
|
||||
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
|
||||
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)
|
||||
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)
|
||||
|
||||
id_with_min =
|
||||
if min == :neg_inf do
|
||||
base_id
|
||||
else
|
||||
lt_min_tdd = create_base_type_tdd(Variable.v_int_lt(min))
|
||||
gte_min_tdd = Algo.negate(lt_min_tdd)
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, base_id, gte_min_tdd)
|
||||
end
|
||||
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)
|
||||
|
||||
if max == :pos_inf do
|
||||
id_with_min
|
||||
@ -1506,49 +1455,18 @@ defmodule Tdd.Compiler do
|
||||
end
|
||||
end
|
||||
|
||||
# ------------------------------------------------------------------
|
||||
# Helpers for Compositional Recursive Types (`cons`, `tuple`)
|
||||
# ------------------------------------------------------------------
|
||||
|
||||
defp sub_problem(sub_key_constructor, tdd_id) do
|
||||
cache_key = {:sub_problem, sub_key_constructor, tdd_id}
|
||||
|
||||
case Store.get_op_cache(cache_key) do
|
||||
{:ok, result_id} ->
|
||||
result_id
|
||||
|
||||
:not_found ->
|
||||
result_id = do_sub_problem(sub_key_constructor, tdd_id)
|
||||
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}} ->
|
||||
lifted_var = sub_key_constructor.(var)
|
||||
lifted_y = sub_problem(sub_key_constructor, y)
|
||||
lifted_n = sub_problem(sub_key_constructor, n)
|
||||
lifted_d = sub_problem(sub_key_constructor, d)
|
||||
Store.find_or_create_node(lifted_var, lifted_y, lifted_n, lifted_d)
|
||||
end
|
||||
end
|
||||
|
||||
defp compile_cons_from_ids(h_id, t_id) do
|
||||
non_empty_list_id = spec_to_id({:intersect, [:list, {:negation, {:literal, []}}]})
|
||||
# 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)
|
||||
|
||||
ids_to_intersect = [non_empty_list_id, head_checker, tail_checker]
|
||||
|
||||
Enum.reduce(ids_to_intersect, Store.true_node_id(), fn id, acc ->
|
||||
[non_empty_list_id, head_checker, tail_checker]
|
||||
|> Enum.reduce(Store.true_node_id(), fn id, acc ->
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
|
||||
end)
|
||||
end
|
||||
@ -1569,19 +1487,38 @@ defmodule Tdd.Compiler do
|
||||
end)
|
||||
end
|
||||
|
||||
# ------------------------------------------------------------------
|
||||
# Helper for Self-Recursive Types (`list_of`) via Fixed-Point Iteration
|
||||
# ------------------------------------------------------------------
|
||||
defp sub_problem(sub_key_constructor, tdd_id) do
|
||||
cache_key = {:sub_problem, sub_key_constructor, tdd_id}
|
||||
case Store.get_op_cache(cache_key) do
|
||||
{:ok, result_id} -> result_id
|
||||
:not_found ->
|
||||
result_id = do_sub_problem(sub_key_constructor, tdd_id)
|
||||
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
|
||||
cache_key = {:compile_list_of, element_spec}
|
||||
|
||||
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
|
||||
|
||||
{:ok, id} -> id
|
||||
:not_found ->
|
||||
id = do_compile_list_of(element_spec)
|
||||
id = do_compile_list_of(norm_elem_spec)
|
||||
Store.put_op_cache(cache_key, id)
|
||||
id
|
||||
end
|
||||
@ -1590,50 +1527,50 @@ defmodule Tdd.Compiler do
|
||||
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 FIX ---
|
||||
defp loop_until_stable(prev_id, step_function) do
|
||||
# At each step, we must simplify the result to get its canonical form.
|
||||
# This ensures we are comparing semantic equality, not just structural.
|
||||
raw_next_id = step_function.(prev_id)
|
||||
next_id = Algo.simplify(raw_next_id)
|
||||
# THIS IS THE FINAL, CORRECTED LOOP
|
||||
defp loop_until_stable(prev_id, step_function, iteration \\ 0) do
|
||||
IO.puts("\n--- Fixed-Point Iteration: #{iteration} ---")
|
||||
IO.inspect(prev_id, label: "prev_id")
|
||||
# Tdd.Debug.print(prev_id) # Optional: uncomment for full graph
|
||||
|
||||
if next_id == prev_id do
|
||||
next_id
|
||||
else
|
||||
loop_until_stable(next_id, step_function)
|
||||
raw_next_id = step_function.(prev_id)
|
||||
IO.inspect(raw_next_id, label: "raw_next_id (after step_function)")
|
||||
Tdd.Debug.print(raw_next_id) # Let's see the raw graph
|
||||
|
||||
# Crucially, simplify after each step for canonical comparison.
|
||||
next_id = Algo.simplify(raw_next_id)
|
||||
IO.inspect(next_id, label: "next_id (after simplify)")
|
||||
Tdd.Debug.print(next_id) # Let's see the simplified graph
|
||||
|
||||
if next_id == prev_id do
|
||||
IO.puts("--- Fixed-Point Reached! ---")
|
||||
next_id
|
||||
else
|
||||
# Add a safety break for debugging
|
||||
if iteration > 2 do
|
||||
IO.inspect Process.info(self(), :current_stacktrace)
|
||||
raise "Fixed-point iteration did not converge after 2 steps. Halting."
|
||||
end
|
||||
loop_until_stable(next_id, step_function, iteration + 1)
|
||||
end
|
||||
end
|
||||
|
||||
# ------------------------------------------------------------------
|
||||
# Private Functions for Terminal Logic
|
||||
# ------------------------------------------------------------------
|
||||
|
||||
defp op_union_terminals(u1_details, u2_details) do
|
||||
case {u1_details, u2_details} do
|
||||
{:true_terminal, _} -> :true_terminal
|
||||
{_, :true_terminal} -> :true_terminal
|
||||
{:false_terminal, t2} -> t2
|
||||
{t1, :false_terminal} -> t1
|
||||
end
|
||||
end
|
||||
|
||||
defp op_intersect_terminals(u1_details, u2_details) do
|
||||
case {u1_details, u2_details} do
|
||||
{:false_terminal, _} -> :false_terminal
|
||||
{_, :false_terminal} -> :false_terminal
|
||||
{:true_terminal, t2} -> t2
|
||||
{t1, :true_terminal} -> t1
|
||||
end
|
||||
end
|
||||
# --- Private Functions for Terminal Logic ---
|
||||
defp op_union_terminals(:true_terminal, _), do: :true_terminal
|
||||
defp op_union_terminals(_, :true_terminal), do: :true_terminal
|
||||
defp op_union_terminals(t, :false_terminal), do: t
|
||||
defp op_union_terminals(:false_terminal, t), do: t
|
||||
defp op_intersect_terminals(:false_terminal, _), do: :false_terminal
|
||||
defp op_intersect_terminals(_, :false_terminal), do: :false_terminal
|
||||
defp op_intersect_terminals(t, :true_terminal), do: t
|
||||
defp op_intersect_terminals(:true_terminal, t), do: t
|
||||
end
|
||||
|
||||
####
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user