diff --git a/test1.exs b/test1.exs new file mode 100644 index 0000000..6b5c2b7 --- /dev/null +++ b/test1.exs @@ -0,0 +1,2208 @@ +doc = """ +# Ternary Decision Diagram (TDD) for Set-Theoretic Types in Elixir + +## 1. Introduction + +This document outlines the design and implementation of a Ternary Decision Diagram (TDD) based system for representing and manipulating set-theoretic types, inspired by systems like CDuce. The goal is to create a robust way to perform type checking, type inference, and other type-level computations for a rich set of datatypes, similar to those found in Elixir. + +A TDD is a directed acyclic graph (DAG) used to represent a function `f(v1, v2, ..., vn) -> {true, false, dont_care}`. In our context, it represents a characteristic function for a type: given a value, the TDD determines if the value belongs to the type (`true`), does not belong (`false`), or if the specific predicates tested so far are insufficient or irrelevant for this particular type operation (`dont_care`). + +The TDDs are kept **ordered** and **reduced** to ensure a canonical representation for each type, making type equivalence checks (and other operations) efficient. +- **Ordered**: Variables (predicates) appear in the same fixed global order on all paths from the root to a terminal. +- **Reduced**: Isomorphic subgraphs are merged (shared), and nodes whose children would make the test redundant under certain TDD algebra rules are eliminated or simplified. + +## 2. Core TDD Structure and Operations + +### 2.1. Nodes + +There are two kinds of nodes: + +1. **Terminal Nodes**: + * `TRUE_TERMINAL` (ID: `1`): Represents the universal set (type `any`). A path ending here means the value (or part of it) satisfies the type constraints along that path. + * `FALSE_TERMINAL` (ID: `0`): Represents the empty set (type `none`). A path ending here means the value fails the type constraints. + +2. **Variable Nodes**: + * Represented as a tuple: `{variable_identifier, yes_child_id, no_child_id, dc_child_id}`. + * `variable_identifier`: A unique, globally ordered term identifying the predicate being tested at this node (e.g., "is the value an atom?", "is the integer value < 10?"). + * `yes_child_id`: The ID of the next TDD node if the predicate is true. + * `no_child_id`: The ID of the next TDD node if the predicate is false. + * `dc_child_id` (Don't Care): The ID of the next TDD node if the predicate is irrelevant for the current type or operation. The semantic interpretation of `dc` is crucial and aligns with common TDD usage (e.g., for a union operation, `dc(A | B) = dc(A) | dc(B)`). + +### 2.2. Node Management (`Tdd` module state) + +The `Tdd` module maintains global state (currently via `Process.put/get` for simplicity, ideally a `GenServer`): + +* `@nodes`: A map from `node_tuple ({variable, yes_id, no_id, dc_id})` to `node_id`. This ensures that structurally identical nodes are shared (part of the "reduced" property). +* `@node_by_id`: A map from `node_id` to its `node_tuple` or a terminal symbol (`:true_terminal`, `:false_terminal`). +* `@next_id`: The next available integer ID for a new node. +* `@op_cache`: A map for memoizing results of operations like `apply` (binary ops), `negate`, and `simplify_with_constraints`. Keys are typically `{{op_name, id1, id2}, result_id}` or `{{op_name, id1}, result_id}`. + +### 2.3. Variable Ordering + +A strict global total order of all possible `variable_identifier`s is essential. This is achieved by defining variable identifiers as Elixir tuples, which have a natural sort order. +The proposed structure for variable identifiers is: +`{category_integer, predicate_type_atom, specific_value_or_nested_id}` + +Example categories: +* `0`: Primary type discriminators (e.g., `is_atom`, `is_integer`, `is_list`). +* `1`: Atom-specific predicates (e.g., `value == :foo`). +* `2`: Integer-specific predicates (e.g., `value < 10`). +* `4`: Tuple-specific predicates (e.g., `size == 2`, `element 0 has_type X`). +* And so on for other types. + +### 2.4. Core Operations + +1. **`make_node_raw(variable, yes_id, no_id, dc_id)`**: + * The fundamental private function for creating or retrieving unique structural nodes. + * Implements structural sharing via the `@nodes` table. + * Implements a basic reduction rule: if `yes_id == no_id == dc_id`, the node is redundant, and that common child ID is returned. + +2. **`check_assumptions_consistency(assumptions_map)`**: + * A private helper function crucial for semantic reduction. + * Takes a map `%{variable_id => value (true/false/:dc)}` representing current path assumptions. + * Returns `:consistent` or `:contradiction` based on predefined semantic rules of the type system (e.g., `is_atom=true` AND `is_tuple=true` is a contradiction). + * This function will be expanded as more types and predicates are added. + +3. **`simplify_with_constraints(tdd_id, assumptions_map)`**: + * A private, memoized, recursive function that takes a `tdd_id` and an `assumptions_map`. + * It produces a new `tdd_id` that is semantically equivalent to the input `tdd_id` under the given assumptions, but potentially simpler. + * **Crucial Behavior**: If `check_assumptions_consistency(assumptions_map)` returns `:contradiction` at any point, `simplify_with_constraints` immediately returns `@false_node_id`. + * If the TDD's variable is already in `assumptions_map`, it follows the constrained path. + * Otherwise, it recursively simplifies children, adding the current node's variable assignment to the assumptions for those deeper calls, and rebuilds the node using `make_node_raw`. + +4. **`apply_raw(op_name, op_lambda, u1_id, u2_id)`**: + * The private, memoized, recursive Shannon expansion algorithm for binary set operations (union, intersection). + * `op_lambda` defines the operation on terminal nodes. + * It selects the `top_var` based on the global variable order. + * Recursively calls `apply_raw` on the children. + * Uses `make_node_raw` to construct result nodes. + * This function computes the *structural* result of the operation. + +5. **Public API Operations (`sum/2`, `intersect/2`, `negate/1`)**: + * These functions orchestrate the operation: + 1. Call the respective `_raw` version (e.g., `apply_raw` for `sum`/`intersect`, `negate_raw` for `negate`). + 2. Take the `raw_result_id` from step 1. + 3. Return `simplify_with_constraints(raw_result_id, %{})`. This final step ensures that all TDDs exposed through the public API are not only structurally canonical (via `make_node_raw` and `apply_raw`) but also *semantically canonical* (i.e., known impossible paths or contradictions are resolved to `@false_node_id`). + +6. **Type Constructors (e.g., `type_atom()`, `type_atom_literal(:foo)`)**: + * These public functions build the TDD for a specific type. + * They use `make_node_raw` to define the basic structure. + * They then return `simplify_with_constraints(raw_id, %{})` to ensure the constructed type is in its simplest semantic form. + +7. **`is_subtype(sub_id, super_id)`**: + * Defined as `simplify_with_constraints(intersect(sub_id, negate(super_id)), %{}) == @false_node_id`. + * Since `intersect` and `negate` now return semantically simplified TDDs, if `A ∩ ¬B` represents an empty set, the result of the intersection will be `@false_node_id`. + +## 3. Datatype Representation Details + +This section outlines how various Elixir-like datatypes are (or will be) represented using TDD variables and constructors. All constructors ensure the final TDD is passed through `simplify_with_constraints(raw_id, %{})`. + +### 3.1. Atoms + +* **Variables**: + * `@v_is_atom = {0, :is_atom}`: Primary type check. + * `v_atom_eq_A = {1, :value, A}`: Checks if the atom's value is `A`. Order by `A`. +* **Constructors**: + * `type_atom()`: Represents any atom. TDD: `make_node_raw(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)`. + * `type_atom_literal(val)`: Represents a specific atom. TDD: `make_node_raw(@v_is_atom, node_for_val_eq, @false_node_id, @false_node_id)` where `node_for_val_eq = make_node_raw(v_atom_eq_A, @true_node_id, @false_node_id, @false_node_id)`. +* **Semantic Constraints for `check_assumptions_consistency`**: + * If `assumptions_map` contains `{{0, :is_atom}, true}` and `{{0, other_primary_type}, true}` -> contradiction. + * If `assumptions_map` contains `{{1, :value, A}, true}` and `{{1, :value, B}, true}` where `A != B` -> contradiction. + +### 3.2. Tuples + +* **Variables**: + * `@v_is_tuple = {0, :is_tuple}`: Primary type check. + * `v_tuple_size_eq_N = {4, :size, N}`: Checks if tuple size is `N`. Order by `N`. + * `v_tuple_elem_I_PRED = {4, :element, Index_I, NESTED_PREDICATE_ID}`: Predicate for element at `Index_I`. `NESTED_PREDICATE_ID` is a variable from the global order, applied to the element. (e.g., `{4, :element, 0, {0, :is_atom}}` checks if element 0 is an atom). Order by `Index_I`, then by `NESTED_PREDICATE_ID`. +* **Constructors**: + * `type_tuple()`: Any tuple. + * `type_empty_tuple()`: The tuple `{}`. + * `type_tuple_sized_any(size)`: Any tuple of a given size. + * `type_tuple_specific(element_type_ids_list)`: e.g., for `{atom(), integer()}`. This will involve creating nodes for size, then for each element, applying the TDD for that element's type. +* **Semantic Constraints**: + * `is_tuple=true` vs. other primary types. + * If `{{4, :size, N}, true}` and `{{4, :size, M}, true}` where `N != M` -> contradiction. + * If `{{4, :size, N}, true}` and a predicate `{{4, :element, I, _}, _}` exists where `I >= N` -> potential contradiction or path simplification (element doesn't exist). + +### 3.3. Integers (Next to Implement) + +* **Variables**: + * `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties). + * INT_CAT variables (names of variables prefixed with `a b c` to force ordering + * `v_int_lt_N = {INT_CAT, :alt, N}` (value < N). + * `v_int_eq_N = {INT_CAT, :beq, N}`. + * `v_int_gt_N = {INT_CAT, :cgt, N}` (value > N). + * *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).* +* **Constructors**: + * `type_integer()`: Any integer. + * `type_int_eq(n)`: A specific integer value. + * `type_int_lt(n)`, `type_int_gt(n)`. + * `type_int_range(min, max, min_inclusive, max_inclusive)`: Integers within a specific range. +* **Semantic Constraints**: + * `is_integer=true` vs. other primary types. + * `eq(N)` and `eq(M)` with `N != M` -> contradiction. + * `eq(N)` and `lt(M)` if `N >= M` -> contradiction. + * `eq(N)` and `gt(M)` if `N <= M` -> contradiction. + * `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 (Implemented) + +* **Variables**: + * `@v_is_list = {0, :is_list}`. + * `v_list_is_empty = {5, :is_empty}`. + * *If not empty*: + * `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()`: 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`, any predicate on the `head` or `tail` is a contradiction. + * Recursive consistency checks on `head` and `tail` sub-types. + +### 3.5. Strings & Binaries (Planned) + +* **Variables**: + * `@v_is_binary = {0, :is_binary}`. + * `@v_is_string = {0, :is_string}` (can be a check after `is_binary` or a distinct primary type if model demands). + * Size/length predicates: `v_binary_size_eq_N`, `v_string_length_eq_N`. + * Content predicates: `v_string_eq_S`, `v_string_prefix_P`, `v_string_suffix_S`, `v_string_matches_regex_R`. +* **Semantic Constraints**: Size vs content (e.g., `size=1` and `prefix="foo"` is a contradiction). `eq(S1)` and `eq(S2)` if `S1 != S2`. + +### 3.6. Maps (Planned - Complex) + +* **Variables**: + * `@v_is_map = {0, :is_map}`. + * `v_map_size_eq_N`. + * `v_map_has_key_K`: (K is a canonical representation of an Elixir term). + * *If `has_key_K` is true*: + * `v_map_key_K_value_VAR = {MAP_CAT, :key_value, K, NESTED_PREDICATE_ID}`: Applies a global predicate to the value associated with key K. + * For `%{pattern_key => pattern_value}` types: + * This requires careful thought. Might involve predicates like `v_map_all_keys_matching_TYPE_X_have_values_matching_TYPE_Y`. +* **Semantic Constraints**: `is_map` vs. others. Size vs. `has_key` interactions. Contradictory type requirements for the same key's value. + +### 3.7. Functions (Planned - Very Complex) + +* Representation of function types (`fun((Arg1Type, Arg2Type, ...) -> ReturnType)`) is a significant challenge for TDDs. +* **Variables (Tentative)**: + * `@v_is_function = {0, :is_function}`. + * `v_fun_arity_eq_A`. + * Predicates for argument types at specific positions (e.g., `v_fun_arg_I_type_VAR`). + * Predicates for return type (e.g., `v_fun_return_type_VAR`). +* Intersection and union of function types involve concepts like contravariance of arguments and covariance of return types. This may require specialized logic beyond simple TDD operations or a very elaborate variable scheme. Often, function types are handled with auxiliary structures in type systems. + +## 4. Current Status & Next Steps + +* **Implemented**: Atoms, basic Tuples (any, empty, sized_any). Core TDD operations (`sum`, `intersect`, `negate`, `is_subtype`) with semantic simplification framework (`simplify_with_constraints` and `check_assumptions_consistency`). +* **Passing Tests**: A suite of tests for atom/tuple interactions, unions, intersections, negations, and subtyping, including resolution of contradictions like `atom & tuple == none`. +* **Next Immediate Step**: Implement **Integer types** as outlined in section 3.3. This will involve: + 1. Defining integer-specific predicates and their global order. + 2. Creating integer type constructors. + 3. Significantly expanding `check_assumptions_consistency` to handle integer comparisons (`eq`, `lt`, `gt`) and their interactions. + 4. Adding comprehensive tests for integers. + +## 5. Future Considerations + +* **Performance**: For very large TDDs or complex types, the number of nodes and cache sizes can grow. Investigate optimizations if needed. +* **Generality of `check_assumptions_consistency`**: Designing this to be easily extensible and correct for many interacting predicates is challenging. A rule-based system or a more abstract way to define predicate interactions might be beneficial. +* **"Don't Care" (`dc`) branch semantics**: Ensure the `dc` branch is consistently and correctly handled in all operations, especially `simplify_with_constraints` if assumptions can make a variable "don't care". Currently, `simplify_with_constraints` assumes `true/false/:dc` values in the `assumptions_map` if a variable is already constrained. +* **Type Inference**: Using the TDD operations to infer types or solve type constraints. +* **Polymorphism**: Representing and operating on types with free type variables. Typically, free variables are treated as `any` or involve substitution before TDD construction. + +This document provides a snapshot of the current TDD system and a roadmap for its extension. The core principle is the combination of structurally canonical ROBDDs (via `make_node_raw` and `apply_raw`) with a semantic simplification layer (`simplify_with_constraints`) that embeds knowledge of the type system's rules. +""" + +defmodule Tdd.Core do + @moduledoc """ + The core, semantically-unaware TDD graph engine. + + This module is responsible for: + - Storing and managing a unique table of TDD nodes. + - Providing a function `make_node/4` that creates nodes while ensuring + structural sharing and basic reduction (redundant nodes). + - Implementing a generic, structural `apply/4` algorithm for binary + operations on TDDs. + + It knows nothing about what the variables (`{0, :is_atom}`, etc.) mean. + """ + + # --- Terminal Node IDs --- + @false_node_id 0 + @true_node_id 1 + + def true_id, do: @true_node_id + def false_id, do: @false_node_id + defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id + + # --- State Management --- + + def init do + Process.put(:tdd_nodes, %{}) + Process.put(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true}) + Process.put(:tdd_next_id, 2) + Process.put(:tdd_op_cache, %{}) + :ok + end + + defp get_state do + %{ + nodes: Process.get(:tdd_nodes, %{}), + node_by_id: Process.get(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true}), + next_id: Process.get(:tdd_next_id, 2), + op_cache: Process.get(:tdd_op_cache, %{}) + } + end + + defp update_state(changes) do + current_state = get_state() + new_state = Map.merge(current_state, changes) + Process.put(:tdd_nodes, new_state.nodes) + Process.put(:tdd_node_by_id, new_state.node_by_id) + Process.put(:tdd_next_id, new_state.next_id) + Process.put(:tdd_op_cache, new_state.op_cache) + end + + def clear_op_cache, do: Process.put(:tdd_op_cache, %{}) + + # --- Public API for the Core Engine --- + + def get_node(id) when is_terminal_id(id), do: if(id == @true_node_id, do: true, else: false) + def get_node(id), do: get_state().node_by_id[id] + + def get_op_cache(key), do: get_state().op_cache[key] + + def put_op_cache(key, value), + do: update_state(%{op_cache: Map.put(get_state().op_cache, key, value)}) + + @doc """ + Creates or retrieves a unique TDD node. + This is the heart of structural canonicalization (the 'R' in ROBDD). + """ + + def make_node(variable, yes_id, no_id, dc_id) do + # NEW, MORE POWERFUL REDUCTION RULE: + # If the 'yes' and 'no' paths lead to the same result, the test on this + # variable is redundant. The entire node can be replaced by that result. + cond do + yes_id == no_id -> + yes_id + + yes_id == dc_id && no_id == dc_id -> + yes_id + + true -> + state = get_state() + node_tuple = {variable, yes_id, no_id, dc_id} + + if Map.has_key?(state.nodes, node_tuple) do + state.nodes[node_tuple] + else + new_id = state.next_id + + update_state(%{ + nodes: Map.put(state.nodes, node_tuple, new_id), + node_by_id: Map.put(state.node_by_id, new_id, node_tuple), + next_id: new_id + 1 + }) + + new_id + end + end + end + + @doc """ + The generic Shannon expansion algorithm for any binary operation. + This is purely structural and relies on the caller (the semantic layer) + to ensure the inputs and results are meaningful. + """ + def apply(op_name, op_lambda, u1_id, u2_id) do + state = get_state() + cache_key = {op_name, Enum.sort([u1_id, u2_id])} + + cond do + Map.has_key?(state.op_cache, cache_key) -> + state.op_cache[cache_key] + + is_terminal_id(u1_id) && is_terminal_id(u2_id) -> + res_terminal = op_lambda.(get_node(u1_id), get_node(u2_id)) + if res_terminal == true, do: @true_node_id, else: @false_node_id + + true -> + u1_details = get_node(u1_id) + u2_details = get_node(u2_id) + + result_id = + cond do + u1_details == true or u1_details == false -> + {var2, y2, n2, d2} = u2_details + res_y = apply(op_name, op_lambda, u1_id, y2) + res_n = apply(op_name, op_lambda, u1_id, n2) + res_d = apply(op_name, op_lambda, u1_id, d2) + make_node(var2, res_y, res_n, res_d) + + u2_details == true or u2_details == false -> + {var1, y1, n1, d1} = u1_details + res_y = apply(op_name, op_lambda, y1, u2_id) + res_n = apply(op_name, op_lambda, n1, u2_id) + res_d = apply(op_name, op_lambda, d1, u2_id) + make_node(var1, res_y, res_n, d1) + + true -> + {var1, y1, n1, d1} = u1_details + {var2, y2, n2, d2} = u2_details + top_var = Enum.min([var1, var2]) + + res_y = + apply( + op_name, + op_lambda, + if(var1 == top_var, do: y1, else: u1_id), + if(var2 == top_var, do: y2, else: u2_id) + ) + + res_n = + apply( + op_name, + op_lambda, + if(var1 == top_var, do: n1, else: u1_id), + if(var2 == top_var, do: n2, else: u2_id) + ) + + res_d = + apply( + op_name, + op_lambda, + if(var1 == top_var, do: d1, else: u1_id), + if(var2 == top_var, do: d2, else: u2_id) + ) + + make_node(top_var, res_y, res_n, res_d) + end + + update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)}) + result_id + end + end +end + +defmodule Tdd.PredicateLogic do + @moduledoc "..." + alias Tdd.Variables, as: V + + @primary_types [:is_atom, :is_tuple, :is_integer, :is_list] + @primary_type_exclusivity_rules (for type <- @primary_types, into: %{} do + antecedent = {{0, type}, true} + + consequents = + for other_type <- @primary_types, + other_type != type, + do: {{{0, other_type}, false}} + + {antecedent, consequents} + end) + @rules @primary_type_exclusivity_rules + + def saturate(assumptions) do + case apply_static_rules(assumptions) do + {:ok, saturated_facts} -> final_check(saturated_facts) + :contradiction -> :contradiction + {:contradiction, _} -> :contradiction + end + end + + defp apply_static_rules(facts) do + Enum.reduce(facts, {:ok, facts}, fn {var, val}, {status, acc_facts} -> + if status == :contradiction do + {:contradiction, %{}} + else + rules_for_fact = Map.get(@rules, {var, val}, []) + + # --- THE CORRECTED PATTERN MATCH IS HERE --- + # The data is `{{{Var, Val}}}`. We need to match this shape. + Enum.reduce_while(rules_for_fact, {:ok, acc_facts}, fn {{consequent_var, consequent_val}}, + {_st, inner_facts} -> + case Map.get(inner_facts, consequent_var) do + nil -> {:cont, {:ok, Map.put(inner_facts, consequent_var, consequent_val)}} + ^consequent_val -> {:cont, {:ok, inner_facts}} + _ -> {:halt, {:contradiction, %{}}} + end + end) + end + end) + end + + defp final_check(facts) do + cond do + check_atom_values(facts) == :contradiction -> :contradiction + check_tuple_values(facts) == :contradiction -> :contradiction + check_integer_ranges(facts) == :contradiction -> :contradiction + check_list_structure(facts) == :contradiction -> :contradiction + true -> {:ok, facts} + end + end + + defp check_atom_values(facts) do + trues = + Enum.reduce(facts, MapSet.new(), fn + {{1, :value, atom_val}, true}, acc -> MapSet.put(acc, atom_val) + _, acc -> acc + end) + + if MapSet.size(trues) > 1, do: :contradiction, else: :ok + end + + defp check_tuple_values(facts) do + trues = + Enum.reduce(facts, MapSet.new(), fn + {{4, :size, size_val}, true}, acc -> MapSet.put(acc, size_val) + _, acc -> acc + end) + + if MapSet.size(trues) > 1, do: :contradiction, else: :ok + end + + defp check_list_structure(facts) do + is_assumed_empty = Map.get(facts, V.v_list_is_empty()) == true + + if is_assumed_empty do + has_head_or_tail_pred = + Enum.any?(facts, fn {var, _} -> + case var do + {5, :head, _} -> true + {5, :tail, _} -> true + _ -> false + end + end) + + if has_head_or_tail_pred, do: :contradiction, else: :ok + else + :ok + end + end + + # --- Integer Logic --- + + # THIS IS THE SINGLE, CORRECT DEFINITION TO USE + defp check_integer_ranges(facts) do + if facts[V.v_is_integer()] != true do + :ok + else + if calculate_integer_interval(facts) == :contradiction, do: :contradiction, else: :ok + end + end + + @doc """ + Checks if a `predicate` is logically implied (or contradicted) by a + set of `constraints`. + + This is the core of semantic simplification. It uses a recursive dispatch + strategy to handle predicates nested within data structures. + + ## Return Values + - `true`: The constraints imply the predicate is true. + (e.g., `x == 5` implies `x < 10`) + - `false`: The constraints imply the predicate is false (i.e., its negation is true). + (e.g., `x == 5` implies `x > 10` is false) + - `:unknown`: The constraints are insufficient to determine the predicate's truth value. + """ + def check_implication(predicate, constraints) do + # The case statement acts as our master dispatcher. + case predicate do + # ----------------------------------------------------------------- + # --- 1. Base Cases: Handling raw, non-nested predicates + # ----------------------------------------------------------------- + {1, :value, _} -> + _atom_implication(predicate, constraints) + + {2, _, _} -> + _integer_implication(predicate, constraints) + + {4, :size, _} -> + _tuple_size_implication(predicate, constraints) + + # ... add other base cases for list_is_empty, etc., if needed ... + + # ----------------------------------------------------------------- + # --- 2. Recursive Cases: Handling nested predicates + # ----------------------------------------------------------------- + {4, :element, index, inner_predicate} -> + # Isolate the sub-problem for this specific tuple element. + element_constraints = + gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1)) + + # Recurse on the sub-problem. + check_implication(inner_predicate, element_constraints) + + {5, :head, inner_predicate} -> + # Isolate the sub-problem for the list head. + head_constraints = + gather_local_constraints(constraints, &match?({5, :head, _}, &1)) + + # Recurse on the sub-problem. + check_implication(inner_predicate, head_constraints) + + {5, :tail, inner_predicate} -> + # Isolate the sub-problem for the list tail. + tail_constraints = + gather_local_constraints(constraints, &match?({5, :tail, _}, &1)) + + # Recurse on the sub-problem. + check_implication(inner_predicate, tail_constraints) + + # ... add other recursive cases for map_key_value, etc., in the future ... + + # ----------------------------------------------------------------- + # --- 3. Default Case + # ----------------------------------------------------------------- + _ -> + # We don't have specific reasoning logic for this predicate type. + :unknown + end + end + + # =================================================================== + # == PRIVATE HELPERS + # =================================================================== + + # --- Constraint Isolation Helper --- + + @doc """ + Gathers, unwraps, and isolates constraints for a specific component. + """ + defp gather_local_constraints(all_constraints, filter_fun) do + for {{var, bool_val}} <- all_constraints, + filter_fun.(var), + into: %{} do + # Unwrap the predicate for the local check. + # e.g., from `{4, :element, 0, {2, :beq, 5}}` we want `{2, :beq, 5}` + inner_predicate = elem(var, tuple_size(var) - 1) + {inner_predicate, bool_val} + end + end + + # --- Base Case Reasoners --- + + # Reasoner for integer predicates. + # Renamed from `check_integer_implication` to `_integer_implication` to denote it's a private helper. + defp _integer_implication(predicate, constraints) do + case calculate_integer_interval(constraints) do + :contradiction -> + # A contradiction implies anything. + true + + {min_val, max_val} -> + {_p_cat, p_type, p_val} = predicate + + cond do + # The current interval [min, max] is a SUBSET of the predicate's interval + (p_type == :alt and is_integer(max_val) and max_val < p_val) or + (p_type == :cgt and is_integer(min_val) and min_val > p_val) or + (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) -> + true + + # The current interval [min, max] is DISJOINT from the predicate's interval + (p_type == :alt and is_integer(min_val) and min_val >= p_val) or + (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or + (p_type == :beq and + ((is_integer(min_val) and min_val > p_val) or + (is_integer(max_val) and max_val < p_val))) -> + false + + true -> + :unknown + end + end + end + + # Reasoner for atom predicates using Enum.reduce + defp _atom_implication(predicate, constraints) do + # The predicate we are testing, e.g., {{1, :value, :foo}, true} + {{1, :value, p_val}, _} = {predicate, true} + + # Use Enum.reduce to find all atom values constrained to be true or false. + {true_atoms, false_atoms} = + Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn + # Match a constraint that an atom value MUST be true + {{1, :value, val}, true}, {true_set, false_set} -> + {MapSet.put(true_set, val), false_set} + + # Match a constraint that an atom value MUST be false + {{1, :value, val}, false}, {true_set, false_set} -> + {true_set, MapSet.put(false_set, val)} + + # Ignore any other kind of constraint + _, acc -> + acc + end) + + cond do + # If the predicate's value is explicitly known to be false. + p_val in false_atoms -> + false + + # If the predicate's value is explicitly known to be true. + p_val in true_atoms -> + true + + # If we know the value MUST be something else (and it's not our predicate's value). + # e.g., constraints say the value is :bar, and we're checking for :foo. + not Enum.empty?(true_atoms) and p_val not in true_atoms -> + false + + # Otherwise, we don't have enough information. + true -> + :unknown + end + end + + # Reasoner for tuple size predicates using Enum.reduce + defp _tuple_size_implication(predicate, constraints) do + # The predicate we are testing, e.g., {{4, :size, 2}, true} + {{4, :size, p_val}, _} = {predicate, true} + + {true_sizes, false_sizes} = + Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn + {{4, :size, val}, true}, {true_set, false_set} -> + {MapSet.put(true_set, val), false_set} + + {{4, :size, val}, false}, {true_set, false_set} -> + {true_set, MapSet.put(false_set, val)} + + _, acc -> + acc + end) + + cond do + # If the predicate's size is explicitly known to be false. + p_val in false_sizes -> + false + + # If the predicate's size is explicitly known to be true. + p_val in true_sizes -> + true + + # If we know the size MUST be something else. + not Enum.empty?(true_sizes) and p_val not in true_sizes -> + false + + # Otherwise, we don't know. + true -> + :unknown + end + end + + defp check_integer_implication(predicate, constraints) do + if constraints[V.v_is_integer()] != true do + :unknown + else + case calculate_integer_interval(constraints) do + :contradiction -> + true + + {min_val, max_val} -> + {_p_cat, p_type, p_val} = predicate + + cond do + (p_type == :alt and is_integer(max_val) and max_val < p_val) or + (p_type == :cgt and is_integer(min_val) and min_val > p_val) or + (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) -> + true + + (p_type == :alt and is_integer(min_val) and min_val >= p_val) or + (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or + (p_type == :beq and + ((is_integer(min_val) and min_val > p_val) or + (is_integer(max_val) and max_val < p_val))) -> + false + + true -> + :unknown + end + end + end + end + + defp calculate_integer_interval(facts) do + bounds = + Enum.reduce(facts, %{eq: nil, min: nil, max: nil}, fn + {var, true}, acc -> + case var do + {2, :beq, n} -> + if(is_nil(acc.eq) or acc.eq == n, do: %{acc | eq: n}, else: %{acc | eq: :conflict}) + + {2, :alt, n} -> + %{acc | max: min_opt(acc.max, n - 1)} + + {2, :cgt, n} -> + %{acc | min: max_opt(acc.min, n + 1)} + + _ -> + acc + end + + {var, false}, acc -> + case var do + {2, :alt, n} -> %{acc | min: max_opt(acc.min, n)} + {2, :cgt, n} -> %{acc | max: min_opt(acc.max, n)} + _ -> acc + end + + _, acc -> + acc + end) + + cond do + bounds.eq == :conflict -> + :contradiction + + is_integer(bounds.eq) -> + if (is_nil(bounds.min) or bounds.eq >= bounds.min) and + (is_nil(bounds.max) or bounds.eq <= bounds.max) do + {bounds.eq, bounds.eq} + else + :contradiction + end + + is_integer(bounds.min) and is_integer(bounds.max) and bounds.min > bounds.max -> + :contradiction + + true -> + {bounds.min, bounds.max} + end + end + + defp min_opt(nil, x), do: x + defp min_opt(x, nil), do: x + defp min_opt(x, y), do: min(x, y) + + defp max_opt(nil, x), do: x + defp max_opt(x, nil), do: x + defp max_opt(x, y), do: max(x, y) +end + +defmodule Tdd do + @moduledoc """ + The main public API and semantic layer for the TDD system. + It uses Tdd.Core for graph manipulation and Tdd.PredicateLogic + for reasoning about type system rules. + + This layer implements the high-level, type-aware algorithms for + intersection, union, negation, and subtyping. + """ + alias Tdd.Core + alias Tdd.PredicateLogic + alias Tdd.Variables, as: V + + # --- System Init --- + def init_tdd_system do + Core.init() + IO.puts("TDD system initialized with new architecture.") + end + + # --- Variable Definitions (could be in their own module) --- + defmodule Variables do + def v_is_atom, do: {0, :is_atom} + def v_is_tuple, do: {0, :is_tuple} + def v_is_integer, do: {0, :is_integer} + def v_is_list, do: {0, :is_list} + def v_atom_eq(v), do: {1, :value, v} + def v_int_eq(n), do: {2, :beq, n} + def v_int_lt(n), do: {2, :alt, n} + def v_int_gt(n), do: {2, :cgt, n} + def v_tuple_size_eq(n), do: {4, :size, n} + def v_tuple_elem_pred(i, v), do: {4, :element, i, v} + def v_list_is_empty, do: {5, :is_empty} + def v_list_head_pred(v), do: {5, :head, v} + def v_list_tail_pred(v), do: {5, :tail, v} + def v_list_all_elements_are(id), do: {5, :all_elements, id} + end + + # --- Type Constructors (Completed) --- + + def type_any, do: Core.true_id() + def type_none, do: Core.false_id() + + # Base type constructors + def type_atom, do: Core.make_node(V.v_is_atom(), type_any(), type_none(), type_none()) + def type_tuple, do: Core.make_node(V.v_is_tuple(), type_any(), type_none(), type_none()) + def type_integer, do: Core.make_node(V.v_is_integer(), type_any(), type_none(), type_none()) + def type_list, do: Core.make_node(V.v_is_list(), type_any(), type_none(), type_none()) + + # --- Atom Constructors --- + + def type_atom_literal(val) do + # A specific atom is the intersection of `atom()` and `value == val`. + constraint_node = Core.make_node(V.v_atom_eq(val), type_any(), type_none(), type_none()) + intersect(type_atom(), constraint_node) + end + + # --- Integer Constructors --- + + def type_int_eq(n) do + # A specific integer is the intersection of `integer()` and `value == n`. + constraint_node = Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none()) + intersect(type_integer(), constraint_node) + end + + def type_int_lt(n) do + # An integer `< n` is the intersection of `integer()` and `value < n`. + constraint_node = Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none()) + intersect(type_integer(), constraint_node) + end + + def type_int_gt(n) do + # An integer `> n` is the intersection of `integer()` and `value > n`. + constraint_node = Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none()) + intersect(type_integer(), constraint_node) + end + + # --- Tuple Constructors --- + + def type_empty_tuple do + # `{}` is the intersection of `tuple()` and `size == 0`. + constraint_node = Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none()) + intersect(type_tuple(), constraint_node) + end + + def type_tuple_sized_any(size) do + # A tuple of a fixed size is the intersection of `tuple()` and `size == N`. + constraint_node = + Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none()) + + intersect(type_tuple(), constraint_node) + end + + def type_tuple(element_type_ids) when is_list(element_type_ids) do + # This is the most complex tuple constructor. It represents a tuple with + # a specific size and specific types for each element. + # e.g., type_tuple([type_atom(), type_integer()]) for `{atom(), integer()}` + + num_elements = length(element_type_ids) + + # 1. Start with the base constraint: a tuple of the correct size. + base_type = type_tuple_sized_any(num_elements) + + # 2. Iteratively intersect with constraints for each element's type. + Enum.reduce(Enum.with_index(element_type_ids), base_type, fn {elem_type_id, index}, acc_tdd -> + # For each element, we create a TDD that represents the constraint on that element. + # `map_tdd_to_component` wraps all predicates of `elem_type_id` inside + # `v_tuple_elem_pred(index, ...)`, effectively focusing the type check + # on just that element of the tuple. + elem_constraint_tdd = + map_tdd_to_component(elem_type_id, &V.v_tuple_elem_pred(index, &1), type_any()) + + # Intersect the accumulated TDD with the new element constraint. + intersect(acc_tdd, elem_constraint_tdd) + end) + end + + # --- List Constructors --- + + def type_empty_list do + # `[]` is the intersection of `list()` and `is_empty == true`. + constraint_node = Core.make_node(V.v_list_is_empty(), type_any(), type_none(), type_none()) + intersect(type_list(), constraint_node) + end + + def type_cons(head_type_id, tail_type_id) do + # A cons cell `[H|T]` is a list that is NOT empty, where the head + # has type H and the tail has type T. + + # 1. Base type: a non-empty list. + non_empty_list = intersect(type_list(), negate(type_empty_list())) + + # 2. Create the constraint for the head's type. + head_constraint = + map_tdd_to_component(head_type_id, &V.v_list_head_pred/1, type_any()) + + # 3. Create the constraint for the tail's type. + tail_constraint = + map_tdd_to_component(tail_type_id, &V.v_list_tail_pred/1, type_any()) + + # 4. Intersect them all together. + non_empty_list + |> intersect(head_constraint) + |> intersect(tail_constraint) + end + + def type_list_of(element_type_id) do + # The type `list(T)` is a list where `all_elements` have type T. + # This predicate `{5, :all_elements, T}` is a "macro" predicate that implies + # a recursive check. The logic for handling its interaction with other + # list predicates must be encoded in the `intersect` algorithm itself + # (or more precisely, in `PredicateLogic` if it implies other simple facts). + # For now, we represent it with a single node. + # If T is `any`, then `list(any)` is just `list()`. + if element_type_id == type_any() do + type_list() + else + constraint_node = + Core.make_node( + V.v_list_all_elements_are(element_type_id), + type_any(), + type_none(), + type_none() + ) + + intersect(type_list(), constraint_node) + end + end + + # --- High-Level Operations --- + + def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{}) + def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) + + def negate(u_id) do + negate_recursive(u_id, %{}) + end + + def is_subtype(sub_id, super_id) do + # A <: B <=> A & ~B == none + IO.inspect("negate(super_id) in is_subtype") + Tdd.print_tdd(negate(super_id)) + IO.inspect("intersect(sub_id, negate(super_id)) in is_subtype") + Tdd.print_tdd(intersect(sub_id, negate(super_id))) + intersect(sub_id, negate(super_id)) == type_none() + end + + # NEW DEDICATED NEGATE FUNCTION + defp negate_recursive(id, constraints) do + # Memoization + cache_key = {:negate, id, Map.to_list(constraints) |> Enum.sort()} + + res = + if cached = Core.get_op_cache(cache_key) do + cached + else + compute_negate(id, constraints) + end + + Core.put_op_cache(cache_key, res) + res + end + + defp compute_negate(id, constraints) do + case PredicateLogic.saturate(constraints) do + :contradiction -> + # not(contradiction) is not(false) which is true + type_any() + + {:ok, saturated_constraints} -> + # First, simplify the node we are about to negate + s_id = simplify(id, saturated_constraints) + + case Core.get_node(s_id) do + true -> + type_none() + + false -> + type_any() + + {var, y, n, d} -> + # Recurse, adding the constraint for each branch + res_y = negate_recursive(y, Map.put(saturated_constraints, var, true)) + res_n = negate_recursive(n, Map.put(saturated_constraints, var, false)) + res_d = negate_recursive(d, Map.put(saturated_constraints, var, :dc)) + Core.make_node(var, res_y, res_n, res_d) + end + end + end + + # --- Core Recursive Operation Logic --- + + defp do_op(op_name, u1_id, u2_id, constraints) do + # Memoization using the Core cache + cache_key = {op_name, Enum.sort([u1_id, u2_id]), Map.to_list(constraints) |> Enum.sort()} + + if cached = Core.get_op_cache(cache_key) do + cached + else + res = compute_op(op_name, u1_id, u2_id, constraints) + Core.put_op_cache(cache_key, res) + res + end + end + + defp compute_op(op_name, u1_id, u2_id, constraints) do + # 1. Saturate constraints to detect contradictions early. + case PredicateLogic.saturate(constraints) do + :contradiction -> + # This path is impossible given the constraints. + # The meaning of a contradiction depends on the operation. + case op_name do + :intersect -> type_none() + # Placeholder for a more robust sum logic + :sum -> if u1_id, do: u2_id, else: u1_id + # not(false) -> true + :negate -> type_any() + end + + {:ok, saturated_constraints} -> + # Simplify inputs based on saturated constraints before recursing. + s1 = simplify(u1_id, saturated_constraints) + s2 = if u2_id, do: simplify(u2_id, saturated_constraints), else: nil + + # Get node details of the *simplified* inputs. + n1 = Core.get_node(s1) + n2 = if s2, do: Core.get_node(s2), else: nil + + # Dispatch to the actual operation logic. + dispatch_op(op_name, s1, n1, s2, n2, saturated_constraints) + end + end + + # If a path is contradictory, what does it mean for the operation? + # For intersection, it's `none`. For union, it depends on the other branch. + # This function is a placeholder for more complex logic if needed. + # For now, `none` for intersect and negate is safe. For `sum`, it's more complex. + defp handle_contradiction(:intersect), do: type_none() + # ¬(false) = true + defp handle_contradiction(:negate), do: type_any() + # a+b, if a is impossible, result is b. Needs other branch info. + defp handle_contradiction(:sum), do: type_none() + + # This is the replacement for the "implied value" check in the old `simplify_with_constraints`. + defp simplify(id, constraints) do + case Core.get_node(id) do + true -> + type_any() + + false -> + type_none() + + {var, y, n, _d} -> + # Check for direct constraint first. + case Map.get(constraints, var) do + true -> + simplify(y, constraints) + + false -> + simplify(n, constraints) + + :dc -> + # For now, we don't have logic to imply :dc, so we just follow the branch. + # A more advanced system might, but it's not needed for these tests. + simplify(_d, constraints) + + nil -> + case PredicateLogic.check_implication(var, constraints) do + true -> simplify(y, constraints) + false -> simplify(n, constraints) + # The path is not forced, so the node cannot be simplified away. + :unknown -> id + end + end + end + end + + defp dispatch_op(op_name, s1, n1, s2, n2, constraints) do + op_lambda = op_lambda(op_name) + + cond do + # Case 1: Both inputs are terminals. This is the base case. + (n1 == true or n1 == false) and (n2 == true or n2 == false) -> + res = op_lambda.(n1, n2) + if res == true, do: type_any(), else: type_none() + + # Case 2: The first input (s1) is a terminal, but s2 is not. + n1 == true or n1 == false -> + {var2, y2, n2_child, d2} = n2 + # Recurse on the children of s2, passing s1 down unchanged. + res_y = do_op(op_name, s1, y2, Map.put(constraints, var2, true)) + res_n = do_op(op_name, s1, n2_child, Map.put(constraints, var2, false)) + res_d = do_op(op_name, s1, d2, Map.put(constraints, var2, :dc)) + Core.make_node(var2, res_y, res_n, res_d) + + # Case 3: The second input (s2) is a terminal, but s1 is not. + n2 == true or n2 == false -> + {var1, y1, n1_child, d1} = n1 + # Recurse on the children of s1, passing s2 down unchanged. + res_y = do_op(op_name, y1, s2, Map.put(constraints, var1, true)) + res_n = do_op(op_name, n1_child, s2, Map.put(constraints, var1, false)) + res_d = do_op(op_name, d1, s2, Map.put(constraints, var1, :dc)) + Core.make_node(var1, res_y, res_n, res_d) + + # Case 4: Neither input is a terminal. This is the main recursive step. + true -> + {var1, y1, n1_child, d1} = n1 + {var2, y2, n2_child, d2} = n2 + top_var = Enum.min([var1, var2]) + + # Determine the children for the recursive call based on the top variable. + # If a node's variable is not the top_var, we pass the node's ID itself. + # If it *is* the top_var, we pass its child's ID. + call_y1 = if(var1 == top_var, do: y1, else: s1) + call_y2 = if(var2 == top_var, do: y2, else: s2) + call_n1 = if(var1 == top_var, do: n1_child, else: s1) + call_n2 = if(var2 == top_var, do: n2_child, else: s2) + call_d1 = if(var1 == top_var, do: d1, else: s1) + call_d2 = if(var2 == top_var, do: d2, else: s2) + + res_y = do_op(op_name, call_y1, call_y2, Map.put(constraints, top_var, true)) + res_n = do_op(op_name, call_n1, call_n2, Map.put(constraints, top_var, false)) + res_d = do_op(op_name, call_d1, call_d2, Map.put(constraints, top_var, :dc)) + Core.make_node(top_var, res_y, res_n, res_d) + end + end + + defp op_lambda(:intersect) do + fn + false, _ -> false + _, false -> false + true, v2 -> v2 + v1, true -> v1 + end + end + + defp op_lambda(:sum) do + fn + true, _ -> true + _, true -> true + false, v2 -> v2 + v1, false -> v1 + end + end + + # Helper from original code, still useful for constructors + defp map_tdd_to_component(tdd_id, wrapper_fun, success_id) do + case Core.get_node(tdd_id) do + true -> + success_id + + false -> + type_none() + + {var, y, n, d} -> + component_var = wrapper_fun.(var) + 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) + Core.make_node(component_var, res_y, res_n, res_d) + end + end + + @doc """ + Prints a human-readable representation of a TDD, starting from the given ID. + It recursively prints the structure of the graph. + """ + def print_tdd(id, indent \\ 0) do + prefix = String.duplicate(" ", indent) + # Use Tdd.Core to get node details + details = Core.get_node(id) + + IO.puts("#{prefix}ID #{id}: #{inspect(details)}") + + case details do + # A variable node + {_var, y, n, d} -> + IO.puts("#{prefix} Yes ->") + print_tdd(y, indent + 1) + IO.puts("#{prefix} No ->") + print_tdd(n, indent + 1) + IO.puts("#{prefix} DC ->") + print_tdd(d, indent + 1) + + # Terminal nodes (:true or :false) + true -> + :ok + + false -> + :ok + + # Handle cases where an ID might not be found + nil -> + IO.puts("#{prefix} Error: Unknown ID #{id}") + end + end +end + +# --- Example Usage --- +Tdd.init_tdd_system() + +# Basic Types +tdd_foo = Tdd.type_atom_literal(:foo) +tdd_bar = Tdd.type_atom_literal(:bar) +tdd_atom = Tdd.type_atom() +tdd_empty_tuple = Tdd.type_empty_tuple() +tdd_any = Tdd.type_any() +tdd_none = Tdd.type_none() + +test = fn name, expected, result -> + current_failures = Process.get(:test_failures, []) + + if expected != result do + Process.put(:test_failures, [name | current_failures]) + end + + status = if expected == result, do: "PASSED", else: "FAILED" + IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}") +end + +# Basic Types +tdd_foo = Tdd.type_atom_literal(:foo) +tdd_bar = Tdd.type_atom_literal(:bar) +tdd_baz = Tdd.type_atom_literal(:baz) +tdd_atom = Tdd.type_atom() +tdd_empty_tuple = Tdd.type_empty_tuple() +tdd_tuple = Tdd.type_tuple() +# Tuple of size 2, e.g. {any, any} +tdd_tuple_s2 = Tdd.type_tuple_sized_any(2) +tdd_any = Tdd.type_any() +tdd_none = Tdd.type_none() + +test_all = fn -> + IO.puts("\n--- TDD for :foo ---") + Tdd.print_tdd(tdd_foo) + + IO.puts("\n--- TDD for not :foo ---") + Tdd.print_tdd(Tdd.negate(tdd_foo)) + + IO.puts("\n--- TDD for atom ---") + Tdd.print_tdd(tdd_atom) + + IO.puts("\n--- TDD for not atom ---") + # Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id) + # This represents "anything that is not an atom". The DC branch becomes true because if + # "is_atom" test is irrelevant for "not atom", it means it's part of "not atom". + Tdd.print_tdd(Tdd.negate(tdd_atom)) + + IO.puts("\n--- TDD for :foo and :bar (should be none) ---") + tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar) + # Expected ID 0: :false_terminal + Tdd.print_tdd(tdd_foo_and_bar) + + IO.puts("\n--- TDD for :foo and atom (should be :foo) ---") + tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom) + # Expected to be structurally identical to tdd_foo + Tdd.print_tdd(tdd_foo_and_atom) + IO.puts("\n--- Basic Subtyping Tests ---") + test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom)) + test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo)) + test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar)) + test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo)) + test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple)) + test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple)) + test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple)) + test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple)) + test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2)) + test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple)) + + IO.puts("\n--- Any/None Subtyping Tests ---") + test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo)) + test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any)) + test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo)) + test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none)) + test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any)) + test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none)) + test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any)) + test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none)) + + IO.puts("\n--- Union related Subtyping ---") + tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar) + tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz) + + test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar)) + test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar)) + test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom)) + test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar)) + + test.( + "(:foo | :bar) <: (:foo | :bar | :baz)", + true, + Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz) + ) + + test.( + "(:foo | :bar | :baz) <: (:foo | :bar)", + false, + Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar) + ) + + # Test against a non-member of the union + test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz)) + + IO.puts("\n--- Intersection related Subtyping ---") + # Should be equivalent to tdd_foo + tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo) + # Should be tdd_none + tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple) + + test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo)) + test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo)) + test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none)) + test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple)) + test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar)) + # An intersection is a subtype of its components + test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom)) + # (none <: atom) + test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom)) + # (none <: tuple) + test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple)) + + IO.puts("\n--- Negation related Subtyping (Contrapositives) ---") + # Reminder: ¬A <: ¬B is equivalent to B <: A (contrapositive) + + # Test 1: ¬atom <: ¬:foo (Equivalent to :foo <: atom, which is true) + test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo))) + + # Test 2: ¬:foo <: ¬atom (Equivalent to atom <: :foo, which is false) + test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom))) + + # Double negation + test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo)) + test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo)))) + + # Disjoint types + test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple))) + test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom))) + test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple))) + + IO.puts("\n--- Mixed Types & Complex Subtyping ---") + tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple) + tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple) + + test.( + "(:foo | {}) <: (atom | tuple)", + true, + Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple) + ) + + test.( + "(atom | tuple) <: (:foo | {})", + false, + Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple) + ) + + test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple)) + test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple)) + + # De Morgan's Law illustration (A | B = ¬(¬A & ¬B)) + # (:foo | :bar) <: ¬(¬:foo & ¬:bar) + tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar)) + + test.( + "(:foo | :bar) <: ¬(¬:foo & ¬:bar)", + true, + Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar)) + ) + + test.( + "¬(¬:foo & ¬:bar) <: (:foo | :bar)", + true, + Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar) + ) + + # Type difference: atom - :foo (represented as atom & ¬:foo) + tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo)) + test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom)) + test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo)) + # True if :bar is in (atom - :foo) + test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar)) + test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo)) + + # (atom - :foo) | :foo should be atom + tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo) + test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom)) + test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom)) + + # (atom | {}) & (tuple | :foo) must be (:foo | {}) + # Represents `atom() | {}` + tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple) + # Represents `tuple() | :foo` + tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo) + intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo) + # Expected result for intersected_complex is tdd_foo_or_empty_tuple + + test.( + "(atom | {}) & (tuple | :foo) <: (:foo | {})", + true, + Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple) + ) + + test.( + "(:foo | {}) <: (atom | {}) & (tuple | :foo)", + true, + Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex) + ) + + # {} | tuple_size_2 should be a subtype of tuple + tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2) + test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple)) + + test.( + "({} | tuple_size_2) <: ({} | tuple_size_2)", + true, + Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2) + ) + + test.( + "({} | tuple_size_2) <: tuple_size_2", + false, + Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2) + ) + + # IO.puts("\n--- TDD structure for (atom - :foo) ---") + # Tdd.print_tdd(tdd_atom_minus_foo) + # IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---") + # Tdd.print_tdd(tdd_recombined_atom) + # IO.puts("\n--- TDD structure for 'atom' for comparison ---") + # Tdd.print_tdd(tdd_atom) + + IO.inspect(Process.get(:test_failures, [])) +end + +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 + +defmodule TupleTests do + import Tdd + + 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 ---") + + # --- 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() + # any tuple + t_tuple = type_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 + +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() + # [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)) + 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) + +a = Tdd.type_tuple([Tdd.type_int_eq(1), Tdd.type_atom_literal(:foo)]) + +b = + Tdd.type_tuple([ + Tdd.type_int_gt(0), + Tdd.sum(Tdd.type_atom_literal(:foo), Tdd.type_atom_literal(:bar)) + ]) + +IO.inspect("type_tuple([type_int_eq(1), type_atom_literal(:foo)])") +a |> Tdd.print_tdd() + +IO.inspect("type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])") +b |> Tdd.print_tdd() + +test.( + "{1, :foo} <: {int_gt_0, :foo | :bar}", + true, + Tdd.is_subtype(a, b) +) + +# output: +# +# TDD system initialized with new architecture. +# "type_tuple([type_int_eq(1), type_atom_literal(:foo)])" +# ID 26: {{0, :is_tuple}, 25, 0, 0} +# Yes -> +# ID 25: {{4, :size, 2}, 24, 0, 0} +# Yes -> +# ID 24: {{4, :element, 0, {0, :is_integer}}, 23, 0, 0} +# Yes -> +# ID 23: {{4, :element, 0, {2, :beq, 1}}, 22, 0, 0} +# Yes -> +# ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0} +# Yes -> +# ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0} +# Yes -> +# ID 1: true +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# "type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])" +# ID 40: {{0, :is_tuple}, 39, 0, 0} +# Yes -> +# ID 39: {{4, :size, 2}, 38, 0, 0} +# Yes -> +# ID 38: {{4, :element, 0, {0, :is_integer}}, 37, 0, 0} +# Yes -> +# ID 37: {{4, :element, 0, {2, :cgt, 0}}, 36, 0, 0} +# Yes -> +# ID 36: {{4, :element, 1, {0, :is_atom}}, 35, 0, 0} +# Yes -> +# ID 35: {{4, :element, 1, {1, :value, :bar}}, 1, 21, 21} +# Yes -> +# ID 1: true +# No -> +# ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0} +# Yes -> +# ID 1: true +# No -> +# ID 0: false +# DC -> +# ID 0: false +# DC -> +# ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0} +# Yes -> +# ID 1: true +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# "negate(super_id) in is_subtype" +# ID 47: {{0, :is_tuple}, 46, 1, 1} +# Yes -> +# ID 46: {{4, :size, 2}, 45, 1, 1} +# Yes -> +# ID 45: {{4, :element, 0, {0, :is_integer}}, 44, 1, 1} +# Yes -> +# ID 44: {{4, :element, 0, {2, :cgt, 0}}, 43, 1, 1} +# Yes -> +# ID 43: {{4, :element, 1, {0, :is_atom}}, 42, 1, 1} +# Yes -> +# ID 42: {{4, :element, 1, {1, :value, :bar}}, 0, 41, 41} +# Yes -> +# ID 0: false +# No -> +# ID 41: {{4, :element, 1, {1, :value, :foo}}, 0, 1, 1} +# Yes -> +# ID 0: false +# No -> +# ID 1: true +# DC -> +# ID 1: true +# DC -> +# ID 41: {{4, :element, 1, {1, :value, :foo}}, 0, 1, 1} +# Yes -> +# ID 0: false +# No -> +# ID 1: true +# DC -> +# ID 1: true +# No -> +# ID 1: true +# DC -> +# ID 1: true +# No -> +# ID 1: true +# DC -> +# ID 1: true +# No -> +# ID 1: true +# DC -> +# ID 1: true +# No -> +# ID 1: true +# DC -> +# ID 1: true +# No -> +# ID 1: true +# DC -> +# ID 1: true +# "intersect(sub_id, negate(super_id)) in is_subtype" +# ID 52: {{0, :is_tuple}, 51, 0, 0} +# Yes -> +# ID 51: {{4, :size, 2}, 50, 0, 0} +# Yes -> +# ID 50: {{4, :element, 0, {0, :is_integer}}, 49, 0, 0} +# Yes -> +# ID 49: {{4, :element, 0, {2, :beq, 1}}, 48, 0, 0} +# Yes -> +# ID 48: {{4, :element, 0, {2, :cgt, 0}}, 0, 22, 22} +# Yes -> +# ID 0: false +# No -> +# ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0} +# Yes -> +# ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0} +# Yes -> +# ID 1: true +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# DC -> +# ID 22: {{4, :element, 1, {0, :is_atom}}, 21, 0, 0} +# Yes -> +# ID 21: {{4, :element, 1, {1, :value, :foo}}, 1, 0, 0} +# Yes -> +# ID 1: true +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# No -> +# ID 0: false +# DC -> +# ID 0: false +# {1, :foo} <: {int_gt_0, :foo | :bar} (Expected: true) -> Result: false - FAILED