diff --git a/.aider.chat.history.md b/.aider.chat.history.md index f48d73a..02fb589 100644 --- a/.aider.chat.history.md +++ b/.aider.chat.history.md @@ -57232,3 +57232,209 @@ This approach leverages the excellent foundation you've already built in the `ti > Model: openrouter/google/gemini-2.5-pro-preview with context edit format > Git repo: .git with 62 files > Repo-map: using 8192 tokens, always refresh +> +> +> ^C again to exit +> Unable to list files in git repo: BadObject: b'df8d705509adca9e964524519a1755d8a584e262' +> Is your git repo corrupted? +> +> +> ^C KeyboardInterrupt + +# aider chat started at 2025-06-16 11:51:46 + +> You can skip this check with --no-gitignore +> Add .aider* to .gitignore (recommended)? (Y)es/(N)o [Yes]: n +> /Users/kacper.marzecki@schibsted.com/.local/bin/aider --model gemini --watch-files --read Conventions.md --thinking-tokens 10k --reasoning-effort high +> Warning: gemini/gemini-2.5-pro-preview-05-06 does not support 'reasoning_effort', ignoring. +> Use --no-check-model-accepts-settings to force the 'reasoning_effort' setting. +> Warning: gemini/gemini-2.5-pro-preview-05-06 does not support 'thinking_tokens', ignoring. +> Use --no-check-model-accepts-settings to force the 'thinking_tokens' setting. +> Aider v0.84.0 +> Main model: gemini/gemini-2.5-pro-preview-05-06 with diff-fenced edit format +> Weak model: gemini/gemini-2.5-flash-preview-04-17 +> Git repo: .git with 65 files +> Repo-map: using 4096 tokens, auto refresh +> Added Conventions.md to the chat (read-only). +> Added test.exs to the chat +> Processing your request... + +Okay, I will add the test case as requested. This involves defining a couple of helper functions to construct TDDs for tuples with specific element types, as this functionality doesn't appear to be available as a built-in constructor. These helpers will use existing TDD primitives. + +Here's the plan: +1. Define two helper functions: + * `build_tuple_element_tdd_h(element_index, element_type_id, success_path_id)`: Recursively builds the TDD part for a single element by adapting the element's type TDD variables to be specific to that element's index. + * `create_specific_tuple_type_h(element_type_ids)`: Uses `build_tuple_element_tdd_h` to construct the full TDD for a tuple with a list of specified element types. +2. Use these helpers to create the TDDs for `{1, :foo}` and `{int_gt_0, :foo | :bar}`. +3. Add the subtyping test using the existing `test` function. +4. This new code will replace the `#AI! ...` comment at the end of the file. + +Here are the *SEARCH/REPLACE* blocks: + +```elixir +test.exs +<<<<<<< SEARCH +|> Tdd.print_tdd(asd) + + +#AI! lets add a test case for {1, :foo} <: {int_gt_0, :foo | :bar} +======= +|> Tdd.print_tdd(asd) + +# Helper function to recursively build TDD for an element's type, +# adapting its variables to be specific to the element's index. +defmodule TupleTestHelpers do + def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module) + when element_type_id == Tdd.type_any() do + # If element type is 'any', this part of the check passes, go to success_path_id + success_path_id + end + + def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module) + when element_type_id == Tdd.type_none() do + # If element type is 'none', this path fails + Tdd.type_none() + end + + def build_tuple_element_tdd_h(element_index, element_type_id, success_path_id, variable_prefix_module) do + node_details = Tdd.get_node_details(element_type_id) + + case node_details do + :true_terminal -> + # Should be caught by guard Tdd.type_any(), but handle defensively + success_path_id + + :false_terminal -> + # Should be caught by guard Tdd.type_none(), but handle defensively + Tdd.type_none() + + {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 = variable_prefix_module.v_tuple_elem_pred(element_index, original_var) + + yes_branch_tdd = + build_tuple_element_tdd_h(element_index, y_id, success_path_id, variable_prefix_module) + + no_branch_tdd = + build_tuple_element_tdd_h(element_index, n_id, success_path_id, variable_prefix_module) + + dc_branch_tdd = + build_tuple_element_tdd_h(element_index, d_id, success_path_id, variable_prefix_module) + + Tdd.make_node_raw(element_specific_var, yes_branch_tdd, no_branch_tdd, dc_branch_tdd) + end + end + + # Helper function to create a TDD for a tuple with specific element types + def create_specific_tuple_type_h(element_type_ids, variable_prefix_module \\ Tdd) 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 -> + element_type_id = Enum.at(element_type_ids, i) + build_tuple_element_tdd_h(i, element_type_id, acc_tdd, variable_prefix_module) + end) + + # Wrap with size check + size_check_node = + Tdd.make_node_raw( + variable_prefix_module.v_tuple_size_eq(num_elements), + final_elements_check_tdd, # If size matches, proceed to element checks + Tdd.type_none(), # If size mismatches, it's not this tuple type + Tdd.type_none() # DC for size usually means not this specific tuple type + ) + + # Wrap with primary tuple type check + raw_final_tdd = + Tdd.make_node_raw( + variable_prefix_module.@v_is_tuple, + size_check_node, # If is_tuple, proceed to size check + Tdd.type_none(), # If not a tuple, then false + Tdd.type_none() # DC for is_tuple usually means not this specific type + ) + + # Simplify the constructed TDD + Tdd.simplify_with_constraints(raw_final_tdd, %{}) + end +end + +IO.puts("\n--- Specific Tuple Subtyping Test ---") + +# Type for {1, :foo} +el1_type1 = Tdd.type_int_eq(1) +el2_type1 = Tdd.type_atom_literal(:foo) +tdd_tuple_1_foo = TupleTestHelpers.create_specific_tuple_type_h([el1_type1, el2_type1]) + +# Type for {int_gt_0, :foo | :bar} +el1_type2 = Tdd.type_int_gt(0) +el2_type2_foo = Tdd.type_atom_literal(:foo) +el2_type2_bar = Tdd.type_atom_literal(:bar) +el2_type2 = Tdd.sum(el2_type2_foo, el2_type2_bar) +tdd_tuple_int_gt0_foo_or_bar = TupleTestHelpers.create_specific_tuple_type_h([el1_type2, el2_type2]) + +# IO.puts("TDD for {1, :foo}:") +# Tdd.print_tdd(tdd_tuple_1_foo) +# IO.puts("TDD for {int_gt_0, :foo | :bar}:") +# Tdd.print_tdd(tdd_tuple_int_gt0_foo_or_bar) + +test.( + "{1, :foo} <: {int_gt_0, :foo | :bar}", + true, + Tdd.is_subtype(tdd_tuple_1_foo, tdd_tuple_int_gt0_foo_or_bar) +) + +IO.inspect(Process.get(:test_failures, []), label: "Current test failures after tuple test") +>>>>>>> REPLACE +``` + +> Tokens: 23k sent, 1.4k received. Cost: $0.04 message, $0.04 session. +> Applied edit to test.exs +> Processing your request... + +Okay, I understand. The issue is that Elixir guards have restrictions on what functions can be called within them. Calls to `Tdd.type_any()` and `Tdd.type_none()` are considered "remote" calls in this context, even if they return simple values. + +To fix this, I will replace the calls to `Tdd.type_any()` and `Tdd.type_none()` in the guard clauses with their literal return values. +- `Tdd.type_any()` returns `@true_node_id` which is `1`. +- `Tdd.type_none()` returns `@false_node_id` which is `0`. + +I will make these changes and remove the "AI!" comment. + +Here is the *SEARCH/REPLACE block*: + +```elixir +test.exs +<<<<<<< SEARCH +defmodule TupleTestHelpers do + def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module) + # AI! You cannot use remote functions inside function guards + when element_type_id == Tdd.type_any() do + # If element type is 'any', this part of the check passes, go to success_path_id + success_path_id + end + + def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module) + when element_type_id == Tdd.type_none() do + # If element type is 'none', this path fails + Tdd.type_none() + end +======= +defmodule TupleTestHelpers do + def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module) + when element_type_id == 1 do # Was Tdd.type_any() + # If element type is 'any', this part of the check passes, go to success_path_id + success_path_id + end + + def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module) + when element_type_id == 0 do # Was Tdd.type_none() + # If element type is 'none', this path fails + Tdd.type_none() + end +>>>>>>> REPLACE +``` + +> Tokens: 25k sent, 457 received. Cost: $0.04 message, $0.08 session. +> Applied edit to test.exs diff --git a/.aider.input.history b/.aider.input.history index fef2f90..cf76248 100644 --- a/.aider.input.history +++ b/.aider.input.history @@ -4182,3 +4182,6 @@ # 2025-06-15 11:56:09.668461 +/context + +# 2025-06-16 11:51:48.065221 ++n diff --git a/test.exs b/test.exs index 605ab5e..04170af 100644 --- a/test.exs +++ b/test.exs @@ -332,6 +332,51 @@ defmodule Tdd do end defp check_assumptions_consistency(assumptions_map) do + # 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}} + {{4, :element, index, _nested_var}, _value} -> {:elem, index} + # 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() + + 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]) + + Enum.reduce_while(element_partitions, :consistent, fn + # The key is {:elem, index}, the value is a list of {var, val} tuples + {{: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) + + # 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 + end) + end + end + + # The original check_assumptions_consistency function is renamed to this. + # It performs the actual logic for a "flat" set of assumptions about a single entity. + defp do_check_flat_consistency(assumptions_map) do # Check 1: Primary type mutual exclusivity primary_true_predicates = Enum.reduce(assumptions_map, MapSet.new(), fn @@ -508,40 +553,23 @@ defmodule Tdd do end if is_implied_true || is_implied_false do - # IO.inspect({assumptions_map, pred_type, n_val, current_interval_min, current_interval_max, implied_true, implied_false}, label: "CAC Int DC Contradiction") - # :dc assumption contradicted by derived interval {:halt, :contradiction} else {:cont, :consistent} end _other_assumption, acc_status -> - # Continue with current status {:cont, acc_status} end) - - # End reduce_while for :dc checks end - # End case for calculate_final_interval - # No integer specific preds or not relevant to check integer logic true -> :consistent end - - # End cond for integer checks end - - # End else for tuple_size_trues end - - # End true for tuple_specific_pred end - - # End cond for tuple_specific_pred end - - # End else for atom_value_trues end raw_result @@ -556,9 +584,9 @@ defmodule Tdd do 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 + def simplify_with_constraints(tdd_id, assumptions_map) do state = get_state() # Sort assumptions for cache key consistency sorted_assumptions_list = Enum.sort(Map.to_list(assumptions_map)) @@ -682,9 +710,12 @@ 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_is_atom, do: @v_is_atom + def v_is_tuple, do: @v_is_tuple + def v_is_integer, do: @v_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} @@ -732,6 +763,70 @@ 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 + :true_terminal -> + # Should be caught by guard Tdd.type_any(), but handle defensively + success_path_id + + :false_terminal -> + # Should be caught by guard Tdd.type_none(), but handle defensively + type_none() + + {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) + end + end + + # TDD for a tuple with specific element types + 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 -> + 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() + ) + + # 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 + simplify_with_constraints(raw_final_tdd, %{}) + 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) @@ -1313,18 +1408,183 @@ defmodule IntegerTests do Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges) ) - Tdd.print_tdd(union_disjoint_ranges) IO.inspect(Process.get(:test_failures, [])) end end -# test_all.() -# IntegerTests.run(test) +defmodule TupleTests do + import Tdd -tdd_int_gt_10 = Tdd.type_int_gt(10) -tdd_int_gt_3 = Tdd.type_int_gt(3) + def run(test_fn) do + Process.put(:test_failures, []) + # Re-init the system for a clean slate for these tests + Tdd.init_tdd_system() + IO.puts("\n--- Running TupleTests ---") -tdd_int = Tdd.type_integer() -Tdd.intersect(Tdd.sum(tdd_int_gt_10, tdd_int_gt_3), tdd_int) -|> Tdd.print_tdd(asd) + # --- Basic Types for convenience --- + t_atom = type_atom() + t_int = type_integer() + t_foo = type_atom_literal(:foo) + t_bar = type_atom_literal(:bar) + t_int_5 = type_int_eq(5) + t_int_6 = type_int_eq(6) + t_int_pos = type_int_gt(0) + t_any = type_any() + t_none = type_none() + t_tuple = type_tuple() # any tuple + t_empty_tuple = type_empty_tuple() + # --- Specific Tuple Types --- + # {atom(), integer()} + tup_atom_int = type_tuple([t_atom, t_int]) + # {:foo, 5} + tup_foo_5 = type_tuple([t_foo, t_int_5]) + # {pos_integer(), atom()} + tup_pos_atom = type_tuple([t_int_pos, t_atom]) + # {atom(), any} + tup_atom_any = type_tuple([t_atom, t_any]) + # {any, integer()} + tup_any_int = type_tuple([t_any, t_int]) + # a tuple of size 2, {any, any} + tup_s2_any = type_tuple_sized_any(2) + # a tuple of size 3, {any, any, any} + tup_s3_any = type_tuple_sized_any(3) + # {integer(), atom()} + tup_int_atom = type_tuple([t_int, t_atom]) + # {{:foo}} + tup_nested_foo = type_tuple([type_tuple([t_foo])]) + # {{atom()}} + tup_nested_atom = type_tuple([type_tuple([t_atom])]) + # {any, none} -> this should resolve to none + tup_with_none = type_tuple([t_any, t_none]) + + IO.puts("\n--- Section: Basic Subtyping ---") + test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int)) + test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5)) + test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom)) + test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int)) + test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple)) + test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int)) + + IO.puts("\n--- Section: Size-related Subtyping ---") + test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any)) + test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int)) + test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any)) + test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any)) + test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple)) + test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any)) + + IO.puts("\n--- Section: Intersection ---") + # {atom, any} & {any, int} -> {atom, int} + intersect1 = intersect(tup_atom_any, tup_any_int) + test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int) + + # {atom, int} & {int, atom} -> none + intersect2 = intersect(tup_atom_int, tup_int_atom) + test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none) + + # tuple_size_2 & tuple_size_3 -> none + intersect3 = intersect(tup_s2_any, tup_s3_any) + test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none) + + # tuple() & {atom, int} -> {atom, int} + intersect4 = intersect(t_tuple, tup_atom_int) + test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int) + + IO.puts("\n--- Section: Union ---") + # {: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)) + + # {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)) + # {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)) + # {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)) + + 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 + test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int))) + # tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ + test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any))) + + # 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)) + + IO.puts("\n--- Section: Nested Tuples ---") + test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom)) + test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo)) + # Intersection of disjoint nested types: {{:foo}} & {{:bar}} + intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])])) + test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none) + # 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)) + + IO.puts("\n--- Section: Edge Cases (any, none) ---") + # A type `{any, none}` should not be possible. The value `none` cannot exist. + # The simplification logic should reduce this to `type_none`. + test_fn.("{any, none} == none", true, tup_with_none == t_none) + + # Intersection with a tuple containing none should result in none + intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none) + test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none) + + # Union with a tuple containing none should be a no-op + union_with_none_tuple = sum(tup_atom_int, tup_with_none) + test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int) + + # --- 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, + is_subtype( + type_tuple([type_int_eq(1), type_atom_literal(:foo)]), + 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, + is_subtype( + type_tuple([type_int_eq(0), type_atom_literal(:foo)]), + 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, + is_subtype( + type_tuple([ + type_int_eq(1), + type_atom_literal(:kek) + ]), + type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))]) + ) + ) + + IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures") + end +end + +test_all.() +IntegerTests.run(test) +TupleTests.run(test)