diff --git a/test.exs b/test.exs index a0a0d9c..70f78f7 100644 --- a/test.exs +++ b/test.exs @@ -301,7 +301,7 @@ defmodule Tdd do end) if MapSet.size(primary_true_predicates) > 1 do - # IO.inspect(assumptions_map, label: "Contradiction: Primary Types") + IO.inspect(assumptions_map, label: "Contradiction: Primary Types") :contradiction else # Check 2: Specific atom value conflicts, e.g. {1, :value, :foo} == true AND {1, :value, :bar} == true @@ -312,7 +312,7 @@ defmodule Tdd do end) if MapSet.size(atom_value_trues) > 1 do - # IO.inspect(assumptions_map, label: "Contradiction: Atom Values") + IO.inspect(assumptions_map, label: "Contradiction: Atom Values") :contradiction else # Check 3: Tuple size conflicts, e.g. {4, :size, 2} == true AND {4, :size, 3} == true @@ -323,16 +323,67 @@ defmodule Tdd do end) if MapSet.size(tuple_size_trues) > 1 do - # IO.inspect(assumptions_map, label: "Contradiction: Tuple Sizes") :contradiction else - # Add more checks as new variable types are introduced - :consistent + # Check 4: Integer predicate conflicts (New) + # Collect all integer constraints assumed to be true + # eq_val stores THE value if an :eq constraint is true. nil otherwise. + # lt_bound stores the smallest N for which `val < N` is true (upper bound, exclusive). nil if none. + # gt_bound stores the largest N for which `val > N` is true (lower bound, exclusive). nil if none. + constraints = + Enum.reduce(assumptions_map, %{eq_val: nil, lt_b: nil, gt_b: nil}, fn + {{2, :eq, n}, true}, acc -> + %{acc | eq_val: if(is_nil(acc.eq_val) or acc.eq_val == n, do: n, else: :conflict)} + + {{2, :lt, n}, true}, acc -> + %{acc | lt_b: min_opt(acc.lt_b, n)} + + {{2, :gt, n}, true}, acc -> + %{acc | gt_b: max_opt(acc.gt_b, n)} + + _otherwise, acc -> + acc + end) + + cond do + # Multiple different equality constraints + constraints.eq_val == :conflict -> + :contradiction + + # Check eq_val against lt_b and gt_b + is_integer(constraints.eq_val) -> + eq_v = constraints.eq_val + lt_ok = is_nil(constraints.lt_b) || eq_v < constraints.lt_b + gt_ok = is_nil(constraints.gt_b) || eq_v > constraints.gt_b + if lt_ok && gt_ok, do: :consistent, else: :contradiction + + # Check lt_b vs gt_b (if no specific eq_val) + is_integer(constraints.lt_b) && is_integer(constraints.gt_b) && + constraints.lt_b <= constraints.gt_b + 1 -> + # e.g., x < 5 AND x > 4 (no integer) OR x < 5 AND x > 3 (only x=4) + # If lt_b <= gt_b + 1, it means there's no integer space or only one possible integer. + # If lt_b == gt_b + 1, it implies x must be that one integer. This isn't a contradiction by itself yet. + # If lt_b <= gt_b, it's a definite contradiction e.g. x < 5 and x > 5. + if constraints.lt_b <= constraints.gt_b, do: :contradiction, else: :consistent + + # No contradiction found from integer constraints alone + true -> + :consistent + end end end end end + # Helper for min, treating nil as infinity + defp min_opt(nil, x), do: x + defp min_opt(x, nil), do: x + defp min_opt(x, y), do: min(x, y) + + # Helper for max, treating nil as -infinity + defp max_opt(nil, x), do: x + defp max_opt(x, nil), do: x + defp max_opt(x, y), do: max(x, y) # --- Semantic Simplification (Memoized) --- defp simplify_with_constraints(tdd_id, assumptions_map) do state = get_state() @@ -410,11 +461,20 @@ defmodule Tdd do @v_is_atom {0, :is_atom} @v_is_tuple {0, :is_tuple} + # New primary type + @v_is_integer {0, :is_integer} def v_atom_eq(atom_val), do: {1, :value, atom_val} def v_tuple_size_eq(size), do: {4, :size, size} def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id} + # Integer Predicates (Category 2) + def v_int_eq(n) when is_integer(n), do: {2, :eq, n} + # strictly less than n + def v_int_lt(n) when is_integer(n), do: {2, :lt, n} + # strictly greater than n + def v_int_gt(n) when is_integer(n), do: {2, :gt, n} + def type_any, do: @true_node_id def type_none, do: @false_node_id @@ -449,6 +509,30 @@ defmodule Tdd do simplify_with_constraints(raw_node, %{}) end + def type_integer do + make_node_for_constructors(@v_is_integer, @true_node_id, @false_node_id, @false_node_id) + end + + def type_int_eq(n) do + int_eq_node = make_node_raw(v_int_eq(n), @true_node_id, @false_node_id, @false_node_id) + raw_node = make_node_raw(@v_is_integer, int_eq_node, @false_node_id, @false_node_id) + simplify_with_constraints(raw_node, %{}) + end + + # Represents integers x where x < n + def type_int_lt(n) do + int_lt_node = make_node_raw(v_int_lt(n), @true_node_id, @false_node_id, @false_node_id) + raw_node = make_node_raw(@v_is_integer, int_lt_node, @false_node_id, @false_node_id) + simplify_with_constraints(raw_node, %{}) + end + + # Represents integers x where x > n + def type_int_gt(n) do + int_gt_node = make_node_raw(v_int_gt(n), @true_node_id, @false_node_id, @false_node_id) + raw_node = make_node_raw(@v_is_integer, int_gt_node, @false_node_id, @false_node_id) + simplify_with_constraints(raw_node, %{}) + end + # --- The APPLY Algorithm (Core Logic, uses make_node_raw) --- # This function computes the raw structural result. Semantic simplification is applied by the caller. defp apply_raw(op_name, op_lambda, u1_id, u2_id) do @@ -868,4 +952,131 @@ test_all = fn -> IO.inspect(Process.get(:test_failures, [])) end -test_all.() +defmodule IntegerTests do + def run(test_fn) do + Process.put(:test_failures, []) + # Reset for each test group if needed, or once globally + Tdd.init_tdd_system() + + # Integer types + tdd_int = Tdd.type_integer() + tdd_int_5 = Tdd.type_int_eq(5) + tdd_int_7 = Tdd.type_int_eq(7) + # x < 10 + tdd_int_lt_10 = Tdd.type_int_lt(10) + # x > 3 + tdd_int_gt_3 = Tdd.type_int_gt(3) + # x < 3 + tdd_int_lt_3 = Tdd.type_int_lt(3) + # x > 10 + tdd_int_gt_10 = Tdd.type_int_gt(10) + tdd_atom_foo = Tdd.type_atom_literal(:foo) + + IO.puts("\n--- Integer Type Structures ---") + IO.puts("Integer:") + Tdd.print_tdd(tdd_int) + IO.puts("Int == 5:") + Tdd.print_tdd(tdd_int_5) + IO.puts("Int < 10:") + Tdd.print_tdd(tdd_int_lt_10) + + IO.puts("\n--- Integer Subtyping Tests ---") + test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int)) + test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5)) + test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7)) + test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5)) + test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo)) + + test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int)) + test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10)) + # 5 < 10 + test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10)) + test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5)) + + test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int)) + # 5 > 3 + test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3)) + test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5)) + + # x < 3 implies x < 10 + test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10)) + # x > 10 implies x > 3 + test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3)) + test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3)) + test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10)) + + IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---") + intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7) + test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none()) + IO.puts("Structure of int_5 & int_7 (should be ID 0):") + Tdd.print_tdd(intersect_5_7) + + # x < 3 AND x > 10 + intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10) + test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none()) + IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):") + Tdd.print_tdd(intersect_lt3_gt10) + + # x < 10 AND x > 3 (e.g. 4,5..9) + intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3) + test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none()) + IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):") + Tdd.print_tdd(intersect_lt10_gt3) + # Test a value within this intersection + test_fn.( + "int_5 <: (int_lt_10 & int_gt_3)", + true, + Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3) + ) + + # x == 5 AND x < 3 + intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3) + test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none()) + + IO.puts("\n--- Integer Union Tests ---") + union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7) + test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7)) + test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7)) + test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7)) + IO.puts("Structure of int_5 | int_7:") + Tdd.print_tdd(union_5_7) + + # (int < 3) | (int > 10) + union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10) + + test_fn.( + "int_eq(0) <: (int < 3 | int > 10)", + true, + Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges) + ) + + test_fn.( + "int_eq(5) <: (int < 3 | int > 10)", + false, + Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges) + ) + + test_fn.( + "int_eq(12) <: (int < 3 | int > 10)", + true, + Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges) + ) + + IO.inspect(Process.get(:test_failures, [])) + end +end + +# test_all.() +# IntegerTests.run(test) + +# x < 3 +tdd_int_lt_3 = Tdd.type_int_lt(3) +# x > 10 +tdd_int_gt_10 = Tdd.type_int_gt(10) +union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10) + +test.( + "int_eq(12) <: (int < 3 | int > 10)", + true, + Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges) +)