fix test
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
assert_equivalent_specs(spec, :integer)
This commit is contained in:
Kacper Marzecki
parent
9c6b3998c2
commit
9a89757bcd
241
lib/til.ex
241
lib/til.ex
@ -1373,87 +1373,131 @@ defmodule Tdd.Algo do
|
||||
|
||||
# This function is correct and does not need to be changed.
|
||||
defp do_apply(op_name, op_lambda, u1_id, u2_id) do
|
||||
with {:ok, u1_details} <- Store.get_node(u1_id),
|
||||
{:ok, u2_details} <- Store.get_node(u2_id) do
|
||||
cond do
|
||||
(u1_details == :true_terminal or u1_details == :false_terminal) and
|
||||
(u2_details == :true_terminal or u2_details == :false_terminal) ->
|
||||
if op_lambda.(u1_details, u2_details) == :true_terminal,
|
||||
do: Store.true_node_id(),
|
||||
else: Store.false_node_id()
|
||||
if u1_id == u2_id do
|
||||
# If both nodes are the same, the result of the operation is idempotent.
|
||||
u1_id
|
||||
else
|
||||
# The core logic for distinct nodes.
|
||||
with {:ok, u1_details} <- Store.get_node(u1_id),
|
||||
{:ok, u2_details} <- Store.get_node(u2_id) do
|
||||
cond do
|
||||
# --- Start of Logic for Placeholders ---
|
||||
|
||||
# TODO: Add cases to handle placeholder nodes co-inductively.
|
||||
# Treat the placeholder as `any`.
|
||||
match?({:ok, {:placeholder, _}}, {:ok, u1_details}) ->
|
||||
# op(placeholder, u2) -> op(any, u2)
|
||||
op_lambda.(:true_terminal, u2_details)
|
||||
|> case do
|
||||
:true_terminal -> Store.true_node_id()
|
||||
:false_terminal -> Store.false_node_id()
|
||||
# This happens if op(any, u2) = u2 (e.g., intersection)
|
||||
_other -> u2_id
|
||||
end
|
||||
# Case 1: u2 is a placeholder. We must handle this based on u1.
|
||||
match?({:placeholder, _}, u2_details) ->
|
||||
case u1_details do
|
||||
# op(true, placeholder) depends on the operation.
|
||||
:true_terminal ->
|
||||
case op_name do
|
||||
:sum -> Store.true_node_id()
|
||||
# intersect(any, p) = p
|
||||
:intersect -> u2_id
|
||||
end
|
||||
|
||||
match?({:ok, {:placeholder, _}}, {:ok, u2_details}) ->
|
||||
# op(u1, placeholder) -> op(u1, any)
|
||||
op_lambda.(u1_details, :true_terminal)
|
||||
|> case do
|
||||
:true_terminal -> Store.true_node_id()
|
||||
:false_terminal -> Store.false_node_id()
|
||||
# This happens if op(u1, any) = u1 (e.g., intersection)
|
||||
_other -> u1_id
|
||||
end
|
||||
# op(false, placeholder) also depends on the operation.
|
||||
:false_terminal ->
|
||||
case op_name do
|
||||
# sum(none, p) = p
|
||||
:sum -> u2_id
|
||||
:intersect -> Store.false_node_id()
|
||||
end
|
||||
|
||||
u1_details == :true_terminal or u1_details == :false_terminal ->
|
||||
{var2, y2, n2, d2} = u2_details
|
||||
# op(node, placeholder) -> recursively apply op to children and placeholder.
|
||||
{var1, y1, n1, d1} ->
|
||||
Store.find_or_create_node(
|
||||
var1,
|
||||
apply(op_name, op_lambda, y1, u2_id),
|
||||
apply(op_name, op_lambda, n1, u2_id),
|
||||
apply(op_name, op_lambda, d1, u2_id)
|
||||
)
|
||||
end
|
||||
|
||||
Store.find_or_create_node(
|
||||
var2,
|
||||
apply(op_name, op_lambda, u1_id, y2),
|
||||
apply(op_name, op_lambda, u1_id, n2),
|
||||
apply(op_name, op_lambda, u1_id, d2)
|
||||
)
|
||||
# Case 2: Symmetric case where u1 is the placeholder.
|
||||
match?({:placeholder, _}, u1_details) ->
|
||||
case u2_details do
|
||||
:true_terminal ->
|
||||
case op_name do
|
||||
:sum -> Store.true_node_id()
|
||||
# intersect(p, any) = p
|
||||
:intersect -> u1_id
|
||||
end
|
||||
|
||||
u2_details == :true_terminal or u2_details == :false_terminal ->
|
||||
{var1, y1, n1, d1} = u1_details
|
||||
:false_terminal ->
|
||||
case op_name do
|
||||
# sum(p, none) = p
|
||||
:sum -> u1_id
|
||||
:intersect -> Store.false_node_id()
|
||||
end
|
||||
|
||||
Store.find_or_create_node(
|
||||
var1,
|
||||
apply(op_name, op_lambda, y1, u2_id),
|
||||
apply(op_name, op_lambda, n1, u2_id),
|
||||
apply(op_name, op_lambda, d1, u2_id)
|
||||
)
|
||||
{var2, y2, n2, d2} ->
|
||||
Store.find_or_create_node(
|
||||
var2,
|
||||
apply(op_name, op_lambda, u1_id, y2),
|
||||
apply(op_name, op_lambda, u1_id, n2),
|
||||
apply(op_name, op_lambda, u1_id, d2)
|
||||
)
|
||||
end
|
||||
|
||||
true ->
|
||||
{var1, y1, n1, d1} = u1_details
|
||||
{var2, y2, n2, d2} = u2_details
|
||||
top_var = Enum.min([var1, var2])
|
||||
# --- End of Placeholder Logic ---
|
||||
# The rest of the function is the standard apply algorithm.
|
||||
|
||||
res_y =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: y1, else: u1_id),
|
||||
if(var2 == top_var, do: y2, else: u2_id)
|
||||
(u1_details == :true_terminal or u1_details == :false_terminal) and
|
||||
(u2_details == :true_terminal or u2_details == :false_terminal) ->
|
||||
if op_lambda.(u1_details, u2_details) == :true_terminal,
|
||||
do: Store.true_node_id(),
|
||||
else: Store.false_node_id()
|
||||
|
||||
u1_details == :true_terminal or u1_details == :false_terminal ->
|
||||
{var2, y2, n2, d2} = u2_details
|
||||
|
||||
Store.find_or_create_node(
|
||||
var2,
|
||||
apply(op_name, op_lambda, u1_id, y2),
|
||||
apply(op_name, op_lambda, u1_id, n2),
|
||||
apply(op_name, op_lambda, u1_id, d2)
|
||||
)
|
||||
|
||||
res_n =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: n1, else: u1_id),
|
||||
if(var2 == top_var, do: n2, else: u2_id)
|
||||
u2_details == :true_terminal or u2_details == :false_terminal ->
|
||||
{var1, y1, n1, d1} = u1_details
|
||||
|
||||
Store.find_or_create_node(
|
||||
var1,
|
||||
apply(op_name, op_lambda, y1, u2_id),
|
||||
apply(op_name, op_lambda, n1, u2_id),
|
||||
apply(op_name, op_lambda, d1, u2_id)
|
||||
)
|
||||
|
||||
res_d =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: d1, else: u1_id),
|
||||
if(var2 == top_var, do: d2, else: u2_id)
|
||||
)
|
||||
true ->
|
||||
{var1, y1, n1, d1} = u1_details
|
||||
{var2, y2, n2, d2} = u2_details
|
||||
top_var = Enum.min([var1, var2])
|
||||
|
||||
Store.find_or_create_node(top_var, res_y, res_n, res_d)
|
||||
res_y =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: y1, else: u1_id),
|
||||
if(var2 == top_var, do: y2, else: u2_id)
|
||||
)
|
||||
|
||||
res_n =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: n1, else: u1_id),
|
||||
if(var2 == top_var, do: n2, else: u2_id)
|
||||
)
|
||||
|
||||
res_d =
|
||||
apply(
|
||||
op_name,
|
||||
op_lambda,
|
||||
if(var1 == top_var, do: d1, else: u1_id),
|
||||
if(var2 == top_var, do: d2, else: u2_id)
|
||||
)
|
||||
|
||||
Store.find_or_create_node(top_var, res_y, res_n, res_d)
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
@ -1539,12 +1583,13 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
defp do_simplify(tdd_id, sorted_assumptions, context) do
|
||||
current_state = {tdd_id, sorted_assumptions}
|
||||
|
||||
if MapSet.member?(context, current_state) do
|
||||
Store.true_node_id()
|
||||
# The context now only tracks the node ID. If we see the same ID again,
|
||||
# it's an unproductive loop, regardless of the path taken to get here.
|
||||
if MapSet.member?(context, tdd_id) do
|
||||
Store.false_node_id()
|
||||
else
|
||||
new_context = MapSet.put(context, current_state)
|
||||
# Add the current ID to the context for all subsequent recursive calls.
|
||||
new_context = MapSet.put(context, tdd_id)
|
||||
assumptions = Map.new(sorted_assumptions)
|
||||
|
||||
if Engine.check(assumptions) == :contradiction do
|
||||
@ -1557,8 +1602,13 @@ defmodule Tdd.Algo do
|
||||
{:ok, :false_terminal} ->
|
||||
Store.false_node_id()
|
||||
|
||||
{:ok, {:placeholder, _}} ->
|
||||
# A placeholder should not exist in a fully formed graph being simplified.
|
||||
# This indicates that the knot-tying in the compiler did not fully resolve
|
||||
# the cycle. Encountering it means this path is unsatisfiable.
|
||||
Store.false_node_id()
|
||||
|
||||
{:ok, {var, y, n, d}} ->
|
||||
# Dispatch to the handler for recursive variables.
|
||||
case var do
|
||||
{5, :c_head, constraint_id, _} ->
|
||||
handle_recursive_subproblem(
|
||||
@ -1975,6 +2025,8 @@ defmodule Tdd.Compiler do
|
||||
id_to_cache =
|
||||
case normalized_spec do
|
||||
{:type_var, var_name} ->
|
||||
Debug.log(Map.get(context, var_name), "{:type_var, var_name}")
|
||||
|
||||
Map.get(context, var_name) ||
|
||||
raise "Tdd.Compiler: Unbound type variable: #{inspect(var_name)}"
|
||||
|
||||
@ -1989,7 +2041,6 @@ defmodule Tdd.Compiler do
|
||||
|
||||
# "Tie the knot": substitute the placeholder with the ID of the body's root.
|
||||
# This correctly forms the cyclic TDD graph using the standard algorithm.
|
||||
# The `substitute` function is designed for this and does not corrupt the store.
|
||||
final_id =
|
||||
Algo.substitute(
|
||||
body_id_with_placeholder,
|
||||
@ -1998,10 +2049,12 @@ defmodule Tdd.Compiler do
|
||||
)
|
||||
|
||||
# The resulting graph may have new simplification opportunities after the knot is tied.
|
||||
# This call to simplify, with the corrected algorithm from Fix #1, is CRITICAL.
|
||||
Algo.simplify(final_id)
|
||||
|
||||
other_spec ->
|
||||
raw_id = do_structural_compile(other_spec, context)
|
||||
# Debug.build_graph_map(raw_id, "other spec id, before simplify")
|
||||
Algo.simplify(raw_id)
|
||||
end
|
||||
|
||||
@ -2058,26 +2111,34 @@ defmodule Tdd.Compiler do
|
||||
Algo.negate(compile_normalized_spec(sub_spec, context))
|
||||
|
||||
{:cons, head_spec, tail_spec} ->
|
||||
id_list = compile_normalized_spec(:list, context)
|
||||
id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
|
||||
id_not_is_empty = Algo.negate(id_is_empty)
|
||||
# --- NEW GUARD CLAUSE ---
|
||||
# If the head or tail of a cons is known to be impossible (:none),
|
||||
# then the entire cons expression is impossible to construct.
|
||||
if head_spec == :none or tail_spec == :none do
|
||||
Store.false_node_id()
|
||||
else
|
||||
# --- EXISTING LOGIC (now safely in the 'else' block) ---
|
||||
id_list = compile_normalized_spec(:list, context)
|
||||
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)
|
||||
non_empty_list_id =
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
|
||||
|
||||
head_id = compile_normalized_spec(head_spec, context)
|
||||
tail_id = compile_normalized_spec(tail_spec, context)
|
||||
head_id = compile_normalized_spec(head_spec, context)
|
||||
tail_id = compile_normalized_spec(tail_spec, context)
|
||||
|
||||
head_checker_var = Variable.v_list_head_pred(head_id)
|
||||
head_checker_tdd = create_base_type_tdd(head_checker_var)
|
||||
head_checker_var = Variable.v_list_head_pred(head_id)
|
||||
head_checker_tdd = create_base_type_tdd(head_checker_var)
|
||||
|
||||
tail_checker_var = Variable.v_list_tail_pred(tail_id)
|
||||
tail_checker_tdd = create_base_type_tdd(tail_checker_var)
|
||||
tail_checker_var = Variable.v_list_tail_pred(tail_id)
|
||||
tail_checker_tdd = create_base_type_tdd(tail_checker_var)
|
||||
|
||||
[non_empty_list_id, head_checker_tdd, tail_checker_tdd]
|
||||
|> Enum.reduce(Store.true_node_id(), fn id, acc ->
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
|
||||
end)
|
||||
[non_empty_list_id, head_checker_tdd, tail_checker_tdd]
|
||||
|> Enum.reduce(Store.true_node_id(), fn id, acc ->
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
|
||||
end)
|
||||
end
|
||||
|
||||
{:tuple, elements_specs} ->
|
||||
size = length(elements_specs)
|
||||
|
||||
@ -32,8 +32,8 @@ defmodule TddSystemTest do
|
||||
quote do
|
||||
id1 = Compiler.spec_to_id(unquote(spec1))
|
||||
id2 = Compiler.spec_to_id(unquote(spec2))
|
||||
Debug.build_graph_map(id1, "assert_equivalent_specs id1")
|
||||
Debug.build_graph_map(id2, "assert_equivalent_specs id2")
|
||||
# Debug.build_graph_map(id1, "assert_equivalent_specs id1")
|
||||
# Debug.build_graph_map(id2, "assert_equivalent_specs id2")
|
||||
Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
|
||||
Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
|
||||
IO.inspect("equvalent specs? #{id1} #{id2}")
|
||||
@ -533,6 +533,9 @@ defmodule TddSystemTest do
|
||||
# list_of(integer & atom) is list_of(:none).
|
||||
# A list of :none can only be the empty list, as no element can ever exist.
|
||||
spec = {:list_of, {:intersect, [:integer, :atom]}}
|
||||
Tdd.Store.init()
|
||||
Debug.print_tdd_graph(Compiler.spec_to_id(spec))
|
||||
Debug.print_tdd_graph(Compiler.spec_to_id({:literal, []}))
|
||||
assert_equivalent_specs(spec, {:literal, []})
|
||||
end
|
||||
end
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user