From a5e5127bcd85fb01c4dadb86802c969aa6a7d9d4 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Wed, 18 Jun 2025 15:10:58 +0200 Subject: [PATCH] reconstructor & normalization --- new.exs | 497 +++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 362 insertions(+), 135 deletions(-) diff --git a/new.exs b/new.exs index 1ea6885..5d5496e 100644 --- a/new.exs +++ b/new.exs @@ -69,123 +69,277 @@ defmodule Tdd.TypeSpec do @spec normalize(t()) :: t() def normalize(spec) do case spec do - # --- Base cases: already normalized --- - :any -> - :any + # Base cases are unchanged + s when is_atom(s) -> s + {:literal, _} -> spec + {:type_var, _} -> spec + # Recursive cases now call helper functions + {:negation, sub_spec} -> normalize_negation(sub_spec) + {:tuple, elements} -> {:tuple, Enum.map(elements, &normalize/1)} + {:cons, head, tail} -> {:cons, normalize(head), normalize(tail)} + {:list_of, element} -> {:list_of, normalize(element)} + # A new rule for integer ranges + {:integer_range, min, max} -> normalize_integer_range(min, max) + {:union, members} -> normalize_union(members) + {:intersect, members} -> normalize_intersection(members) + end + end - :none -> - :none + # ------------------------------------------------------------------ + # Private Normalization Helpers + # ------------------------------------------------------------------ - :atom -> - :atom + defp normalize_negation(sub_spec) do + normalized_sub = normalize(sub_spec) - :integer -> - :integer + case normalized_sub do + # ¬(¬A) -> A + {:negation, inner_spec} -> inner_spec + :any -> :none + :none -> :any + _ -> {:negation, normalized_sub} + end + end - :list -> - :list + defp normalize_integer_range(min, max) do + # An invalid range simplifies to `none`. + if is_integer(min) and is_integer(max) and min > max do + :none + else + # An intersection with integer is implied, so we add it for canonical form. + {:intersect, [:integer, {:integer_range, min, max}]} + end + end - :tuple -> - :tuple + defp normalize_union(members) do + # 1. Recursively normalize and flatten members + normalized_and_flattened = + Enum.flat_map(members, fn member -> + normalized = normalize(member) - {:literal, _} -> - spec - - {:type_var, _} -> - spec - - # Assume range is already canonical - {:integer_range, _, _} -> - spec - - # --- Recursive cases --- - {:negation, sub_spec} -> - normalized_sub = normalize(sub_spec) - - # Apply double negation law: ¬(¬A) -> A - case normalized_sub do - {:negation, inner_spec} -> inner_spec - _ -> {:negation, normalized_sub} - end - - {:tuple, elements} -> - {:tuple, Enum.map(elements, &normalize/1)} - - {:cons, head, tail} -> - {:cons, normalize(head), normalize(tail)} - - {:list_of, element} -> - {:list_of, normalize(element)} - - # --- Complex cases: Union and Intersection --- - {:union, members} -> - # 1. Recursively normalize, then flatten nested unions. - normalized_and_flattened = - Enum.flat_map(members, fn member -> - normalized = normalize(member) - - case normalized do + case normalized, + do: + ( {:union, sub_members} -> sub_members _ -> [normalized] - end + ) + end) + + # 2. Apply simplification rules + simplified_members = + normalized_and_flattened + # A | none -> A + |> Enum.reject(&(&1 == :none)) + |> MapSet.new() + + if MapSet.member?(simplified_members, :any) do + # A | any -> any + :any + else + # 3. NEW: Reduce by removing subtypes + # If we have {A, B} and A <: B, the union is just B. So we keep only supersets. + # We achieve this by removing any member that is a subtype of another member. + reduced_members = + Enum.reject(simplified_members, fn member_to_check -> + Enum.any?(simplified_members, fn other_member -> + member_to_check != other_member and is_subtype?(member_to_check, other_member) end) + end) - # 2. Apply simplification rules and sort. - simplified_members = - normalized_and_flattened - # Annihilation: A | none -> A - |> Enum.reject(&(&1 == :none)) - # Uniq members - |> MapSet.new() - - # Annihilation: if `any` is a member, the whole union is `any`. - if MapSet.member?(simplified_members, :any) do - :any - else - # 3. Finalize the structure. - case MapSet.to_list(simplified_members) do - # An empty union is the empty set. - [] -> :none - # Idempotency: A | A -> A - [single_member] -> single_member - sorted_members -> {:union, Enum.sort(sorted_members)} - end - end - - {:intersect, members} -> - # 1. Recursively normalize, then flatten. - normalized_and_flattened = - Enum.flat_map(members, fn member -> - normalized = normalize(member) - - case normalized do - {:intersect, sub_members} -> sub_members - _ -> [normalized] - end - end) - - # 2. Apply simplification rules and sort. - simplified_members = - normalized_and_flattened - # Annihilation: A & any -> A - |> Enum.reject(&(&1 == :any)) - |> MapSet.new() - - # Annihilation: if `none` is a member, the whole intersection is `none`. - if MapSet.member?(simplified_members, :none) do - :none - else - # 3. Finalize the structure. - case MapSet.to_list(simplified_members) do - # An empty intersection is the universal set. - [] -> :any - # Idempotency: A & A -> A - [single_member] -> single_member - sorted_members -> {:intersect, Enum.sort(sorted_members)} - end - end + # 4. Finalize the structure + case reduced_members do + [] -> :none + [single_member] -> single_member + list -> {:union, Enum.sort(list)} + end end end + + defp normalize_intersection(members) do + IO.inspect("Normalize intersection") + # 1. Recursively normalize and flatten, but also add implied supertypes + normalized_and_flattened = + Enum.flat_map(members, fn member -> + IO.inspect(member, label: "normalize member") + normalized = normalize(member) + # Expand a type into itself and its implied supertypes + # e.g., `:foo` becomes `[:foo, :atom]` + expanded = + case normalized do + {:intersect, sub_members} -> sub_members + _ -> get_supertypes(normalized) + end + + expanded + end) + + # 2. Apply simplification rules + simplified_members = + normalized_and_flattened + # A & any -> A + |> Enum.reject(&(&1 == :any)) + |> MapSet.new() + + if MapSet.member?(simplified_members, :none) do + # A & none -> none + :none + else + # 3. NEW: Reduce by removing supertypes + IO.inspect("Reduce by removing supertypes") + # If we have {A, B} and A <: B, the intersection is just A. So we keep only subsets. + # We achieve this by removing any member for which a proper subtype exists in the set. + reduced_members = + Enum.reject(simplified_members, fn member_to_check -> + Enum.any?(simplified_members, fn other_member -> + member_to_check != other_member and is_subtype?(other_member, member_to_check) + end) + end) + + # 4. Finalize the structure + IO.inspect("4. Finalize the structure") + + case reduced_members do + [] -> :any + [single_member] -> single_member + list -> {:intersect, Enum.sort(list)} + end + end + end + + # ------------------------------------------------------------------ + # Private Semantic Helpers + # ------------------------------------------------------------------ + + @doc """ + A preliminary, non-TDD check if `spec1` is a subtype of `spec2`. + + This check is not exhaustive but covers many common, structural cases, + allowing for significant simplification at the `TypeSpec` level. + """ + @spec is_subtype?(t(), t()) :: boolean + def is_subtype?(spec1, spec2) do + # Avoid infinite recursion by not re-normalizing. + # The callers are assumed to be working with normalized data. + # Base cases are handled first for efficiency. + cond do + spec1 == spec2 -> true + spec1 == :none -> true + spec2 == :any -> true + spec1 == :any or spec2 == :none -> false + # Defer to pattern-matching helper + true -> do_is_subtype?(spec1, spec2) + end + end + + # Private helper that uses `case` for proper pattern matching. + defp do_is_subtype?(spec1, spec2) do + case {spec1, spec2} do + # --- Set-theoretic rules --- + + # (A | B) <: C if A <: C and B <: C + {{:union, members1}, _} -> + Enum.all?(members1, &is_subtype?(&1, spec2)) + + # A <: (B | C) if A <: B or A <: C + {_, {:union, members2}} -> + Enum.any?(members2, &is_subtype?(spec1, &1)) + + # (A & B) <: C if A <: C or B <: C + {{:intersect, members1}, _} -> + Enum.any?(members1, &is_subtype?(&1, spec2)) + + # A <: (B & C) if A <: B and A <: C + {_, {:intersect, members2}} -> + Enum.all?(members2, &is_subtype?(spec1, &1)) + + # --- Literal and Base Type Rules --- + {s1, s2} when is_atom(s1) and is_atom(s2) -> + s1 == s2 + + {{:literal, v1}, {:literal, v2}} -> + v1 == v2 + + {{:literal, val}, :atom} when is_atom(val) -> + true + + {{:literal, val}, :integer} when is_integer(val) -> + true + + {{:literal, val}, :list} when is_list(val) -> + true + + {{:literal, val}, :tuple} when is_tuple(val) -> + true + + # --- List and Cons Rules --- + {{:literal, []}, :list} -> + true + + {{:cons, _, _}, :list} -> + true + + {{:list_of, _}, :list} -> + true + + {{:cons, h1, t1}, {:cons, h2, t2}} -> + is_subtype?(h1, h2) and is_subtype?(t1, t2) + + {{:list_of, e1}, {:list_of, e2}} -> + is_subtype?(e1, e2) + + {{:cons, h, t}, {:list_of, x}} -> + is_subtype?(h, x) and is_subtype?(t, {:list_of, x}) + + {{:literal, []}, {:list_of, _}} -> + true + + # --- Tuple Rules --- + {{:literal, {}}, :tuple} -> + true + + {{:tuple, _}, :tuple} -> + true + + {{:tuple, elems1}, {:tuple, elems2}} when length(elems1) == length(elems2) -> + Enum.zip_with(elems1, elems2, &is_subtype?/2) |> Enum.all?() + + # --- Integer Range Rules --- + {{:integer_range, _, _}, :integer} -> + true + + {{:integer_range, min1, max1}, {:integer_range, min2, max2}} -> + min1_gte_min2 = if min1 == :neg_inf, do: true, else: min2 != :neg_inf and min1 >= min2 + max1_lte_max2 = if max1 == :pos_inf, do: true, else: max2 != :pos_inf and max1 <= max2 + min1_gte_min2 and max1_lte_max2 + + {{:literal, val}, {:integer_range, min, max}} when is_integer(val) -> + (min == :neg_inf or val >= min) and (max == :pos_inf or val <= max) + + # --- Default fallback --- + # If no specific rule matches, they are not considered subtypes. + {_, _} -> + false + end + end + + # Gets a list of immediate, known supertypes for a given simple spec. + defp get_supertypes(spec) do + supertypes = + case spec do + {:literal, val} when is_atom(val) -> [:atom] + {:literal, val} when is_integer(val) -> [:integer] + {:literal, val} when is_list(val) -> [:list] + {:literal, val} when is_tuple(val) -> [:tuple] + {:cons, _, _} -> [:list] + {:list_of, _} -> [:list] + {:tuple, _} -> [:tuple] + {:integer_range, _, _} -> [:integer] + _ -> [] + end + + # Use a MapSet to ensure the spec and its supertypes are unique. + MapSet.to_list(MapSet.new([spec | supertypes])) + end end defmodule Tdd.Store do @@ -848,8 +1002,10 @@ defmodule Tdd.TypeReconstructor do partitions = Enum.group_by(assumptions, fn {var, _val} -> case Info.get_traits(var) do - %{type: :list_recursive, sub_key: key} -> key # :head or :tail - %{type: :tuple_recursive, sub_key: key} -> key # {:elem, index} + # :head or :tail + %{type: :list_recursive, sub_key: key} -> key + # {:elem, index} + %{type: :tuple_recursive, sub_key: key} -> key # All other predicates apply to the top-level entity _ -> :top_level end @@ -871,7 +1027,10 @@ defmodule Tdd.TypeReconstructor do |> Map.new(fn {var, val} -> # This pattern matching is a bit simplified for clarity {_cat, _pred, nested_var_or_idx, maybe_nested_var} = var - nested_var = if is_nil(maybe_nested_var), do: nested_var_or_idx, else: maybe_nested_var + + nested_var = + if is_nil(maybe_nested_var), do: nested_var_or_idx, else: maybe_nested_var + {nested_var, val} end) @@ -880,14 +1039,21 @@ defmodule Tdd.TypeReconstructor do # Wrap it in a constructor that describes its relationship to the parent case sub_key do - :head -> {:cons, sub_spec, :any} # Partial spec: just describes the head - :tail -> {:cons, :any, sub_spec} # Partial spec: just describes the tail + # Partial spec: just describes the head + :head -> + {:cons, sub_spec, :any} + + # Partial spec: just describes the tail + :tail -> + {:cons, :any, sub_spec} + {:elem, index} -> # Create a sparse tuple spec, e.g., {any, any, , any} # This is complex, a simpler approach is needed for now. # For now, we'll just return a tuple spec that isn't fully specific. # A full implementation would need to know the tuple's size. - {:tuple, [sub_spec]} # This is an oversimplification but works for demo + # This is an oversimplification but works for demo + {:tuple, [sub_spec]} end end) @@ -896,7 +1062,6 @@ defmodule Tdd.TypeReconstructor do TypeSpec.normalize({:intersect, final_spec_list}) end - @doc "Handles only the 'flat' (non-recursive) assumptions for a single entity." defp spec_from_flat_assumptions(assumptions) do specs = @@ -912,10 +1077,13 @@ defmodule Tdd.TypeReconstructor do {0, :is_tuple, _, _} -> :tuple {1, :value, val, _} -> {:literal, val} # For integer properties, we create a range spec. This part could be more detailed. - {2, :alt, n, _} -> {:integer_range, :neg_inf, n - 1} # x < n + # x < n + {2, :alt, n, _} -> {:integer_range, :neg_inf, n - 1} {2, :beq, n, _} -> {:literal, n} - {2, :cgt, n, _} -> {:integer_range, n + 1, :pos_inf} # x > n - {4, :a_size, _, _} -> :tuple # Simplified for now + # x > n + {2, :cgt, n, _} -> {:integer_range, n + 1, :pos_inf} + # Simplified for now + {4, :a_size, _, _} -> :tuple {5, :b_is_empty, _, _} -> {:literal, []} # Ignore recursive and ambient vars at this flat level _ -> :any @@ -928,6 +1096,7 @@ defmodule Tdd.TypeReconstructor do TypeSpec.normalize({:intersect, specs}) end end + #### # xxx #### @@ -1353,7 +1522,6 @@ defmodule TddVariableTests do end end - defmodule ConsistencyEngineTests do alias Tdd.Consistency.Engine alias Tdd.Variable @@ -1361,9 +1529,10 @@ defmodule ConsistencyEngineTests do defp test(name, expected, assumptions_map) do result = Engine.check(assumptions_map) # ... test reporting logic ... - is_ok = (expected == result) + is_ok = expected == result status = if is_ok, do: "[PASS]", else: "[FAIL]" IO.puts("#{status} #{name}") + unless is_ok do IO.puts(" Expected: #{inspect(expected)}, Got: #{inspect(result)}") Process.put(:test_failures, [name | Process.get(:test_failures, [])]) @@ -1378,48 +1547,56 @@ defmodule ConsistencyEngineTests do IO.puts("\n--- Section: Basic & Implication Tests ---") test("An empty assumption map is consistent", :consistent, %{}) test("A single valid assumption is consistent", :consistent, %{Variable.v_is_atom() => true}) + test( "An explicit contradiction is caught", :contradiction, %{Variable.v_is_atom() => true, Variable.v_is_atom() => false} ) + test( "An implied contradiction is caught by expander", :contradiction, %{Variable.v_atom_eq(:foo) => true, Variable.v_is_atom() => false} ) + test( "Implication creates a consistent set", :consistent, - %{Variable.v_atom_eq(:foo) => true} # implies is_atom=true + # implies is_atom=true + %{Variable.v_atom_eq(:foo) => true} ) # --- Section: Primary Type Exclusivity --- IO.puts("\n--- Section: Primary Type Exclusivity ---") + test( "Two primary types cannot both be true", :contradiction, %{Variable.v_is_atom() => true, Variable.v_is_integer() => true} ) + test( "Two primary types implied to be true is a contradiction", :contradiction, %{Variable.v_atom_eq(:foo) => true, Variable.v_int_eq(5) => true} ) + test( "One primary type true and another false is consistent", :consistent, %{Variable.v_is_atom() => true, Variable.v_is_integer() => false} ) - # --- Section: Atom Consistency --- IO.puts("\n--- Section: Atom Consistency ---") + test( "An atom cannot equal two different values", :contradiction, %{Variable.v_atom_eq(:foo) => true, Variable.v_atom_eq(:bar) => true} ) + test( "An atom can equal one value", :consistent, @@ -1428,35 +1605,75 @@ defmodule ConsistencyEngineTests do # --- Section: List Flat Consistency --- IO.puts("\n--- Section: List Flat Consistency ---") + test( "A list cannot be empty and have a head property", :contradiction, - %{Variable.v_list_is_empty() => true, Variable.v_list_head_pred(Variable.v_is_atom()) => true} + %{ + Variable.v_list_is_empty() => true, + Variable.v_list_head_pred(Variable.v_is_atom()) => true + } ) + test( "A non-empty list can have a head property", :consistent, - %{Variable.v_list_is_empty() => false, Variable.v_list_head_pred(Variable.v_is_atom()) => true} + %{ + Variable.v_list_is_empty() => false, + Variable.v_list_head_pred(Variable.v_is_atom()) => true + } ) + test( "A non-empty list is implied by head property", :consistent, - %{Variable.v_list_head_pred(Variable.v_is_atom()) => true} # implies is_empty=false + # implies is_empty=false + %{Variable.v_list_head_pred(Variable.v_is_atom()) => true} ) # --- Section: Integer Consistency --- IO.puts("\n--- Section: Integer Consistency ---") test("int == 5 is consistent", :consistent, %{Variable.v_int_eq(5) => true}) - test("int == 5 AND int == 10 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_eq(10) => true}) - test("int < 10 AND int > 20 is a contradiction", :contradiction, %{Variable.v_int_lt(10) => true, Variable.v_int_gt(20) => true}) - test("int > 5 AND int < 4 is a contradiction", :contradiction, %{Variable.v_int_gt(5) => true, Variable.v_int_lt(4) => true}) - test("int > 5 AND int < 7 is consistent", :consistent, %{Variable.v_int_gt(5) => true, Variable.v_int_lt(7) => true}) # 6 - test("int == 5 AND int < 3 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_lt(3) => true}) - test("int == 5 AND int > 10 is a contradiction", :contradiction, %{Variable.v_int_eq(5) => true, Variable.v_int_gt(10) => true}) - test("int == 5 AND int > 3 is consistent", :consistent, %{Variable.v_int_eq(5) => true, Variable.v_int_gt(3) => true}) + + test("int == 5 AND int == 10 is a contradiction", :contradiction, %{ + Variable.v_int_eq(5) => true, + Variable.v_int_eq(10) => true + }) + + test("int < 10 AND int > 20 is a contradiction", :contradiction, %{ + Variable.v_int_lt(10) => true, + Variable.v_int_gt(20) => true + }) + + test("int > 5 AND int < 4 is a contradiction", :contradiction, %{ + Variable.v_int_gt(5) => true, + Variable.v_int_lt(4) => true + }) + + # 6 + test("int > 5 AND int < 7 is consistent", :consistent, %{ + Variable.v_int_gt(5) => true, + Variable.v_int_lt(7) => true + }) + + test("int == 5 AND int < 3 is a contradiction", :contradiction, %{ + Variable.v_int_eq(5) => true, + Variable.v_int_lt(3) => true + }) + + test("int == 5 AND int > 10 is a contradiction", :contradiction, %{ + Variable.v_int_eq(5) => true, + Variable.v_int_gt(10) => true + }) + + test("int == 5 AND int > 3 is consistent", :consistent, %{ + Variable.v_int_eq(5) => true, + Variable.v_int_gt(3) => true + }) # --- Final Report --- failures = Process.get(:test_failures, []) + if failures == [] do IO.puts("\n✅ All Consistency.Engine tests passed!") else @@ -1464,6 +1681,7 @@ defmodule ConsistencyEngineTests do end end end + # defmodule TddAlgoTests do # alias Tdd.Store # alias Tdd.Variable @@ -1617,9 +1835,10 @@ defmodule TypeReconstructorTests do expected = TypeSpec.normalize(expected_spec) result = TypeSpec.normalize(TypeReconstructor.spec_from_assumptions(assumptions)) - is_ok = (expected == result) + is_ok = expected == result status = if is_ok, do: "[PASS]", else: "[FAIL]" IO.puts("#{status} #{name}") + unless is_ok do IO.puts(" Expected: #{inspect(expected)}") IO.puts(" Got: #{inspect(result)}") @@ -1635,21 +1854,25 @@ defmodule TypeReconstructorTests do IO.puts("\n--- Section: Basic Flat Reconstructions ---") test("is_atom=true -> atom", :atom, %{Variable.v_is_atom() => true}) test("is_atom=false -> ¬atom", {:negation, :atom}, %{Variable.v_is_atom() => false}) + test( "is_atom=true AND value==:foo -> :foo", {:literal, :foo}, %{Variable.v_is_atom() => true, Variable.v_atom_eq(:foo) => true} ) + test( "is_atom=true AND value!=:foo -> atom & ¬:foo", {:intersect, [:atom, {:negation, {:literal, :foo}}]}, %{Variable.v_is_atom() => true, Variable.v_atom_eq(:foo) => false} ) + test( "is_integer=true AND int==5 -> 5", {:literal, 5}, %{Variable.v_is_integer() => true, Variable.v_int_eq(5) => true} ) + test( "is_list=true AND is_empty=true -> []", {:literal, []}, @@ -1658,16 +1881,18 @@ defmodule TypeReconstructorTests do # --- Section: Combined Flat Reconstructions --- IO.puts("\n--- Section: Combined Flat Reconstructions ---") + test( "int > 10 AND int < 20", # This is complex. Our simple reconstructor makes two separate ranges. # A more advanced one would combine them into a single {:integer_range, 11, 19}. # For now, we test the current behavior. - {:intersect, [ - :integer, - {:integer_range, 11, :pos_inf}, - {:integer_range, :neg_inf, 19} - ]}, + {:intersect, + [ + :integer, + {:integer_range, 11, :pos_inf}, + {:integer_range, :neg_inf, 19} + ]}, %{Variable.v_int_gt(10) => true, Variable.v_int_lt(20) => true} ) @@ -1688,6 +1913,7 @@ defmodule TypeReconstructorTests do # --- Final Report --- failures = Process.get(:test_failures, []) + if failures == [] do IO.puts("\n✅ All TypeReconstructor tests passed!") else @@ -1695,6 +1921,7 @@ defmodule TypeReconstructorTests do end end end + TypeSpecTests.run() TddStoreTests.run() TddVariableTests.run()