From 7d02481d9ff47a7bee30e9b2cac3e3114b4301dc Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Tue, 17 Jun 2025 10:31:39 +0200 Subject: [PATCH] checkpoint --- review.md | 2829 +++++++++++++++++++++++++++++++++++++++++++++++++++++ test1.exs | 1052 +++++--------------- 2 files changed, 3068 insertions(+), 813 deletions(-) create mode 100644 review.md diff --git a/review.md b/review.md new file mode 100644 index 0000000..add8e2b --- /dev/null +++ b/review.md @@ -0,0 +1,2829 @@ +lets review the implementation, approach and design of this logic, why does the test fail - any shortcomings in our implementation, fundamental design flaws ? +``` +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 + + def terminal_id?(id) when is_terminal_id(id), do: true + def terminal_id?(_), do: false + + # --- 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 """ + A general-purpose reasoner that uses the main `saturate` function. + It determines if a predicate is implied true or false by a set of constraints + by checking if adding its opposite leads to a contradiction. + """ + defp _reason_by_contradiction(predicate, constraints) do + # Is `predicate` implied TRUE? (i.e., is `constraints AND NOT predicate` a contradiction?) + cond do + saturate(Map.put(constraints, predicate, false)) == :contradiction -> + true + + # Is `predicate` implied FALSE? (i.e., is `constraints AND predicate` a contradiction?) + saturate(Map.put(constraints, predicate, true)) == :contradiction -> + false + + true -> + :unknown + end + end + + @doc """ + Checks if a `predicate` is logically implied (or contradicted) by a + set of `constraints`. + """ + def check_implication(predicate, constraints) do + case predicate do + # --- NEW HANDLER for primary type predicates --- + {0, _} -> + _reason_by_contradiction(predicate, constraints) + + # --- EXISTING BASE CASES --- + {1, :value, _} -> + _atom_implication(predicate, constraints) + + {2, _, _} -> + _integer_implication(predicate, constraints) + + {4, :size, _} -> + _tuple_size_implication(predicate, constraints) + + # --- EXISTING RECURSIVE CASES --- + {4, :element, index, inner_predicate} -> + element_constraints = + gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1)) + + check_implication(inner_predicate, element_constraints) + + {5, :head, inner_predicate} -> + head_constraints = + gather_local_constraints(constraints, &match?({5, :head, _}, &1)) + + check_implication(inner_predicate, head_constraints) + + {5, :tail, inner_predicate} -> + tail_constraints = + gather_local_constraints(constraints, &match?({5, :tail, _}, &1)) + + check_implication(inner_predicate, tail_constraints) + + # --- 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, %{}) |> simplify(%{}) + def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) |> simplify(%{}) + + def negate(u_id) do + negate_recursive(u_id, %{}) + |> simplify(%{}) + end + + def is_subtype(sub_id, super_id) do + # A <: B <=> A & ~B == none + IO.inspect("sub_id in is_subtype") + Tdd.print_tdd(sub_id) + 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 + case PredicateLogic.saturate(constraints) do + :contradiction -> + # This path is impossible. For an intersection, the result is the empty set. + handle_contradiction(op_name) + + {:ok, saturated_constraints} -> + # REMOVED: No more pre-simplifying inputs here. + # We pass the original IDs and the full context to dispatch_op. + n1 = Core.get_node(u1_id) + n2 = Core.get_node(u2_id) + dispatch_op(op_name, u1_id, n1, u2_id, 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`. + def simplify(id, constraints) do + # Memoization is critical for performance + cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()} + + if cached = Core.get_op_cache(cache_key) do + cached + else + # We will call saturate at the beginning of the operation (in compute_op), + # so we can assume constraints are consistent here. + res = compute_simplify(id, constraints) + Core.put_op_cache(cache_key, res) + res + end + end + + defp compute_simplify(id, constraints) do + case Core.get_node(id) do + true -> + type_any() + + false -> + type_none() + + {var, y, n, d} -> + contradiction = + case var do + {5, :head, head_predicate} -> + all_elements_type_id = + Enum.find_value(constraints, fn + {{5, :all_elements, type_id}, true} -> type_id + _ -> nil + end) + + if all_elements_type_id do + head_type = predicate_to_tdd(head_predicate) + # Is the required head type compatible with the element type? + intersect(head_type, all_elements_type_id) == type_none() + else + false + end + + {5, :tail, tail_predicate} -> + all_elements_type_id = + Enum.find_value(constraints, fn + {{5, :all_elements, type_id}, true} -> type_id + _ -> nil + end) + + if all_elements_type_id do + tail_type = predicate_to_tdd(tail_predicate) + # The tail must be a list of the element type. + required_tail_type = type_list_of(all_elements_type_id) + intersect(tail_type, required_tail_type) == type_none() + else + false + end + + _ -> + false + end + + if contradiction do + # The 'yes' branch is impossible. The node simplifies to its 'no' branch. + simplify(n, constraints) + else + case Map.get(constraints, var) do + true -> + simplify(y, constraints) + + false -> + simplify(n, constraints) + + :dc -> + simplify(d, constraints) + + nil -> + case PredicateLogic.check_implication(var, constraints) do + true -> + simplify(y, constraints) + + false -> + simplify(n, constraints) + + :unknown -> + res_y = simplify(y, Map.put(constraints, var, true)) + res_n = simplify(n, Map.put(constraints, var, false)) + res_d = simplify(d, Map.put(constraints, var, :dc)) + Core.make_node(var, res_y, res_n, res_d) + end + end + end + end + end + + defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do + # --- Step 1: Simplify the current nodes under the given constraints. --- + # This is the crucial change. We simplify first, before doing anything else. + s1_id = simplify(u1_id, constraints) + s2_id = simplify(u2_id, constraints) + + # If simplification resolved either to a terminal, we can take a shortcut. + if Core.terminal_id?(s1_id) or Core.terminal_id?(s2_id) do + apply_terminals(op_name, s1_id, s2_id) + else + # --- Step 2: Get details of the *simplified* nodes and proceed. --- + sn1 = Core.get_node(s1_id) + sn2 = Core.get_node(s2_id) + + {var1, y1, n1_child, d1} = sn1 + {var2, y2, n2_child, d2} = sn2 + top_var = Enum.min([var1, var2]) + + # Determine children for the recursive call based on top_var. + call_y1 = if(var1 == top_var, do: y1, else: s1_id) + call_y2 = if(var2 == top_var, do: y2, else: s2_id) + call_n1 = if(var1 == top_var, do: n1_child, else: s1_id) + call_n2 = if(var2 == top_var, do: n2_child, else: s2_id) + call_d1 = if(var1 == top_var, do: d1, else: s1_id) + call_d2 = if(var2 == top_var, do: d2, else: s2_id) + + # --- Step 3: Recurse with the original do_op entry point --- + 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 apply_terminals(op_name, id1, id2) do + lambda = op_lambda(op_name) + n1 = Core.get_node(id1) + n2 = Core.get_node(id2) + + # If both are terminals, just apply the op. + if Core.terminal_id?(id1) and Core.terminal_id?(id2) do + if lambda.(n1, n2), do: type_any(), else: type_none() + else + # If only one is a terminal, we must recurse on the other's children. + # This ensures correctness for operations like `A & true -> A`. + non_terminal_id = if(Core.terminal_id?(id1), do: id2, else: id1) + terminal_id = if(Core.terminal_id?(id1), do: id1, else: id2) + {var, y, n, d} = Core.get_node(non_terminal_id) + + res_y = apply_terminals(op_name, y, terminal_id) + res_n = apply_terminals(op_name, n, terminal_id) + res_d = apply_terminals(op_name, d, terminal_id) + Core.make_node(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 """ + Converts a single predicate variable into a full TDD type. + This is the key to comparing predicates with other TDD types. + """ + defp predicate_to_tdd(predicate) do + # Memoize for performance, as this might be called repeatedly. + cache_key = {:predicate_to_tdd, predicate} + + if cached = Core.get_op_cache(cache_key) do + cached + else + res = + case predicate do + {0, :is_atom} -> type_atom() + {0, :is_tuple} -> type_tuple() + {0, :is_integer} -> type_integer() + {0, :is_list} -> type_list() + {1, :value, val} -> type_atom_literal(val) + {2, :beq, n} -> type_int_eq(n) + {2, :alt, n} -> type_int_lt(n) + {2, :cgt, n} -> type_int_gt(n) + {4, :size, n} -> type_tuple_sized_any(n) + {5, :is_empty} -> type_empty_list() + # A head/tail predicate implies the value is a list AND has that head/tail. + # The inner predicate is what we care about for the type check. + {5, :head, inner_p} -> predicate_to_tdd(inner_p) + {5, :tail, inner_p} -> predicate_to_tdd(inner_p) + {5, :all_elements, type_id} -> type_list_of(type_id) + # A tuple element predicate is about the element, not the tuple itself. + {4, :element, _, inner_p} -> predicate_to_tdd(inner_p) + # Fallback for unknown/complex predicates: assume they can be anything. + _ -> type_any() + end + + Core.put_op_cache(cache_key, res) + res + 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 + +defmodule AdhocTest do + import Tdd + + def run(test_fn) do + # --- Basic Types --- + t_int = type_integer() + t_pos_int = type_int_gt(0) + + # --- list(X) Types --- + t_list_of_int = type_list_of(t_int) + t_list_of_pos_int = type_list_of(t_pos_int) + print_tdd(t_list_of_int) + print_tdd(t_list_of_pos_int ) + + # --- Specific List Types --- + intersect1 = intersect(t_list_of_int, t_list_of_pos_int) + print_tdd(intersect1) + print_tdd(14) + print_tdd(16) + test_fn.( + "(list(int) & list(pos_int)) == list(pos_int)", + true, + intersect1 == t_list_of_pos_int + ) + end +end + +# test_all.() +# IntegerTests.run(test) +# TupleTests.run(test) +# ListTests.run(test) +# ListOfTests.run(test) +AdhocTest.run(test) +``` + + +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== + + +Excellent and very thorough submission. This is a professional-grade implementation of a complex concept, and the design document is clear and well-structured. The core idea of separating the structural engine (`Tdd.Core`) from the semantic layer (`Tdd` and `Tdd.PredicateLogic`) is exactly the right approach. + +Let's break down the review into the parts you asked for: why the test fails, implementation shortcomings, and fundamental design flaws. + +--- + +### 1. Why the Test Fails: The Root Cause + +The failing test is `(list(int) & list(pos_int)) == list(pos_int)` in `ListOfTests` (and `AdhocTest`). + +This test fails because of a **fundamental design flaw in how `list_of(T)` types are represented and handled by the intersection logic.** + +**The Problem:** + +1. **Representation:** You've chosen to represent the `list_of(T)` constraint with a special variable: `{5, :all_elements, element_type_id}`. The crucial part is that the `element_type_id` (an integer) is part of the variable itself. +2. **Distinct Variables:** This means the variable for `list(integer)` is `{5, :all_elements, }` and the variable for `list(positive_integer)` is `{5, :all_elements, }`. Because the type IDs are different, **the TDD system sees these as two completely separate, unrelated predicates.** +3. **Structural Intersection:** The `intersect` operation is structural. When it intersects `list(int)` and `list(pos_int)`, it sees two different predicate nodes. It correctly follows the Shannon expansion and creates a new TDD that essentially says: "the type must be a list AND `all_elements` must be `integer` AND `all_elements` must be `positive_integer`". +4. **Lack of Semantic Simplification:** The resulting TDD has *two* test nodes (`{5, :all_elements, ...}`) on its main path. The `list(pos_int)` TDD only has *one*. Although they are logically equivalent (since `pos_int <: int`), they are **not structurally identical**. Your system currently has no semantic rule in `PredicateLogic` or `simplify` to perform this reduction: + `({5, :all_elements, T1}, true)` and `({5, :all_elements, T2}, true)` should simplify to `({5, :all_elements, intersect(T1, T2)}, true)`. + +Because the system cannot perform this semantic simplification, the resulting TDD from the intersection is not canonical, and the `==` check against the canonical `list(pos_int)` TDD fails. + +--- + +### 2. Analysis of the Design and Implementation + +This single failing test reveals a deeper pattern of challenges with this design. Let's analyze the broader shortcomings and flaws. + +#### Flaw 1: "Macro" Predicates with Embedded IDs (The Root Cause Generalized) + +This is the most critical design flaw. You use predicates that embed a TDD `id` inside the variable tuple itself. This appears in: +* `{5, :all_elements, element_type_id}` +* `{4, :element, Index, NESTED_PREDICATE_ID}` +* `{5, :head, NESTED_PREDICATE_ID}` +* `{5, :tail, NESTED_PREDICATE_ID}` + +This approach has several severe problems: + +1. **Breaks Canonicity:** The global ordering of variables is the bedrock of a canonical TDD/BDD. Since `id`s are generated sequentially, the variable order now depends on the *creation order of types*. If you create `list(pos_int)` before `list(int)` in one test run, and in a different order in another, the TDD variables will have a different sort order, potentially leading to different (but logically equivalent) TDD structures. This completely undermines the goal of having a single canonical form. +2. **Semantic Blindness:** As seen in the failing test, the core `apply` and `simplify` logic cannot reason about the relationship between two such variables. It can't know that `is_subtype(id1, id2)` implies a relationship. +3. **Combinatorial Explosion of Variables:** You are creating a new variable in the global order for every single `list_of(T)` type. This leads to an unnecessarily large and sparse variable set. + +**Solution / Better Design:** +A more robust design avoids embedding IDs in variables. A predicate should represent a property of the value being tested, not a property of another TDD. + +* **For Tuples/Lists:** Instead of `v_list_head_pred({0, :is_atom})`, the variable should just be `{5, :head}`. The children of this node would then be TDDs that operate on the *head element itself*. This is a concept known as "Functional BDDs" or using context-shifting operators. It's much more complex to implement. +* **A Pragmatic Fix (within your current architecture):** You must significantly enhance `PredicateLogic.check_implication` and `Tdd.simplify` to be aware of these macro predicates. For example, `simplify` would need a rule that says: "If my constraints already include `{{5, :all_elements, T1}, true}` and I encounter a node for `{{5, :all_elements, T2}, ...}`, I must check the relationship between `T1` and `T2`." + + ```elixir + # In Tdd.simplify, when examining a node with var = {5, :all_elements, T2} + # find any existing all_elements constraints + existing_constraint = Enum.find(constraints, &match?({{5, :all_elements, _}, true}, &1)) + + if existing_constraint do + {{5, :all_elements, t1_id}, true} = existing_constraint + intersection_type = intersect(t1_id, t2) + + if intersection_type == type_none() do + # Contradiction: this path is impossible. Simplify the 'no' branch. + return simplify(n, constraints) + end + end + ``` + This is complex, requires careful management of the constraint set, and is a patch on the fundamental design issue, but it would fix the immediate problem. + +#### Flaw 2: Incomplete Simplification Logic + +The `simplify` function is the heart of semantic reduction, but it's missing key logic. + +1. **`list_of` vs `cons`:** The interaction logic you added for `list_of(T)` with `:head` and `:tail` is a great start. It correctly identifies contradictions (e.g., `list(integer) & [:foo | _] == none`). However, it doesn't handle the non-contradictory case correctly. + * **The Bug:** When checking `list(integer) & [5 | list(atom)]`, your current logic would find no contradiction in the head (`5` is an integer). It would then check the tail, `list(atom)`, against the `all_elements` constraint `list(integer)`. Your code does `intersect(tail_type, required_tail_type)` which is `intersect(list(atom), list(integer))`. This correctly results in `type_empty_list`. However, this should result in a contradiction for any non-empty tail, but your code only prunes the branch if the intersection is exactly `type_none()`. `type_empty_list()` is not `type_none()`. This interaction is very subtle and needs to be more robust. + +2. **Integer Range Logic:** `PredicateLogic.check_integer_ranges` and `calculate_integer_interval` are well-implemented and correctly find contradictions within a set of assumptions. However, `check_implication` for integers is incomplete. It correctly checks if a predicate is implied (`true`) or contradicted (`false`), but it doesn't handle overlapping ranges correctly during intersection. For example, `intersect(lt(10), lt(5))` should simplify to `lt(5)`. Your current `intersect` will create a TDD with two nodes (`<10` and `<5`), because `check_implication` reports `:unknown` for `<5` given `<10`. + +#### Shortcoming 3: Over-reliance on Memoization with Complex Keys + +Your memoization keys often include a sorted list of the entire `constraints` map: +`cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()}` + +This is correct for ensuring correctness, but it can be inefficient. As the path in the TDD gets deeper, the `constraints` map grows, making cache keys large and cache hits less likely than they could be. More advanced systems often find ways to canonicalize the constraint set itself or use structural hashing on the fly. For your scale, this is acceptable, but it's a potential performance bottleneck. + +--- + +### 3. Summary of Recommendations + +1. **Fix the Failing Test (and the Core Flaw):** + * **The Best Long-Term Fix:** Redesign your variables to remove embedded TDD IDs. This is a major undertaking. + * **The Pragmatic Short-Term Fix:** Enhance `Tdd.simplify` and/or `Tdd.PredicateLogic.saturate` to handle the interaction between multiple "macro" predicates. The logic should be: + * When multiple `{{5, :all_elements, T_i}, true}` constraints exist, compute the intersection of all `T_i`. Replace the multiple constraints with a single one for the new intersection type. If the intersection is `none`, the path is a contradiction. + * Apply the same logic for tuple elements. + +2. **Improve Integer Logic:** In `PredicateLogic._integer_implication`, when you have a constraint like `{min: nil, max: 9}` (from `lt(10)`) and you are checking the implication of `lt(5)`, you can see that `lt(5)` is not fully implied but also not contradicted. To simplify `lt(10) & lt(5)`, the `intersect` logic needs to recognize that the result is simply `lt(5)`. This requires more powerful reasoning than just checking for `:contradiction`. The `saturate` function is the right place for this: it should refine the bounds in the constraint set. + +3. **Refine `dc` (Don't Care) Semantics:** The design doc mentions the `dc` branch, and the code includes it, but its semantic meaning isn't fully leveraged. In many TDD papers, `negate({v,y,n,d})` is defined as `{v, negate(y), negate(n), negate(d)}`. Your `negate_recursive` implementation correctly does this. The key is to ensure the base types are constructed correctly. For `type_atom()`, you have `{v_is_atom, any, none, none}`. Negating this gives `{v_is_atom, none, any, any}`, which is correct for `¬atom`. This part of your implementation seems sound. + +### Conclusion + +You have built a powerful and well-architected system that is very close to working correctly. The core issue is a design choice about how to represent recursive/nested types that, while seemingly intuitive, breaks the assumptions that the canonical `apply` algorithm relies on. + +By focusing on adding the missing *semantic rules* to your `PredicateLogic` and `simplify` functions to handle these "macro" predicates, you can fix the failing tests and make the system significantly more robust without having to re-architect the entire variable scheme. This is an excellent foundation to build upon. + +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== + +Lets design how a migration to a redesigned TDD with no type ids in variables would look like, what would it entail and if/how it would simplify implementation. + + +============================================================================== +============================================================================== +============================================================================== + +Of course. This is an excellent question because it gets to the heart of the system's design. Migrating away from variables-with-IDs is a significant but highly beneficial architectural change. + +Here is a detailed design for that migration, outlining what it would entail and how it dramatically simplifies the implementation. + +--- + +### The New Design Philosophy: "Contextualized Predicates" + +The core problem with the old design is that a variable like `{5, :head, }` conflates two separate concepts: +1. **The Context:** "We are now testing the head of a list." +2. **The Predicate:** "Is this value an atom?" + +The new design separates these. The TDD for a component (like a tuple element or a list head) will be built using the **same fundamental set of variables** as a top-level type, but those variables will be systematically *namespaced* or *prefixed* to indicate their context. + +#### 1. The New Variable Structure + +Variables will be tuples that naturally sort into the correct global order. The context becomes a prefix to the base predicate. + +* **Base Predicates (as before):** + * `{0, :is_atom}` + * `{2, :beq, 5}` + * `{4, :size, 2}` + +* **New Contextualized Predicates:** + * `{:element, 0, {0, :is_atom}}` - "Is the 0th element of the tuple an atom?" + * `{:element, 1, {2, :beq, 5}}` - "Is the 1st element of the tuple equal to 5?" + * `{:head, {0, :is_atom}}` - "Is the head of the list an atom?" + * `{:tail, {0, :is_list}}` - "Is the tail of the list a list?" (Note: the predicate here is `{0, :is_list}`, not `{5, ...}`) + +This structure has a critical advantage: Elixir's default tuple sorting creates a **stable, predictable, and canonical global variable order**. +* `{:element, 0, ...}` variables will always come before `{:element, 1, ...}`. +* `{:element, ...}` variables can be ordered before or after `{:head, ...}` based on the atom sorting. +* Most importantly, the variable no longer depends on a runtime-generated ID. + +#### 2. The New Design for Recursive Types (`list_of(T)`) + +The "prefixing" strategy above works perfectly for fixed-size structures like tuples. For recursive types like `list_of(T)`, which have unbounded depth, prefixing every possible element (`{:head, ...}`, `{:tail, {:head, ...}}`, etc.) would create an infinite TDD. + +This requires a different, more powerful representation. Instead of embedding a type ID, we make the *child of the node* be the type TDD. + +* **New "Applicator" Variable:** We introduce a new kind of variable that acts as an instruction. + * `{5, :for_all_elements}` + +* **New Node Interpretation in `Tdd.Core`:** A node with this variable is interpreted differently. + * `{var, yes_id, no_id, dc_id}` + * If `var == {5, :for_all_elements}`, then `yes_id` is the TDD ID of the type that all elements must conform to. The `no` and `dc` branches are not used for this special node type and could be `type_any` or `type_none`. + +* **How `intersect` Works:** This is the magic. + * Let `L1 = type_list_of(T1)` and `L2 = type_list_of(T2)`. + * Their TDDs will look like: + * `L1_tdd`: `is_list? -> yes -> { {5, :for_all_elements}, T1_id, any, any }` + * `L2_tdd`: `is_list? -> yes -> { {5, :for_all_elements}, T2_id, any, any }` + * When the `apply` algorithm in `Tdd.Core` gets to these nodes, it sees they share the **exact same variable** `{5, :for_all_elements}`. + * It will then recursively call `apply` on their children: `intersect(T1_id, T2_id)`. + * The result is a new node `{ {5, :for_all_elements}, intersect(T1, T2), any, any }`. + +This is exactly the behavior needed to solve the failing test: `intersect(list(int), list(pos_int))` will correctly and structurally produce `list(intersect(int, pos_int))`, which is `list(pos_int)`. + +--- + +### Migration Plan: What it Entails + +#### Step 1: Redefine Variable Generation +The function `map_tdd_to_component` is the central place to change. + +**Old Code:** +```elixir +# wrapper_fun was &V.v_list_head_pred/1, which returned {5, :head, var} +component_var = wrapper_fun.(var) +``` +**New Code:** +```elixir +defp map_tdd_to_component(tdd_id, context_prefix, success_id) do + # ... + # e.g., context_prefix = :head + component_var = {context_prefix, var} # or {:element, index, var} + # ... +end +``` +The type constructors (`type_tuple`, `type_cons`) will now pass atom contexts like `:head`, `:tail`, or `{:element, index}` to `map_tdd_to_component`. + +#### Step 2: Rewrite `Tdd.PredicateLogic` for Simplicity +This is where the biggest simplification occurs. The logic no longer needs to know about specific predicate categories (`5` for lists, `4` for tuples). It can be written recursively. + +**Old `saturate` logic:** +- Had to check for `{{0, :is_atom}, true}` and `{{0, :is_tuple}, true}`. +- Had to check for `{{1, :value, A}, true}` and `{{1, :value, B}, true}`. +- All checks were on a flat map of constraints. + +**New `saturate` logic:** +```elixir +def saturate(constraints) do + # 1. Group constraints by their context prefix. + # The key `_` (or `nil`) holds the top-level constraints. + grouped_by_context = + Enum.group_by(constraints, fn + {{context, _inner_var}, _val} when is_atom(context) -> context + {{context, _index, _inner_var}, _val} when context == :element -> {context, _index} + _ -> :top_level + end) + + # 2. Check for contradictions at the top level first. + case check_flat_consistency(grouped_by_context[:top_level] || []) do + :contradiction -> :contradiction + {:ok, saturated_top_level} -> + # 3. Recursively check consistency for each sub-context. + # This re-uses the exact same logic! + Enum.reduce_while(grouped_by_context, {:ok, saturated_top_level}, fn + (:top_level, _), acc -> {:cont, acc} # Already handled + ({_context, sub_constraints}), acc -> + case saturate(sub_constraints) do # Recursive call! + :contradiction -> {:halt, :contradiction} + {:ok, _} -> {:cont, acc} + end + end) + end +end + +# check_flat_consistency is what your old `saturate` did, but it's +# now a simpler helper that only works on a flat list of simple predicates. +``` +The `check_implication` function benefits from the same recursive structure. The code becomes shorter, more general, and vastly easier to reason about and extend. + +#### Step 3: Update Type Constructors +- `type_tuple(element_types)` now uses `map_tdd_to_component` with prefixes like `{:element, 0}`, `{:element, 1}`, etc. +- `type_cons(head_type, tail_type)` now uses `map_tdd_to_component` with prefixes `:head` and `:tail`. +- `type_list_of(element_type)` is completely rewritten to use the new "applicator" node design. + +```elixir +# New list_of constructor +def type_list_of(element_type_id) do + # A list where all elements have this type is the union of + # the empty list and a list that satisfies the property. + applicator_node = Core.make_node({5, :for_all_elements}, element_type_id, type_any(), type_any()) + prop_list = intersect(type_list(), applicator_node) + + # The actual type is "it's empty OR it's a non-empty list with this property" + # This part is subtle. For intersection, the simple `applicator_node` is sufficient. + # A full representation would be `sum(type_empty_list(), intersect(non_empty_list, applicator_node))` + # For now, let's focus on the intersection-friendly form. + intersect(type_list(), applicator_node) +end +``` + +#### Step 4: Update `simplify` +The `simplify` function also becomes more elegant. When it encounters a contextualized variable like `v = {:head, inner_var}`, it can simplify the children by passing the `inner_var` constraint down into a sub-context, which `PredicateLogic` now understands natively. + +--- + +### How the Implementation is Simplified + +1. **Canonicity Guaranteed:** The primary goal is achieved. TDDs will have a single, canonical representation because the variable order is now stable and independent of creation order. `Tdd.intersect(A, B) == Tdd.intersect(B, A)` becomes trivial. + +2. **Drastic Simplification of `PredicateLogic`:** + * **No More Magic Numbers:** The logic no longer has hardcoded knowledge of category numbers (`0`, `1`, `4`, `5`). + * **Logic Reuse:** The same consistency-checking logic is applied at the top level and recursively to every component (`head`, `tail`, `element[i]`). This eliminates huge amounts of redundant, error-prone code. + * **Extensibility:** Adding a new kind of container or context (e.g., map keys/values) becomes a matter of defining a new context prefix, not rewriting the core reasoning engine. + +3. **Correctness of Operations:** The `intersect(list(int), list(pos_int))` problem is solved structurally and elegantly by the new "applicator" node design, without requiring complex, special-cased semantic rules in `simplify`. The generic `apply` algorithm handles it automatically. + +4. **Improved Debugging:** A variable like `{:element, 1, {2, :lt, 10}}` is far more self-describing and human-readable than `{4, :element, 1, {2, :alt, 10}}` was, and vastly better than `{4, :element, 1, }` would have been. + +### Trade-offs + +* **Initial Refactoring Effort:** This is a significant architectural change that touches `Tdd.Core` (to recognize applicator nodes), `Tdd.PredicateLogic`, and all type constructors. +* **Variable Complexity:** The variable tuples themselves become more deeply nested. This is a minor cost for the massive gain in clarity and canonicity. + +In summary, this migration moves the "context" information from an ad-hoc part of the variable's value into a systematic, structural prefix. This allows the semantic reasoning engine (`PredicateLogic`) to become simpler, more general, and recursive, while simultaneously fixing fundamental correctness and canonicity issues with operations on complex types. It is a textbook example of how a better data representation simplifies the algorithms that operate on it. + + +============================================================================== +============================================================================== +============================================================================== +@ functions -> intersections between functions in elixir need to work differently I think - multiple function heads can match on different types of arguments. When a function is applied, we cannot have a single general type for the function, but need to find the part of the intersection that matches the arguments -> and use this function head. +@ polymorphism -> if this approach Youve outlined is only `limited to good` what'd be a state of the art approach ? +============================================================================== +============================================================================== +============================================================================== + +Excellent points. You've correctly identified the nuances of Elixir's multiple function clauses and are pushing for the true state-of-the-art in polymorphism. Let's dive deep into both. + +--- + +### Part 1: Functions in Elixir and Set-Theoretic Types + +You are absolutely right. A single Elixir function name like `my_func` is not a single function type but a **union of function types**, where each clause corresponds to one type in the union. + +Let's say you have: +```elixir +def my_func(x) when is_atom(x), do: :a +def my_func(x) when is_integer(x), do: :i +``` + +This is not a single `fun(any -> atom())`. It is `(fun(atom -> :a)) | (fun(integer -> :i))`. This is often called an **overloaded function** or a **disjoint function union**. + +The TDD system you've designed is *perfectly suited* to represent this! + +#### How it Works with Your TDD Design + +1. **Representing a Single Clause:** Each function clause is a simple function type. + * `def my_func(x) when is_atom(x)` is `fun(atom() -> any())`. Let's call its TDD `F_atom`. + * `def my_func(x) when is_integer(x)` is `fun(integer() -> any())`. Let's call its TDD `F_int`. + +2. **Representing the Whole Function:** The entire `my_func` is the union of these types. + * `Tdd_my_func = Tdd.sum(F_atom, F_int)` + +This model correctly captures the semantics. + +#### Intersection of Overloaded Functions + +Now, what does it mean to intersect two such functions? Let's say we have another function: +```elixir +def other_func(x) when is_integer(x), do: "hello" +def other_func(x) when is_binary(x), do: "world" +``` +This is the type `(fun(integer -> string)) | (fun(binary -> string))`. Let's call its TDD `Tdd_other_func`. + +The intersection `Tdd.intersect(Tdd_my_func, Tdd_other_func)` means: "What is the set of functions that conform to *both* `my_func`'s type signature and `other_func`'s?" + +This is `((fun(atom->any)) | (fun(int->any))) & ((fun(int->string)) | (fun(binary->string)))`. + +Distributing the intersection over the union gives: +* `(fun(atom->any) & fun(int->string))` -> `fun((atom|int) -> (any&string))` +* `(fun(atom->any) & fun(binary->string))` -> `fun((atom|binary) -> (any&string))` +* `(fun(int->any) & fun(int->string))` -> `fun((int|int) -> (any&string))` which simplifies to `fun(int -> string)` +* `(fun(int->any) & fun(binary->string))` -> `fun((int|binary) -> (any&string))` + +The result is a complex union of function types. This is where the simple `fun(A1|A2 -> R1&R2)` meet operation shows its limits. + +A more accurate model for intersection of overloaded functions is to find the **domain of overlap**. A value can be passed to the "intersected function" if and only if it's accepted by *both* original functions. The return type is the intersection of the return types for that specific domain. + +* `my_func` accepts `atom | integer`. +* `other_func` accepts `integer | binary`. +* The overlapping domain is `(atom | integer) & (integer | binary) = integer`. +* For an `integer` input: + * `my_func` returns `any`. + * `other_func` returns `string`. + * The intersection return type is `any & string = string`. +* Therefore, the semantic intersection is `fun(integer -> string)`. + +**How to Implement This with TDDs:** +You would need a specialized `apply_function_intersect(f1_id, f2_id)` function. It cannot be generic. +1. Deconstruct `f1` and `f2` into their union components (e.g., `(fun(A1->R1) | fun(A2->R2))`). This is hard with a TDD representation. +2. For each pair of components `(fun(Ai->Ri))` from `f1` and `(fun(Bj->Sj))` from `f2`: + a. Calculate the domain intersection: `D_ij = intersect(Ai, Bj)`. + b. If `D_ij` is not `none`, calculate the return type intersection: `R_ij = intersect(Ri, Sj)`. + c. The result for this pair is `fun(D_ij -> R_ij)`. +3. The final result is the `sum` of all `fun(D_ij -> R_ij)` from step 2c. + +**Conclusion for Functions:** Your observation is spot on. Elixir functions are unions of types. The TDD can represent this union, but operating on them (like `intersect`) requires highly specialized, non-generic logic that understands the specific semantics of function overloading and variance. The TDD becomes a data structure to represent the argument/return types, but the main algorithm is custom. + +--- + +### Part 2: State-of-the-Art Polymorphism + +Your "limited to good" assessment is fair. The constraint-generation approach is powerful but can be improved. The state-of-the-art revolves around a concept called **Bidirectional Type Checking** and integrating the constraint solver more deeply. + +#### The State-of-the-Art Approach: "Semantic Subtyping" with Bidirectional Checking + +Instead of making the TDD operations (`intersect`, `sum`) generate constraints, we keep them purely about concrete types. Polymorphism is handled by the type checker/inference engine itself, which uses the TDDs as a tool. + +The core algorithm is `is_subtype(sub_id, super_id)`. We redefine it to handle polymorphism. + +Let's call it `check(Value, Type)` and `infer(Expression)`. + +**Key Idea:** +When we check `Value :: Type`, if `Type` is polymorphic (contains free type variables like `a`), we don't try to build a TDD for `list(a)`. Instead, we **check** the value against the type's structure and **gather constraints** on the type variables as we go. + +**Example: Checking `[1, 2, 3] :: list(a)`** + +1. **`check([1, 2, 3], list(a))`** + * The `check` function for `list(a)` first checks that `[1, 2, 3]` is indeed a list. The TDD operation `is_subtype(type_of([1,2,3]), type_list())` passes. + * Now, it must check the elements. It iterates through `[1, 2, 3]`. + * For element `1`: It recursively calls `check(1, a)`. + * For element `2`: It recursively calls `check(2, a)`. + * For element `3`: It recursively calls `check(3, a)`. + +2. **`check(Value, a)` (where `a` is a type variable)** + * This is the crucial step. This function doesn't return `true/false`. It generates a constraint. + * `check(1, a)` infers the type of `1` is `integer()`. It generates the constraint: **`integer <: a`**. + * `check(2, a)` generates **`integer <: a`**. + * `check(3, a)` generates **`integer <: a`**. + +3. **Constraint Solving** + * After checking the whole expression, we have a set of constraints: `{ integer <: a, integer <: a, integer <: a }`. + * We pass this set to a **constraint solver**. The solver finds the "principal type" or the most general solution. + * The solution to `integer <: a` is `a = integer`. (Or more generally, `a` could be `any` or `number`, but `integer` is the tightest bound, which is what we want). + +**Why is this State-of-the-Art?** + +1. **Separation of Concerns:** The TDD engine remains a pure, powerful engine for reasoning about **concrete** set-theoretic types. It does one thing and does it well. The type checker/inference engine handles the separate concern of polymorphism and constraint generation. + +2. **Bidirectionality:** The system has two modes: + * **Inference Mode (`infer`):** "What is the most specific type of this expression?" `infer([1, 2, 3])` would use the TDD `sum` operation to produce `type_list_of(type_int_eq(1) | type_int_eq(2) | type_int_eq(3))`. The TDD engine is perfect for this. + * **Checking Mode (`check`):** "Does this expression conform to this (potentially polymorphic) type?" This is where constraints are generated. + +3. **Higher-Rank Polymorphism:** This approach scales naturally to higher-rank types (e.g., `fun(f :: (a -> a)) -> ...`). When checking an argument against `(a -> a)`, you introduce a *local, scoped* type variable `a` and check that the provided function works for *any* choice of `a`. + +4. **Integration with TDDs:** The TDDs are the "oracle" that the constraint generator consults. + * When solving constraints like `Type1 <: a` and `Type2 <: a`, the solver needs to find the **least upper bound (LUB)** or **join** of `Type1` and `Type2`. This is `Tdd.sum(Type1, Type2)`! + * When solving `a <: Type1` and `a <: Type2`, the solver needs the **greatest lower bound (GLB)** or **meet**. This is `Tdd.intersect(Type1, Type2)`! + +The TDD engine becomes the computational backend for the constraint solver. + +### Summary of State-of-the-Art Design + +* **TDD Engine:** + * Uses the "Contextualized Predicates" design. + * Represents and operates on **concrete (monomorphic)** types ONLY. + * Provides `intersect` (meet/GLB), `sum` (join/LUB), `negate`, and `is_subtype` (for concrete types). + * The engine itself knows nothing about polymorphism. + +* **Type Checker / Inference Engine (The "Brain"):** + * Is built on top of the TDD engine. + * Implements a bidirectional algorithm (`check` and `infer`). + * When it encounters a polymorphic type in `check` mode, it traverses the type's structure and the expression's structure in parallel. + * It uses `infer` to get the concrete type of parts of the expression. + * It generates constraints on type variables (e.g., `Tdd_id_of_int <: a`). + +* **Constraint Solver:** + * Receives a set of constraints from the Type Checker. + * Uses the TDD engine's `sum` and `intersect` operations to solve for the type variables. + * Reports success or a type error if constraints are unsatisfiable (e.g., `integer <: a` and `atom <: a` are generated, so `a` must be `integer | atom`. But if later `a <: integer` is required, this leads to `integer | atom <: integer`, which `is_subtype` will report as false -> contradiction). + +This layered architecture is robust, modular, and mirrors the design of systems like TypeScript, Flow, and other modern typed languages. It lets each component do what it's best at. + +============================================================================== +============================================================================== +============================================================================== +============================================================================== +@ functions -> I don't think what You've outlined I need +``` +def t(int) when is_integer(int), do: :integer +def t(binary) when is_binary(int), do: :binary +def t(other) do: nil +``` +the return types of `t` are 3 separate literal atoms. When someone applies `t(1)` the type of the return should be literal `:integer` +============================================================================== +============================================================================== +============================================================================== +You are absolutely right. My previous explanation was too focused on the general case of function type intersection and didn't fully capture the precise, practical need you've described for Elixir. Your example clarifies the goal perfectly: **type analysis should be able to determine the *exact* return type based on the *exact* input type, respecting Elixir's clause matching rules.** + +This isn't about intersecting two different functions; it's about **specializing a single overloaded function's type for a given input type.** + +Let's design a system that does exactly this. It's a fantastic application of the TDD engine. + +--- + +### The Goal: A `specialize` Function + +What we need is a function with this signature: +`specialize(function_type_id, input_argument_type_id) -> return_type_id` + +Given a TDD for an overloaded function and a TDD for an input argument, it should return the TDD for the corresponding output. + +**Example Usage:** +* `specialize(Tdd_t, Tdd_integer) -> Tdd_literal_integer_atom` +* `specialize(Tdd_t, Tdd_binary) -> Tdd_literal_binary_atom` +* `specialize(Tdd_t, Tdd_atom) -> Tdd_nil` (since `:atom` will match the `other` clause) +* `specialize(Tdd_t, Tdd_int_or_bin) -> Tdd_integer_atom_or_binary_atom` + +### Representing an Overloaded Function + +First, we need a better way to represent the function `t`. As we discussed, it's a union of function types, but a simple TDD sum loses the crucial link between a specific input domain and its specific return type. + +The ideal representation is not a single TDD, but a **list of pairs**, where each pair represents one function clause: + +```elixir +# This is a meta-level data structure, not a single TDD. +function_t_clauses = [ + {Tdd.type_integer(), Tdd.type_atom_literal(:integer)}, # fun(integer -> :integer) + {Tdd.type_binary(), Tdd.type_atom_literal(:binary)}, # fun(binary -> :binary) + {Tdd.type_any(), Tdd.type_atom_literal(nil)} # fun(any -> nil) +] +``` + +**Crucial Rule:** This list must be ordered exactly like Elixir's function clauses. The first match wins. The final `any` clause is the catch-all. + +### The `specialize` Algorithm + +Now, we can implement `specialize(function_clauses, input_arg_type_id)`. + +```elixir +def specialize(function_clauses, input_arg_type_id) do + # We start with the full set of possible inputs we're considering. + # As we find matches, we'll subtract the matched portion from this set. + remaining_input_type = input_arg_type_id + + # This will accumulate the possible return types from all matched clauses. + # We start with `none` because no matches have been found yet. + total_return_type = Tdd.type_none() + + for {clause_input_domain, clause_return_type} <- function_clauses do + # If there are no more possible inputs to match, we can stop early. + if remaining_input_type == Tdd.type_none() do + break + end + + # Step 1: Find the portion of our input that matches this specific clause. + # This is the core TDD operation. + # e.g., if remaining_input is `integer() | atom()` and clause_domain is `integer()`, + # the matching_part is `integer()`. + matching_part = Tdd.intersect(remaining_input_type, clause_input_domain) + + # Step 2: Check if there was any overlap. + if matching_part != Tdd.type_none() do + # If there was a match, the return type for this part is this clause's return type. + # We add it to our total set of possible return types. + total_return_type = Tdd.sum(total_return_type, clause_return_type) + + # Step 3: VERY IMPORTANT - Remove the matched part from the remaining inputs. + # This ensures that a given input type can only match ONE clause (the first one). + # remaining_input = remaining_input - matching_part + # which is equivalent to: remaining_input & ~matching_part + remaining_input_type = Tdd.intersect(remaining_input_type, Tdd.negate(matching_part)) + end + end + + # The final result is the union of all possible return types from the matching clauses. + total_return_type +end +``` + +### Let's Trace the Algorithm + +**Case 1: `specialize(clauses, Tdd.type_int_eq(5))`** + +1. `remaining_input_type` = `int(5)` +2. `total_return_type` = `none` + +3. **Clause 1: `{integer, :integer}`** + * `matching_part` = `intersect(int(5), integer)` -> `int(5)` (since `int(5)` is a subtype of `integer`) + * `matching_part` is not `none`. + * `total_return_type` = `sum(none, :integer)` -> `:integer` + * `remaining_input_type` = `intersect(int(5), negate(int(5)))` -> `none` + +4. Loop sees `remaining_input_type` is `none` and breaks. + +5. **Return:** `Tdd.type_atom_literal(:integer)`. **Correct!** + +**Case 2: `specialize(clauses, Tdd.sum(type_int_eq(10), type_binary()))`** + +1. `remaining_input_type` = `int(10) | binary()` +2. `total_return_type` = `none` + +3. **Clause 1: `{integer, :integer}`** + * `matching_part` = `intersect(int(10)|binary, integer)` -> `int(10)` + * `matching_part` is not `none`. + * `total_return_type` = `sum(none, :integer)` -> `:integer` + * `remaining_input_type` = `intersect(int(10)|binary, negate(int(10)))` -> `binary()` + *(The integer part was "consumed" by the match)* + +4. **Clause 2: `{binary, :binary}`** + * `remaining_input_type` is now `binary()`. + * `matching_part` = `intersect(binary, binary)` -> `binary()` + * `matching_part` is not `none`. + * `total_return_type` = `sum(:integer, :binary)` -> `:integer | :binary` + * `remaining_input_type` = `intersect(binary, negate(binary))` -> `none` + +5. Loop sees `remaining_input_type` is `none` and breaks. + +6. **Return:** `Tdd.sum(type_atom_literal(:integer), type_atom_literal(:binary))`. **Correct!** The type system knows that if you pass in `int(10) | binary()`, the possible return values are `:integer` or `:binary`. + +### Advantages of this Design + +* **Precision:** It perfectly models Elixir's first-match policy for function clauses. +* **Composability:** It's built entirely from the core TDD primitives (`intersect`, `sum`, `negate`, `== type_none()`). You don't need to change the TDD engine itself, only add this higher-level algorithm. +* **Correctness:** It correctly handles partial and overlapping input types, producing a precise union of possible return types. +* **Handles Guards:** The `when` guards in Elixir are just part of the domain type. `def f(x) when is_integer(x) and x > 0` simply means the domain is `Tdd.intersect(type_integer(), type_int_gt(0))`. The model handles this for free. + +This `specialize` function is precisely what's needed for practical, sound type analysis of Elixir code. It bridges the gap between the general, set-theoretic world of the TDDs and the specific, ordered-clause semantics of the language.============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +alright, would that play nice with out approach to polymorphism ? ============================================================================== +============================================================================== +============================================================================== +Excellent question. Let's analyze how this new, precise `specialize` function for overloaded functions interacts with the state-of-the-art bidirectional approach to polymorphism we discussed. + +The short answer is: **Yes, it plays together beautifully.** They are complementary parts of a complete type system, each handling a different aspect of the problem. + +Here's the detailed breakdown of how they work in concert. + +--- + +### The Roles of Each Component + +Let's recap the roles in our state-of-the-art system: + +1. **TDD Engine:** The "calculator" for **concrete** types. Knows `intersect`, `sum`, `negate`. It is pure and dumb about polymorphism and function application. + +2. **`specialize` Algorithm:** The "Elixir function expert." It knows how to calculate the return type of an overloaded function for a given **concrete** input type. It uses the TDD engine as its calculator. + +3. **Bidirectional Type Checker (`check`/`infer`):** The "brain" of the operation. It handles polymorphism, generates constraints, and orchestrates the other two components. + +### How They Interact: A Complete Trace + +Let's trace a complex, polymorphic example from end to end. + +**The Code to Analyze:** +```elixir +# The overloaded function `t` from before. +def t(int) when is_integer(int), do: :integer +def t(binary) when is_binary(binary), do: :binary +def t(other), do: nil + +# A polymorphic function `process` that uses `t`. +# @spec process(list(a)) :: list(return_type_of_t_for_a) +def process(list) do + Enum.map(list, &t/1) +end + +# The specific call we want to type-check. +process([1, "hello"]) +``` + +The goal is to infer the return type of `process([1, "hello"])`. The expected result should be `list(:integer | :binary)`. + +**Step-by-Step Execution:** + +1. **`infer(process([1, "hello"]))`** + * The type checker sees a function call. It needs to know the type of `process` and the type of its argument `[1, "hello"]`. + * It first calls `infer([1, "hello"])`. + * The TDD engine is used here. `infer(1)` is `type_int_eq(1)`. `infer("hello")` is `type_string_literal("hello")`. + * The inferred type of the list is `list_of(sum(type_int_eq(1), type_string_literal("hello")))`. Let's call this concrete input list type `T_InputList`. + +2. **Lookup Type of `process`** + * The checker looks up the polymorphic type spec for `process`: `fun(list(a) -> list(return_type_of_t_for_a))`. + * This type signature contains a free type variable, `a`. It also contains a *dependent type* in the return signature. We will model this as a constraint. The type is `fun(list(a) -> b) where b = list(specialize(t, a))`. + +3. **Unification / Constraint Generation** + * The checker now has to match the call `process(T_InputList)` with the signature `fun(list(a) -> b)`. + * This triggers `check(T_InputList, list(a))`. + * As we designed before, this generates a constraint. `T_InputList` must be a subtype of `list(a)`. + * This implies that the *elements* of `T_InputList` must be a subtype of `a`. + * The element type of `T_InputList` is `sum(type_int_eq(1), type_string_literal("hello"))`. + * So, the first constraint generated is: **`C1: sum(type_int_eq(1), type_string_literal("hello")) <: a`**. + +4. **Solving for the Return Type** + * The signature tells us the return type `b` depends on `a`. We have the constraint `b = list(specialize(t, a))`. + * The constraint solver now takes over. It has one job: find the most specific types for `a` and `b` that satisfy the constraints. + * From `C1`, the most specific solution for `a` is `a = sum(type_int_eq(1), type_string_literal("hello"))`. Let's call this `T_a`. + +5. **Invoking the `specialize` Algorithm** + * Now the solver must compute `b`. It uses the second constraint: `b = list(specialize(t, T_a))`. + * This is the moment of contact! The high-level polymorphic checker **invokes our `specialize` function**. + * It calls `specialize(function_t_clauses, T_a)`. + * `T_a` is `int(1) | string("hello")`. + * The trace proceeds exactly as in my previous answer: + * The `integer` clause matches the `int(1)` part, adding `:integer` to the return union. + * The `binary` clause matches the `string("hello")` part (assuming string is a binary), adding `:binary` to the return union. + * The result from `specialize` is `sum(type_atom_literal(:integer), type_atom_literal(:binary))`. Let's call this `T_return_elements`. + +6. **Final Result Construction** + * The solver now knows `b = list(T_return_elements)`. + * The final inferred type for `process([1, "hello"])` is `list(sum(type_atom_literal(:integer), type_atom_literal(:binary)))`. + +**The result is `list(:integer | :binary)`. Success!** + +### How it "Plays Nice" - The Synergy + +* **Orthogonality:** The `specialize` function provides a key semantic capability (how to resolve overloaded functions) without needing to know anything about polymorphism. It operates on concrete TDDs. The bidirectional checker handles polymorphism without needing to know the specific rules of Elixir function resolution; it just needs a way to ask "what happens when I call this function with this type?" +* **Pluggable Semantics:** The `specialize` algorithm is a "semantic oracle" for the polymorphic type checker. The checker generates a concrete question (`specialize(t, T_a)`), and `specialize` provides a concrete answer by using the TDD engine. +* **No Leaky Abstractions:** The TDD engine remains pure. The `specialize` function contains the domain-specific logic for Elixir. The `check`/`infer` engine contains the domain-specific logic for polymorphism. They are clean, well-defined layers. +* **Dependent Types:** This interaction is a form of a dependent type system, where the return type depends on the *value* (or in this case, the *type*) of an input argument. The combination of a polymorphic checker and the `specialize` function is exactly what's needed to model this. + +In conclusion, not only do they play nice, they are essential partners. The polymorphic checker provides the framework for handling type variables, and the `specialize` function provides the concrete, language-specific meaning required to resolve the constraints generated by that framework.============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== +============================================================================== diff --git a/test1.exs b/test1.exs index 7f0b30a..cdd613b 100644 --- a/test1.exs +++ b/test1.exs @@ -220,14 +220,10 @@ 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. + It supports three kinds of nodes: + - Terminals (true/false) + - Test Nodes: {variable, yes_id, no_id, dc_id} + - Applicator Nodes: {{:all_elements}, element_type_id} """ # --- Terminal Node IDs --- @@ -244,7 +240,8 @@ defmodule Tdd.Core do # --- State Management --- def init do - Process.put(:tdd_nodes, %{}) + Process.put(:tdd_test_nodes, %{}) + Process.put(:tdd_applicator_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, %{}) @@ -253,7 +250,8 @@ defmodule Tdd.Core do defp get_state do %{ - nodes: Process.get(:tdd_nodes, %{}), + test_nodes: Process.get(:tdd_test_nodes, %{}), + applicator_nodes: Process.get(:tdd_applicator_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, %{}) @@ -263,7 +261,8 @@ defmodule Tdd.Core do 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_test_nodes, new_state.test_nodes) + Process.put(:tdd_applicator_nodes, new_state.applicator_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) @@ -271,8 +270,6 @@ defmodule Tdd.Core do 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] @@ -281,33 +278,22 @@ defmodule Tdd.Core do 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 == no_id && yes_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] + if Map.has_key?(state.test_nodes, node_tuple) do + state.test_nodes[node_tuple] else new_id = state.next_id update_state(%{ - nodes: Map.put(state.nodes, node_tuple, new_id), + test_nodes: Map.put(state.test_nodes, node_tuple, new_id), node_by_id: Map.put(state.node_by_id, new_id, node_tuple), next_id: new_id + 1 }) @@ -317,83 +303,28 @@ defmodule Tdd.Core do 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 + def make_applicator_node(element_type_id) do state = get_state() - cache_key = {op_name, Enum.sort([u1_id, u2_id])} + node_tuple = {{:all_elements}, element_type_id} - cond do - Map.has_key?(state.op_cache, cache_key) -> - state.op_cache[cache_key] + if Map.has_key?(state.applicator_nodes, node_tuple) do + state.applicator_nodes[node_tuple] + else + new_id = state.next_id - 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 + update_state(%{ + applicator_nodes: Map.put(state.applicator_nodes, node_tuple, new_id), + node_by_id: Map.put(state.node_by_id, new_id, node_tuple), + next_id: new_id + 1 + }) - 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 + new_id end end end defmodule Tdd.PredicateLogic do - @moduledoc "..." + @moduledoc "Reasons about base predicates within a single context." alias Tdd.Variables, as: V @primary_types [:is_atom, :is_tuple, :is_integer, :is_list] @@ -401,12 +332,13 @@ defmodule Tdd.PredicateLogic do antecedent = {{0, type}, true} consequents = - for other_type <- @primary_types, - other_type != type, - do: {{{0, other_type}, false}} + for other_type <- @primary_types, other_type != type do + {{{0, other_type}, false}} + end {antecedent, consequents} end) + @rules @primary_type_exclusivity_rules def saturate(assumptions) do @@ -424,8 +356,6 @@ defmodule Tdd.PredicateLogic do 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 @@ -442,16 +372,30 @@ defmodule Tdd.PredicateLogic 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 + check_integer_ranges(facts) == :contradiction -> :contradiction true -> {:ok, facts} end end + def check_implication(predicate, constraints) do + case saturate(Map.put(constraints, predicate, true)) do + :contradiction -> + false + + _ -> + case saturate(Map.put(constraints, predicate, false)) do + :contradiction -> true + _ -> :unknown + end + end + end + + # --- PRIVATE HELPERS --- defp check_atom_values(facts) do trues = Enum.reduce(facts, MapSet.new(), fn - {{1, :value, atom_val}, true}, acc -> MapSet.put(acc, atom_val) + {{1, :value, v}, true}, acc -> MapSet.put(acc, v) _, acc -> acc end) @@ -461,7 +405,7 @@ defmodule Tdd.PredicateLogic do defp check_tuple_values(facts) do trues = Enum.reduce(facts, MapSet.new(), fn - {{4, :size, size_val}, true}, acc -> MapSet.put(acc, size_val) + {{4, :size, v}, true}, acc -> MapSet.put(acc, v) _, acc -> acc end) @@ -469,27 +413,14 @@ defmodule Tdd.PredicateLogic do end defp check_list_structure(facts) do - is_assumed_empty = Map.get(facts, V.v_list_is_empty()) == true + is_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) + has_head_tail = + Enum.any?(facts, fn {var, _} -> match?({5, :head, _}, var) or match?({5, :tail, _}, var) end) - if has_head_or_tail_pred, do: :contradiction, else: :ok - else - :ok - end + if is_empty and has_head_tail, do: :contradiction, else: :ok 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 @@ -498,234 +429,6 @@ defmodule Tdd.PredicateLogic do end end - @doc """ - A general-purpose reasoner that uses the main `saturate` function. - It determines if a predicate is implied true or false by a set of constraints - by checking if adding its opposite leads to a contradiction. - """ - defp _reason_by_contradiction(predicate, constraints) do - # Is `predicate` implied TRUE? (i.e., is `constraints AND NOT predicate` a contradiction?) - cond do - saturate(Map.put(constraints, predicate, false)) == :contradiction -> - true - - # Is `predicate` implied FALSE? (i.e., is `constraints AND predicate` a contradiction?) - saturate(Map.put(constraints, predicate, true)) == :contradiction -> - false - - true -> - :unknown - end - end - - @doc """ - Checks if a `predicate` is logically implied (or contradicted) by a - set of `constraints`. - """ - def check_implication(predicate, constraints) do - case predicate do - # --- NEW HANDLER for primary type predicates --- - {0, _} -> - _reason_by_contradiction(predicate, constraints) - - # --- EXISTING BASE CASES --- - {1, :value, _} -> - _atom_implication(predicate, constraints) - - {2, _, _} -> - _integer_implication(predicate, constraints) - - {4, :size, _} -> - _tuple_size_implication(predicate, constraints) - - # --- EXISTING RECURSIVE CASES --- - {4, :element, index, inner_predicate} -> - element_constraints = - gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1)) - - check_implication(inner_predicate, element_constraints) - - {5, :head, inner_predicate} -> - head_constraints = - gather_local_constraints(constraints, &match?({5, :head, _}, &1)) - - check_implication(inner_predicate, head_constraints) - - {5, :tail, inner_predicate} -> - tail_constraints = - gather_local_constraints(constraints, &match?({5, :tail, _}, &1)) - - check_implication(inner_predicate, tail_constraints) - - # --- 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 @@ -785,25 +488,12 @@ defmodule Tdd.PredicateLogic do 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 + def init_tdd_system, do: Core.init() - # --- 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} @@ -814,506 +504,247 @@ defmodule Tdd do 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_tuple_elem(i, base_var), do: {4, :element, i, base_var} 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} + def v_list_head(base_var), do: {5, :head, base_var} + def v_list_tail(base_var), do: {5, :tail, base_var} end - # --- Type Constructors (Completed) --- + # --- Type Constructors --- 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: intersect(type_atom(), Core.make_node(V.v_atom_eq(val), type_any(), type_none(), type_none())) + def type_int_eq(n), do: intersect(type_integer(), Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none())) + def type_int_lt(n), do: intersect(type_integer(), Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none())) + def type_int_gt(n), do: intersect(type_integer(), Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none())) - 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_empty_tuple, do: intersect(type_tuple(), Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none())) + def type_tuple_sized_any(size), do: intersect(type_tuple(), Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none())) 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. + base_type = type_tuple_sized_any(length(element_type_ids)) 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. + elem_constraint_tdd = prefix_tdd_vars(elem_type_id, &V.v_tuple_elem(index, &1)) 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_empty_list, do: intersect(type_list(), Core.make_node(V.v_list_is_empty(), type_any(), type_none(), type_none())) 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) + head_constraint = prefix_tdd_vars(head_type_id, &V.v_list_head/1) + tail_constraint = prefix_tdd_vars(tail_type_id, &V.v_list_tail/1) + 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) + applicator_node = Core.make_applicator_node(element_type_id) + # A `list_of(T)` is a list that is also constrained by this applicator. + intersect(type_list(), applicator_node) end end # --- High-Level Operations --- - def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{}) |> simplify(%{}) - def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) |> simplify(%{}) - - def negate(u_id) do - negate_recursive(u_id, %{}) - |> simplify(%{}) - end - - def is_subtype(sub_id, super_id) do - # A <: B <=> A & ~B == none - IO.inspect("sub_id in is_subtype") - Tdd.print_tdd(sub_id) - 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 + 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, %{}) + def is_subtype(sub_id, super_id), do: intersect(sub_id, negate(super_id)) == type_none() # --- 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()} - + defp do_op(op_name, u1_id, u2_id) do + cache_key = {op_name, Enum.sort([u1_id, u2_id])} if cached = Core.get_op_cache(cache_key) do cached else - res = compute_op(op_name, u1_id, u2_id, constraints) + # Final simplification is now part of the operation itself + res = dispatch_op(op_name, u1_id, u2_id, %{}) |> simplify(%{}) Core.put_op_cache(cache_key, res) res end end - defp compute_op(op_name, u1_id, u2_id, constraints) do - case PredicateLogic.saturate(constraints) do - :contradiction -> - # This path is impossible. For an intersection, the result is the empty set. - handle_contradiction(op_name) - - {:ok, saturated_constraints} -> - # REMOVED: No more pre-simplifying inputs here. - # We pass the original IDs and the full context to dispatch_op. - n1 = Core.get_node(u1_id) - n2 = Core.get_node(u2_id) - dispatch_op(op_name, u1_id, n1, u2_id, 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`. - def simplify(id, constraints) do - # Memoization is critical for performance - cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()} - - if cached = Core.get_op_cache(cache_key) do - cached - else - # We will call saturate at the beginning of the operation (in compute_op), - # so we can assume constraints are consistent here. - res = compute_simplify(id, constraints) - Core.put_op_cache(cache_key, res) - res - end - end - - defp compute_simplify(id, constraints) do - case Core.get_node(id) do - true -> - type_any() - - false -> - type_none() - - {var, y, n, d} -> - contradiction = - case var do - {5, :head, head_predicate} -> - all_elements_type_id = - Enum.find_value(constraints, fn - {{5, :all_elements, type_id}, true} -> type_id - _ -> nil - end) - - if all_elements_type_id do - head_type = predicate_to_tdd(head_predicate) - # Is the required head type compatible with the element type? - intersect(head_type, all_elements_type_id) == type_none() - else - false - end - - {5, :tail, tail_predicate} -> - all_elements_type_id = - Enum.find_value(constraints, fn - {{5, :all_elements, type_id}, true} -> type_id - _ -> nil - end) - - if all_elements_type_id do - tail_type = predicate_to_tdd(tail_predicate) - # The tail must be a list of the element type. - required_tail_type = type_list_of(all_elements_type_id) - intersect(tail_type, required_tail_type) == type_none() - else - false - end - - _ -> - false - end - - if contradiction do - # The 'yes' branch is impossible. The node simplifies to its 'no' branch. - simplify(n, constraints) - else - case Map.get(constraints, var) do - true -> - simplify(y, constraints) - - false -> - simplify(n, constraints) - - :dc -> - simplify(d, constraints) - - nil -> - case PredicateLogic.check_implication(var, constraints) do - true -> - simplify(y, constraints) - - false -> - simplify(n, constraints) - - :unknown -> - res_y = simplify(y, Map.put(constraints, var, true)) - res_n = simplify(n, Map.put(constraints, var, false)) - res_d = simplify(d, Map.put(constraints, var, :dc)) - Core.make_node(var, res_y, res_n, res_d) - end - end - end - end - end - - defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do - # --- Step 1: Simplify the current nodes under the given constraints. --- - # This is the crucial change. We simplify first, before doing anything else. + defp dispatch_op(op_name, u1_id, u2_id, constraints) do s1_id = simplify(u1_id, constraints) s2_id = simplify(u2_id, constraints) - # If simplification resolved either to a terminal, we can take a shortcut. - if Core.terminal_id?(s1_id) or Core.terminal_id?(s2_id) do - apply_terminals(op_name, s1_id, s2_id) - else - # --- Step 2: Get details of the *simplified* nodes and proceed. --- - sn1 = Core.get_node(s1_id) - sn2 = Core.get_node(s2_id) - - {var1, y1, n1_child, d1} = sn1 - {var2, y2, n2_child, d2} = sn2 - top_var = Enum.min([var1, var2]) - - # Determine children for the recursive call based on top_var. - call_y1 = if(var1 == top_var, do: y1, else: s1_id) - call_y2 = if(var2 == top_var, do: y2, else: s2_id) - call_n1 = if(var1 == top_var, do: n1_child, else: s1_id) - call_n2 = if(var2 == top_var, do: n2_child, else: s2_id) - call_d1 = if(var1 == top_var, do: d1, else: s1_id) - call_d2 = if(var2 == top_var, do: d2, else: s2_id) - - # --- Step 3: Recurse with the original do_op entry point --- - 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 apply_terminals(op_name, id1, id2) do - lambda = op_lambda(op_name) - n1 = Core.get_node(id1) - n2 = Core.get_node(id2) - - # If both are terminals, just apply the op. - if Core.terminal_id?(id1) and Core.terminal_id?(id2) do - if lambda.(n1, n2), do: type_any(), else: type_none() - else - # If only one is a terminal, we must recurse on the other's children. - # This ensures correctness for operations like `A & true -> A`. - non_terminal_id = if(Core.terminal_id?(id1), do: id2, else: id1) - terminal_id = if(Core.terminal_id?(id1), do: id1, else: id2) - {var, y, n, d} = Core.get_node(non_terminal_id) - - res_y = apply_terminals(op_name, y, terminal_id) - res_n = apply_terminals(op_name, n, terminal_id) - res_d = apply_terminals(op_name, d, terminal_id) - Core.make_node(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 + cond do + s1_id == s2_id -> s1_id + op_name == :intersect and (s1_id == type_none() or s2_id == type_none()) -> type_none() + op_name == :intersect and s1_id == type_any() -> s2_id + op_name == :intersect and s2_id == type_any() -> s1_id + op_name == :sum and (s1_id == type_any() or s2_id == type_any()) -> type_any() + op_name == :sum and s1_id == type_none() -> s2_id + op_name == :sum and s2_id == type_none() -> s1_id 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) + n1 = Core.get_node(s1_id) + n2 = Core.get_node(s2_id) + handle_op(op_name, s1_id, n1, s2_id, n2, constraints) end end - @doc """ - Converts a single predicate variable into a full TDD type. - This is the key to comparing predicates with other TDD types. - """ - defp predicate_to_tdd(predicate) do - # Memoize for performance, as this might be called repeatedly. - cache_key = {:predicate_to_tdd, predicate} + # --- RENAMED AND CORRECTED DISPATCHER --- + defp handle_op(op_name, s1_id, n1, s2_id, n2, constraints) do + # IO.inspect({op_name, s1_id, s2_id}, label: "HANDLE_OP") + case {n1, n2} do + # Case 1: The key logic for two `list_of` types. This is a terminal case for the recursion. + {{{_app = :all_elements}, t1_id}, {{_app, _}, t2_id}} -> + op_fun = if op_name == :intersect, do: &intersect/2, else: &sum/2 + result_element_type = op_fun.(t1_id, t2_id) + # We must return the *full* `list_of` type, which is `list & applicator` + if result_element_type == type_none() do + type_empty_list() + else + type_list_of(result_element_type) + end + # Case 2: Any other combination falls through to the robust Shannon expansion. + _ -> + shannon_expand(op_name, s1_id, n1, s2_id, n2, constraints) + end + end + + defp handle_applicators_or_expand(op_name, s1_id, n1, s2_id, n2, constraints) do + case {n1, n2} do + {{{_app = :all_elements}, t1_id}, {{_app, _}, t2_id}} -> + op_fun = if op_name == :intersect, do: &intersect/2, else: &sum/2 + result_element_type = op_fun.(t1_id, t2_id) + type_list_of(result_element_type) + + # All other combinations (Test/Test, App/Test, Test/App) fall through to expansion. + _ -> + shannon_expand(op_name, s1_id, n1, s2_id, n2, constraints) + end + end + + defp get_var_from_node({var, _, _, _}), do: var + defp get_var_from_node(other_node) do + IO.inspect(other_node,label: "GET_VAR_FROM_OTHER_NODE") + :infinity # Terminals and applicators sort last + end + +defp shannon_expand(op_name, s1_id, n1, s2_id, n2, constraints) do + var1 = get_var_from_node(n1) + var2 = get_var_from_node(n2) + + top_var = Enum.min_by([var1, var2], fn + :infinity -> {1, nil} + var -> {0, var} + end) + + if top_var == :infinity, do: raise("shannon_expand called with two non-test nodes") + + {_, y1, n1_child, d1} = if var1 == top_var, do: n1, else: {nil, s1_id, s1_id, s1_id} + {_, y2, n2_child, d2} = if var2 == top_var, do: n2, else: {nil, s1_id, s1_id, s1_id} + + res_y = dispatch_op(op_name, y1, y2, Map.put(constraints, top_var, true)) + res_n = dispatch_op(op_name, n1_child, n2_child, Map.put(constraints, top_var, false)) + res_d = dispatch_op(op_name, d1, d2, Map.put(constraints, top_var, :dc)) + + Core.make_node(top_var, res_y, res_n, res_d) + end + + + defp negate_recursive(id, constraints) do + cache_key = {:negate, id, Map.to_list(constraints) |> Enum.sort()} + if cached = Core.get_op_cache(cache_key) do + cached + else + s_id = simplify(id, constraints) + res = + case Core.get_node(s_id) do + true -> type_none() + false -> type_any() + {{:all_elements}, t_id} -> + sum(negate(type_list()), type_list_of(negate(t_id))) + {var, y, n, d} -> + res_y = negate_recursive(y, Map.put(constraints, var, true)) + res_n = negate_recursive(n, Map.put(constraints, var, false)) + res_d = negate_recursive(d, Map.put(constraints, var, :dc)) + Core.make_node(var, res_y, res_n, res_d) + end + Core.put_op_cache(cache_key, res) + res + end + end + + def simplify(id, constraints) do + cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()} if cached = Core.get_op_cache(cache_key) do cached else res = - case predicate do - {0, :is_atom} -> type_atom() - {0, :is_tuple} -> type_tuple() - {0, :is_integer} -> type_integer() - {0, :is_list} -> type_list() - {1, :value, val} -> type_atom_literal(val) - {2, :beq, n} -> type_int_eq(n) - {2, :alt, n} -> type_int_lt(n) - {2, :cgt, n} -> type_int_gt(n) - {4, :size, n} -> type_tuple_sized_any(n) - {5, :is_empty} -> type_empty_list() - # A head/tail predicate implies the value is a list AND has that head/tail. - # The inner predicate is what we care about for the type check. - {5, :head, inner_p} -> predicate_to_tdd(inner_p) - {5, :tail, inner_p} -> predicate_to_tdd(inner_p) - {5, :all_elements, type_id} -> type_list_of(type_id) - # A tuple element predicate is about the element, not the tuple itself. - {4, :element, _, inner_p} -> predicate_to_tdd(inner_p) - # Fallback for unknown/complex predicates: assume they can be anything. - _ -> type_any() + case Core.get_node(id) do + true -> type_any() + false -> type_none() + # Applicators and terminals are already simple + {{:all_elements}, _} -> id + # Now, it must be a test node + {var, y, n, d} -> + case PredicateLogic.check_implication(var, constraints) do + true -> simplify(y, constraints) + false -> simplify(n, constraints) + :unknown -> + res_y = simplify(y, Map.put(constraints, var, true)) + res_n = simplify(n, Map.put(constraints, var, false)) + res_d = simplify(d, Map.put(constraints, var, :dc)) + Core.make_node(var, res_y, res_n, res_d) + end + end + Core.put_op_cache(cache_key, res) + res + end + end + + defp prefix_tdd_vars(tdd_id, prefix_fun) do + cache_key = {:prefix, tdd_id, inspect(prefix_fun)} + if cached = Core.get_op_cache(cache_key) do + cached + else + res = + case Core.get_node(tdd_id) do + true -> + type_any() + false -> + type_none() + {{:all_elements}, _} -> + raise "Cannot prefix a TDD containing an applicator node" + {var, y, n, d} -> + new_var = prefix_fun.(var) + res_y = prefix_tdd_vars(y, prefix_fun) + res_n = prefix_tdd_vars(n, prefix_fun) + res_d = prefix_tdd_vars(d, prefix_fun) + Core.make_node(new_var, res_y, res_n, res_d) end - Core.put_op_cache(cache_key, res) res 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}") + 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) + {{:all_elements}, elem_id} -> + IO.puts("#{prefix} Element Type ->"); print_tdd(elem_id, indent + 1) + _ -> :ok end end end @@ -2084,37 +1515,32 @@ defmodule AdhocTest do def run(test_fn) do # --- 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) + print_tdd(t_list_of_int) + print_tdd(t_list_of_pos_int) # --- 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)) - intersect4 = intersect(t_list_of_int, t_list_one_int) - IO.inspect("first_subtype") - a = is_subtype(intersect4, t_list_one_int) - IO.inspect("second_subtype") - b = is_subtype(t_list_one_int, intersect4) - test_fn.("list(integer) & [5] == [5]", true, a == b) + intersect1 = intersect(t_list_of_int, t_list_of_pos_int) + print_tdd(intersect1) + print_tdd(14) + print_tdd(16) + + test_fn.( + "(list(int) & list(pos_int)) == list(pos_int)", + true, + intersect1 == t_list_of_pos_int + ) end end -# test_all.() +test_all.() # IntegerTests.run(test) # TupleTests.run(test) # ListTests.run(test) # ListOfTests.run(test) -AdhocTest.run(test) +# AdhocTest.run(test)