consistency fixed
This commit is contained in:
Kacper Marzecki
parent
5736c30fa2
commit
7fa469518d
366
new.exs
366
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()
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user