Compare commits
No commits in common. "130d36973444c2c94dc96c48e97d0f7a79351527" and "5bf920da3ae7e5f76a8008f3487ef8a04be9c5b9" have entirely different histories.
130d369734
...
5bf920da3a
284
refactor.md
284
refactor.md
@ -1,284 +0,0 @@
|
|||||||
|
|
||||||
## Motivation for Architectural Evolution of the TDD-based Type System
|
|
||||||
|
|
||||||
**To:** Project Stakeholders & Technical Team
|
|
||||||
**From:** System Architect
|
|
||||||
**Date:** October 26, 2023
|
|
||||||
**Subject:** A Principled Path Forward for Stability, Extensibility, and Polymorphism
|
|
||||||
|
|
||||||
### 1. Introduction & Current Success
|
|
||||||
|
|
||||||
The existing Ternary Decision Diagram (TDD) implementation has been remarkably successful in proving the core value of a set-theoretic approach to types. By representing types as canonical graphs, we have achieved powerful and efficient operations for union, intersection, negation, and subtyping. The system's ability to automatically simplify complex type expressions like `(atom | tuple) & (tuple | :foo)` into a canonical form `(tuple | :foo)` is a testament to the power of this model.
|
|
||||||
|
|
||||||
However, as we scale the system to represent more complex, real-world data structures—specifically recursive types like `list(X)`—a foundational architectural issue has been identified. This issue currently compromises the system's correctness and severely limits its future potential.
|
|
||||||
|
|
||||||
This document motivates a series of architectural changes designed to address this issue, creating a robust foundation for future growth, including the long-term goal of supporting polymorphism.
|
|
||||||
|
|
||||||
### 2. The Core Challenge: The Unstable Variable Problem
|
|
||||||
|
|
||||||
The correctness of an Ordered TDD relies on a **fixed, global, total order of all predicate variables**. Our current implementation for recursive types like `list_of(X)` violates this principle.
|
|
||||||
|
|
||||||
- **The Flaw:** We currently construct predicate variables by embedding the integer TDD ID of the element type `X`. For instance, `list_of(atom)` might use the variable `{5, :all_elements, 4}` if `type_atom()` resolves to TDD ID `4`.
|
|
||||||
- **The Consequence:** TDD IDs are artifacts of construction order; they are not stable. If `type_integer()` is created before `type_atom()`, their IDs will swap, and the global variable order will change. This means that **semantically identical types can produce structurally different TDDs**, breaking the canonical representation that is the central promise of our system. This is not a theoretical concern; it is a critical bug that invalidates equivalence checks and subtyping operations under different run conditions.
|
|
||||||
|
|
||||||
This instability is a symptom of a deeper issue: we are conflating a type's **logical description** with its **compiled, set-theoretic representation**.
|
|
||||||
|
|
||||||
### 3. The Proposed Solution: A Separation of Concerns
|
|
||||||
|
|
||||||
To solve this, we will introduce a principled separation between the "what" and the "how" of our types.
|
|
||||||
|
|
||||||
1. **`TypeSpec`: The Logical "What"**
|
|
||||||
We will introduce a new, stable, declarative data structure called a `TypeSpec`. A `TypeSpec` is a structural description of a type (e.g., `{:list_of, :atom}`, `{:union, [:integer, :atom]}`). This becomes the **new public API and canonical language** for defining types. It is human-readable, stable, and completely independent of the TDD implementation.
|
|
||||||
|
|
||||||
2. **TDD ID: The Compiled "How"**
|
|
||||||
The TDD graph and its ID will be treated as a **compiled artifact**. It is the powerful, efficient, set-theoretic representation of a concrete `TypeSpec`. The `Tdd` module will evolve into a low-level "backend" or "compiler engine."
|
|
||||||
|
|
||||||
This separation yields immediate and long-term benefits:
|
|
||||||
|
|
||||||
- **Guaranteed Correctness & Stability:** By using the stable `TypeSpec` within our TDD variables (e.g., `{5, :all_elements, {:base, :atom}}`), we restore a fixed global variable order. This guarantees that our TDDs are once again truly canonical, ensuring the reliability of all type operations.
|
|
||||||
- **Clean Architecture & API:** The public-facing API will be vastly improved, operating on clear, declarative `TypeSpec`s instead of opaque integer IDs. The internal complexity of the TDD machinery is encapsulated behind a new `Compiler` module, improving maintainability.
|
|
||||||
- **Unlocking Future Capabilities:** This architecture is not just a bug fix; it is an enabling refactor. A system that "compiles" a `TypeSpec` to a TDD is naturally extensible to polymorphism. The `TypeSpec` for `list(A)` can be represented as `{:list_of, {:type_var, :A}}`. A higher-level type inference engine can then operate on these specs, substituting variables and using our TDD compiler for concrete subtype checks. This provides a clear, principled path to our goal of supporting polymorphic functions and data structures.
|
|
||||||
|
|
||||||
### 4. Phased Implementation Plan
|
|
||||||
|
|
||||||
We will roll out these changes in three deliberate phases to manage complexity and deliver value incrementally.
|
|
||||||
|
|
||||||
- **Phase 1: Stabilize the Core.** Introduce `TypeSpec` and the `Compiler` to fix the unstable variable problem. This is the highest priority, as it ensures the correctness of our existing feature set.
|
|
||||||
- **Phase 2: Refine the Public API.** Build a new, high-level `TypeSystem` module that operates exclusively on `TypeSpec`s, providing a clean and intuitive interface for users of our library.
|
|
||||||
- **Phase 3: Introduce Polymorphism.** With the stable foundation in place, implement the unification and substitution logic required to handle `TypeSpec`s containing type variables, enabling the checking of polymorphic function schemas.
|
|
||||||
|
|
||||||
### 5. Conclusion
|
|
||||||
|
|
||||||
The current TDD system is a powerful proof of concept that is on the verge of becoming a robust, general-purpose tool. By addressing the foundational "unstable variable" problem through a principled separation of a type's specification from its implementation, we not only fix a critical bug but also pave a clear and logical path toward our most ambitious goals. This architectural evolution is a necessary investment in the long-term stability, correctness, and extensibility of our type system.
|
|
||||||
|
|
||||||
|
|
||||||
### Phase 1: Fix the Core Instability & Introduce `TypeSpec`
|
|
||||||
|
|
||||||
This phase is non-negotiable. It makes your current system sound and stable.
|
|
||||||
|
|
||||||
**1. Introduce the `TypeSpec` Data Structure:**
|
|
||||||
This will be the new "source of truth" for defining types. It's a stable, structural representation. This becomes the primary vocabulary for your public API.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
# In a new file, e.g., typespec.ex
|
|
||||||
defmodule Tdd.TypeSpec do
|
|
||||||
@typedoc """
|
|
||||||
A stable, structural representation of a type.
|
|
||||||
This is the primary way users and the higher-level system will describe types.
|
|
||||||
"""
|
|
||||||
@type t ::
|
|
||||||
# Base Types
|
|
||||||
:any
|
|
||||||
| :none
|
|
||||||
| :atom
|
|
||||||
| :integer
|
|
||||||
| :tuple # any tuple
|
|
||||||
| :list # any list
|
|
||||||
|
|
||||||
# Literal Types (canonical form of a value)
|
|
||||||
| {:literal, term()}
|
|
||||||
|
|
||||||
# Set-theoretic Combinators
|
|
||||||
| {:union, [t()]}
|
|
||||||
| {:intersect, [t()]}
|
|
||||||
| {:negation, t()}
|
|
||||||
|
|
||||||
# Parameterized Structural Types
|
|
||||||
| {:tuple, [t()]} # A tuple with specific element types
|
|
||||||
| {:cons, t(), t()} # A non-empty list [H|T]
|
|
||||||
| {:list_of, t()} # A list of any length where elements are of a type
|
|
||||||
|
|
||||||
# Integer Range (example of specific properties)
|
|
||||||
| {:integer_range, integer() | :neg_inf, integer() | :pos_inf}
|
|
||||||
|
|
||||||
# Polymorphic Variable (for Phase 3)
|
|
||||||
| {:type_var, atom()}
|
|
||||||
end
|
|
||||||
```
|
|
||||||
|
|
||||||
**2. Create a "Compiler": `Tdd.Compiler.spec_to_id/1`**
|
|
||||||
This is the new heart of your system. It's a memoized function that takes a `TypeSpec` and returns a canonical TDD ID. Your existing `Tdd` module becomes the "backend" for this compiler.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
# In a new file, e.g., compiler.ex
|
|
||||||
defmodule Tdd.Compiler do
|
|
||||||
# This module manages the cache from spec -> id
|
|
||||||
# Process.put(:spec_to_id_cache, %{})
|
|
||||||
|
|
||||||
def spec_to_id(spec) do
|
|
||||||
# 1. Normalize the spec (e.g., sort unions) to improve cache hits.
|
|
||||||
normalized_spec = Tdd.TypeSpec.normalize(spec)
|
|
||||||
|
|
||||||
# 2. Check cache for `normalized_spec`. If found, return ID.
|
|
||||||
|
|
||||||
# 3. If not found, compile it by calling private helpers.
|
|
||||||
id =
|
|
||||||
case normalized_spec do
|
|
||||||
:atom -> Tdd.type_atom()
|
|
||||||
:integer -> Tdd.type_integer()
|
|
||||||
{:literal, val} -> build_literal_tdd(val)
|
|
||||||
{:union, specs} ->
|
|
||||||
ids = Enum.map(specs, &spec_to_id/1)
|
|
||||||
Enum.reduce(ids, Tdd.type_none(), &Tdd.sum/2)
|
|
||||||
# ... and so on ...
|
|
||||||
{:list_of, element_spec} -> build_list_of_tdd(element_spec)
|
|
||||||
end
|
|
||||||
|
|
||||||
# 4. Cache and return the new ID.
|
|
||||||
id
|
|
||||||
end
|
|
||||||
|
|
||||||
# The key fix is here:
|
|
||||||
defp build_list_of_tdd(element_spec) do
|
|
||||||
# A) Compile the element spec to get its ID for semantic checks.
|
|
||||||
element_id = spec_to_id(element_spec)
|
|
||||||
|
|
||||||
# B) Create the TDD variable using the STABLE element_spec.
|
|
||||||
# This is the critical change.
|
|
||||||
stable_var = Tdd.v_list_all_elements_are(element_spec)
|
|
||||||
|
|
||||||
# C) Use Tdd module to build the node, passing both the stable
|
|
||||||
# variable and the compiled ID for the consistency checker.
|
|
||||||
# (This requires a small change in the Tdd module).
|
|
||||||
Tdd.type_list_of_internal(stable_var, element_id)
|
|
||||||
end
|
|
||||||
end
|
|
||||||
```
|
|
||||||
|
|
||||||
**3. Modify the `Tdd` Module to be a "Low-Level Backend":**
|
|
||||||
The public API of `Tdd` shrinks. Its main users are now `Tdd.Compiler` and `Tdd.TypeSystem` (Phase 2).
|
|
||||||
|
|
||||||
* **Change Variable Constructors:** `v_list_all_elements_are` now takes a `TypeSpec`.
|
|
||||||
```elixir
|
|
||||||
# In Tdd module
|
|
||||||
# The variable now contains the stable TypeSpec, not a volatile ID.
|
|
||||||
def v_list_all_elements_are(element_spec), do: {5, :all_elements, element_spec}
|
|
||||||
```
|
|
||||||
|
|
||||||
* **Update `check_assumptions_consistency`:** This function now needs access to the compiler to handle the new variable format.
|
|
||||||
```elixir
|
|
||||||
# In Tdd module, inside the consistency checker
|
|
||||||
# ... when it encounters a `v_list_all_elements_are` assumption...
|
|
||||||
{{5, :all_elements, element_spec}, true} ->
|
|
||||||
# It needs to know the TDD ID for this spec to do subtyping checks.
|
|
||||||
ambient_type_for_head = Tdd.Compiler.spec_to_id(element_spec)
|
|
||||||
# ... rest of the logic proceeds as before ...
|
|
||||||
```
|
|
||||||
This creates a circular dependency (`Compiler` -> `Tdd` -> `Compiler`), which is a sign of deep coupling. It's acceptable for now, but a sign that this logic might eventually belong in the compiler itself.
|
|
||||||
|
|
||||||
* **Refactor Type Constructors:** Your old `type_list_of`, `type_tuple`, etc., are either removed or renamed to `_internal` and used by the new `Compiler`.
|
|
||||||
|
|
||||||
---
|
|
||||||
|
|
||||||
### Phase 2: Build the High-Level Type System API
|
|
||||||
|
|
||||||
This is the new public-facing interface. It operates on `TypeSpec`s and uses the `Compiler` and `Tdd` modules as its engine.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
# In a new file, e.g., type_system.ex
|
|
||||||
defmodule TypeSystem do
|
|
||||||
alias Tdd.TypeSpec, as: Spec
|
|
||||||
|
|
||||||
# --- Public Type Constructors (using TypeSpecs) ---
|
|
||||||
def type_atom, do: :atom
|
|
||||||
def type_integer, do: :integer
|
|
||||||
def type_union(specs), do: {:union, specs}
|
|
||||||
def type_list_of(spec), do: {:list_of, spec}
|
|
||||||
# ... and so on ...
|
|
||||||
|
|
||||||
# --- Public Operations ---
|
|
||||||
@doc """
|
|
||||||
Checks if spec1 is a subtype of spec2.
|
|
||||||
"""
|
|
||||||
def is_subtype(spec1, spec2) do
|
|
||||||
# 1. Compile both specs to their canonical TDD IDs.
|
|
||||||
id1 = Tdd.Compiler.spec_to_id(spec1)
|
|
||||||
id2 = Tdd.Compiler.spec_to_id(spec2)
|
|
||||||
|
|
||||||
# 2. Use the fast, low-level TDD check.
|
|
||||||
Tdd.is_subtype(id1, id2)
|
|
||||||
end
|
|
||||||
|
|
||||||
def intersect(spec1, spec2) do
|
|
||||||
# This is a choice:
|
|
||||||
# Option A (easy): Just return {:intersect, [spec1, spec2]} and let the compiler
|
|
||||||
# handle it lazily when `spec_to_id` is called.
|
|
||||||
# Option B (better): Do some immediate simplifications here before compiling.
|
|
||||||
# e.g., intersect(:atom, :integer) -> :none
|
|
||||||
{:intersect, [spec1, spec2]}
|
|
||||||
end
|
|
||||||
end
|
|
||||||
```
|
|
||||||
|
|
||||||
**At the end of Phase 2, you have a sound, stable, and extensible set-theoretic type checker.** The "god function" problem still exists in `check_assumptions_consistency`, but the system is no longer fundamentally broken.
|
|
||||||
|
|
||||||
---
|
|
||||||
|
|
||||||
### Phase 3: Introduce Polymorphism
|
|
||||||
|
|
||||||
Now you leverage the `TypeSpec` architecture.
|
|
||||||
|
|
||||||
**1. Define Polymorphic Function Schemas:**
|
|
||||||
These are data structures, living outside the TDD world.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
# A function schema
|
|
||||||
@type fun_schema :: {:function,
|
|
||||||
forall: [:atom], # list of quantified type variables
|
|
||||||
args: [Spec.t()], # argument types (can use quantified vars)
|
|
||||||
return: Spec.t() # return type (can use quantified vars)
|
|
||||||
}
|
|
||||||
|
|
||||||
# Example: Enum.map/2
|
|
||||||
# forall A, B. (list(A), (A -> B)) -> list(B)
|
|
||||||
map_schema = {:function,
|
|
||||||
forall: [:A, :B],
|
|
||||||
args: [
|
|
||||||
{:list_of, {:type_var, :A}},
|
|
||||||
{:function, forall: [], args: [{:type_var, :A}], return: {:type_var, :B}}
|
|
||||||
],
|
|
||||||
return: {:list_of, {:type_var, :B}}
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
**2. Implement a Unification/Substitution Engine:**
|
|
||||||
This is a new, separate module that operates *only on `TypeSpec`s and schemas*.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
defmodule Type.Unify do
|
|
||||||
# Takes a spec with variables and a concrete spec, returns a substitution map
|
|
||||||
# or :error.
|
|
||||||
# unify({:list_of, {:type_var, :A}}, {:list_of, :integer}) -> {:ok, %{A: :integer}}
|
|
||||||
def unify(polymorphic_spec, concrete_spec) do
|
|
||||||
# ... recursive pattern matching logic ...
|
|
||||||
end
|
|
||||||
|
|
||||||
# Applies a substitution map to a spec.
|
|
||||||
# substitute({:list_of, {:type_var, :A}}, %{A: :integer}) -> {:list_of, :integer}
|
|
||||||
def substitute(spec, substitution_map) do
|
|
||||||
# ... recursive substitution logic ...
|
|
||||||
end
|
|
||||||
end
|
|
||||||
```
|
|
||||||
|
|
||||||
**3. Build the Type Checker for Function Calls:**
|
|
||||||
This is the final piece that ties everything together.
|
|
||||||
|
|
||||||
```elixir
|
|
||||||
# In TypeSystem module
|
|
||||||
def check_function_call(function_schema, concrete_arg_specs) do
|
|
||||||
# 1. Unify the schema's arg specs with the concrete arg specs.
|
|
||||||
# This will produce a substitution map, e.g., %{A: :integer, B: :atom}.
|
|
||||||
{:ok, substitution_map} = Unify.unify(function_schema.args, concrete_arg_specs)
|
|
||||||
|
|
||||||
# 2. Check that the concrete args are valid subtypes.
|
|
||||||
# (This step is actually part of unification itself).
|
|
||||||
|
|
||||||
# 3. Infer the concrete return type by substituting into the schema's return spec.
|
|
||||||
concrete_return_spec = Unify.substitute(function_schema.return, substitution_map)
|
|
||||||
|
|
||||||
{:ok, concrete_return_spec}
|
|
||||||
end
|
|
||||||
```
|
|
||||||
|
|
||||||
This phased approach solves your immediate problem correctly, provides a clean public API, and builds the exact foundation needed to add a polymorphic layer on top without requiring another major architectural upheaval.
|
|
||||||
796
tests.exs
796
tests.exs
@ -1,796 +0,0 @@
|
|||||||
|
|
||||||
# --- Example Usage ---
|
|
||||||
Tdd.init_tdd_system()
|
|
||||||
|
|
||||||
# Basic Types
|
|
||||||
tdd_foo = Tdd.type_atom_literal(:foo)
|
|
||||||
tdd_bar = Tdd.type_atom_literal(:bar)
|
|
||||||
tdd_atom = Tdd.type_atom()
|
|
||||||
tdd_empty_tuple = Tdd.type_empty_tuple()
|
|
||||||
tdd_any = Tdd.type_any()
|
|
||||||
tdd_none = Tdd.type_none()
|
|
||||||
|
|
||||||
test = fn name, expected, result ->
|
|
||||||
current_failures = Process.get(:test_failures, [])
|
|
||||||
|
|
||||||
if expected != result do
|
|
||||||
Process.put(:test_failures, [name | current_failures])
|
|
||||||
end
|
|
||||||
|
|
||||||
status = if expected == result, do: "PASSED", else: "FAILED"
|
|
||||||
IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
|
|
||||||
end
|
|
||||||
|
|
||||||
# Basic Types
|
|
||||||
tdd_foo = Tdd.type_atom_literal(:foo)
|
|
||||||
tdd_bar = Tdd.type_atom_literal(:bar)
|
|
||||||
tdd_baz = Tdd.type_atom_literal(:baz)
|
|
||||||
tdd_atom = Tdd.type_atom()
|
|
||||||
tdd_empty_tuple = Tdd.type_empty_tuple()
|
|
||||||
tdd_tuple = Tdd.type_tuple()
|
|
||||||
# Tuple of size 2, e.g. {any, any}
|
|
||||||
tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
|
|
||||||
tdd_any = Tdd.type_any()
|
|
||||||
tdd_none = Tdd.type_none()
|
|
||||||
|
|
||||||
test_all = fn ->
|
|
||||||
IO.puts("\n--- TDD for :foo ---")
|
|
||||||
Tdd.print_tdd(tdd_foo)
|
|
||||||
|
|
||||||
IO.puts("\n--- TDD for not :foo ---")
|
|
||||||
Tdd.print_tdd(Tdd.negate(tdd_foo))
|
|
||||||
|
|
||||||
IO.puts("\n--- TDD for atom ---")
|
|
||||||
Tdd.print_tdd(tdd_atom)
|
|
||||||
|
|
||||||
IO.puts("\n--- TDD for not atom ---")
|
|
||||||
# Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
|
|
||||||
# This represents "anything that is not an atom". The DC branch becomes true because if
|
|
||||||
# "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
|
|
||||||
Tdd.print_tdd(Tdd.negate(tdd_atom))
|
|
||||||
|
|
||||||
IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
|
|
||||||
tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
|
|
||||||
# Expected ID 0: :false_terminal
|
|
||||||
Tdd.print_tdd(tdd_foo_and_bar)
|
|
||||||
|
|
||||||
IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
|
|
||||||
tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
|
|
||||||
# Expected to be structurally identical to tdd_foo
|
|
||||||
Tdd.print_tdd(tdd_foo_and_atom)
|
|
||||||
IO.puts("\n--- Basic Subtyping Tests ---")
|
|
||||||
test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
|
|
||||||
test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
|
|
||||||
test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
|
|
||||||
test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
|
|
||||||
test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
|
|
||||||
test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
|
|
||||||
test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
|
|
||||||
test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
|
|
||||||
test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
|
|
||||||
test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))
|
|
||||||
|
|
||||||
IO.puts("\n--- Any/None Subtyping Tests ---")
|
|
||||||
test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
|
|
||||||
test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
|
|
||||||
test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
|
|
||||||
test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
|
|
||||||
test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
|
|
||||||
test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
|
|
||||||
test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
|
|
||||||
test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))
|
|
||||||
|
|
||||||
IO.puts("\n--- Union related Subtyping ---")
|
|
||||||
tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
|
|
||||||
tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)
|
|
||||||
|
|
||||||
test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
|
|
||||||
test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
|
|
||||||
test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
|
|
||||||
test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(:foo | :bar) <: (:foo | :bar | :baz)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(:foo | :bar | :baz) <: (:foo | :bar)",
|
|
||||||
false,
|
|
||||||
Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
|
|
||||||
)
|
|
||||||
|
|
||||||
# Test against a non-member of the union
|
|
||||||
test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))
|
|
||||||
|
|
||||||
IO.puts("\n--- Intersection related Subtyping ---")
|
|
||||||
# Should be equivalent to tdd_foo
|
|
||||||
tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
|
|
||||||
# Should be tdd_none
|
|
||||||
tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
|
|
||||||
|
|
||||||
test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
|
|
||||||
test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
|
|
||||||
test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
|
|
||||||
test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
|
|
||||||
test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
|
|
||||||
# An intersection is a subtype of its components
|
|
||||||
test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
|
|
||||||
# (none <: atom)
|
|
||||||
test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
|
|
||||||
# (none <: tuple)
|
|
||||||
test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))
|
|
||||||
|
|
||||||
IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
|
|
||||||
# Reminder: ¬A <: ¬B is equivalent to B <: A (contrapositive)
|
|
||||||
|
|
||||||
# Test 1: ¬atom <: ¬:foo (Equivalent to :foo <: atom, which is true)
|
|
||||||
test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))
|
|
||||||
|
|
||||||
# Test 2: ¬:foo <: ¬atom (Equivalent to atom <: :foo, which is false)
|
|
||||||
test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))
|
|
||||||
|
|
||||||
# Double negation
|
|
||||||
test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
|
|
||||||
test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))
|
|
||||||
|
|
||||||
# Disjoint types
|
|
||||||
test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
|
|
||||||
test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
|
|
||||||
test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))
|
|
||||||
|
|
||||||
IO.puts("\n--- Mixed Types & Complex Subtyping ---")
|
|
||||||
tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
|
|
||||||
tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(:foo | {}) <: (atom | tuple)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(atom | tuple) <: (:foo | {})",
|
|
||||||
false,
|
|
||||||
Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
|
|
||||||
test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))
|
|
||||||
|
|
||||||
# De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
|
|
||||||
# (:foo | :bar) <: ¬(¬:foo & ¬:bar)
|
|
||||||
tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"¬(¬:foo & ¬:bar) <: (:foo | :bar)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
|
|
||||||
)
|
|
||||||
|
|
||||||
# Type difference: atom - :foo (represented as atom & ¬:foo)
|
|
||||||
tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
|
|
||||||
test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
|
|
||||||
test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
|
|
||||||
# True if :bar is in (atom - :foo)
|
|
||||||
test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
|
|
||||||
test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
|
|
||||||
|
|
||||||
# (atom - :foo) | :foo should be atom
|
|
||||||
tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo)
|
|
||||||
test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom))
|
|
||||||
test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom))
|
|
||||||
|
|
||||||
# (atom | {}) & (tuple | :foo) must be (:foo | {})
|
|
||||||
# Represents `atom() | {}`
|
|
||||||
tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
|
|
||||||
# Represents `tuple() | :foo`
|
|
||||||
tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
|
|
||||||
intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
|
|
||||||
# Expected result for intersected_complex is tdd_foo_or_empty_tuple
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(atom | {}) & (tuple | :foo) <: (:foo | {})",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple)
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"(:foo | {}) <: (atom | {}) & (tuple | :foo)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex)
|
|
||||||
)
|
|
||||||
|
|
||||||
# {} | tuple_size_2 should be a subtype of tuple
|
|
||||||
tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2)
|
|
||||||
test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple))
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"({} | tuple_size_2) <: ({} | tuple_size_2)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2)
|
|
||||||
)
|
|
||||||
|
|
||||||
test.(
|
|
||||||
"({} | tuple_size_2) <: tuple_size_2",
|
|
||||||
false,
|
|
||||||
Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2)
|
|
||||||
)
|
|
||||||
|
|
||||||
# IO.puts("\n--- TDD structure for (atom - :foo) ---")
|
|
||||||
# Tdd.print_tdd(tdd_atom_minus_foo)
|
|
||||||
# IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
|
|
||||||
# Tdd.print_tdd(tdd_recombined_atom)
|
|
||||||
# IO.puts("\n--- TDD structure for 'atom' for comparison ---")
|
|
||||||
# Tdd.print_tdd(tdd_atom)
|
|
||||||
|
|
||||||
IO.inspect(Process.get(:test_failures, []))
|
|
||||||
end
|
|
||||||
defmodule IntegerTests do
|
|
||||||
def run(test_fn) do
|
|
||||||
Process.put(:test_failures, [])
|
|
||||||
# Reset for each test group if needed, or once globally
|
|
||||||
Tdd.init_tdd_system()
|
|
||||||
|
|
||||||
# Integer types
|
|
||||||
tdd_int = Tdd.type_integer()
|
|
||||||
tdd_int_5 = Tdd.type_int_eq(5)
|
|
||||||
tdd_int_7 = Tdd.type_int_eq(7)
|
|
||||||
# x < 10
|
|
||||||
tdd_int_lt_10 = Tdd.type_int_lt(10)
|
|
||||||
# x > 3
|
|
||||||
tdd_int_gt_3 = Tdd.type_int_gt(3)
|
|
||||||
# x < 3
|
|
||||||
tdd_int_lt_3 = Tdd.type_int_lt(3)
|
|
||||||
# x > 10
|
|
||||||
tdd_int_gt_10 = Tdd.type_int_gt(10)
|
|
||||||
tdd_atom_foo = Tdd.type_atom_literal(:foo)
|
|
||||||
#
|
|
||||||
# IO.puts("\n--- Integer Type Structures ---")
|
|
||||||
# IO.puts("Integer:")
|
|
||||||
# Tdd.print_tdd(tdd_int)
|
|
||||||
# IO.puts("Int == 5:")
|
|
||||||
# Tdd.print_tdd(tdd_int_5)
|
|
||||||
# IO.puts("Int < 10:")
|
|
||||||
# Tdd.print_tdd(tdd_int_lt_10)
|
|
||||||
|
|
||||||
IO.puts("\n--- Integer Subtyping Tests ---")
|
|
||||||
test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
|
|
||||||
test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5))
|
|
||||||
test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7))
|
|
||||||
test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5))
|
|
||||||
test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo))
|
|
||||||
|
|
||||||
test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int))
|
|
||||||
test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10))
|
|
||||||
# 5 < 10
|
|
||||||
test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10))
|
|
||||||
test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5))
|
|
||||||
|
|
||||||
test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int))
|
|
||||||
# 5 > 3
|
|
||||||
test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3))
|
|
||||||
test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5))
|
|
||||||
|
|
||||||
# x < 3 implies x < 10
|
|
||||||
test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10))
|
|
||||||
# x > 10 implies x > 3
|
|
||||||
test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
|
|
||||||
test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3))
|
|
||||||
test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10))
|
|
||||||
|
|
||||||
IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
|
|
||||||
intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7)
|
|
||||||
test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none())
|
|
||||||
# IO.puts("Structure of int_5 & int_7 (should be ID 0):")
|
|
||||||
# Tdd.print_tdd(intersect_5_7)
|
|
||||||
|
|
||||||
# x < 3 AND x > 10
|
|
||||||
intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10)
|
|
||||||
test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none())
|
|
||||||
# IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
|
|
||||||
# Tdd.print_tdd(intersect_lt3_gt10)
|
|
||||||
|
|
||||||
# x < 10 AND x > 3 (e.g. 4,5..9)
|
|
||||||
intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3)
|
|
||||||
test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none())
|
|
||||||
# IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
|
|
||||||
# Tdd.print_tdd(intersect_lt10_gt3)
|
|
||||||
# Test a value within this intersection
|
|
||||||
test_fn.(
|
|
||||||
"int_5 <: (int_lt_10 & int_gt_3)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3)
|
|
||||||
)
|
|
||||||
|
|
||||||
# x == 5 AND x < 3
|
|
||||||
intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3)
|
|
||||||
test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none())
|
|
||||||
|
|
||||||
IO.puts("\n--- Integer Union Tests ---")
|
|
||||||
union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7)
|
|
||||||
test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7))
|
|
||||||
test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7))
|
|
||||||
test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7))
|
|
||||||
# IO.puts("Structure of int_5 | int_7:")
|
|
||||||
# Tdd.print_tdd(union_5_7)
|
|
||||||
|
|
||||||
# (int < 3) | (int > 10)
|
|
||||||
union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"int_eq(0) <: (int < 3 | int > 10)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"int_eq(5) <: (int < 3 | int > 10)",
|
|
||||||
false,
|
|
||||||
Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"int_eq(12) <: (int < 3 | int > 10)",
|
|
||||||
true,
|
|
||||||
Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.inspect(Process.get(:test_failures, []))
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
defmodule TupleTests do
|
|
||||||
import Tdd
|
|
||||||
|
|
||||||
def run(test_fn) do
|
|
||||||
Process.put(:test_failures, [])
|
|
||||||
# Re-init the system for a clean slate for these tests
|
|
||||||
Tdd.init_tdd_system()
|
|
||||||
IO.puts("\n--- Running TupleTests ---")
|
|
||||||
|
|
||||||
# --- Basic Types for convenience ---
|
|
||||||
t_atom = type_atom()
|
|
||||||
t_int = type_integer()
|
|
||||||
t_foo = type_atom_literal(:foo)
|
|
||||||
t_bar = type_atom_literal(:bar)
|
|
||||||
t_int_5 = type_int_eq(5)
|
|
||||||
t_int_6 = type_int_eq(6)
|
|
||||||
t_int_pos = type_int_gt(0)
|
|
||||||
t_any = type_any()
|
|
||||||
t_none = type_none()
|
|
||||||
# any tuple
|
|
||||||
t_tuple = type_tuple()
|
|
||||||
t_empty_tuple = type_empty_tuple()
|
|
||||||
|
|
||||||
# --- Specific Tuple Types ---
|
|
||||||
# {atom(), integer()}
|
|
||||||
tup_atom_int = type_tuple([t_atom, t_int])
|
|
||||||
# {:foo, 5}
|
|
||||||
tup_foo_5 = type_tuple([t_foo, t_int_5])
|
|
||||||
# {pos_integer(), atom()}
|
|
||||||
tup_pos_atom = type_tuple([t_int_pos, t_atom])
|
|
||||||
# {atom(), any}
|
|
||||||
tup_atom_any = type_tuple([t_atom, t_any])
|
|
||||||
# {any, integer()}
|
|
||||||
tup_any_int = type_tuple([t_any, t_int])
|
|
||||||
# a tuple of size 2, {any, any}
|
|
||||||
tup_s2_any = type_tuple_sized_any(2)
|
|
||||||
# a tuple of size 3, {any, any, any}
|
|
||||||
tup_s3_any = type_tuple_sized_any(3)
|
|
||||||
# {integer(), atom()}
|
|
||||||
tup_int_atom = type_tuple([t_int, t_atom])
|
|
||||||
# {{:foo}}
|
|
||||||
tup_nested_foo = type_tuple([type_tuple([t_foo])])
|
|
||||||
# {{atom()}}
|
|
||||||
tup_nested_atom = type_tuple([type_tuple([t_atom])])
|
|
||||||
# {any, none} -> this should resolve to none
|
|
||||||
tup_with_none = type_tuple([t_any, t_none])
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Basic Subtyping ---")
|
|
||||||
test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
|
|
||||||
test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
|
|
||||||
test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
|
|
||||||
test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
|
|
||||||
test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
|
|
||||||
test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Size-related Subtyping ---")
|
|
||||||
test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
|
|
||||||
test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
|
|
||||||
test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
|
|
||||||
test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
|
|
||||||
test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
|
|
||||||
test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Intersection ---")
|
|
||||||
# {atom, any} & {any, int} -> {atom, int}
|
|
||||||
intersect1 = intersect(tup_atom_any, tup_any_int)
|
|
||||||
test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)
|
|
||||||
|
|
||||||
# {atom, int} & {int, atom} -> none
|
|
||||||
intersect2 = intersect(tup_atom_int, tup_int_atom)
|
|
||||||
test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)
|
|
||||||
|
|
||||||
# tuple_size_2 & tuple_size_3 -> none
|
|
||||||
intersect3 = intersect(tup_s2_any, tup_s3_any)
|
|
||||||
test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)
|
|
||||||
|
|
||||||
# tuple() & {atom, int} -> {atom, int}
|
|
||||||
intersect4 = intersect(t_tuple, tup_atom_int)
|
|
||||||
test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Union ---")
|
|
||||||
# {:foo, 5} | {pos_int, atom}
|
|
||||||
union1 = sum(tup_foo_5, tup_pos_atom)
|
|
||||||
test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
|
|
||||||
true,
|
|
||||||
is_subtype(tup_pos_atom, union1)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{atom, int} <: ({:foo, 5} | {pos_int, atom})",
|
|
||||||
false,
|
|
||||||
is_subtype(tup_atom_int, union1)
|
|
||||||
)
|
|
||||||
|
|
||||||
# {atom, any} | {any, int} -> a complex type, let's check subtyping against it
|
|
||||||
union2 = sum(tup_atom_any, tup_any_int)
|
|
||||||
# {atom, int} is in both parts of the union.
|
|
||||||
test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
|
|
||||||
# {:foo, :bar} is only in {atom, any}.
|
|
||||||
test_fn.(
|
|
||||||
"{:foo, :bar} <: ({atom,any} | {any,int})",
|
|
||||||
true,
|
|
||||||
is_subtype(type_tuple([t_foo, t_bar]), union2)
|
|
||||||
)
|
|
||||||
|
|
||||||
# {5, 6} is only in {any, int}.
|
|
||||||
test_fn.(
|
|
||||||
"{5, 6} <: ({atom,any} | {any,int})",
|
|
||||||
true,
|
|
||||||
is_subtype(type_tuple([t_int_5, t_int_6]), union2)
|
|
||||||
)
|
|
||||||
|
|
||||||
# {5, :foo} is in neither part of the union.
|
|
||||||
test_fn.(
|
|
||||||
"{5, :foo} <: ({atom,any} | {any,int})",
|
|
||||||
false,
|
|
||||||
is_subtype(type_tuple([t_int_5, t_foo]), union2)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Negation and Type Difference ---")
|
|
||||||
# atom is disjoint from tuple, so atom <: ¬tuple
|
|
||||||
test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))
|
|
||||||
|
|
||||||
# A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
|
|
||||||
test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
|
|
||||||
# {int, atom} is a subtype of ¬{atom, int} because their elements differ
|
|
||||||
test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
|
|
||||||
# tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
|
|
||||||
test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))
|
|
||||||
|
|
||||||
# Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
|
|
||||||
diff1 = intersect(tup_s2_any, negate(tup_atom_any))
|
|
||||||
|
|
||||||
# {integer, integer} has a first element that is not an atom, so it should be in the difference.
|
|
||||||
tup_int_int = type_tuple([t_int, t_int])
|
|
||||||
test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{atom, int} <: (tuple_size_2 - {atom, any})",
|
|
||||||
false,
|
|
||||||
is_subtype(tup_atom_int, diff1)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Nested Tuples ---")
|
|
||||||
test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
|
|
||||||
test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
|
|
||||||
# Intersection of disjoint nested types: {{:foo}} & {{:bar}}
|
|
||||||
intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
|
|
||||||
test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
|
|
||||||
# Union of nested types
|
|
||||||
union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
|
|
||||||
test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{{:bar}} <: ({{:foo}} | {{:bar}})",
|
|
||||||
true,
|
|
||||||
is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{{atom}} <: ({{:foo}} | {{:bar}})",
|
|
||||||
false,
|
|
||||||
is_subtype(tup_nested_atom, union_nested)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Edge Cases (any, none) ---")
|
|
||||||
# A type `{any, none}` should not be possible. The value `none` cannot exist.
|
|
||||||
# The simplification logic should reduce this to `type_none`.
|
|
||||||
test_fn.("{any, none} == none", true, tup_with_none == t_none)
|
|
||||||
|
|
||||||
# Intersection with a tuple containing none should result in none
|
|
||||||
intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
|
|
||||||
test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)
|
|
||||||
|
|
||||||
# Union with a tuple containing none should be a no-op
|
|
||||||
union_with_none_tuple = sum(tup_atom_int, tup_with_none)
|
|
||||||
test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)
|
|
||||||
|
|
||||||
# --- Original tests from problem description for regression ---
|
|
||||||
IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{1, :foo} <: {int_gt_0, :foo | :bar}",
|
|
||||||
true,
|
|
||||||
is_subtype(
|
|
||||||
type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
|
|
||||||
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
|
|
||||||
)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{0, :foo} <: {int_gt_0, :foo | :bar}",
|
|
||||||
false,
|
|
||||||
is_subtype(
|
|
||||||
type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
|
|
||||||
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
|
|
||||||
)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"{1, :kek} <: {int_gt_0, :foo | :bar}",
|
|
||||||
false,
|
|
||||||
is_subtype(
|
|
||||||
type_tuple([
|
|
||||||
type_int_eq(1),
|
|
||||||
type_atom_literal(:kek)
|
|
||||||
]),
|
|
||||||
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
|
|
||||||
)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
defmodule ListTests do
|
|
||||||
import Tdd
|
|
||||||
|
|
||||||
def run(test_fn) do
|
|
||||||
Process.put(:test_failures, [])
|
|
||||||
Tdd.init_tdd_system()
|
|
||||||
IO.puts("\n--- Running ListTests ---")
|
|
||||||
|
|
||||||
# --- Basic Types ---
|
|
||||||
t_atom = type_atom()
|
|
||||||
t_int = type_integer()
|
|
||||||
t_foo = type_atom_literal(:foo)
|
|
||||||
t_bar = type_atom_literal(:bar)
|
|
||||||
t_any = type_any()
|
|
||||||
t_none = type_none()
|
|
||||||
|
|
||||||
# --- List Types ---
|
|
||||||
t_list = type_list()
|
|
||||||
t_empty_list = type_empty_list()
|
|
||||||
# [atom | list]
|
|
||||||
t_cons_atom_list = type_cons(t_atom, t_list)
|
|
||||||
# [:foo | []]
|
|
||||||
t_cons_foo_empty = type_cons(t_foo, t_empty_list)
|
|
||||||
# [atom | []]
|
|
||||||
t_cons_atom_empty = type_cons(t_atom, t_empty_list)
|
|
||||||
# [any | []]
|
|
||||||
t_cons_any_empty = type_cons(t_any, t_empty_list)
|
|
||||||
# [integer | list]
|
|
||||||
t_cons_int_list = type_cons(t_int, t_list)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Basic List Subtyping ---")
|
|
||||||
test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
|
|
||||||
test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
|
|
||||||
test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
|
|
||||||
test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
|
|
||||||
test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
|
|
||||||
test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
|
|
||||||
test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
|
|
||||||
test_fn.("atom <: list", false, is_subtype(t_atom, t_list))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
|
|
||||||
# Head is a subtype
|
|
||||||
test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
|
|
||||||
test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
|
|
||||||
# Tail is a subtype
|
|
||||||
test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
|
|
||||||
test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
|
|
||||||
# Both are subtypes
|
|
||||||
test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
|
|
||||||
# Neither is a subtype
|
|
||||||
test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
|
|
||||||
# A list of length 1 is a subtype of a list of any element of length 1
|
|
||||||
test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: List Intersection ---")
|
|
||||||
# [atom|list] & [integer|list] -> should be none due to head conflict
|
|
||||||
intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
|
|
||||||
test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)
|
|
||||||
|
|
||||||
# [any|[]] & [atom|list] -> should be [atom|[]]
|
|
||||||
intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
|
|
||||||
test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)
|
|
||||||
|
|
||||||
# [] & [atom|list] -> should be none because one is empty and one is not
|
|
||||||
intersect3 = intersect(t_empty_list, t_cons_atom_list)
|
|
||||||
test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: List Union ---")
|
|
||||||
# [] | [atom|[]]
|
|
||||||
union1 = sum(t_empty_list, t_cons_atom_empty)
|
|
||||||
test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
|
|
||||||
test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"[integer|[]] <: ([] | [atom|[]])",
|
|
||||||
false,
|
|
||||||
is_subtype(type_cons(t_int, t_empty_list), union1)
|
|
||||||
)
|
|
||||||
|
|
||||||
# [:foo|[]] | [:bar|[]]
|
|
||||||
union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
|
|
||||||
# This union is a subtype of [atom|[]]
|
|
||||||
test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
|
|
||||||
test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: List Negation ---")
|
|
||||||
# list is a subtype of not(atom)
|
|
||||||
test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
|
|
||||||
# A non-empty list is a subtype of not an empty list
|
|
||||||
test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
|
|
||||||
# [integer|list] is a subtype of not [atom|list]
|
|
||||||
test_fn.(
|
|
||||||
"[integer|list] <: ¬[atom|list]",
|
|
||||||
true,
|
|
||||||
is_subtype(t_cons_int_list, negate(t_cons_atom_list))
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
defmodule ListOfTests do
|
|
||||||
import Tdd
|
|
||||||
|
|
||||||
def run(test_fn) do
|
|
||||||
Process.put(:test_failures, [])
|
|
||||||
Tdd.init_tdd_system()
|
|
||||||
IO.puts("\n--- Running ListOfTests ---")
|
|
||||||
|
|
||||||
# --- Basic Types ---
|
|
||||||
t_atom = type_atom()
|
|
||||||
t_int = type_integer()
|
|
||||||
t_pos_int = type_int_gt(0)
|
|
||||||
t_int_5 = type_int_eq(5)
|
|
||||||
|
|
||||||
# --- list(X) Types ---
|
|
||||||
t_list_of_int = type_list_of(t_int)
|
|
||||||
t_list_of_pos_int = type_list_of(t_pos_int)
|
|
||||||
t_list_of_atom = type_list_of(t_atom)
|
|
||||||
|
|
||||||
# --- Specific List Types ---
|
|
||||||
t_list = type_list()
|
|
||||||
t_empty_list = type_empty_list()
|
|
||||||
# [5]
|
|
||||||
t_list_one_int = type_cons(t_int_5, t_empty_list)
|
|
||||||
# [:foo]
|
|
||||||
t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
|
|
||||||
# [5, :foo]
|
|
||||||
t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Basic list(X) Subtyping ---")
|
|
||||||
test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
|
|
||||||
test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
|
|
||||||
test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
|
|
||||||
test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
|
|
||||||
test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
|
|
||||||
test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"[5, :foo] <: list(any)",
|
|
||||||
true,
|
|
||||||
is_subtype(t_list_int_and_atom, type_list_of(type_any()))
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Covariance of list(X) ---")
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"list(pos_integer) <: list(integer)",
|
|
||||||
true,
|
|
||||||
is_subtype(t_list_of_pos_int, t_list_of_int)
|
|
||||||
)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"list(integer) <: list(pos_integer)",
|
|
||||||
false,
|
|
||||||
is_subtype(t_list_of_int, t_list_of_pos_int)
|
|
||||||
)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Intersection of list(X) ---")
|
|
||||||
# list(integer) & list(pos_integer) should be list(pos_integer)
|
|
||||||
intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
|
|
||||||
|
|
||||||
test_fn.(
|
|
||||||
"(list(int) & list(pos_int)) == list(pos_int)",
|
|
||||||
true,
|
|
||||||
intersect1 == t_list_of_pos_int
|
|
||||||
)
|
|
||||||
|
|
||||||
# list(integer) & list(atom) should be just [] (empty list is the only common member)
|
|
||||||
# The system simplifies this intersection to a type that only accepts the empty list.
|
|
||||||
intersect2 = intersect(t_list_of_int, t_list_of_atom)
|
|
||||||
test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
|
|
||||||
test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
|
|
||||||
test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
|
|
||||||
# It should be equivalent to `type_empty_list`
|
|
||||||
test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)
|
|
||||||
|
|
||||||
IO.puts("\n--- Section: Intersection of list(X) with cons ---")
|
|
||||||
# list(integer) & [:foo | []] -> should be none
|
|
||||||
intersect3 = intersect(t_list_of_int, t_list_one_atom)
|
|
||||||
test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())
|
|
||||||
|
|
||||||
# list(integer) & [5 | []] -> should be [5 | []]
|
|
||||||
intersect4 = intersect(t_list_of_int, t_list_one_int)
|
|
||||||
test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)
|
|
||||||
|
|
||||||
# list(integer) & [5, :foo] -> should be none
|
|
||||||
intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
|
|
||||||
test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())
|
|
||||||
|
|
||||||
IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
defmodule AdhocTest do
|
|
||||||
import Tdd
|
|
||||||
|
|
||||||
def run(test_fn) do
|
|
||||||
# --- Basic Types ---
|
|
||||||
t_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))
|
|
||||||
intersect4 = intersect(t_list_of_int, t_list_one_int)
|
|
||||||
IO.inspect("first_subtype")
|
|
||||||
a = is_subtype(intersect4, t_list_one_int)
|
|
||||||
IO.inspect("second_subtype")
|
|
||||||
b = is_subtype(t_list_one_int, intersect4)
|
|
||||||
test_fn.("list(integer) & [5] == [5]", true, a == b)
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
|
|
||||||
test_all.()
|
|
||||||
Loading…
x
Reference in New Issue
Block a user