From b5a731edad43b593eca57ff5e2e6735b35ec3167 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Mon, 14 Jul 2025 22:30:53 +0200 Subject: [PATCH] one less test failing --- lib/debug.ex | 155 ++++++++++++++++++++++++++++++++++++++++++++++ lib/til.ex | 85 ++++++++++++++++--------- test/til_test.exs | 46 +++++++++----- 3 files changed, 241 insertions(+), 45 deletions(-) diff --git a/lib/debug.ex b/lib/debug.ex index 5621414..a58bdf1 100644 --- a/lib/debug.ex +++ b/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 diff --git a/lib/til.ex b/lib/til.ex index aa3ac5a..25b90f9 100644 --- a/lib/til.ex +++ b/lib/til.ex @@ -78,37 +78,65 @@ 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? - final_members = - Enum.reject(unique_no_any, fn member_to_check -> - Enum.any?(unique_no_any, fn other_member -> - member_to_check != other_member and - is_subtype?(other_member, member_to_check, true) - end) - end) + # Separate the members into unions and non-unions. + {unions, non_unions} = Enum.split_with(flattened_members, &match?({:union, _}, &1)) - case Enum.sort(final_members) do - [] -> :any - [single] -> single - list_members -> {:intersect, list_members} + 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(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 @@ -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 diff --git a/test/til_test.exs b/test/til_test.exs index bc64346..3244b9c 100644 --- a/test/til_test.exs +++ b/test/til_test.exs @@ -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