From 9f6cd2814a3cce0c81067791eedbbe2cd42e4740 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Wed, 18 Jun 2025 15:00:36 +0200 Subject: [PATCH] checkpoint --- new.exs | 915 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 910 insertions(+), 5 deletions(-) diff --git a/new.exs b/new.exs index 3f601b1..1ea6885 100644 --- a/new.exs +++ b/new.exs @@ -386,6 +386,552 @@ defmodule Tdd.Variable do def v_list_tail_pred(nested_pred_var), do: {5, :d_tail, nested_pred_var, nil} end +defmodule Tdd.Predicate.Info do + @moduledoc "A knowledge base for the properties of TDD predicate variables." + alias Tdd.Variable + + @doc "Returns a map of traits for a given predicate variable." + @spec get_traits(term()) :: map() | nil + def get_traits({0, :is_atom, _, _}), do: %{type: :primary, category: :atom} + def get_traits({0, :is_integer, _, _}), do: %{type: :primary, category: :integer} + def get_traits({0, :is_list, _, _}), do: %{type: :primary, category: :list} + def get_traits({0, :is_tuple, _, _}), do: %{type: :primary, category: :tuple} + + def get_traits({1, :value, _val, _}) do + %{type: :atom_value, category: :atom, implies: [{Variable.v_is_atom(), true}]} + end + + def get_traits({2, :alt, _, _}), + do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]} + + def get_traits({2, :beq, _, _}), + do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]} + + def get_traits({2, :cgt, _, _}), + do: %{type: :integer_prop, category: :integer, implies: [{Variable.v_is_integer(), true}]} + + def get_traits({4, :a_size, _, _}) do + %{type: :tuple_prop, category: :tuple, implies: [{Variable.v_is_tuple(), true}]} + end + + def get_traits({4, :b_element, index, _nested_var}) do + %{ + type: :tuple_recursive, + category: :tuple, + sub_key: {:elem, index}, + implies: [{Variable.v_is_tuple(), true}] + } + end + + def get_traits({5, :a_all_elements, element_spec, _}) do + %{ + type: :list_recursive_ambient, + category: :list, + ambient_constraint_spec: element_spec, + implies: [{Variable.v_is_list(), true}] + } + end + + def get_traits({5, :b_is_empty, _, _}) do + %{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]} + end + + def get_traits({5, :c_head, _nested_var, _}) do + %{ + type: :list_recursive, + category: :list, + sub_key: :head, + implies: [{Variable.v_is_list(), true}, {Variable.v_list_is_empty(), false}] + } + end + + def get_traits({5, :d_tail, _nested_var, _}) do + %{ + type: :list_recursive, + category: :list, + sub_key: :tail, + implies: [{Variable.v_is_list(), true}, {Variable.v_list_is_empty(), false}] + } + end + + # Default case for unknown variables + def get_traits(_), do: nil +end + +# in a new file, e.g., lib/tdd/consistency/engine.ex +defmodule Tdd.Consistency.Engine do + @moduledoc """ + A rule-based engine for checking the semantic consistency of a set of assumptions. + Placeholders: The check_atom_consistency and check_integer_consistency functions are placeholders. They would need to be filled in with the logic for checking unique values and valid ranges, respectively. + + The Circular Dependency: The check_recursive_consistency function highlights the deepest challenge. To properly check if a head's assumed type is compatible with a list_of(X) constraint, the consistency engine needs to ask the TDD compiler: "What is the TDD for the type implied by these head assumptions?" and "What is the TDD for X?", and then call is_subtype. This creates a cycle: Algo.simplify -> Engine.check -> Compiler.spec_to_id -> Algo.simplify. + + Breaking the Cycle: The standard way to break this cycle is to pass a "compiler handle" or context down through the calls. Engine.check wouldn't call the top-level compiler, but a recursive version that knows it's already inside a compilation. For now, we will leave this logic incomplete, as fully implementing it is a major task. The key is that we have isolated where this hard problem lives. + """ + + alias Tdd.Predicate.Info + + @doc "Checks if a map of assumptions is logically consistent." + @spec check(map()) :: :consistent | :contradiction + def check(assumptions) do + with {:ok, expanded} <- expand_with_implications(assumptions), + :ok <- check_flat_consistency(expanded), + :ok <- check_recursive_consistency(expanded) do + :consistent + else + :error -> :contradiction + end + end + + # Expands the assumption set by recursively adding all implied truths. + defp expand_with_implications(assumptions, new_implications \\ true) do + if new_implications == false do + {:ok, assumptions} + else + {next_assumptions, added_new} = + Enum.reduce(assumptions, {assumptions, false}, fn + {var, true}, {acc, changed} -> + case Info.get_traits(var) do + %{implies: implies_list} -> + Enum.reduce(implies_list, {acc, changed}, fn {implied_var, implied_val}, + {inner_acc, inner_changed} -> + case Map.get(inner_acc, implied_var) do + nil -> {Map.put(inner_acc, implied_var, implied_val), true} + ^implied_val -> {inner_acc, inner_changed} + # Mark for immediate failure + _ -> {Map.put(inner_acc, :__contradiction__, true), true} + end + end) + + _ -> + {acc, changed} + end + + _other_assumption, acc -> + acc + end) + + if Map.has_key?(next_assumptions, :__contradiction__) do + :error + else + expand_with_implications(next_assumptions, added_new) + end + end + end + + # Checks for contradictions on a "flat" set of properties for a single entity. + defp check_flat_consistency(assumptions) do + # Group assumptions by category defined in Predicate.Info + by_category = + Enum.group_by(assumptions, fn {var, _val} -> + case Info.get_traits(var) do + %{category: cat} -> cat + _ -> :unknown + end + end) + + # Chain together all the individual checks + # Add tuple, etc. checks here + with :ok <- + check_primary_exclusivity( + Map.get(by_category, :atom, []), + Map.get(by_category, :integer, []), + Map.get(by_category, :list, []), + Map.get(by_category, :tuple, []) + ), + :ok <- check_atom_consistency(Map.get(by_category, :atom, [])), + :ok <- check_integer_consistency(Map.get(by_category, :integer, [])), + :ok <- check_list_flat_consistency(Map.get(by_category, :list, [])) do + :ok + else + :error -> :error + end + end + + # Checks that at most one primary type is true. + defp check_primary_exclusivity(atom_asm, int_asm, list_asm, tuple_asm) do + # Simplified: count how many primary types are constrained to be true + true_primary_types = + [atom_asm, int_asm, list_asm, tuple_asm] + |> Enum.count(fn assumptions_list -> + # A primary type is true if its main var is explicitly true, + # or if any of its property vars are true. + Enum.any?(assumptions_list, fn {_, val} -> val == true end) + end) + + if true_primary_types > 1, do: :error, else: :ok + end + + # Placeholder for atom-specific checks (e.g., cannot be :foo and :bar) + defp check_atom_consistency(_assumptions), do: :ok + + # Placeholder for integer-specific checks (e.g., x < 5 and x > 10) + defp check_integer_consistency(_assumptions), do: :ok + + # Checks for flat contradictions on a list, e.g. is_empty and has_head. + defp check_list_flat_consistency(assumptions) do + is_empty_true = + Enum.any?(assumptions, fn {var, val} -> + val == true and Info.get_traits(var)[:type] == :list_prop + end) + + has_head_or_tail_prop = + Enum.any?(assumptions, fn {var, val} -> + val == true and Info.get_traits(var)[:type] == :list_recursive + end) + + if is_empty_true and has_head_or_tail_prop, do: :error, else: :ok + end + + # Handles recursive checks for structured types. + defp check_recursive_consistency(assumptions) do + # This is still a complex piece of logic, but it's now more structured. + # Partition assumptions into sub-problems (head, tail, elements) + sub_problems = + Enum.reduce(assumptions, %{}, fn {var, val}, acc -> + case Info.get_traits(var) do + %{type: :list_recursive, sub_key: key} -> + # var is e.g. {5, :c_head, {0, :is_atom, nil, nil}, nil} + # we want to create a sub-problem for :head with assumption {{0, :is_atom, nil, nil} => val} + {_cat, _pred, nested_var, _pad} = var + Map.update(acc, key, [{nested_var, val}], &[{nested_var, val} | &1]) + + %{type: :tuple_recursive, sub_key: key} -> + # Similar logic for tuples + {_cat, _pred, _index, nested_var} = var + Map.update(acc, key, [{nested_var, val}], &[{nested_var, val} | &1]) + + _ -> + acc + end + end) + + # Get ambient constraints (e.g., from `list_of(X)`) + ambient_constraints = + Enum.reduce(assumptions, %{}, fn {var, true}, acc -> + case Info.get_traits(var) do + %{type: :list_recursive_ambient, ambient_constraint_spec: spec} -> + # This part is tricky. How do we enforce this? + # We need to know that the sub-problem's type is a subtype of this spec. + # This requires the TDD compiler. This is the main circular dependency. + # simplified for now + Map.put(acc, :head, spec) + + _ -> + acc + end + end) + + # Recursively check each sub-problem + Enum.reduce_while(sub_problems, :ok, fn {sub_key, sub_assumptions_list}, _acc -> + sub_assumptions_map = Map.new(sub_assumptions_list) + # Here we would also need to check against ambient constraints. + # e.g. is_subtype(build_type_from(sub_assumptions_map), ambient_constraints[sub_key]) + # This logic remains complex. + + case check(sub_assumptions_map) do + :consistent -> {:cont, :ok} + :contradiction -> {:halt, :error} + end + end) + end +end + +# in a new file, e.g., lib/tdd/algo.ex +# defmodule Tdd.Algo do +# @moduledoc "Implements the core, stateless algorithms for TDD manipulation." +# alias Tdd.Store +# alias Tdd.Consistency.Engine +# +# # --- Binary Operation: Apply --- +# @spec apply(atom, (atom, atom -> atom), non_neg_integer, non_neg_integer) :: non_neg_integer +# def apply(op_name, op_lambda, u1_id, u2_id) do +# cache_key = {op_name, Enum.sort([u1_id, u2_id])} +# +# case Store.get_op_cache(cache_key) do +# {:ok, result_id} -> +# result_id +# +# :not_found -> +# result_id = do_apply(op_name, op_lambda, u1_id, u2_id) +# Store.put_op_cache(cache_key, result_id) +# result_id +# end +# end +# +# defp do_apply(op_name, op_lambda, u1_id, u2_id) do +# # This is the classic Shannon Expansion algorithm (ITE - If-Then-Else) +# with {:ok, u1_details} <- Store.get_node(u1_id), +# {:ok, u2_details} <- Store.get_node(u2_id) do +# cond do +# # Terminal cases +# (u1_details == :true_terminal or u1_details == :false_terminal) and +# (u2_details == :true_terminal or u2_details == :false_terminal) -> +# res_terminal_symbol = op_lambda.(u1_details, u2_details) +# +# if res_terminal_symbol == :true_terminal, +# do: Store.true_node_id(), +# else: Store.false_node_id() +# +# # One is terminal, one is not +# u1_details == :true_terminal or u1_details == :false_terminal -> +# {var2, y2, n2, d2} = u2_details +# res_y = apply(op_name, op_lambda, u1_id, y2) +# res_n = apply(op_name, op_lambda, u1_id, n2) +# res_d = apply(op_name, op_lambda, u1_id, d2) +# Store.find_or_create_node(var2, res_y, res_n, res_d) +# +# u2_details == :true_terminal or u2_details == :false_terminal -> +# {var1, y1, n1, d1} = u1_details +# res_y = apply(op_name, op_lambda, y1, u2_id) +# res_n = apply(op_name, op_lambda, n1, u2_id) +# res_d = apply(op_name, op_lambda, d1, u2_id) +# Store.find_or_create_node(var1, res_y, res_n, res_d) +# +# # Both are non-terminals +# true -> +# {var1, y1, n1, d1} = u1_details +# {var2, y2, n2, d2} = u2_details +# # Select top variable based on global order +# top_var = Enum.min([var1, var2]) +# +# res_y = +# apply( +# op_name, +# op_lambda, +# if(var1 == top_var, do: y1, else: u1_id), +# if(var2 == top_var, do: y2, else: u2_id) +# ) +# +# res_n = +# apply( +# op_name, +# op_lambda, +# if(var1 == top_var, do: n1, else: u1_id), +# if(var2 == top_var, do: n2, else: u2_id) +# ) +# +# res_d = +# apply( +# op_name, +# op_lambda, +# if(var1 == top_var, do: d1, else: u1_id), +# if(var2 == top_var, do: d2, else: u2_id) +# ) +# +# Store.find_or_create_node(top_var, res_y, res_n, res_d) +# end +# end +# end +# +# # --- Unary Operation: Negation --- +# @spec negate(non_neg_integer) :: non_neg_integer +# def negate(tdd_id) do +# cache_key = {:negate, tdd_id} +# +# case Store.get_op_cache(cache_key) do +# {:ok, result_id} -> +# result_id +# +# :not_found -> +# result_id = +# case Store.get_node(tdd_id) do +# {:ok, :true_terminal} -> +# Store.false_node_id() +# +# {:ok, :false_terminal} -> +# Store.true_node_id() +# +# {:ok, {var, y, n, d}} -> +# res_y = negate(y) +# res_n = negate(n) +# res_d = negate(d) +# Store.find_or_create_node(var, res_y, res_n, res_d) +# end +# +# Store.put_op_cache(cache_key, result_id) +# result_id +# end +# end +# +# # --- Unary Operation: Semantic Simplification --- +# @spec simplify(non_neg_integer(), map()) :: non_neg_integer() +# def simplify(tdd_id, assumptions) do +# sorted_assumptions = Enum.sort(assumptions) +# cache_key = {:simplify, tdd_id, sorted_assumptions} +# +# case Store.get_op_cache(cache_key) do +# {:ok, result_id} -> +# result_id +# +# :not_found -> +# result_id = do_simplify(tdd_id, assumptions) +# Store.put_op_cache(cache_key, result_id) +# result_id +# end +# end +# +# defp do_simplify(tdd_id, assumptions) do +# # 1. Check if current path is contradictory. +# if Engine.check(assumptions) == :contradiction do +# Store.false_node_id() +# else +# case Store.get_node(tdd_id) do +# # 2. Handle terminal nodes. +# {:ok, :true_terminal} -> +# Store.true_node_id() +# +# {:ok, :false_terminal} -> +# Store.false_node_id() +# +# # 3. Handle non-terminal nodes. +# {:ok, {var, y, n, d}} -> +# # 4. Check if the variable is already constrained. +# case Map.get(assumptions, var) do +# true -> +# simplify(y, assumptions) +# +# false -> +# simplify(n, assumptions) +# +# :dc -> +# simplify(d, assumptions) +# +# nil -> +# # Not constrained, so we check for implied constraints. +# # Note: This is an expensive part of the algorithm. +# # (As noted, the recursive part of the check is still incomplete) +# implies_true = Engine.check(Map.put(assumptions, var, false)) == :contradiction +# implies_false = Engine.check(Map.put(assumptions, var, true)) == :contradiction +# +# cond do +# # Should be caught by initial check +# implies_true and implies_false -> +# Store.false_node_id() +# +# implies_true -> +# simplify(y, assumptions) +# +# implies_false -> +# simplify(n, assumptions) +# +# true -> +# # Recurse on all branches with new assumptions +# s_y = simplify(y, Map.put(assumptions, var, true)) +# s_n = simplify(n, Map.put(assumptions, var, false)) +# s_d = simplify(d, Map.put(assumptions, var, :dc)) +# Store.find_or_create_node(var, s_y, s_n, s_d) +# end +# end +# end +# end +# end +# end +defmodule Tdd.TypeReconstructor do + @moduledoc """ + Reconstructs a high-level `TypeSpec` from a low-level assumption map. + + This module performs the inverse operation of the TDD compiler. It takes a + set of predicate assumptions (e.g., from a path in a TDD) and synthesizes + the most specific `TypeSpec` that satisfies all of those assumptions. + """ + alias Tdd.TypeSpec + alias Tdd.Predicate.Info + alias Tdd.Variable + + @doc """ + Takes a map of `{variable, boolean}` assumptions and returns a `TypeSpec`. + """ + @spec spec_from_assumptions(map()) :: TypeSpec.t() + def spec_from_assumptions(assumptions) do + # 1. Partition assumptions into groups for the top-level entity and its sub-components. + 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} + # All other predicates apply to the top-level entity + _ -> :top_level + end + end) + + # 2. Reconstruct the spec for the top-level entity from its flat assumptions. + top_level_assumptions = Map.get(partitions, :top_level, []) |> Map.new() + top_level_spec = spec_from_flat_assumptions(top_level_assumptions) + + # 3. Recursively reconstruct specs for all sub-problems (head, tail, elements). + sub_problem_specs = + partitions + |> Map.drop([:top_level]) + |> Enum.map(fn {sub_key, sub_assumptions_list} -> + # Re-map the nested variables back to their base form for the recursive call. + # e.g., {{5, :c_head, NESTED_VAR, _}, val} -> {NESTED_VAR, val} + remapped_assumptions = + sub_assumptions_list + |> 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, val} + end) + + # Recursively build the spec for the sub-problem + sub_spec = spec_from_assumptions(remapped_assumptions) + + # 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 + {: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 + end + end) + + # 4. The final spec is the intersection of the top-level spec and all sub-problem specs. + final_spec_list = [top_level_spec | sub_problem_specs] + 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 = + Enum.map(assumptions, fn {var, bool_val} -> + # Convert each assumption into a `TypeSpec`. + # A `true` assumption means the type is `X`. + # A `false` assumption means the type is `¬X`. + spec = + case var do + {0, :is_atom, _, _} -> :atom + {0, :is_integer, _, _} -> :integer + {0, :is_list, _, _} -> :list + {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 + {2, :beq, n, _} -> {:literal, n} + {2, :cgt, n, _} -> {:integer_range, n + 1, :pos_inf} # x > n + {4, :a_size, _, _} -> :tuple # Simplified for now + {5, :b_is_empty, _, _} -> {:literal, []} + # Ignore recursive and ambient vars at this flat level + _ -> :any + end + + if bool_val, do: spec, else: {:negation, spec} + end) + + # The result is the intersection of all the individual specs. + TypeSpec.normalize({:intersect, specs}) + end +end +#### +# xxx +#### + defmodule TddStoreTests do def test(name, expected, result) do if expected == result do @@ -695,21 +1241,31 @@ defmodule TddVariableTests do test("v_is_atom returns correct tuple", {0, :is_atom, nil, nil}, Variable.v_is_atom()) test("v_atom_eq returns correct tuple", {1, :value, :foo, nil}, Variable.v_atom_eq(:foo)) test("v_int_lt returns correct tuple", {2, :alt, 10, nil}, Variable.v_int_lt(10)) - test("v_tuple_size_eq returns correct tuple", {4, :a_size, 2, nil}, Variable.v_tuple_size_eq(2)) + + test( + "v_tuple_size_eq returns correct tuple", + {4, :a_size, 2, nil}, + Variable.v_tuple_size_eq(2) + ) test( "v_tuple_elem_pred nests a variable correctly", - {4, :b_element, 0, {0, :is_integer, nil, nil }}, + {4, :b_element, 0, {0, :is_integer, nil, nil}}, Variable.v_tuple_elem_pred(0, Variable.v_is_integer()) ) - test("v_list_is_empty returns correct tuple", {5, :b_is_empty, nil, nil}, Variable.v_list_is_empty()) + test( + "v_list_is_empty returns correct tuple", + {5, :b_is_empty, nil, nil}, + Variable.v_list_is_empty() + ) test( "v_list_head_pred nests a variable correctly", {5, :c_head, {0, :is_atom, nil, nil}, nil}, Variable.v_list_head_pred(Variable.v_is_atom()) ) + test( "v_list_all_elements_are nests a TypeSpec correctly", {5, :a_all_elements, {:union, [:atom, :integer]}, nil}, @@ -760,8 +1316,13 @@ defmodule TddVariableTests do Variable.v_tuple_elem_pred(0, Variable.v_is_atom()) < Variable.v_tuple_elem_pred(0, Variable.v_is_integer()) ) -IO.inspect(Variable.v_list_all_elements_are(:atom), label: "Variable.v_list_all_elements_are(:atom)") + + IO.inspect(Variable.v_list_all_elements_are(:atom), + label: "Variable.v_list_all_elements_are(:atom)" + ) + IO.inspect(Variable.v_list_is_empty(), label: "Variable.v_list_is_empty()") + test( "List :a_all_elements var < List :b_is_empty var", true, @@ -792,7 +1353,351 @@ IO.inspect(Variable.v_list_all_elements_are(:atom), label: "Variable.v_list_all_ end end -# To run the tests, you would call this function: + +defmodule ConsistencyEngineTests do + alias Tdd.Consistency.Engine + alias Tdd.Variable + + defp test(name, expected, assumptions_map) do + result = Engine.check(assumptions_map) + # ... test reporting logic ... + 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, [])]) + end + end + + def run() do + IO.puts("\n--- Running Tdd.Consistency.Engine Tests ---") + Process.put(:test_failures, []) + + # --- Section: Basic & Implication Tests --- + 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 + ) + + # --- 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, + %{Variable.v_atom_eq(:foo) => true} + ) + + # --- 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} + ) + 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} + ) + 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 + ) + + # --- 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}) + + # --- Final Report --- + failures = Process.get(:test_failures, []) + if failures == [] do + IO.puts("\n✅ All Consistency.Engine tests passed!") + else + IO.puts("\n❌ Found #{length(failures)} test failures.") + 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 + alias Tdd.TypeSpec + + defp test(name, expected_spec, assumptions) do + # Normalize both expected and result for a canonical comparison + expected = TypeSpec.normalize(expected_spec) + result = TypeSpec.normalize(TypeReconstructor.spec_from_assumptions(assumptions)) + + 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)}") + Process.put(:test_failures, [name | Process.get(:test_failures, [])]) + end + end + + def run() do + IO.puts("\n--- Running Tdd.TypeReconstructor Tests ---") + Process.put(:test_failures, []) + + # --- Section: Basic Flat Reconstructions --- + 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, []}, + %{Variable.v_is_list() => true, Variable.v_list_is_empty() => true} + ) + + # --- 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} + ]}, + %{Variable.v_int_gt(10) => true, Variable.v_int_lt(20) => true} + ) + + # --- Section: Recursive Reconstructions (Simplified) --- + IO.puts("\n--- Section: Recursive Reconstructions ---") + # This tests the partitioning and recursive call logic. + # Our simple implementation of recursive cases means we can only test simple things. + test( + "head is an atom", + {:intersect, [:list, {:cons, :atom, :any}]}, + # Assumption for `is_list=true` is implied by `v_list_head_pred` + %{Variable.v_list_head_pred(Variable.v_is_atom()) => true} + ) + + # Note: The recursive tests are limited by the simplifications made in the + # implementation (e.g., tuple reconstruction). A full implementation would + # require more context (like tuple size) to be passed down. + + # --- Final Report --- + failures = Process.get(:test_failures, []) + if failures == [] do + IO.puts("\n✅ All TypeReconstructor tests passed!") + else + IO.puts("\n❌ Found #{length(failures)} test failures.") + end + end +end TypeSpecTests.run() TddStoreTests.run() TddVariableTests.run() +# TddAlgoTests.run() +# ConsistencyEngineTests.run() +TypeReconstructorTests.run()