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