1301 lines
48 KiB
Elixir
1301 lines
48 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.
|
||
"""
|
||
|
||
######################## TDD FOR SET-THEORETIC TYPES (v2 Path Edition) ########################
|
||
#
|
||
# 0. High-level summary ––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
|
||
#
|
||
# • Each decision-node variable is a **path** - a list of **steps** that describe how to
|
||
# reach a primitive predicate inside a value.
|
||
#
|
||
# [
|
||
# {:tag, :is_tuple}, # primary discriminator
|
||
# {:field, 0}, # tuple element 0
|
||
# {:primitive, {:value_eq, lit(:foo)}} # primitive test on that element
|
||
# ]
|
||
#
|
||
# • **Global order** is Erlang term ordering on the path list (lexicographic).
|
||
# Canonicality proofs need no extra machinery.
|
||
#
|
||
# • **Step alphabet (finite):**
|
||
# {:tag, primary_atom}
|
||
# {:field, index} – tuple element
|
||
# {:head} | {:tail} – list
|
||
# {:key, lit_id} | {:has_key, lit_id} – map predicates
|
||
# {:primitive, primitive_test}
|
||
# {:typevar, var_atom}
|
||
#
|
||
# • Literals are interned to small integers via `Tdd.Path.lit/1`. No runtime node-IDs ever
|
||
# appear in a variable key.
|
||
#
|
||
# • Everything else (hash-consing, operations, tests) works unchanged.
|
||
#
|
||
# ----------------------------------------------------------------------------------------------
|
||
#
|
||
#
|
||
|
||
defmodule Tdd.Path do
|
||
@moduledoc """
|
||
Helper for building and analysing **path-based predicate keys**.
|
||
|
||
A *path* is a list of *steps* (tuples). Erlang term ordering on the list is
|
||
the global order required for canonical TDDs.
|
||
"""
|
||
|
||
# -- Literal interning -------------------------------------------------------
|
||
|
||
@lit_table :tdd_literal_table
|
||
|
||
def start_link, do: :ets.new(@lit_table, [:named_table, :set, :public])
|
||
|
||
@doc "Return a stable small integer for any literal (atom/int/binary/etc.)"
|
||
def lit(x) do
|
||
case :ets.lookup(@lit_table, x) do
|
||
[{^x, id}] ->
|
||
id
|
||
|
||
[] ->
|
||
id = :erlang.unique_integer([:positive, :monotonic])
|
||
:ets.insert(@lit_table, {x, id})
|
||
id
|
||
end
|
||
end
|
||
|
||
# -- Step constructors -------------------------------------------------------
|
||
|
||
def tag(t), do: [{:tag, t}]
|
||
def is_atom, do: tag(:is_atom)
|
||
def is_tuple, do: tag(:is_tuple)
|
||
def is_integer, do: tag(:is_integer)
|
||
def is_list, do: tag(:is_list)
|
||
|
||
def value_eq(val), do: [{:primitive, {:value_eq, lit(val)}}]
|
||
def int_interval({lo, hi}), do: [{:primitive, {:interval, :int, {lo, hi}}}]
|
||
|
||
def tuple_size_eq(n),
|
||
do: [{:tag, :is_tuple}, {:primitive, {:length, :tuple, n}}]
|
||
|
||
def tuple_field(i, inner_path),
|
||
do: [{:tag, :is_tuple}, {:field, i} | inner_path]
|
||
|
||
def list_is_empty, do: [{:tag, :is_list}, {:primitive, {:length, :list, 0}}]
|
||
def list_head(inner), do: [{:tag, :is_list}, {:head} | inner]
|
||
def list_tail(inner), do: [{:tag, :is_list}, {:tail} | inner]
|
||
def list_all(inner_tid), do: [{:tag, :is_list}, {:primitive, {:all_elements, inner_tid}}]
|
||
|
||
# Type variables
|
||
def typevar(v), do: [{:typevar, v}]
|
||
|
||
# -- Path inspection utilities ----------------------------------------------
|
||
|
||
def primary_tag([{:tag, t} | _]), do: t
|
||
def primary_tag(_), do: :unknown
|
||
|
||
def primitive([{:primitive, p}]), do: p
|
||
def primitive([_ | rest]), do: primitive(rest)
|
||
def primitive(_), do: nil
|
||
|
||
def starts_with?(path, prefix), do: Enum.take(path, length(prefix)) == prefix
|
||
|
||
def pretty(path) do
|
||
path
|
||
|> Enum.map(&step_to_string/1)
|
||
|> Enum.join("/")
|
||
end
|
||
|
||
defp step_to_string({:tag, t}), do: Atom.to_string(t)
|
||
defp step_to_string({:field, i}), do: "[#{i}]"
|
||
defp step_to_string({:head}), do: "head"
|
||
defp step_to_string({:tail}), do: "tail"
|
||
defp step_to_string({:typevar, v}), do: "var(#{v})"
|
||
defp step_to_string({:primitive, p}), do: inspect(p)
|
||
defp step_to_string(other), do: inspect(other)
|
||
end
|
||
|
||
defmodule Tdd.Variables do
|
||
@moduledoc false
|
||
alias Tdd.Path
|
||
|
||
# Primary tags
|
||
def v_is_atom, do: Path.is_atom()
|
||
def v_is_tuple, do: Path.is_tuple()
|
||
def v_is_integer, do: Path.is_integer()
|
||
def v_is_list, do: Path.is_list()
|
||
|
||
# Atom predicates
|
||
def v_atom_eq(a), do: Path.is_atom() ++ Path.value_eq(a)
|
||
|
||
# Integer predicates (encode eq/lt/gt via intervals)
|
||
def v_int_eq(n), do: Path.is_integer() ++ Path.int_interval({n, n})
|
||
def v_int_lt(n), do: Path.is_integer() ++ Path.int_interval({:neg_inf, n - 1})
|
||
def v_int_gt(n), do: Path.is_integer() ++ Path.int_interval({n + 1, :pos_inf})
|
||
|
||
# Tuple predicates
|
||
def v_tuple_size_eq(n), do: Path.tuple_size_eq(n)
|
||
|
||
def v_tuple_elem_pred(i, inner_var_path),
|
||
do: Path.tuple_field(i, inner_var_path)
|
||
|
||
# List predicates
|
||
def v_list_is_empty, do: Path.list_is_empty()
|
||
def v_list_head_pred(inner), do: Path.list_head(inner)
|
||
def v_list_tail_pred(inner), do: Path.list_tail(inner)
|
||
def v_list_all_elements_are(tid), do: Path.list_all(tid)
|
||
end
|
||
|
||
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
|
||
if yes_id == no_id and no_id == dc_id do
|
||
yes_id
|
||
else
|
||
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, res_d)
|
||
|
||
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 false
|
||
alias Tdd.Path
|
||
alias Tdd.Variables, as: V
|
||
|
||
# 1. Mutual exclusivity of primary tags
|
||
@primary [:is_atom, :is_tuple, :is_integer, :is_list]
|
||
@primary_pairs for a <- @primary, b <- @primary, a < b, do: {a, b}
|
||
|
||
# ------------ public API ----------------------------------------------------
|
||
|
||
def saturate(facts) do
|
||
with {:ok, s} <- static_exclusions(facts),
|
||
:ok <- further_checks(s) do
|
||
{:ok, s}
|
||
else
|
||
_ -> :contradiction
|
||
end
|
||
end
|
||
|
||
def check_implication(var, constraints) do
|
||
case {Path.primary_tag(var), Path.primitive(var)} do
|
||
{:is_atom, {:value_eq, id}} ->
|
||
atom_implication(id, constraints)
|
||
|
||
{:is_tuple, {:length, :tuple, n}} ->
|
||
tuple_size_implication(n, constraints)
|
||
|
||
{:is_integer, {:interval, :int, intv}} ->
|
||
int_implication(intv, constraints)
|
||
|
||
_ ->
|
||
:unknown
|
||
end
|
||
end
|
||
|
||
# ------------ static exclusions --------------------------------------------
|
||
|
||
defp static_exclusions(facts) do
|
||
Enum.reduce_while(@primary_pairs, {:ok, facts}, fn {a, b}, {:ok, acc} ->
|
||
v_a = V.v_is_atom() |> path_with_tag(a)
|
||
v_b = V.v_is_atom() |> path_with_tag(b)
|
||
|
||
case {Map.get(acc, v_a), Map.get(acc, v_b)} do
|
||
{true, true} -> {:halt, :contradiction}
|
||
_ -> {:cont, {:ok, acc}}
|
||
end
|
||
end)
|
||
end
|
||
|
||
# helper
|
||
defp path_with_tag(_sample, tag), do: [{:tag, tag}]
|
||
|
||
# ------------ fine-grained checks ------------------------------------------
|
||
|
||
defp further_checks(facts) do
|
||
cond do
|
||
atom_val_conflict?(facts) -> :contradiction
|
||
tuple_size_conflict?(facts) -> :contradiction
|
||
int_interval_conflict?(facts) -> :contradiction
|
||
list_structure_conflict?(facts) -> :contradiction
|
||
true -> :ok
|
||
end
|
||
end
|
||
|
||
# atom value clash
|
||
defp atom_val_conflict?(facts) do
|
||
vals =
|
||
for {path, true} <- facts,
|
||
Path.primary_tag(path) == :is_atom,
|
||
{:value_eq, id} <- [Path.primitive(path)] do
|
||
id
|
||
end
|
||
|
||
Enum.uniq(vals) |> length() > 1
|
||
end
|
||
|
||
# tuple size clash
|
||
defp tuple_size_conflict?(facts) do
|
||
sizes = for {p, true} <- facts, {:length, :tuple, n} <- [Path.primitive(p)], do: n
|
||
Enum.uniq(sizes) |> length > 1
|
||
end
|
||
|
||
# integer interval contradiction helper
|
||
defp int_interval_conflict?(facts) do
|
||
intervals =
|
||
for {p, true} <- facts, {:interval, :int, intv} <- [Path.primitive(p)], do: intv
|
||
|
||
case intervals do
|
||
[] ->
|
||
false
|
||
|
||
_ ->
|
||
Enum.reduce_while(intervals, {:neg_inf, :pos_inf}, fn
|
||
{:neg_inf, hi}, {:neg_inf, cur_hi} when hi < cur_hi ->
|
||
{:cont, {:neg_inf, hi}}
|
||
|
||
{lo, :pos_inf}, {cur_lo, :pos_inf} when lo > cur_lo ->
|
||
{:cont, {lo, :pos_inf}}
|
||
|
||
{lo1, hi1}, {lo2, hi2} ->
|
||
lo = max(lo1, lo2)
|
||
hi = min(hi1, hi2)
|
||
if compare_bounds(lo, hi) <= 0, do: {:cont, {lo, hi}}, else: {:halt, :conflict}
|
||
end) == :conflict
|
||
end
|
||
end
|
||
|
||
defp compare_bounds(:neg_inf, _), do: -1
|
||
defp compare_bounds(_, :pos_inf), do: -1
|
||
defp compare_bounds(a, b), do: a - b
|
||
|
||
# list head/tail vs empty
|
||
defp list_structure_conflict?(facts) do
|
||
empty? = Map.get(facts, V.v_list_is_empty()) == true
|
||
|
||
if empty? do
|
||
Enum.any?(facts, fn {p, _} ->
|
||
Path.starts_with?(p, Path.list_head([])) or
|
||
Path.starts_with?(p, Path.list_tail([]))
|
||
end)
|
||
else
|
||
false
|
||
end
|
||
end
|
||
|
||
# ------------ implication helpers ------------------------------------------
|
||
|
||
def atom_implication(id, constr) do
|
||
case {Map.get(constr, V.v_atom_eq(id)), find_any_atom_true(constr)} do
|
||
{true, _} -> true
|
||
{false, _} -> false
|
||
{nil, nil} -> :unknown # <- ⬅️ special-case “no info”
|
||
{nil, other} when other != id -> false # <- only different, real atom
|
||
end
|
||
end
|
||
|
||
defp find_any_atom_true(constr) do
|
||
constr
|
||
|> Enum.map(fn x -> {x, Path.primary_tag(x)} end)
|
||
|
||
Enum.find_value(constr, fn
|
||
{{p, true}, :is_atom} ->
|
||
case Path.primitive(p) do
|
||
{:value_eq, id} -> id
|
||
_ -> nil
|
||
end
|
||
|
||
_ ->
|
||
nil
|
||
end)
|
||
end
|
||
|
||
defp tuple_size_implication(n, constr) do
|
||
case {Map.get(constr, V.v_tuple_size_eq(n)), any_tuple_size_true(constr)} do
|
||
{true, _} -> true
|
||
{false, _} -> false
|
||
{nil, true_n} when true_n != n -> false
|
||
_ -> :unknown
|
||
end
|
||
end
|
||
|
||
defp any_tuple_size_true(constr) do
|
||
Enum.find_value(constr, fn
|
||
{p, true} ->
|
||
case Path.primitive(p) do
|
||
{:length, :tuple, sz} -> sz
|
||
_ -> nil
|
||
end
|
||
|
||
_ ->
|
||
nil
|
||
end)
|
||
end
|
||
|
||
defp int_implication(intv, constr) do
|
||
# intersect current interval with candidate; if unchanged ⇒ implied
|
||
with {:ok, {lo, hi}} <- current_int_interval(constr) do
|
||
if subset?(lo, hi, intv), do: true, else: :unknown
|
||
else
|
||
:none -> :unknown
|
||
:contradiction -> true
|
||
end
|
||
end
|
||
|
||
defp current_int_interval(constr) do
|
||
intvs = for {p, true} <- constr, {:interval, :int, iv} = Path.primitive(p), do: iv
|
||
|
||
case intvs do
|
||
[] ->
|
||
:none
|
||
|
||
list ->
|
||
Enum.reduce_while(list, {:neg_inf, :pos_inf}, fn
|
||
{:neg_inf, hi}, {:neg_inf, cur_hi} ->
|
||
{:cont, {:neg_inf, min(hi, cur_hi)}}
|
||
|
||
{lo, :pos_inf}, {cur_lo, :pos_inf} ->
|
||
{:cont, {max(lo, cur_lo), :pos_inf}}
|
||
|
||
{lo1, hi1}, {lo2, hi2} ->
|
||
lo = max(lo1, lo2)
|
||
hi = min(hi1, hi2)
|
||
if compare_bounds(lo, hi) <= 0, do: {:cont, {lo, hi}}, else: {:halt, :contradiction}
|
||
end)
|
||
end
|
||
end
|
||
|
||
defp subset?(lo, hi, {lo2, hi2}) do
|
||
compare_bounds(lo2, lo) <= 0 and compare_bounds(hi, hi2) <= 0
|
||
end
|
||
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
|
||
try do
|
||
Tdd.Path.start_link()
|
||
rescue
|
||
_ -> nil
|
||
end
|
||
|
||
Core.init()
|
||
IO.puts("TDD system initialized with new architecture.")
|
||
end
|
||
|
||
def type_any, do: Core.true_id()
|
||
def type_none, do: Core.false_id()
|
||
|
||
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())
|
||
|
||
def type_atom_literal(a) do
|
||
id = Core.make_node(V.v_atom_eq(a), type_any(), type_none(), type_none())
|
||
IO.inspect("BEFORE SIMPLIFICATION")
|
||
print_tdd(id)
|
||
|
||
after_simplification = id |> Tdd.simplify(%{})
|
||
|
||
IO.inspect("AFTER SIMPLIFICATION")
|
||
print_tdd(after_simplification)
|
||
after_simplification
|
||
end
|
||
|
||
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_empty_tuple,
|
||
do:
|
||
intersect(
|
||
type_tuple(),
|
||
Core.make_node(V.v_tuple_size_eq(0), 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.
|
||
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
|
||
|
||
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())
|
||
)
|
||
|
||
# --- 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} ->
|
||
# ----------- detect head / tail predicates in path form ---------------
|
||
contradiction =
|
||
case var do
|
||
# list head
|
||
[{:tag, :is_list}, {:head} | inner] ->
|
||
all_elements_type(constraints)
|
||
|> incompatible?(inner)
|
||
|
||
# list tail
|
||
[{:tag, :is_list}, {:tail} | inner] ->
|
||
all_elements_type(constraints)
|
||
|> incompatible_tail?(inner)
|
||
|
||
_ ->
|
||
false
|
||
end
|
||
|
||
if contradiction do
|
||
simplify(n, constraints)
|
||
else
|
||
follow_or_recurse(var, y, n, d, constraints)
|
||
end
|
||
end
|
||
end
|
||
|
||
# --- small helpers ----------------------------------------------------------
|
||
defp all_elements_type(constraints) do
|
||
Enum.find_value(constraints, fn
|
||
{p, true} ->
|
||
case Tdd.Path.primitive(p) do
|
||
{:all_elements, tid} -> tid
|
||
_ -> nil
|
||
end
|
||
|
||
_ ->
|
||
nil
|
||
end)
|
||
end
|
||
|
||
defp incompatible?(nil, _inner), do: false
|
||
defp incompatible?(tid, inner), do: intersect(predicate_to_tdd(inner), tid) == type_none()
|
||
|
||
# tail must be a *list* whose elements have the requested type
|
||
defp incompatible_tail?(nil, _inner), do: false
|
||
|
||
defp incompatible_tail?(tid, inner) do
|
||
required_tail = type_list_of(tid)
|
||
|
||
intersect(predicate_to_tdd(inner), required_tail) == type_none()
|
||
end
|
||
|
||
# unchanged logic, just factored out
|
||
defp follow_or_recurse(var, y, n, d, constraints) do
|
||
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
|
||
|
||
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(path) do
|
||
cache_key = {:predicate_to_tdd, path}
|
||
|
||
if cached = Core.get_op_cache(cache_key) do
|
||
cached
|
||
else
|
||
# generic “predicate-is-true” node
|
||
id = Core.make_node(path, type_any(), type_none(), type_none())
|
||
|
||
# specialised shorthands for a few common paths
|
||
id =
|
||
cond do
|
||
path == V.v_is_atom() ->
|
||
type_atom()
|
||
|
||
path == V.v_is_tuple() ->
|
||
type_tuple()
|
||
|
||
path == V.v_is_integer() ->
|
||
type_integer()
|
||
|
||
path == V.v_is_list() ->
|
||
type_list()
|
||
|
||
# list(all_elements = T)
|
||
{:all_elements, tid} = Tdd.Path.primitive(path) ->
|
||
type_list_of(tid)
|
||
|
||
true ->
|
||
id
|
||
end
|
||
|
||
Core.put_op_cache(cache_key, id)
|
||
id
|
||
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)
|
||
details = Tdd.Core.get_node(id)
|
||
|
||
variable =
|
||
case details do
|
||
{path, _, _, _} -> " " <> Tdd.Path.pretty(path)
|
||
bool when bool in [true, false] -> ""
|
||
_ -> ""
|
||
end
|
||
|
||
IO.puts("#{prefix}ID #{id}: #{inspect(details)}#{variable}")
|
||
|
||
case details do
|
||
{_, 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)
|
||
|
||
_ ->
|
||
:ok
|
||
end
|
||
end
|
||
end
|
||
|
||
Tdd.init_tdd_system()
|
||
tdd_atom = Tdd.type_atom()
|
||
tdd_empty_tuple = Tdd.type_empty_tuple()
|
||
tdd_tuple = Tdd.type_tuple()
|
||
tdd_foo = Tdd.type_atom_literal(:foo)
|
||
tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
|
||
tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
|
||
intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
|
||
tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
|
||
# Tdd.print_tdd(intersected_complex)
|
||
# Tdd.print_tdd(tdd_foo_or_empty_tuple)
|
||
# !!!!!!!!!!!!!!!!!!
|
||
tdd_foo = Tdd.type_atom_literal(:foo)
|
||
Tdd.print_tdd(tdd_foo)
|
||
# outputs: ID 0: false
|
||
# 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)
|
||
# )
|
||
Code.require_file("./tests.exs")
|
||
|
||
# IntegerTests.run(test)
|
||
# TupleTests.run(test)
|
||
# ListTests.run(test)
|
||
# ListOfTests.run(test)
|
||
# AdhocTest.run(test)
|