diff --git a/test.exs b/test.exs index 57e5b06..51661b0 100644 --- a/test.exs +++ b/test.exs @@ -331,7 +331,7 @@ defmodule Tdd do end defp check_assumptions_consistency(assumptions_map, ambient_constraints \\ %{}) do - # 1. Merge ambient constraints into the main map. + # 1. Merge ambient constraints into the main map. # This ensures, for example, that if we are checking the `head` of a `list(X)`, # the constraint `is_subtype(head, X)` is enforced. assumptions_map = Map.merge(ambient_constraints, assumptions_map) @@ -498,7 +498,7 @@ defmodule Tdd do end # (The original integer checking logic is moved into this helper) -defp check_integer_logic(assumptions_map, primary_true_predicates) do + defp check_integer_logic(assumptions_map, primary_true_predicates) do has_true_integer_specific_pred = Enum.any?(assumptions_map, fn {var_id, truth_value} -> elem(var_id, 0) == 2 && truth_value == true @@ -584,8 +584,10 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do :alt -> is_integer(current_interval_max) && current_interval_max < n_val + :cgt -> is_integer(current_interval_min) && current_interval_min > n_val + _ -> false end @@ -595,10 +597,13 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do :beq -> (is_integer(current_interval_min) && current_interval_min > n_val) || (is_integer(current_interval_max) && current_interval_max < n_val) + :alt -> is_integer(current_interval_min) && current_interval_min >= n_val + :cgt -> is_integer(current_interval_max) && current_interval_max <= n_val + _ -> false end @@ -636,8 +641,10 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do # A predicate on head or tail exists, e.g. {{5, :head, _}, _} has_head_or_tail_pred = - Enum.any?(assumptions_map, fn {{_cat, ptype, _}, _} -> ptype == :head or ptype == :tail - _ -> false end) + Enum.any?(assumptions_map, fn + {{_cat, ptype, _}, _} -> ptype == :head or ptype == :tail + _ -> false + end) cond do # Contradiction: list-specific rule is assumed, but type is not a list. @@ -926,20 +933,29 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do # 5. Simplify the final result. simplify_with_constraints(raw_final_tdd, %{}) end -def type_list_of(element_type_id) when is_integer(element_type_id) do - # An empty list satisfies any list_of constraint vacuously. - # The type is effectively `[] | [X | list(X)]` - # We can't build this recursively, so we use a specialized predicate. - # This type is trivially `any` if element type is `any` - if element_type_id == type_any() do - type_list() - else - all_elems_check = make_node_raw(v_list_all_elements_are(element_type_id), @true_node_id, @false_node_id, @false_node_id) - raw_node = make_node_raw(v_is_list(), all_elems_check, @false_node_id, @false_node_id) - simplify_with_constraints(raw_node, %{}) + def type_list_of(element_type_id) when is_integer(element_type_id) do + # An empty list satisfies any list_of constraint vacuously. + # The type is effectively `[] | [X | list(X)]` + # We can't build this recursively, so we use a specialized predicate. + + # This type is trivially `any` if element type is `any` + if element_type_id == type_any() do + type_list() + else + all_elems_check = + make_node_raw( + v_list_all_elements_are(element_type_id), + @true_node_id, + @false_node_id, + @false_node_id + ) + + raw_node = make_node_raw(v_is_list(), all_elems_check, @false_node_id, @false_node_id) + simplify_with_constraints(raw_node, %{}) + end end -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) @@ -1843,6 +1859,7 @@ defmodule ListTests do IO.inspect(Process.get(:test_failures, []), label: "ListTests failures") end end + defmodule ListOfTests do import Tdd @@ -1865,9 +1882,12 @@ defmodule ListOfTests do # --- Specific List Types --- t_list = type_list() t_empty_list = type_empty_list() - t_list_one_int = type_cons(t_int_5, t_empty_list) # [5] - t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list) # [:foo] - t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list)) # [5, :foo] + # [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)) IO.puts("\n--- Section: Basic list(X) Subtyping ---") test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list)) @@ -1876,16 +1896,36 @@ defmodule ListOfTests do test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int)) test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int)) test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int)) - test_fn.("[5, :foo] <: list(any)", true, is_subtype(t_list_int_and_atom, type_list_of(type_any()))) + + test_fn.( + "[5, :foo] <: list(any)", + true, + is_subtype(t_list_int_and_atom, type_list_of(type_any())) + ) IO.puts("\n--- Section: Covariance of list(X) ---") - test_fn.("list(pos_integer) <: list(integer)", true, is_subtype(t_list_of_pos_int, t_list_of_int)) - test_fn.("list(integer) <: list(pos_integer)", false, is_subtype(t_list_of_int, t_list_of_pos_int)) + + test_fn.( + "list(pos_integer) <: list(integer)", + true, + is_subtype(t_list_of_pos_int, t_list_of_int) + ) + + test_fn.( + "list(integer) <: list(pos_integer)", + false, + is_subtype(t_list_of_int, t_list_of_pos_int) + ) IO.puts("\n--- Section: Intersection of list(X) ---") # list(integer) & list(pos_integer) should be list(pos_integer) intersect1 = intersect(t_list_of_int, t_list_of_pos_int) - test_fn.("(list(int) & list(pos_int)) == list(pos_int)", true, intersect1 == t_list_of_pos_int) + + test_fn.( + "(list(int) & list(pos_int)) == list(pos_int)", + true, + intersect1 == t_list_of_pos_int + ) # list(integer) & list(atom) should be just [] (empty list is the only common member) # The system simplifies this intersection to a type that only accepts the empty list. @@ -1896,7 +1936,6 @@ defmodule ListOfTests do # It should be equivalent to `type_empty_list` test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list) - IO.puts("\n--- Section: Intersection of list(X) with cons ---") # list(integer) & [:foo | []] -> should be none intersect3 = intersect(t_list_of_int, t_list_one_atom) @@ -1905,7 +1944,7 @@ defmodule ListOfTests do # list(integer) & [5 | []] -> should be [5 | []] intersect4 = intersect(t_list_of_int, t_list_one_int) test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int) - + # list(integer) & [5, :foo] -> should be none intersect5 = intersect(t_list_of_int, t_list_int_and_atom) test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none()) @@ -1913,6 +1952,7 @@ defmodule ListOfTests do IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures") end end + test_all.() IntegerTests.run(test) TupleTests.run(test)