diff --git a/test.exs b/test.exs index 04170af..57e5b06 100644 --- a/test.exs +++ b/test.exs @@ -148,23 +148,22 @@ defmodule Tdd do * `lt(N)` and `gt(M)` if `N <= M+1` (or `N <= M` if `gt` means `>=`) -> contradiction. (e.g., `x < 5` and `x > 4` has no integer solution). * *Strategy for complex integer constraints*: Maintain a "current allowed interval" `[min_assumed, max_assumed]` based on `assumptions_map`. If this interval becomes empty or invalid, it's a contradiction. Each new integer assumption (`lt, gt, eq`) refines this interval. - ### 3.4. Lists (Planned) + ### 3.4. Lists (Implemented) * **Variables**: * `@v_is_list = {0, :is_list}`. - * `v_list_is_empty = {LIST_CAT, :is_empty}`. + * `v_list_is_empty = {5, :is_empty}`. * *If not empty*: - * `v_list_head_VAR = {LIST_CAT, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head. - * `v_list_tail_VAR = {LIST_CAT, :tail, NESTED_PREDICATE_ID_FOR_TAIL_LIST}`: Applies a global predicate (usually list predicates) to the tail. - * *(Alternative for fixed-length lists/known structure: `{LIST_CAT, :elem, Index_I, NESTED_PREDICATE_ID}` similar to tuples).* + * `v_list_head_pred = {5, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head. + * `v_list_tail_pred = {5, :tail, NESTED_PREDICATE_ID_FOR_TAIL}`: Applies a global predicate (usually list predicates) to the tail. * **Constructors**: - * `type_list_any()`. - * `type_empty_list()`. - * `type_cons(head_type_id, tail_type_id)`. - * `type_list_of(element_type_id)`: e.g., `list(integer())`. + * `type_list()`: Represents any list. + * `type_empty_list()`: Represents the empty list `[]`. + * `type_cons(head_type_id, tail_type_id)`: Represents a non-empty list `[H|T]` where `H` is of type `head_type_id` and `T` is of type `tail_type_id`. * **Semantic Constraints**: * `is_list=true` vs. other primary types. - * If `is_empty=true`, then any predicate about `head` or non-empty `tail` structure is contradictory if it implies existence. + * If `is_empty=true`, any predicate on the `head` or `tail` is a contradiction. + * Recursive consistency checks on `head` and `tail` sub-types. ### 3.5. Strings & Binaries (Planned) @@ -331,45 +330,96 @@ defmodule Tdd do end end - defp check_assumptions_consistency(assumptions_map) do + defp check_assumptions_consistency(assumptions_map, ambient_constraints \\ %{}) do + # 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) # 1. Partition assumptions by the entity they apply to. - # :top_level for the main value, and {:elem, index} for tuple elements. partitioned_assumptions = Enum.group_by(assumptions_map, fn - # Variable for a tuple element's property. Example: {4, :element, 0, {0, :is_integer}} + # Tuple element property: {4, :element, 0, {0, :is_integer}} {{4, :element, index, _nested_var}, _value} -> {:elem, index} + # List head property: {5, :head, {0, :is_atom}} + {{5, :head, _nested_var}, _value} -> :head + # List tail property: {5, :tail, {5, :is_empty}} + {{5, :tail, _nested_var}, _value} -> :tail # All other variables _ -> :top_level end) - # 2. Extract and check the assumptions for the top-level entity. - top_level_assumptions = - Map.get(partitioned_assumptions, :top_level, []) - |> Map.new() + # 2. Check the assumptions for the top-level entity. + top_level_assumptions = Map.get(partitioned_assumptions, :top_level, []) |> Map.new() case do_check_flat_consistency(top_level_assumptions) do :contradiction -> :contradiction :consistent -> - # 3. If top-level is consistent, check each tuple element's assumptions. - element_partitions = Map.drop(partitioned_assumptions, [:top_level]) + # 4. If top-level is consistent, gather new ambient constraints and check sub-problems. + all_elems_constraints = + Enum.reduce(top_level_assumptions, [], fn + {{5, :all_elements, type_id}, true}, acc -> [type_id | acc] + _, acc -> acc + end) - Enum.reduce_while(element_partitions, :consistent, fn - # The key is {:elem, index}, the value is a list of {var, val} tuples + sub_problems = Map.drop(partitioned_assumptions, [:top_level]) + + Enum.reduce_while(sub_problems, :consistent, fn + # For a tuple element (no ambient constraints from parent needed for now) {{:elem, _index}, assumptions_list}, _acc -> - # Transform the list of assumptions into a "flat" map for the element, - # by extracting the nested predicate. sub_assumptions = assumptions_list - |> Map.new(fn {{_vcat, _ptype, _idx, nested_var}, value} -> {nested_var, value} end) + |> Map.new(fn {{_, :element, _, nested_var}, value} -> {nested_var, value} end) - # 4. Recursively call the main consistency checker on the sub-problem. - # This allows for arbitrarily nested tuple types. case check_assumptions_consistency(sub_assumptions) do :contradiction -> {:halt, :contradiction} :consistent -> {:cont, :consistent} end + + # For a list head + {:head, assumptions_list}, _acc -> + # The head must conform to every `all_elements` constraint on the list. + # We build a TDD for the intersection of all these constraints. + ambient_type_for_head = + Enum.reduce(all_elems_constraints, type_any(), &intersect/2) + + head_sub_assumptions = + assumptions_list + |> Map.new(fn {{_, :head, nested_var}, value} -> {nested_var, value} end) + + # Check if the explicitly assumed head type contradicts the ambient one. + head_type_from_assumptions = + simplify_with_constraints(@true_node_id, head_sub_assumptions) + + if is_subtype(head_type_from_assumptions, ambient_type_for_head) do + # Recursively check internal consistency of the head's own assumptions. + case check_assumptions_consistency(head_sub_assumptions) do + :contradiction -> {:halt, :contradiction} + :consistent -> {:cont, :consistent} + end + else + {:halt, :contradiction} + end + + # For a list tail + {:tail, assumptions_list}, _acc -> + # The tail must also be a list conforming to the same `all_elements` constraints. + # So we pass the parent's `all_elements` assumptions down as ambient constraints for the tail. + ambient_for_tail = + Enum.reduce(all_elems_constraints, %{}, fn type_id, acc -> + Map.put(acc, v_list_all_elements_are(type_id), true) + end) + + tail_sub_assumptions = + assumptions_list + |> Map.new(fn {{_, :tail, nested_var}, value} -> {nested_var, value} end) + + # Recursively check the tail's assumptions *with the ambient constraints*. + case check_assumptions_consistency(tail_sub_assumptions, ambient_for_tail) do + :contradiction -> {:halt, :contradiction} + :consistent -> {:cont, :consistent} + end end) end end @@ -384,195 +434,224 @@ defmodule Tdd do _otherwise, acc_set -> acc_set end) - raw_result = - if MapSet.size(primary_true_predicates) > 1 do + if MapSet.size(primary_true_predicates) > 1 do + :contradiction + else + # Perform checks for each type category... + # (Existing atom, tuple, integer checks are chained via `cond`) + # If no specific checks resulted in contradiction, it's consistent. + check_atom_logic(assumptions_map, primary_true_predicates) || + check_tuple_logic(assumptions_map, primary_true_predicates) || + check_integer_logic(assumptions_map, primary_true_predicates) || + check_list_logic(assumptions_map, primary_true_predicates) || + :consistent + end + end + + # Helper functions to break down the massive cond block + defp check_atom_logic(assumptions_map, primary_true_predicates) do + has_true_atom_specific_pred = + Enum.any?(assumptions_map, fn {var_id, truth_value} -> + elem(var_id, 0) == 1 && truth_value == true + end) + + is_explicitly_not_atom = + Map.get(assumptions_map, @v_is_atom) == false || + (MapSet.size(primary_true_predicates) == 1 && + !MapSet.member?(primary_true_predicates, :is_atom)) + + if has_true_atom_specific_pred && is_explicitly_not_atom do + :contradiction + else + atom_value_trues = + Enum.reduce(assumptions_map, MapSet.new(), fn + {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val) + _otherwise, acc_set -> acc_set + end) + + if MapSet.size(atom_value_trues) > 1, do: :contradiction, else: false + end + end + + defp check_tuple_logic(assumptions_map, primary_true_predicates) do + has_true_tuple_specific_pred = + Enum.any?(assumptions_map, fn {var_id, truth_value} -> + elem(var_id, 0) == 4 && truth_value == true + end) + + is_explicitly_not_tuple = + Map.get(assumptions_map, @v_is_tuple) == false || + (MapSet.size(primary_true_predicates) == 1 && + !MapSet.member?(primary_true_predicates, :is_tuple)) + + if has_true_tuple_specific_pred && is_explicitly_not_tuple do + :contradiction + else + tuple_size_trues = + Enum.reduce(assumptions_map, MapSet.new(), fn + {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val) + _otherwise, acc_set -> acc_set + end) + + if MapSet.size(tuple_size_trues) > 1, do: :contradiction, else: false + end + end + + # (The original integer checking logic is moved into this helper) +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 + end) + + is_explicitly_not_integer_or_different_primary = + Map.get(assumptions_map, @v_is_integer) == false || + (MapSet.size(primary_true_predicates) == 1 && + !MapSet.member?(primary_true_predicates, :is_integer)) + + should_check_integer_logic = + Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 2 end) || + MapSet.member?(primary_true_predicates, :is_integer) + + cond do + has_true_integer_specific_pred && + is_explicitly_not_integer_or_different_primary -> :contradiction - else - # --- Atom-specific checks --- - has_true_atom_specific_pred = - Enum.any?(assumptions_map, fn {var_id, truth_value} -> - elem(var_id, 0) == 1 && truth_value == true - end) - is_explicitly_not_atom_or_different_primary = - Map.get(assumptions_map, @v_is_atom) == false || - (MapSet.size(primary_true_predicates) == 1 && - !MapSet.member?(primary_true_predicates, :is_atom)) + should_check_integer_logic -> + initial_bounds_from_true_false = %{eq_val: nil, min_b: nil, max_b: nil} - cond do - has_true_atom_specific_pred && is_explicitly_not_atom_or_different_primary -> + bounds_acc = + Enum.reduce( + assumptions_map, + initial_bounds_from_true_false, + fn + {{2, :beq, n}, true}, acc -> + cond do + acc.eq_val == :conflict -> acc + is_nil(acc.eq_val) -> %{acc | eq_val: n} + acc.eq_val != n -> %{acc | eq_val: :conflict} + true -> acc + end + + # value < n => value <= n-1 + {{2, :alt, n}, true}, acc -> + new_max_b = + if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1) + + %{acc | max_b: new_max_b} + + # value > n => value >= n+1 + {{2, :cgt, n}, true}, acc -> + new_min_b = + if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1) + + %{acc | min_b: new_min_b} + + # value >= n + {{2, :alt, n}, false}, acc -> + new_min_b = if is_nil(acc.min_b), do: n, else: max(acc.min_b, n) + %{acc | min_b: new_min_b} + + # value <= n + {{2, :cgt, n}, false}, acc -> + new_max_b = if is_nil(acc.max_b), do: n, else: min(acc.max_b, n) + %{acc | max_b: new_max_b} + + # Ignore other preds for this pass + _otherwise, acc -> + acc + end + ) + + case calculate_final_interval_from_bounds(bounds_acc) do + {:contradiction, _, _} -> :contradiction - true -> - atom_value_trues = - Enum.reduce(assumptions_map, MapSet.new(), fn - {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val) - _otherwise, acc_set -> acc_set + {:consistent, current_interval_min, current_interval_max} -> + # Interval from true/false preds is consistent. Now check for other implied contradictions. + # This logic was missing from my simplified version and is critical. + res = + Enum.reduce_while(assumptions_map, :consistent, fn + {{2, pred_type, n_val}, :dc}, _acc_status -> + is_implied_true = + case pred_type 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_max) && current_interval_max < n_val + :cgt -> + is_integer(current_interval_min) && current_interval_min > n_val + _ -> + false + end + + is_implied_false = + case pred_type 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 + + if is_implied_true || is_implied_false do + {:halt, :contradiction} + else + {:cont, :consistent} + end + + _other_assumption, acc_status -> + {:cont, acc_status} end) - if MapSet.size(atom_value_trues) > 1 do - :contradiction - else - # --- Tuple-specific checks --- - has_true_tuple_specific_pred = - Enum.any?(assumptions_map, fn {var_id, truth_value} -> - elem(var_id, 0) == 4 && truth_value == true - end) - - is_explicitly_not_tuple_or_different_primary = - Map.get(assumptions_map, @v_is_tuple) == false || - (MapSet.size(primary_true_predicates) == 1 && - !MapSet.member?(primary_true_predicates, :is_tuple)) - - cond do - has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary -> - :contradiction - - true -> - tuple_size_trues = - Enum.reduce(assumptions_map, MapSet.new(), fn - {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val) - _otherwise, acc_set -> acc_set - end) - - if MapSet.size(tuple_size_trues) > 1 do - :contradiction - else - # --- Integer predicate checks (REVISED LOGIC) --- - has_true_integer_specific_pred = - Enum.any?(assumptions_map, fn {var_id, truth_value} -> - elem(var_id, 0) == 2 && truth_value == true - end) - - is_explicitly_not_integer_or_different_primary = - Map.get(assumptions_map, @v_is_integer) == false || - (MapSet.size(primary_true_predicates) == 1 && - !MapSet.member?(primary_true_predicates, :is_integer)) - - should_check_integer_logic = - Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 2 end) || - MapSet.member?(primary_true_predicates, :is_integer) - - cond do - has_true_integer_specific_pred && - is_explicitly_not_integer_or_different_primary -> - :contradiction - - should_check_integer_logic -> - initial_bounds_from_true_false = %{eq_val: nil, min_b: nil, max_b: nil} - - bounds_acc = - Enum.reduce( - assumptions_map, - initial_bounds_from_true_false, - fn - {{2, :beq, n}, true}, acc -> - cond do - acc.eq_val == :conflict -> acc - is_nil(acc.eq_val) -> %{acc | eq_val: n} - acc.eq_val != n -> %{acc | eq_val: :conflict} - true -> acc - end - - # value < n => value <= n-1 - {{2, :alt, n}, true}, acc -> - new_max_b = - if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1) - - %{acc | max_b: new_max_b} - - # value > n => value >= n+1 - {{2, :cgt, n}, true}, acc -> - new_min_b = - if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1) - - %{acc | min_b: new_min_b} - - # value >= n - {{2, :alt, n}, false}, acc -> - new_min_b = if is_nil(acc.min_b), do: n, else: max(acc.min_b, n) - %{acc | min_b: new_min_b} - - # value <= n - {{2, :cgt, n}, false}, acc -> - new_max_b = if is_nil(acc.max_b), do: n, else: min(acc.max_b, n) - %{acc | max_b: new_max_b} - - # Ignore non-integer or :dc preds for this pass - _otherwise, acc -> - acc - end - ) - - case calculate_final_interval_from_bounds(bounds_acc) do - {:contradiction, _, _} -> - :contradiction - - {:consistent, current_interval_min, current_interval_max} -> - # Interval from true/false preds is consistent. Now check :dc preds against it. - Enum.reduce_while(assumptions_map, :consistent, fn - {{2, pred_type, n_val}, :dc}, _acc_status -> - is_implied_true = - case pred_type 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_max) && - current_interval_max < n_val - - :cgt -> - is_integer(current_interval_min) && - current_interval_min > n_val - - _ -> - false - end - - is_implied_false = - case pred_type 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 - - if is_implied_true || is_implied_false do - {:halt, :contradiction} - else - {:cont, :consistent} - end - - _other_assumption, acc_status -> - {:cont, acc_status} - end) - end - - true -> - :consistent - end - end - end - end + # Return :contradiction if found, otherwise `false` to allow the `||` chain to continue. + if res == :contradiction, do: :contradiction, else: false end - end - raw_result + true -> + false + end + end + + ### NEW ### + # Logic for list consistency checks + defp check_list_logic(assumptions_map, primary_true_predicates) do + # A predicate like {5, :is_empty} or {5, :head, ...} exists + has_list_specific_pred = + Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 5 end) + + is_explicitly_not_list = + Map.get(assumptions_map, v_is_list()) == false || + (MapSet.size(primary_true_predicates) == 1 && + !MapSet.member?(primary_true_predicates, :is_list)) + + # 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) + + cond do + # Contradiction: list-specific rule is assumed, but type is not a list. + has_list_specific_pred && is_explicitly_not_list -> + :contradiction + + # Contradiction: assumed to be an empty list, but also has assumptions about head/tail. + Map.get(assumptions_map, v_list_is_empty()) == true && has_head_or_tail_pred -> + :contradiction + + # No flat contradictions found for lists. Recursive checks are done in the main function. + true -> + false + end end # Helper for min, treating nil as infinity @@ -711,15 +790,24 @@ defmodule Tdd do @v_is_atom {0, :is_atom} @v_is_tuple {0, :is_tuple} @v_is_integer {0, :is_integer} + @v_is_list {0, :is_list} def v_is_atom, do: @v_is_atom def v_is_tuple, do: @v_is_tuple def v_is_integer, do: @v_is_integer + ### NEW ### + def v_is_list, do: @v_is_list 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} + # List Predicates (Category 5) + def v_list_is_empty, do: {5, :is_empty} + def v_list_head_pred(nested_var), do: {5, :head, nested_var} + def v_list_tail_pred(nested_var), do: {5, :tail, nested_var} + def v_list_all_elements_are(element_type_id), do: {5, :all_elements, element_type_id} + # Integer Predicates (Category 2) # strictly less than n def v_int_lt(n) when is_integer(n), do: {2, :alt, n} @@ -763,70 +851,95 @@ defmodule Tdd do make_node_for_constructors(@v_is_integer, @true_node_id, @false_node_id, @false_node_id) end - def type_tuple_elem(element_index, element_type_id, success_path_id) do - node_details = get_node_details(element_type_id) - - case node_details do + # A recursive helper that maps a TDD onto a component (e.g., list head, tuple element). + # It takes a tdd_id, a `wrapper_fun` (like `&v_list_head_pred/1`), and the ID to jump to on success. + defp map_tdd_to_component(tdd_id, wrapper_fun, success_id) do + case get_node_details(tdd_id) do :true_terminal -> - # Should be caught by guard Tdd.type_any(), but handle defensively - success_path_id + success_id :false_terminal -> - # Should be caught by guard Tdd.type_none(), but handle defensively - type_none() + @false_node_id - {original_var, y_id, n_id, d_id} -> - # Adapt original_var to be specific to this element_index - # The Tdd.v_tuple_elem_pred function creates the correctly prefixed variable - element_specific_var = v_tuple_elem_pred(element_index, original_var) - - yes_branch_tdd = type_tuple_elem(element_index, y_id, success_path_id) - no_branch_tdd = type_tuple_elem(element_index, n_id, success_path_id) - dc_branch_tdd = type_tuple_elem(element_index, d_id, success_path_id) - make_node(element_specific_var, yes_branch_tdd, no_branch_tdd, dc_branch_tdd) + {var, y, n, d} -> + # Wrap the original variable to be specific to this component. + component_var = wrapper_fun.(var) + # Recurse on children, passing the success_id down. + res_y = map_tdd_to_component(y, wrapper_fun, success_id) + res_n = map_tdd_to_component(n, wrapper_fun, success_id) + res_d = map_tdd_to_component(d, wrapper_fun, success_id) + make_node_raw(component_var, res_y, res_n, res_d) end end - # TDD for a tuple with specific element types + def type_tuple_elem(element_index, element_type_id, success_path_id) do + map_tdd_to_component(element_type_id, &v_tuple_elem_pred(element_index, &1), success_path_id) + end + def type_tuple(element_type_ids) do num_elements = length(element_type_ids) - # Build TDD for element checks from last to first - # The 'success_path_id' for the last element's check is Tdd.type_any() (representing TRUE) final_elements_check_tdd = - Enum.reduce(Enum.reverse(0..(num_elements - 1)), Tdd.type_any(), fn i, acc_tdd -> + Enum.reduce(Enum.reverse(0..(num_elements - 1)), type_any(), fn i, acc_tdd -> element_type_id = Enum.at(element_type_ids, i) type_tuple_elem(i, element_type_id, acc_tdd) end) - # Wrap with size check size_check_node = - make_node( - v_tuple_size_eq(num_elements), - # If size matches, proceed to element checks - final_elements_check_tdd, - # If size mismatches, it's not this tuple type - type_none(), - # DC for size usually means not this specific tuple type - type_none() - ) + make_node(v_tuple_size_eq(num_elements), final_elements_check_tdd, type_none(), type_none()) - # Wrap with primary tuple type check - raw_final_tdd = - make_node( - v_is_tuple(), - # If is_tuple, proceed to size check - size_check_node, - # If not a tuple, then false - type_none(), - # DC for is_tuple usually means not this specific type - type_none() - ) - - # Simplify the constructed TDD + raw_final_tdd = make_node(v_is_tuple(), size_check_node, type_none(), type_none()) simplify_with_constraints(raw_final_tdd, %{}) end + # List Type Constructors + def type_list, + do: make_node_for_constructors(v_is_list(), @true_node_id, @false_node_id, @false_node_id) + + def type_empty_list, + do: + make_node_for_constructors( + v_is_list(), + make_node_raw(v_list_is_empty(), @true_node_id, @false_node_id, @false_node_id), + @false_node_id, + @false_node_id + ) + + def type_cons(head_type_id, tail_type_id) do + # 1. Build the TDD for the tail constraint. + # On success, this will proceed to the head constraint check. + tail_check_tdd = map_tdd_to_component(tail_type_id, &v_list_tail_pred/1, @true_node_id) + + # 2. Build the TDD for the head constraint. + # On success, it proceeds to the TDD we just built for the tail. + head_and_tail_check_tdd = + map_tdd_to_component(head_type_id, &v_list_head_pred/1, tail_check_tdd) + + # 3. A cons cell is never empty. + # If is_empty is true, it's a failure. If false, proceed to head/tail checks. + is_empty_check_node = + make_node(v_list_is_empty(), @false_node_id, head_and_tail_check_tdd, @false_node_id) + + # 4. Wrap in the primary list type check. + raw_final_tdd = make_node(v_is_list(), is_empty_check_node, @false_node_id, @false_node_id) + + # 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, %{}) + 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) @@ -1431,7 +1544,8 @@ defmodule TupleTests do t_int_pos = type_int_gt(0) t_any = type_any() t_none = type_none() - t_tuple = type_tuple() # any tuple + # any tuple + t_tuple = type_tuple() t_empty_tuple = type_empty_tuple() # --- Specific Tuple Types --- @@ -1495,23 +1609,48 @@ defmodule TupleTests do # {:foo, 5} | {pos_int, atom} union1 = sum(tup_foo_5, tup_pos_atom) test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1)) - test_fn.("{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_pos_atom, union1)) - test_fn.("{atom, int} <: ({:foo, 5} | {pos_int, atom})", false, is_subtype(tup_atom_int, union1)) + + test_fn.( + "{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})", + true, + is_subtype(tup_pos_atom, union1) + ) + + test_fn.( + "{atom, int} <: ({:foo, 5} | {pos_int, atom})", + false, + is_subtype(tup_atom_int, union1) + ) # {atom, any} | {any, int} -> a complex type, let's check subtyping against it union2 = sum(tup_atom_any, tup_any_int) # {atom, int} is in both parts of the union. test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2)) # {:foo, :bar} is only in {atom, any}. - test_fn.("{:foo, :bar} <: ({atom,any} | {any,int})", true, is_subtype(type_tuple([t_foo, t_bar]), union2)) + test_fn.( + "{:foo, :bar} <: ({atom,any} | {any,int})", + true, + is_subtype(type_tuple([t_foo, t_bar]), union2) + ) + # {5, 6} is only in {any, int}. - test_fn.("{5, 6} <: ({atom,any} | {any,int})", true, is_subtype(type_tuple([t_int_5, t_int_6]), union2)) + test_fn.( + "{5, 6} <: ({atom,any} | {any,int})", + true, + is_subtype(type_tuple([t_int_5, t_int_6]), union2) + ) + # {5, :foo} is in neither part of the union. - test_fn.("{5, :foo} <: ({atom,any} | {any,int})", false, is_subtype(type_tuple([t_int_5, t_foo]), union2)) + test_fn.( + "{5, :foo} <: ({atom,any} | {any,int})", + false, + is_subtype(type_tuple([t_int_5, t_foo]), union2) + ) IO.puts("\n--- Section: Negation and Type Difference ---") # atom is disjoint from tuple, so atom <: ¬tuple test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple))) + # A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple))) # {int, atom} is a subtype of ¬{atom, int} because their elements differ @@ -1521,10 +1660,16 @@ defmodule TupleTests do # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples. diff1 = intersect(tup_s2_any, negate(tup_atom_any)) + # {integer, integer} has a first element that is not an atom, so it should be in the difference. tup_int_int = type_tuple([t_int, t_int]) test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1)) - test_fn.("{atom, int} <: (tuple_size_2 - {atom, any})", false, is_subtype(tup_atom_int, diff1)) + + test_fn.( + "{atom, int} <: (tuple_size_2 - {atom, any})", + false, + is_subtype(tup_atom_int, diff1) + ) IO.puts("\n--- Section: Nested Tuples ---") test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom)) @@ -1535,8 +1680,18 @@ defmodule TupleTests do # Union of nested types union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])])) test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested)) - test_fn.("{{:bar}} <: ({{:foo}} | {{:bar}})", true, is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)) - test_fn.("{{atom}} <: ({{:foo}} | {{:bar}})", false, is_subtype(tup_nested_atom, union_nested)) + + test_fn.( + "{{:bar}} <: ({{:foo}} | {{:bar}})", + true, + is_subtype(type_tuple([type_tuple([t_bar])]), union_nested) + ) + + test_fn.( + "{{atom}} <: ({{:foo}} | {{:bar}})", + false, + is_subtype(tup_nested_atom, union_nested) + ) IO.puts("\n--- Section: Edge Cases (any, none) ---") # A type `{any, none}` should not be possible. The value `none` cannot exist. @@ -1553,6 +1708,7 @@ defmodule TupleTests do # --- Original tests from problem description for regression --- IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---") + test_fn.( "{1, :foo} <: {int_gt_0, :foo | :bar}", true, @@ -1561,6 +1717,7 @@ defmodule TupleTests do type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))]) ) ) + test_fn.( "{0, :foo} <: {int_gt_0, :foo | :bar}", false, @@ -1569,6 +1726,7 @@ defmodule TupleTests do type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))]) ) ) + test_fn.( "{1, :kek} <: {int_gt_0, :foo | :bar}", false, @@ -1585,6 +1743,178 @@ defmodule TupleTests do end end +defmodule ListTests do + import Tdd + + def run(test_fn) do + Process.put(:test_failures, []) + Tdd.init_tdd_system() + IO.puts("\n--- Running ListTests ---") + + # --- Basic Types --- + t_atom = type_atom() + t_int = type_integer() + t_foo = type_atom_literal(:foo) + t_bar = type_atom_literal(:bar) + t_any = type_any() + t_none = type_none() + + # --- List Types --- + t_list = type_list() + t_empty_list = type_empty_list() + # [atom | list] + t_cons_atom_list = type_cons(t_atom, t_list) + # [:foo | []] + t_cons_foo_empty = type_cons(t_foo, t_empty_list) + # [atom | []] + t_cons_atom_empty = type_cons(t_atom, t_empty_list) + # [any | []] + t_cons_any_empty = type_cons(t_any, t_empty_list) + # [integer | list] + t_cons_int_list = type_cons(t_int, t_list) + + IO.puts("\n--- Section: Basic List Subtyping ---") + test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list)) + test_fn.("list <: []", false, is_subtype(t_list, t_empty_list)) + test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list)) + test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list)) + test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list)) + test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list)) + test_fn.("list <: atom", false, is_subtype(t_list, t_atom)) + test_fn.("atom <: list", false, is_subtype(t_atom, t_list)) + + IO.puts("\n--- Section: Cons Subtyping (Covariance) ---") + # Head is a subtype + test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty)) + test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty)) + # Tail is a subtype + test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list)) + test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty)) + # Both are subtypes + test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list)) + # Neither is a subtype + test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty)) + # A list of length 1 is a subtype of a list of any element of length 1 + test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty)) + + IO.puts("\n--- Section: List Intersection ---") + # [atom|list] & [integer|list] -> should be none due to head conflict + intersect1 = intersect(t_cons_atom_list, t_cons_int_list) + test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none) + + # [any|[]] & [atom|list] -> should be [atom|[]] + intersect2 = intersect(t_cons_any_empty, t_cons_atom_list) + test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty) + + # [] & [atom|list] -> should be none because one is empty and one is not + intersect3 = intersect(t_empty_list, t_cons_atom_list) + test_fn.("[] & [atom|list] == none", true, intersect3 == t_none) + + IO.puts("\n--- Section: List Union ---") + # [] | [atom|[]] + union1 = sum(t_empty_list, t_cons_atom_empty) + test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1)) + test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1)) + + test_fn.( + "[integer|[]] <: ([] | [atom|[]])", + false, + is_subtype(type_cons(t_int, t_empty_list), union1) + ) + + # [:foo|[]] | [:bar|[]] + union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list)) + # This union is a subtype of [atom|[]] + test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty)) + test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2)) + + IO.puts("\n--- Section: List Negation ---") + # list is a subtype of not(atom) + test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom))) + # A non-empty list is a subtype of not an empty list + test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list))) + # [integer|list] is a subtype of not [atom|list] + test_fn.( + "[integer|list] <: ¬[atom|list]", + true, + is_subtype(t_cons_int_list, negate(t_cons_atom_list)) + ) + + IO.inspect(Process.get(:test_failures, []), label: "ListTests failures") + end +end +defmodule ListOfTests do + import Tdd + + def run(test_fn) do + Process.put(:test_failures, []) + Tdd.init_tdd_system() + IO.puts("\n--- Running ListOfTests ---") + + # --- Basic Types --- + t_atom = type_atom() + t_int = type_integer() + t_pos_int = type_int_gt(0) + t_int_5 = type_int_eq(5) + + # --- 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() + 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] + + IO.puts("\n--- Section: Basic list(X) Subtyping ---") + test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list)) + test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int)) + test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int)) + 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()))) + + 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)) + + 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) + + # 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. + intersect2 = intersect(t_list_of_int, t_list_of_atom) + test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2)) + test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2)) + test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2)) + # 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) + test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none()) + + # 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()) + + IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures") + end +end test_all.() IntegerTests.run(test) TupleTests.run(test) +ListTests.run(test) +ListOfTests.run(test)