From 7fa469518dcb3de5e06f7eb2ce9d3103cf34f518 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Wed, 18 Jun 2025 16:13:29 +0200 Subject: [PATCH] consistency fixed --- new.exs | 366 +++++++++++++++++++++++++++++++++----------------------- 1 file changed, 214 insertions(+), 152 deletions(-) diff --git a/new.exs b/new.exs index b3f4630..da15dae 100644 --- a/new.exs +++ b/new.exs @@ -107,7 +107,9 @@ defmodule Tdd.TypeSpec do :none else # An intersection with integer is implied, so we add it for canonical form. + # TODO: revisit {:intersect, [:integer, {:integer_range, min, max}]} + {:integer_range, min, max} end end @@ -156,11 +158,11 @@ defmodule Tdd.TypeSpec do end defp normalize_intersection(members) do - IO.inspect("Normalize intersection") + # 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") + # IO.inspect(member, label: "normalize member") normalized = normalize(member) # Expand a type into itself and its implied supertypes # e.g., `:foo` becomes `[:foo, :atom]` @@ -185,7 +187,7 @@ defmodule Tdd.TypeSpec do :none else # 3. NEW: Reduce by removing supertypes - IO.inspect("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 = @@ -196,7 +198,7 @@ defmodule Tdd.TypeSpec do end) # 4. Finalize the structure - IO.inspect("4. Finalize the structure") + # IO.inspect("4. Finalize the structure") case reduced_members do [] -> :any @@ -766,7 +768,7 @@ defmodule Tdd.Consistency.Engine do if is_empty and (has_head_prop or has_tail_prop), do: :error, else: :ok end -defp check_integer_consistency(assumptions) do + defp check_integer_consistency(assumptions) do initial_range = {:neg_inf, :pos_inf} result = @@ -782,7 +784,12 @@ defp check_integer_consistency(assumptions) do end end) - case result, do: (:invalid -> :error; _ -> :ok) + case result, + do: + ( + :invalid -> :error + _ -> :ok + ) end # **IMPROVED**: A clearer implementation for checking range validity. @@ -792,7 +799,8 @@ defp check_integer_consistency(assumptions) do {:neg_inf, _} -> false {_, :pos_inf} -> false {m, n} when is_integer(m) and is_integer(n) -> m > n - _ -> false # Should not happen with safe helpers + # Should not happen with safe helpers + _ -> false end if is_invalid, do: {:halt, :invalid}, else: {:cont, {min, max}} @@ -1280,6 +1288,60 @@ defmodule Tdd.Compiler do Store.false_node_id() ) + {:integer_range, min, max} -> + # A helper function to define the intersection operation once. + op_intersect = fn + :false_terminal, _ -> :false_terminal + _, :false_terminal -> :false_terminal + :true_terminal, t2 -> t2 + t1, :true_terminal -> t1 + end + + # Start with the base type, `integer`. + # Note: We call spec_to_id here, which is safe because `:integer` is a base case. + base_id = spec_to_id(:integer) + + # Intersect with the lower bound condition, if it exists. + id_with_min = + if min == :neg_inf do + base_id + else + # The condition is `value >= min`, which is equivalent to `NOT (value < min)`. + # The variable for `value < min` is `v_int_lt(min)`. + lt_min_tdd = + Store.find_or_create_node( + Variable.v_int_lt(min), + Store.true_node_id(), + Store.false_node_id(), + Store.false_node_id() + ) + + gte_min_tdd = Algo.negate(lt_min_tdd) + Algo.apply(:intersect, op_intersect, base_id, gte_min_tdd) + end + + # Intersect the result with the upper bound condition, if it exists. + id_with_max = + if max == :pos_inf do + id_with_min + else + # The condition is `value <= max`, which is equivalent to `value < max + 1`. + # The variable for this is `v_int_lt(max + 1)`. + lt_max_plus_1_tdd = + Store.find_or_create_node( + Variable.v_int_lt(max + 1), + Store.true_node_id(), + Store.false_node_id(), + Store.false_node_id() + ) + + Algo.apply(:intersect, op_intersect, id_with_min, lt_max_plus_1_tdd) + end + + # The raw TDD is now built. The final call to Algo.simplify at the end + # of do_spec_to_id will canonicalize it. + id_with_max + # Add other literals as needed # --- Set-Theoretic Combinators --- @@ -1927,149 +1989,149 @@ defmodule ConsistencyEngineTests do end end -# defmodule TddAlgoTests do -# alias Tdd.Store -# alias Tdd.Variable -# alias Tdd.Algo -# alias Tdd.TypeSpec # We need this to create stable variables -# -# # --- Test Helper --- -# defp test(name, expected, result) do -# # A simple equality test is sufficient here. -# if expected == result do -# IO.puts("[PASS] #{name}") -# else -# IO.puts("[FAIL] #{name}") -# IO.puts(" Expected: #{inspect(expected)}") -# IO.puts(" Got: #{inspect(result)}") -# Process.put(:test_failures, [name | Process.get(:test_failures, [])]) -# end -# end -# -# # Helper to pretty print a TDD for debugging -# defp print_tdd(id, indent \\ 0) do -# prefix = String.duplicate(" ", indent) -# case Store.get_node(id) do -# {:ok, details} -> -# IO.puts("#{prefix}ID #{id}: #{inspect(details)}") -# case details do -# {_var, y, n, d} -> -# IO.puts("#{prefix} Yes ->"); print_tdd(y, indent + 1) -# IO.puts("#{prefix} No ->"); print_tdd(n, indent + 1) -# IO.puts("#{prefix} DC ->"); print_tdd(d, indent + 1) -# _ -> :ok -# end -# {:error, reason} -> -# IO.puts("#{prefix}ID #{id}: Error - #{reason}") -# end -# end -# -# # --- Test Runner --- -# def run() do -# IO.puts("\n--- Running Tdd.Algo & Tdd.Consistency.Engine Tests ---") -# Process.put(:test_failures, []) -# -# # Setup: Initialize the store and define some basic TDDs using the new modules. -# Store.init() -# true_id = Store.true_node_id() -# false_id = Store.false_node_id() -# -# # --- Manually build some basic type TDDs for testing --- -# # t_atom = if is_atom then true else false -# t_atom = Store.find_or_create_node(Variable.v_is_atom(), true_id, false_id, false_id) -# # t_int = if is_int then true else false -# t_int = Store.find_or_create_node(Variable.v_is_integer(), true_id, false_id, false_id) -# -# # t_foo = if is_atom then (if value == :foo then true else false) else false -# foo_val_check = Store.find_or_create_node(Variable.v_atom_eq(:foo), true_id, false_id, false_id) -# t_foo = Store.find_or_create_node(Variable.v_is_atom(), foo_val_check, false_id, false_id) -# -# # t_bar = if is_atom then (if value == :bar then true else false) else false -# bar_val_check = Store.find_or_create_node(Variable.v_atom_eq(:bar), true_id, false_id, false_id) -# t_bar = Store.find_or_create_node(Variable.v_is_atom(), bar_val_check, false_id, false_id) -# -# # --- Section: Negate Algorithm --- -# IO.puts("\n--- Section: Algo.negate ---") -# negated_true = Algo.negate(true_id) -# test("negate(true) is false", false_id, negated_true) -# negated_false = Algo.negate(false_id) -# test("negate(false) is true", true_id, negated_false) -# # Double negation should be identity -# test("negate(negate(t_atom)) is t_atom", t_atom, Algo.negate(Algo.negate(t_atom))) -# -# # --- Section: Apply Algorithm (Union & Intersection) --- -# IO.puts("\n--- Section: Algo.apply (raw structural operations) ---") -# op_sum = fn -# :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal -# t, :false_terminal -> t; :false_terminal, t -> t -# end -# op_intersect = fn -# :false_terminal, _ -> :false_terminal; _, :false_terminal -> :false_terminal -# t, :true_terminal -> t; :true_terminal, t -> t -# end -# -# # atom | int -# sum_atom_int = Algo.apply(:sum, op_sum, t_atom, t_int) -# # The result should be a node that checks is_atom, then if false, checks is_int -# # We expect a structure like: if is_atom -> true, else -> t_int -# is_atom_node = {Variable.v_is_atom(), true_id, t_int, t_int} -# expected_sum_structure_id = Store.find_or_create_node(elem(is_atom_node, 0), elem(is_atom_node, 1), elem(is_atom_node, 2), elem(is_atom_node, 3)) -# test("Structure of 'atom | int' is correct", expected_sum_structure_id, sum_atom_int) -# -# # :foo & :bar (structurally, before simplification) -# # It should build a tree that checks is_atom, then value==:foo, then value==:bar -# # This will be complex, but the key is that it's NOT the false_id yet. -# intersect_foo_bar_raw = Algo.apply(:intersect, op_intersect, t_foo, t_bar) -# test(":foo & :bar (raw) is not the false node", false, intersect_foo_bar_raw == false_id) -# -# # --- Section: Simplify Algorithm (Flat Types) --- -# IO.puts("\n--- Section: Algo.simplify (with Consistency.Engine) ---") -# -# # An impossible structure: node that requires a value to be an atom AND an integer -# # This tests the `check_primary_exclusivity` rule. -# contradictory_assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true} -# # Simplifying ANYTHING under contradictory assumptions should yield `false`. -# simplified_under_contradiction = Algo.simplify(true_id, contradictory_assumptions) -# test("Simplifying under contradictory assumptions (atom & int) results in false", false_id, simplified_under_contradiction) -# -# # Test implication: A property implies its primary type -# # A value being `:foo` implies it is an atom. -# assumptions_with_foo = %{Variable.v_atom_eq(:foo) => true} -# # If we simplify t_int under this assumption, it should become false. -# # The engine expands to `{is_atom: true, value==:foo: true}`. Then it sees that -# # the t_int node's variable `is_integer` must be false (from exclusivity rule). -# simplified_int_given_foo = Algo.simplify(t_int, assumptions_with_foo) -# test("Simplifying 'integer' given 'value==:foo' results in false", false_id, simplified_int_given_foo) -# -# # Now, let's simplify the raw intersection of :foo and :bar -# simplified_foo_bar = Algo.simplify(intersect_foo_bar_raw, %{}) -# # The simplify algorithm should discover the contradiction that an atom cannot be -# # both :foo and :bar at the same time. (This requires `check_atom_consistency` to be implemented). -# # For now, we stub it and test the plumbing. -# # Let's test a simpler contradiction that we *have* implemented. -# intersect_atom_int_raw = Algo.apply(:intersect, op_intersect, t_atom, t_int) -# simplified_atom_int = Algo.simplify(intersect_atom_int_raw, %{}) -# test("Simplifying 'atom & int' results in false", false_id, simplified_atom_int) -# -# # Test path collapsing -# # If we simplify 'atom | int' under the assumption 'is_atom == true', it should become `true`. -# simplified_sum_given_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => true}) -# test("Simplifying 'atom | int' given 'is_atom==true' results in true", true_id, simplified_sum_given_atom) -# # If we simplify 'atom | int' under the assumption 'is_atom == false', it should become `t_int`. -# simplified_sum_given_not_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => false}) -# test("Simplifying 'atom | int' given 'is_atom==false' results in 'integer'", t_int, simplified_sum_given_not_atom) -# -# -# # --- Final Report --- -# failures = Process.get(:test_failures, []) -# if failures == [] do -# IO.puts("\n✅ All Tdd.Algo tests passed!") -# else -# IO.puts("\n❌ Found #{length(failures)} test failures.") -# # Optional: print details of failed tests if needed -# end -# end -# end +defmodule TddAlgoTests do + alias Tdd.Store + alias Tdd.Variable + alias Tdd.Algo + alias Tdd.TypeSpec # We need this to create stable variables + + # --- Test Helper --- + defp test(name, expected, result) do + # A simple equality test is sufficient here. + if expected == result do + IO.puts("[PASS] #{name}") + else + IO.puts("[FAIL] #{name}") + IO.puts(" Expected: #{inspect(expected)}") + IO.puts(" Got: #{inspect(result)}") + Process.put(:test_failures, [name | Process.get(:test_failures, [])]) + end + end + + # Helper to pretty print a TDD for debugging + defp print_tdd(id, indent \\ 0) do + prefix = String.duplicate(" ", indent) + case Store.get_node(id) do + {:ok, details} -> + IO.puts("#{prefix}ID #{id}: #{inspect(details)}") + case details do + {_var, y, n, d} -> + IO.puts("#{prefix} Yes ->"); print_tdd(y, indent + 1) + IO.puts("#{prefix} No ->"); print_tdd(n, indent + 1) + IO.puts("#{prefix} DC ->"); print_tdd(d, indent + 1) + _ -> :ok + end + {:error, reason} -> + IO.puts("#{prefix}ID #{id}: Error - #{reason}") + end + end + + # --- Test Runner --- + def run() do + IO.puts("\n--- Running Tdd.Algo & Tdd.Consistency.Engine Tests ---") + Process.put(:test_failures, []) + + # Setup: Initialize the store and define some basic TDDs using the new modules. + Store.init() + true_id = Store.true_node_id() + false_id = Store.false_node_id() + + # --- Manually build some basic type TDDs for testing --- + # t_atom = if is_atom then true else false + t_atom = Store.find_or_create_node(Variable.v_is_atom(), true_id, false_id, false_id) + # t_int = if is_int then true else false + t_int = Store.find_or_create_node(Variable.v_is_integer(), true_id, false_id, false_id) + + # t_foo = if is_atom then (if value == :foo then true else false) else false + foo_val_check = Store.find_or_create_node(Variable.v_atom_eq(:foo), true_id, false_id, false_id) + t_foo = Store.find_or_create_node(Variable.v_is_atom(), foo_val_check, false_id, false_id) + + # t_bar = if is_atom then (if value == :bar then true else false) else false + bar_val_check = Store.find_or_create_node(Variable.v_atom_eq(:bar), true_id, false_id, false_id) + t_bar = Store.find_or_create_node(Variable.v_is_atom(), bar_val_check, false_id, false_id) + + # --- Section: Negate Algorithm --- + IO.puts("\n--- Section: Algo.negate ---") + negated_true = Algo.negate(true_id) + test("negate(true) is false", false_id, negated_true) + negated_false = Algo.negate(false_id) + test("negate(false) is true", true_id, negated_false) + # Double negation should be identity + test("negate(negate(t_atom)) is t_atom", t_atom, Algo.negate(Algo.negate(t_atom))) + + # --- Section: Apply Algorithm (Union & Intersection) --- + IO.puts("\n--- Section: Algo.apply (raw structural operations) ---") + op_sum = fn + :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal + t, :false_terminal -> t; :false_terminal, t -> t + end + op_intersect = fn + :false_terminal, _ -> :false_terminal; _, :false_terminal -> :false_terminal + t, :true_terminal -> t; :true_terminal, t -> t + end + + # atom | int + sum_atom_int = Algo.apply(:sum, op_sum, t_atom, t_int) + # The result should be a node that checks is_atom, then if false, checks is_int + # We expect a structure like: if is_atom -> true, else -> t_int + is_atom_node = {Variable.v_is_atom(), true_id, t_int, t_int} + expected_sum_structure_id = Store.find_or_create_node(elem(is_atom_node, 0), elem(is_atom_node, 1), elem(is_atom_node, 2), elem(is_atom_node, 3)) + test("Structure of 'atom | int' is correct", expected_sum_structure_id, sum_atom_int) + + # :foo & :bar (structurally, before simplification) + # It should build a tree that checks is_atom, then value==:foo, then value==:bar + # This will be complex, but the key is that it's NOT the false_id yet. + intersect_foo_bar_raw = Algo.apply(:intersect, op_intersect, t_foo, t_bar) + test(":foo & :bar (raw) is not the false node", false, intersect_foo_bar_raw == false_id) + + # --- Section: Simplify Algorithm (Flat Types) --- + IO.puts("\n--- Section: Algo.simplify (with Consistency.Engine) ---") + + # An impossible structure: node that requires a value to be an atom AND an integer + # This tests the `check_primary_exclusivity` rule. + contradictory_assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true} + # Simplifying ANYTHING under contradictory assumptions should yield `false`. + simplified_under_contradiction = Algo.simplify(true_id, contradictory_assumptions) + test("Simplifying under contradictory assumptions (atom & int) results in false", false_id, simplified_under_contradiction) + + # Test implication: A property implies its primary type + # A value being `:foo` implies it is an atom. + assumptions_with_foo = %{Variable.v_atom_eq(:foo) => true} + # If we simplify t_int under this assumption, it should become false. + # The engine expands to `{is_atom: true, value==:foo: true}`. Then it sees that + # the t_int node's variable `is_integer` must be false (from exclusivity rule). + simplified_int_given_foo = Algo.simplify(t_int, assumptions_with_foo) + test("Simplifying 'integer' given 'value==:foo' results in false", false_id, simplified_int_given_foo) + + # Now, let's simplify the raw intersection of :foo and :bar + simplified_foo_bar = Algo.simplify(intersect_foo_bar_raw, %{}) + # The simplify algorithm should discover the contradiction that an atom cannot be + # both :foo and :bar at the same time. (This requires `check_atom_consistency` to be implemented). + # For now, we stub it and test the plumbing. + # Let's test a simpler contradiction that we *have* implemented. + intersect_atom_int_raw = Algo.apply(:intersect, op_intersect, t_atom, t_int) + simplified_atom_int = Algo.simplify(intersect_atom_int_raw, %{}) + test("Simplifying 'atom & int' results in false", false_id, simplified_atom_int) + + # Test path collapsing + # If we simplify 'atom | int' under the assumption 'is_atom == true', it should become `true`. + simplified_sum_given_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => true}) + test("Simplifying 'atom | int' given 'is_atom==true' results in true", true_id, simplified_sum_given_atom) + # If we simplify 'atom | int' under the assumption 'is_atom == false', it should become `t_int`. + simplified_sum_given_not_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => false}) + test("Simplifying 'atom | int' given 'is_atom==false' results in 'integer'", t_int, simplified_sum_given_not_atom) + + + # --- Final Report --- + failures = Process.get(:test_failures, []) + if failures == [] do + IO.puts("\n✅ All Tdd.Algo tests passed!") + else + IO.puts("\n❌ Found #{length(failures)} test failures.") + # Optional: print details of failed tests if needed + end + end +end defmodule TypeReconstructorTests do alias Tdd.TypeReconstructor alias Tdd.Variable @@ -2369,7 +2431,7 @@ end TypeSpecTests.run() TddStoreTests.run() TddVariableTests.run() -# TddAlgoTests.run() +TddAlgoTests.run() ConsistencyEngineTests.run() TypeReconstructorTests.run() -# CompilerAlgoTests.run() +CompilerAlgoTests.run()