diff --git a/test1.exs b/test1.exs index c4537f6..c0a8eff 100644 --- a/test1.exs +++ b/test1.exs @@ -1081,34 +1081,77 @@ defmodule Tdd do type_none() {var, y, n, d} -> - # First, check if the variable is directly constrained - case Map.get(constraints, var) do - true -> - simplify(y, constraints) + # --- START OF THE CRUCIAL NEW LOGIC --- + # Special check for list head/tail vs. all_elements contradiction. + # This logic MUST be here because it requires calling TDD operations (intersect). + contradiction = + case var do + {5, :head, head_predicate} -> + all_elements_type_id = + Enum.find_value(constraints, fn + {{5, :all_elements, type_id}, true} -> type_id + _ -> nil + end) - false -> - simplify(n, constraints) + if all_elements_type_id do + head_type = predicate_to_tdd(head_predicate) + # Is the required head type compatible with the element type? + intersect(head_type, all_elements_type_id) == type_none() + else + false + end - :dc -> - simplify(d, constraints) + {5, :tail, tail_predicate} -> + all_elements_type_id = + Enum.find_value(constraints, fn + {{5, :all_elements, type_id}, true} -> type_id + _ -> nil + end) - # If not directly constrained, check for an *implied* constraint - nil -> - case PredicateLogic.check_implication(var, constraints) do - true -> - simplify(y, constraints) + if all_elements_type_id do + tail_type = predicate_to_tdd(tail_predicate) + # The tail must be a list of the element type. + required_tail_type = type_list_of(all_elements_type_id) + intersect(tail_type, required_tail_type) == type_none() + else + false + end - false -> - simplify(n, constraints) + _ -> + false + end - # If the node cannot be eliminated, we MUST simplify its children - # and rebuild the node. This is the key fix. - :unknown -> - res_y = simplify(y, Map.put(constraints, var, true)) - res_n = simplify(n, Map.put(constraints, var, false)) - res_d = simplify(d, Map.put(constraints, var, :dc)) - Core.make_node(var, res_y, res_n, res_d) - end + if contradiction do + # The 'yes' branch is impossible. The node simplifies to its 'no' branch. + simplify(n, constraints) + else + # --- END OF NEW LOGIC --- + # Proceed with the original simplification logic. + case Map.get(constraints, var) do + true -> + simplify(y, constraints) + + false -> + simplify(n, constraints) + + :dc -> + simplify(d, constraints) + + nil -> + case PredicateLogic.check_implication(var, constraints) do + true -> + simplify(y, constraints) + + false -> + simplify(n, constraints) + + :unknown -> + res_y = simplify(y, Map.put(constraints, var, true)) + res_n = simplify(n, Map.put(constraints, var, false)) + res_d = simplify(d, Map.put(constraints, var, :dc)) + Core.make_node(var, res_y, res_n, res_d) + end + end end end end @@ -1206,6 +1249,45 @@ defmodule Tdd do end end + @doc """ + Converts a single predicate variable into a full TDD type. + This is the key to comparing predicates with other TDD types. + """ + defp predicate_to_tdd(predicate) do + # Memoize for performance, as this might be called repeatedly. + cache_key = {:predicate_to_tdd, predicate} + + if cached = Core.get_op_cache(cache_key) do + cached + else + res = + case predicate do + {0, :is_atom} -> type_atom() + {0, :is_tuple} -> type_tuple() + {0, :is_integer} -> type_integer() + {0, :is_list} -> type_list() + {1, :value, val} -> type_atom_literal(val) + {2, :beq, n} -> type_int_eq(n) + {2, :alt, n} -> type_int_lt(n) + {2, :cgt, n} -> type_int_gt(n) + {4, :size, n} -> type_tuple_sized_any(n) + {5, :is_empty} -> type_empty_list() + # A head/tail predicate implies the value is a list AND has that head/tail. + # The inner predicate is what we care about for the type check. + {5, :head, inner_p} -> predicate_to_tdd(inner_p) + {5, :tail, inner_p} -> predicate_to_tdd(inner_p) + {5, :all_elements, type_id} -> type_list_of(type_id) + # A tuple element predicate is about the element, not the tuple itself. + {4, :element, _, inner_p} -> predicate_to_tdd(inner_p) + # Fallback for unknown/complex predicates: assume they can be anything. + _ -> type_any() + end + + Core.put_op_cache(cache_key, res) + res + end + end + @doc """ Prints a human-readable representation of a TDD, starting from the given ID. It recursively prints the structure of the graph. @@ -2006,20 +2088,38 @@ defmodule AdhocTest do import Tdd def run(test_fn) do - tup_atom_any = type_tuple([type_atom(), type_any()]) - tup_s2_any = type_tuple_sized_any(2) - # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples. - diff1 = intersect(tup_s2_any, negate(tup_atom_any)) + # --- Basic Types --- + t_atom = type_atom() + t_int = type_integer() + t_pos_int = type_int_gt(0) + t_int_5 = type_int_eq(5) - # {integer, integer} has a first element that is not an atom, so it should be in the difference. - tup_int_int = type_tuple([type_integer(), type_integer()]) - test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1)) + # --- list(X) Types --- + t_list_of_int = type_list_of(t_int) + t_list_of_pos_int = type_list_of(t_pos_int) + t_list_of_atom = type_list_of(t_atom) + + # --- Specific List Types --- + t_list = type_list() + t_empty_list = type_empty_list() + # [5] + t_list_one_int = type_cons(t_int_5, t_empty_list) + # [:foo] + t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list) + # [5, :foo] + t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list)) + intersect4 = intersect(t_list_of_int, t_list_one_int) + IO.inspect("first_subtype") + a = is_subtype(intersect4, t_list_one_int) + IO.inspect("second_subtype") + b = is_subtype(t_list_one_int, intersect4) + test_fn.("list(integer) & [5] == [5]", true, a == b) end end -test_all.() -IntegerTests.run(test) -TupleTests.run(test) -ListTests.run(test) -ListOfTests.run(test) -# AdhocTest.run(test) +# test_all.() +# IntegerTests.run(test) +# TupleTests.run(test) +# ListTests.run(test) +# ListOfTests.run(test) +AdhocTest.run(test)