one less test failing
This commit is contained in:
Kacper Marzecki
parent
2854c4559c
commit
b5a731edad
155
lib/debug.ex
155
lib/debug.ex
@ -694,4 +694,159 @@ defmodule Tdd.Debug do
|
||||
# Return the value
|
||||
value
|
||||
end
|
||||
|
||||
@doc """
|
||||
Builds a map representation of the TDD starting from a root ID.
|
||||
|
||||
This is the main entry point. It initializes the process with an empty set
|
||||
of visited nodes.
|
||||
"""
|
||||
def build_graph_map(root_id, label) do
|
||||
# The result of the recursive build is a tuple {map_data, visited_set}.
|
||||
# We only need the map_data, so we extract it with elem().
|
||||
asd =
|
||||
elem(do_build_node_map(root_id, MapSet.new(), Tdd.Store), 0)
|
||||
|> IO.inspect(label: label)
|
||||
end
|
||||
|
||||
def to_json(kv_list) do
|
||||
kv_list
|
||||
# Jason.encode!(kv_list, pretty: true)
|
||||
end
|
||||
|
||||
@doc false
|
||||
# This private helper does the actual recursive work.
|
||||
# It returns a tuple: {node_map, visited_set} so the set of visited
|
||||
# nodes can be tracked through the recursion.
|
||||
defp do_build_node_map(0, visited, _), do: {false, visited}
|
||||
defp do_build_node_map(1, visited, _), do: {true, visited}
|
||||
|
||||
defp do_build_node_map(id, visited, store_module) do
|
||||
if MapSet.member?(visited, id) do
|
||||
# A cycle or a previously processed node. Return a reference.
|
||||
{[id: id, ref: "recursive_or_seen"], visited}
|
||||
else
|
||||
# Add the current ID to the visited set before any recursion.
|
||||
new_visited = MapSet.put(visited, id)
|
||||
|
||||
case store_module.get_node(id) do
|
||||
{:ok, :true_terminal} ->
|
||||
{[id: id, value: true], new_visited}
|
||||
|
||||
{:ok, :false_terminal} ->
|
||||
{[id: id, value: false], new_visited}
|
||||
|
||||
{:ok, {var, y_id, n_id, dc_id}} ->
|
||||
# First, process the variable. This is important because the variable
|
||||
# itself might contain a sub-TDD that adds nodes to our visited set.
|
||||
{var_map, visited_after_var} = format_variable(var, new_visited, store_module)
|
||||
|
||||
# Now, recursively build the children, threading the visited set through each call.
|
||||
{yes_map, visited_after_yes} = do_build_node_map(y_id, visited_after_var, store_module)
|
||||
{no_map, visited_after_no} = do_build_node_map(n_id, visited_after_yes, store_module)
|
||||
{dc_map, final_visited} = do_build_node_map(dc_id, visited_after_no, store_module)
|
||||
|
||||
node = [
|
||||
id: id,
|
||||
# The (potentially expanded) variable map
|
||||
variable: var_map,
|
||||
yes: yes_map,
|
||||
no: no_map,
|
||||
dont_care: dc_map
|
||||
]
|
||||
|
||||
{node, final_visited}
|
||||
|
||||
{:error, reason} ->
|
||||
{[id: id, type: "error", reason: reason], new_visited}
|
||||
end
|
||||
end
|
||||
|> case do
|
||||
{node, v} ->
|
||||
n = Enum.sort_by(node, fn {k, _} -> Enum.find_index([:id, :value], &(&1 == k)) end)
|
||||
# {Jason.OrderedObject.new(n), v}
|
||||
{n, v}
|
||||
end
|
||||
end
|
||||
|
||||
@doc false
|
||||
# This helper now takes the visited set and store_module to handle nested TDDs.
|
||||
# It returns a tuple: {variable_map, updated_visited_set}.
|
||||
defp format_variable(var, visited, store_module) do
|
||||
case var do
|
||||
# --- Variables with nested TDDs ---
|
||||
{4, :b_element, index, sub_tdd_id} ->
|
||||
# Recursively build the map for the sub-TDD.
|
||||
{sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
|
||||
|
||||
var_map = [
|
||||
type: "tuple_element_predicate",
|
||||
index: index,
|
||||
predicate_tdd: sub_tdd_map
|
||||
]
|
||||
|
||||
{var_map, new_visited}
|
||||
|
||||
{5, :c_head, sub_tdd_id, nil} ->
|
||||
{sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
|
||||
|
||||
var_map = [
|
||||
type: "list_head_predicate",
|
||||
predicate_tdd: sub_tdd_map
|
||||
]
|
||||
|
||||
{var_map, new_visited}
|
||||
|
||||
{5, :d_tail, sub_tdd_id, nil} ->
|
||||
{sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
|
||||
|
||||
var_map = [
|
||||
type: "list_tail_predicate",
|
||||
predicate_tdd: sub_tdd_map
|
||||
]
|
||||
|
||||
{var_map, new_visited}
|
||||
|
||||
# --- Simple variables (no nested TDDs) ---
|
||||
{0, :is_atom, _, _} ->
|
||||
{[type: "is_atom"], visited}
|
||||
|
||||
{0, :is_integer, _, _} ->
|
||||
{[type: "is_integer"], visited}
|
||||
|
||||
{0, :is_list, _, _} ->
|
||||
{[type: "is_list"], visited}
|
||||
|
||||
{0, :is_tuple, _, _} ->
|
||||
{[type: "is_tuple"], visited}
|
||||
|
||||
{1, :value, atom_val, _} ->
|
||||
{[type: "atom_equals", value: atom_val], visited}
|
||||
|
||||
{2, :alt, n, _} ->
|
||||
{[type: "integer_less_than", value: n], visited}
|
||||
|
||||
{2, :beq, n, _} ->
|
||||
{[type: "integer_equals", value: n], visited}
|
||||
|
||||
{2, :cgt, n, _} ->
|
||||
{[type: "integer_greater_than", value: n], visited}
|
||||
|
||||
{4, :a_size, size, _} ->
|
||||
{[type: "tuple_size_equals", value: size], visited}
|
||||
|
||||
{5, :b_is_empty, _, _} ->
|
||||
{[type: "list_is_empty"], visited}
|
||||
|
||||
# --- Fallback for any other format ---
|
||||
_ ->
|
||||
{[type: "unknown", value: inspect(var)], visited}
|
||||
end
|
||||
|> case do
|
||||
{node, v} ->
|
||||
n = Enum.sort_by(node, fn {k, _} -> Enum.find_index([:id, :value], &(&1 == k)) end)
|
||||
# {Jason.OrderedObject.new(n), v}
|
||||
{n, v}
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
67
lib/til.ex
67
lib/til.ex
@ -78,38 +78,66 @@ defmodule Tdd.TypeSpec do
|
||||
end
|
||||
|
||||
{:intersect, members} ->
|
||||
recursively_reduced_members = Enum.map(members, &apply_subtype_reduction/1)
|
||||
|
||||
expanded_flattened_members =
|
||||
Enum.flat_map(recursively_reduced_members, fn
|
||||
# First, recursively reduce all members and flatten any nested intersections.
|
||||
flattened_members =
|
||||
members
|
||||
|> Enum.map(&apply_subtype_reduction/1)
|
||||
|> Enum.flat_map(fn
|
||||
{:intersect, sub_members} -> sub_members
|
||||
# get_supertypes expects normalized spec, and its output is also normalized
|
||||
# Pass flag
|
||||
m -> get_supertypes(m, true)
|
||||
# :any is the identity for intersection, so we can remove it.
|
||||
m when m == :any -> []
|
||||
m -> [m]
|
||||
end)
|
||||
|
||||
unique_no_any =
|
||||
expanded_flattened_members
|
||||
|> Enum.reject(&(&1 == :any))
|
||||
|> Enum.uniq()
|
||||
|
||||
if Enum.member?(unique_no_any, :none) do
|
||||
# If :none (the absorbing element) is present, the whole intersection is :none.
|
||||
if Enum.member?(flattened_members, :none) do
|
||||
:none
|
||||
else
|
||||
# Pass `true` for already_normalized flag to is_subtype?
|
||||
# Separate the members into unions and non-unions.
|
||||
{unions, non_unions} = Enum.split_with(flattened_members, &match?({:union, _}, &1))
|
||||
|
||||
if Enum.empty?(unions) do
|
||||
# BASE CASE: No unions to distribute. Just a simple intersection.
|
||||
# We remove any member that is a supertype of another member.
|
||||
final_members =
|
||||
Enum.reject(unique_no_any, fn member_to_check ->
|
||||
Enum.any?(unique_no_any, fn other_member ->
|
||||
Enum.reject(non_unions, fn member_to_check ->
|
||||
Enum.any?(non_unions, fn other_member ->
|
||||
member_to_check != other_member and
|
||||
is_subtype?(other_member, member_to_check, true)
|
||||
end)
|
||||
end)
|
||||
|
||||
# Further check for contradictions, e.g., intersect(:atom, :integer)
|
||||
# This is an advanced step, but for now, the TDD compiler handles it.
|
||||
# A simple check could be added here if needed.
|
||||
|
||||
case Enum.sort(final_members) do
|
||||
[] -> :any
|
||||
[single] -> single
|
||||
list_members -> {:intersect, list_members}
|
||||
end
|
||||
else
|
||||
# RECURSIVE CASE: Distribute the intersection over a union.
|
||||
[{:union, union_to_distribute} | other_unions] = unions
|
||||
|
||||
remaining_intersection =
|
||||
case non_unions ++ other_unions do
|
||||
[] -> :any
|
||||
[single] -> single
|
||||
multiple -> {:intersect, multiple}
|
||||
end
|
||||
|
||||
# Distribute: (A | B | ...) & Remainder => (A & Remainder) | (B & Remainder) | ...
|
||||
new_union_members =
|
||||
Enum.map(union_to_distribute, fn member_of_union ->
|
||||
# Recursively call apply_subtype_reduction on the new, smaller intersections.
|
||||
apply_subtype_reduction({:intersect, [member_of_union, remaining_intersection]})
|
||||
end)
|
||||
|
||||
# The result is a new union, which we also need to simplify.
|
||||
apply_subtype_reduction({:union, new_union_members})
|
||||
end
|
||||
end
|
||||
|
||||
{:negation, body} ->
|
||||
@ -2113,15 +2141,14 @@ defmodule Tdd.Compiler do
|
||||
Store.init()
|
||||
|
||||
id1 = spec_to_id(spec1)
|
||||
Debug.print_tdd_graph(id1, "IS_SUBTYPE id1")
|
||||
id2 = spec_to_id(spec2)
|
||||
Debug.print_tdd_graph(id2, "IS_SUBTYPE id2")
|
||||
Debug.build_graph_map(id1, "IS_SUBTYPE id1")
|
||||
Debug.build_graph_map(id2, "IS_SUBTYPE id2")
|
||||
IO.inspect("___________________________________")
|
||||
neg_id2 = Algo.negate(id2)
|
||||
Debug.print_tdd_graph(neg_id2, "IS_SUBTYPE neg_id2")
|
||||
Debug.build_graph_map(neg_id2, "IS_SUBTYPE neg_id2")
|
||||
intersect_id = Algo.apply(:intersect, &op_intersect_terminals/2, id1, neg_id2)
|
||||
Debug.print_tdd_graph(intersect_id, "IS_SUBTYPE intersect")
|
||||
|
||||
Debug.build_graph_map(intersect_id, "IS_SUBTYPE intersect")
|
||||
final_id = Algo.check_emptiness(intersect_id)
|
||||
final_id == Store.false_node_id()
|
||||
end
|
||||
|
||||
@ -30,14 +30,25 @@ defmodule TddSystemTest do
|
||||
# Helper to check for equivalence by comparing TDD IDs.
|
||||
defmacro assert_equivalent_specs(spec1, spec2) do
|
||||
quote do
|
||||
assert Compiler.spec_to_id(unquote(spec1)) == Compiler.spec_to_id(unquote(spec2))
|
||||
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")
|
||||
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}")
|
||||
assert id1 == id2
|
||||
end
|
||||
end
|
||||
|
||||
# Helper to check for subtyping using the TDD compiler.
|
||||
defmacro assert_subtype(spec1, spec2) do
|
||||
quote do
|
||||
assert Compiler.is_subtype(unquote(spec1), unquote(spec2))
|
||||
IO.inspect("assert is_subtype #{inspect(unquote(spec1))}, #{inspect(unquote(spec2))}")
|
||||
is_subtype? = Compiler.is_subtype(unquote(spec1), unquote(spec2))
|
||||
Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
|
||||
Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
|
||||
assert is_subtype?
|
||||
end
|
||||
end
|
||||
|
||||
@ -474,10 +485,11 @@ defmodule TddSystemTest do
|
||||
@doc "Tests A | (B & C) versus (A | B) & (A | C) -- they are NOT always equivalent"
|
||||
test "subtyping with distributivity" do
|
||||
# Let's test `A | (B & C) <: (A | B) & (A | C)`
|
||||
spec_left = {:union, [:atom, {:intersect, [:integer, :positive_integer]}]}
|
||||
spec_left = {:union, [:atom, {:intersect, [:integer, {:integer_range, 0, :pos_inf}]}]}
|
||||
|
||||
spec_right =
|
||||
{:intersect, [{:union, [:atom, :integer]}, {:union, [:atom, :positive_integer]}]}
|
||||
{:intersect,
|
||||
[{:union, [:atom, :integer]}, {:union, [:atom, {:integer_range, 0, :pos_inf}]}]}
|
||||
|
||||
# `spec_left` normalizes to `atom | positive_integer`
|
||||
# `spec_right` normalizes to `(atom | integer) & (atom | positive_integer)`
|
||||
@ -485,14 +497,9 @@ defmodule TddSystemTest do
|
||||
# simplifies to `atom | positive_integer`. Therefore, they are equivalent in this case.
|
||||
assert_equivalent_specs(spec_left, spec_right)
|
||||
|
||||
# However, let's create a case where it's only a subtype relationship
|
||||
# `integer | (atom & pid)` should be `integer | :none` which is `integer`.
|
||||
# `(integer | atom) & (integer | pid)` is a much larger type.
|
||||
# simplifies to :integer
|
||||
spec_sub = {:union, [:integer, {:intersect, [:atom, :pid]}]}
|
||||
spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :pid]}]}
|
||||
spec_sub = {:union, [:integer, {:intersect, [:atom, :tuple]}]}
|
||||
spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :tuple]}]}
|
||||
assert_subtype(spec_sub, spec_super)
|
||||
refute_subtype(spec_super, spec_sub)
|
||||
end
|
||||
end
|
||||
|
||||
@ -526,6 +533,12 @@ 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, []}))
|
||||
|
||||
Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
|
||||
Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
|
||||
assert_equivalent_specs(spec, {:literal, []})
|
||||
end
|
||||
end
|
||||
@ -546,11 +559,6 @@ defmodule TddSystemTest do
|
||||
|
||||
@doc "Tests a non-sensical recursion that should simplify away"
|
||||
test "μ-types that should normalize to a non-recursive form" do
|
||||
# A type defined as "itself or an integer" should be equivalent to just "integer",
|
||||
# because any finite instance of it must eventually terminate with an integer.
|
||||
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
|
||||
assert_equivalent_specs(spec, :integer)
|
||||
|
||||
# A type defined as "a cons of an atom and itself, or none" should be equivalent to `list_of(atom)`.
|
||||
# This tests if our manual mu-calculus definition matches the syntactic sugar.
|
||||
manual_list_of_atom = {:mu, :L, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :L}}]}}
|
||||
@ -558,6 +566,11 @@ defmodule TddSystemTest do
|
||||
assert_equivalent_specs(manual_list_of_atom, sugar_list_of_atom)
|
||||
end
|
||||
|
||||
test "infer termination of recursive types" do
|
||||
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
|
||||
assert_equivalent_specs(spec, :integer)
|
||||
end
|
||||
|
||||
@doc "Tests polymorphism with multiple type parameters."
|
||||
test "lambda with multiple parameters: (Λ(A,B). {A,B})(int, atom)" do
|
||||
# λ(A, B). {A, B}
|
||||
@ -595,6 +608,7 @@ defmodule TddSystemTest do
|
||||
assert_subtype(list_of_trees_instance, list_of_trees)
|
||||
end
|
||||
|
||||
# failing
|
||||
@doc "An 'ill-formed' recursive type that should evaluate to :none"
|
||||
test "μ-types that are self-contradictory should be :none" do
|
||||
# A type defined as `μX. cons(integer, X)`. This describes an infinite list
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user