9a89757bcd
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
assert_equivalent_specs(spec, :integer)
618 lines
24 KiB
Elixir
618 lines
24 KiB
Elixir
defmodule TddSystemTest do
|
||
# Most tests mutate Tdd.Store, so they cannot run concurrently.
|
||
use ExUnit.Case, async: false
|
||
|
||
alias Tdd.TypeSpec
|
||
alias Tdd.Store
|
||
alias Tdd.Variable
|
||
alias Tdd.Compiler
|
||
alias Tdd.Consistency.Engine
|
||
alias Tdd.Algo
|
||
alias Tdd.Debug
|
||
|
||
# Helper to mimic the old test structure and provide better failure messages
|
||
# for spec comparisons.
|
||
defp assert_spec_normalized(expected, input_spec) do
|
||
result = TypeSpec.normalize(input_spec)
|
||
# The normalization process should produce a canonical, sorted form.
|
||
assert expected == result, """
|
||
Input Spec:
|
||
#{inspect(input_spec, pretty: true)}
|
||
|
||
Expected Normalized:
|
||
#{inspect(expected, pretty: true)}
|
||
|
||
Actual Normalized:
|
||
#{inspect(result, pretty: true)}
|
||
"""
|
||
end
|
||
|
||
# Helper to check for equivalence by comparing TDD IDs.
|
||
defmacro assert_equivalent_specs(spec1, spec2) do
|
||
quote do
|
||
id1 = Compiler.spec_to_id(unquote(spec1))
|
||
id2 = Compiler.spec_to_id(unquote(spec2))
|
||
# Debug.build_graph_map(id1, "assert_equivalent_specs id1")
|
||
# Debug.build_graph_map(id2, "assert_equivalent_specs id2")
|
||
Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
|
||
Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
|
||
IO.inspect("equvalent specs? #{id1} #{id2}")
|
||
assert id1 == id2
|
||
end
|
||
end
|
||
|
||
# Helper to check for subtyping using the TDD compiler.
|
||
defmacro assert_subtype(spec1, spec2) do
|
||
quote do
|
||
IO.inspect("assert is_subtype #{inspect(unquote(spec1))}, #{inspect(unquote(spec2))}")
|
||
is_subtype? = Compiler.is_subtype(unquote(spec1), unquote(spec2))
|
||
Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
|
||
Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
|
||
assert is_subtype?
|
||
end
|
||
end
|
||
|
||
defmacro refute_subtype(spec1, spec2) do
|
||
quote do
|
||
refute Compiler.is_subtype(unquote(spec1), unquote(spec2))
|
||
end
|
||
end
|
||
|
||
# Setup block that initializes the Tdd.Store before each test.
|
||
# This ensures that node IDs and caches are clean for every test case.
|
||
setup do
|
||
Tdd.Store.init()
|
||
:ok
|
||
end
|
||
|
||
# ---
|
||
# Tdd.Store Tests
|
||
# These tests validate the lowest-level state management of the TDD system.
|
||
# The Store is responsible for creating and storing the nodes of the decision diagram graph.
|
||
# ---
|
||
describe "Tdd.Store: Core state management for the TDD graph" do
|
||
@doc """
|
||
Tests that the store initializes with the correct, reserved IDs for the
|
||
terminal nodes representing TRUE (:any) and FALSE (:none).
|
||
"""
|
||
test "initialization and terminals" do
|
||
assert Store.true_node_id() == 1
|
||
assert Store.false_node_id() == 0
|
||
assert Store.get_node(1) == {:ok, :true_terminal}
|
||
assert Store.get_node(0) == {:ok, :false_terminal}
|
||
assert Store.get_node(99) == {:error, :not_found}
|
||
end
|
||
|
||
@doc """
|
||
Tests the core functionality of creating nodes. It verifies that new nodes receive
|
||
incrementing IDs and that requesting an identical node reuses the existing one
|
||
(structural sharing), which is fundamental to the efficiency of TDDs.
|
||
"""
|
||
test "node creation and structural sharing" do
|
||
var_a = {:is_atom}
|
||
var_b = {:is_integer}
|
||
true_id = Store.true_node_id()
|
||
false_id = Store.false_node_id()
|
||
|
||
# First created node gets ID 2 (after 0 and 1 are taken by terminals)
|
||
id1 = Store.find_or_create_node(var_a, true_id, false_id, false_id)
|
||
assert id1 == 2
|
||
assert Store.get_node(id1) == {:ok, {var_a, true_id, false_id, false_id}}
|
||
|
||
# Second, different node gets the next ID
|
||
id2 = Store.find_or_create_node(var_b, id1, false_id, false_id)
|
||
assert id2 == 3
|
||
|
||
# Creating the first node again returns the same ID, not a new one
|
||
id1_again = Store.find_or_create_node(var_a, true_id, false_id, false_id)
|
||
assert id1_again == id1
|
||
|
||
# Next new node gets the correct subsequent ID, proving no ID was wasted
|
||
id3 = Store.find_or_create_node(var_b, true_id, false_id, false_id)
|
||
assert id3 == 4
|
||
end
|
||
|
||
@doc """
|
||
Tests a key reduction rule: if a node's 'yes', 'no', and 'don't care' branches
|
||
all point to the same child node, the parent node is redundant and should be
|
||
replaced by the child node itself.
|
||
"""
|
||
test "node reduction rule for identical children" do
|
||
var_a = {:is_atom}
|
||
# from previous test logic
|
||
id3 = 4
|
||
id_redundant = Store.find_or_create_node(var_a, id3, id3, id3)
|
||
assert id_redundant == id3
|
||
end
|
||
|
||
@doc """
|
||
Tests the memoization cache for operations like 'apply', 'negate', etc.
|
||
This ensures that repeated operations with the same inputs do not trigger
|
||
redundant computations.
|
||
"""
|
||
test "operation caching" do
|
||
cache_key = {:my_op, 1, 2}
|
||
assert Store.get_op_cache(cache_key) == :not_found
|
||
|
||
Store.put_op_cache(cache_key, :my_result)
|
||
assert Store.get_op_cache(cache_key) == {:ok, :my_result}
|
||
|
||
Store.put_op_cache(cache_key, :new_result)
|
||
assert Store.get_op_cache(cache_key) == {:ok, :new_result}
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Tdd.TypeSpec.normalize/1 Tests
|
||
# These tests focus on ensuring the `normalize` function correctly transforms
|
||
# any TypeSpec into its canonical, simplified form.
|
||
# ---
|
||
describe "Tdd.TypeSpec.normalize/1: Base & Simple Types" do
|
||
@doc "Tests that normalizing already-simple specs doesn't change them (idempotency)."
|
||
test "normalizing :any is idempotent" do
|
||
assert_spec_normalized(:any, :any)
|
||
end
|
||
|
||
test "normalizing :none is idempotent" do
|
||
assert_spec_normalized(:none, :none)
|
||
end
|
||
|
||
test "normalizing :atom is idempotent" do
|
||
assert_spec_normalized(:atom, :atom)
|
||
end
|
||
|
||
test "normalizing a literal is idempotent" do
|
||
assert_spec_normalized({:literal, :foo}, {:literal, :foo})
|
||
end
|
||
end
|
||
|
||
describe "Tdd.TypeSpec.normalize/1: Double Negation" do
|
||
@doc "Tests the logical simplification that ¬(¬A) is equivalent to A."
|
||
test "¬(¬atom) simplifies to atom" do
|
||
assert_spec_normalized(:atom, {:negation, {:negation, :atom}})
|
||
end
|
||
|
||
@doc "Tests that a single negation is preserved when it cannot be simplified further."
|
||
test "A single negation is preserved" do
|
||
assert_spec_normalized({:negation, :integer}, {:negation, :integer})
|
||
end
|
||
|
||
@doc "Tests that an odd integer of negations simplifies to a single negation."
|
||
test "¬(¬(¬atom)) simplifies to ¬atom" do
|
||
assert_spec_normalized({:negation, :atom}, {:negation, {:negation, {:negation, :atom}}})
|
||
end
|
||
end
|
||
|
||
describe "Tdd.TypeSpec.normalize/1: Union Normalization" do
|
||
@doc """
|
||
Tests that unions are canonicalized by flattening nested unions, sorting the members,
|
||
and removing duplicates. e.g., `int | (list | atom | int)` becomes `(atom | int | list)`.
|
||
"""
|
||
test "flattens, sorts, and uniques members" do
|
||
input = {:union, [:integer, {:union, [:list, :atom, :integer]}]}
|
||
expected = {:union, [:atom, :integer, :list]}
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
|
||
@doc "Tests `A | none` simplifies to `A`, as `:none` is the identity for union."
|
||
test "simplifies a union with :none (A | none -> A)" do
|
||
assert_spec_normalized(:atom, {:union, [:atom, :none]})
|
||
end
|
||
|
||
@doc "Tests `A | any` simplifies to `any`, as `:any` is the absorbing element for union."
|
||
test "simplifies a union with :any (A | any -> any)" do
|
||
assert_spec_normalized(:any, {:union, [:atom, :any]})
|
||
end
|
||
|
||
@doc "An empty set of types is logically equivalent to `:none`."
|
||
test "an empty union simplifies to :none" do
|
||
assert_spec_normalized(:none, {:union, []})
|
||
end
|
||
|
||
@doc "A union containing just one type should simplify to that type itself."
|
||
test "a union of a single element simplifies to the element itself" do
|
||
assert_spec_normalized(:atom, {:union, [:atom]})
|
||
end
|
||
end
|
||
|
||
describe "Tdd.TypeSpec.normalize/1: Intersection Normalization" do
|
||
@doc "Tests that intersections are canonicalized like unions (flatten, sort, unique)."
|
||
test "flattens, sorts, and uniques members" do
|
||
input = {:intersect, [:integer, {:intersect, [:list, :atom, :integer]}]}
|
||
expected = {:intersect, [:atom, :integer, :list]}
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
|
||
@doc "Tests `A & any` simplifies to `A`, as `:any` is the identity for intersection."
|
||
test "simplifies an intersection with :any (A & any -> A)" do
|
||
assert_spec_normalized(:atom, {:intersect, [:atom, :any]})
|
||
end
|
||
|
||
@doc "Tests `A & none` simplifies to `none`, as `:none` is the absorbing element."
|
||
test "simplifies an intersection with :none (A & none -> none)" do
|
||
assert_spec_normalized(:none, {:intersect, [:atom, :none]})
|
||
end
|
||
|
||
@doc "An intersection of zero types is logically `any` (no constraints)."
|
||
test "an empty intersection simplifies to :any" do
|
||
assert_spec_normalized(:any, {:intersect, []})
|
||
end
|
||
|
||
@doc "An intersection of one type simplifies to the type itself."
|
||
test "an intersection of a single element simplifies to the element itself" do
|
||
assert_spec_normalized(:atom, {:intersect, [:atom]})
|
||
end
|
||
end
|
||
|
||
describe "Tdd.TypeSpec.normalize/1: Subtype Reduction" do
|
||
@doc """
|
||
Tests a key simplification: if a union contains a type and its own subtype,
|
||
the subtype is redundant and should be removed. E.g., `(1 | integer)` is just `integer`.
|
||
Here, `:foo` and `:bar` are subtypes of `:atom`, so the union simplifies to `:atom`.
|
||
"""
|
||
test "(:foo | :bar | atom) simplifies to atom" do
|
||
input = {:union, [{:literal, :foo}, {:literal, :bar}, :atom]}
|
||
expected = :atom
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
end
|
||
|
||
describe "Tdd.TypeSpec: Advanced Normalization (μ, Λ, Apply)" do
|
||
@doc """
|
||
Tests alpha-conversion for recursive types. The bound variable name (`:X`)
|
||
should be renamed to a canonical name (`:m_var0`) to ensure structural equality
|
||
regardless of the name chosen by the user.
|
||
"""
|
||
test "basic alpha-conversion for μ-variable" do
|
||
input = {:mu, :X, {:type_var, :X}}
|
||
expected = {:mu, :m_var0, {:type_var, :m_var0}}
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
|
||
@doc """
|
||
Tests that the syntactic sugar `{:list_of, T}` is correctly desugared into
|
||
its underlying recursive definition: `μT.[] | cons(T, μT)`.
|
||
"""
|
||
test "list_of(integer) normalizes to a μ-expression with canonical var" do
|
||
input = {:list_of, :integer}
|
||
|
||
expected =
|
||
{:mu, :m_var0, {:union, [{:literal, []}, {:cons, :integer, {:type_var, :m_var0}}]}}
|
||
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
|
||
@doc """
|
||
Tests beta-reduction (function application). Applying the identity function
|
||
`(ΛT.T)` to `integer` should result in `integer`.
|
||
"""
|
||
test "simple application: (ΛT.T) integer -> integer" do
|
||
input = {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer]}
|
||
expected = :integer
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
|
||
@doc """
|
||
Tests a more complex beta-reduction. Applying a list constructor lambda
|
||
to `:atom` should produce the normalized form of `list_of(atom)`.
|
||
"""
|
||
test "application with structure: (ΛT. list_of(T)) atom -> list_of(atom) (normalized form)" do
|
||
input = {:type_apply, {:type_lambda, [:T], {:list_of, {:type_var, :T}}}, [:atom]}
|
||
expected = {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var0}}]}}
|
||
assert_spec_normalized(expected, input)
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Tdd.Consistency.Engine Tests
|
||
# These tests validate the logic that detects contradictions in a set of predicate assumptions.
|
||
# ---
|
||
describe "Tdd.Consistency.Engine: Logic for detecting contradictions" do
|
||
# This setup is local to this describe block, which is fine.
|
||
setup do
|
||
Tdd.Store.init()
|
||
id_atom = Tdd.Compiler.spec_to_id(:atom)
|
||
%{id_atom: id_atom}
|
||
end
|
||
|
||
@doc "An empty set of assumptions has no contradictions."
|
||
test "an empty assumption map is consistent" do
|
||
assert Engine.check(%{}) == :consistent
|
||
end
|
||
|
||
@doc """
|
||
Tests that the engine uses predicate traits to find implied contradictions.
|
||
`v_atom_eq(:foo)` implies `v_is_atom()` is true, which contradicts the explicit
|
||
assumption that `v_is_atom()` is false.
|
||
"""
|
||
test "an implied contradiction is caught by expander" do
|
||
assumptions = %{Variable.v_atom_eq(:foo) => true, Variable.v_is_atom() => false}
|
||
assert Engine.check(assumptions) == :contradiction
|
||
end
|
||
|
||
@doc "A term cannot belong to two different primary types like :atom and :integer."
|
||
test "two primary types cannot both be true" do
|
||
assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true}
|
||
assert Engine.check(assumptions) == :contradiction
|
||
end
|
||
|
||
@doc "A list cannot be empty and simultaneously have properties on its head (which wouldn't exist)."
|
||
test "a list cannot be empty and have a head property", %{id_atom: id_atom} do
|
||
assumptions = %{
|
||
Variable.v_list_is_empty() => true,
|
||
Variable.v_list_head_pred(id_atom) => true
|
||
}
|
||
|
||
assert Engine.check(assumptions) == :contradiction
|
||
end
|
||
|
||
@doc "Tests for logical contradictions in integer ranges."
|
||
test "int < 10 AND int > 20 is a contradiction" do
|
||
assumptions = %{
|
||
Variable.v_int_lt(10) => true,
|
||
Variable.v_int_gt(20) => true
|
||
}
|
||
|
||
assert Engine.check(assumptions) == :contradiction
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Compiler & Algo Integration Tests
|
||
# These tests ensure that the high-level public APIs (`is_subtype`, `spec_to_id`)
|
||
# work correctly by integrating the compiler and the graph algorithms.
|
||
# ---
|
||
describe "Tdd.Compiler and Tdd.Algo Integration: High-level API validation" do
|
||
@doc "Verifies semantic equivalence of types using TDD IDs. e.g., `atom & any` is the same type as `atom`."
|
||
test "basic equivalences" do
|
||
assert_equivalent_specs({:intersect, [:atom, :any]}, :atom)
|
||
assert_equivalent_specs({:union, [:atom, :none]}, :atom)
|
||
assert_equivalent_specs({:intersect, [:atom, :integer]}, :none)
|
||
end
|
||
|
||
@doc "Tests the main `is_subtype` public API for simple, non-recursive types."
|
||
test "basic subtyping" do
|
||
assert_subtype({:literal, :foo}, :atom)
|
||
refute_subtype(:atom, {:literal, :foo})
|
||
assert_subtype(:none, :atom)
|
||
assert_subtype(:atom, :any)
|
||
end
|
||
|
||
@doc "Tests that impossible type intersections compile to the `:none` (FALSE) node."
|
||
test "contradictions" do
|
||
assert Compiler.spec_to_id({:intersect, [:atom, :integer]}) == Store.false_node_id()
|
||
|
||
assert Compiler.spec_to_id({:intersect, [{:literal, :foo}, {:literal, :bar}]}) ==
|
||
Store.false_node_id()
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Tdd.Compiler Advanced Feature Tests
|
||
# These tests target the most complex features: recursive and polymorphic types.
|
||
# ---
|
||
describe "Tdd.Compiler: Advanced Features (μ, Λ, Apply)" do
|
||
test "list subtyping: list(int) <: list(any)" do
|
||
int_list = {:list_of, :integer}
|
||
any_list = {:list_of, :any}
|
||
assert_subtype(:integer, :any)
|
||
assert_subtype(int_list, any_list)
|
||
assert_subtype({:cons, {:literal, 1}, {:literal, []}}, int_list)
|
||
end
|
||
|
||
test "list subtyping: list(any) <! list(integer)" do
|
||
int_list = {:list_of, :integer}
|
||
any_list = {:list_of, :any}
|
||
assert_subtype(:integer, :any)
|
||
refute_subtype({:cons, {:literal, :a}, {:literal, []}}, int_list)
|
||
refute_subtype(any_list, int_list)
|
||
end
|
||
|
||
@doc "Tests that manually-defined recursive types (like a binary tree) can be compiled and checked correctly."
|
||
test "explicit μ-types" do
|
||
leaf_node = {:literal, :empty_tree}
|
||
|
||
tree_spec =
|
||
{:mu, :Tree,
|
||
{:union,
|
||
[
|
||
leaf_node,
|
||
{:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]}
|
||
]}}
|
||
|
||
# Test that it compiles to a valid TDD ID
|
||
assert is_integer(Compiler.spec_to_id(tree_spec))
|
||
|
||
# Test that an instance of the tree is correctly identified as a subtype
|
||
simple_tree_instance = {:tuple, [{:literal, :a}, leaf_node, leaf_node]}
|
||
assert_subtype(simple_tree_instance, tree_spec)
|
||
end
|
||
|
||
@doc """
|
||
Tests that a polymorphic type created via lambda application is equivalent
|
||
to its manually specialized counterpart. e.g., `(List<T>)(int)` should be the
|
||
same as `List<int>`.
|
||
"""
|
||
test "polymorphism (Λ, Apply)" do
|
||
gen_list_lambda = {:type_lambda, [:Tparam], {:list_of, {:type_var, :Tparam}}}
|
||
list_of_int_from_apply = {:type_apply, gen_list_lambda, [:integer]}
|
||
int_list = {:list_of, :integer}
|
||
|
||
assert_equivalent_specs(list_of_int_from_apply, int_list)
|
||
end
|
||
|
||
test "negate list type" do
|
||
refute_subtype({:negation, {:list_of, :integer}}, :none)
|
||
end
|
||
end
|
||
|
||
describe "Logical Equivalences: De Morgan's Laws & Distributivity" do
|
||
@doc "Tests ¬(A ∪ B) <=> (¬A ∩ ¬B)"
|
||
test "De Morgan's Law for negated unions" do
|
||
# ¬(atom | integer)
|
||
spec1 = {:negation, {:union, [:atom, :integer]}}
|
||
# ¬atom & ¬integer
|
||
spec2 = {:intersect, [{:negation, :atom}, {:negation, :integer}]}
|
||
assert_equivalent_specs(spec1, spec2)
|
||
end
|
||
|
||
@doc "Tests ¬(A ∩ B) <=> (¬A ∪ ¬B)"
|
||
test "De Morgan's Law for negated intersections" do
|
||
# ¬(integer & atom)
|
||
spec1 = {:negation, {:intersect, [:integer, :atom]}}
|
||
# ¬integer | ¬atom
|
||
spec2 = {:union, [{:negation, :integer}, {:negation, :atom}]}
|
||
assert_equivalent_specs(spec1, spec2)
|
||
end
|
||
|
||
@doc "Tests A ∩ (B ∪ C) <=> (A ∩ B) ∪ (A ∩ C)"
|
||
test "Distributive Law: intersection over union" do
|
||
# We'll use types where some intersections are meaningful and others are :none
|
||
# `integer` is a supertype of `integer` and `tuple`
|
||
# `(integer | tuple) & (atom | integer)`
|
||
spec1 =
|
||
{:intersect, [{:union, [:integer, :tuple]}, {:union, [:atom, :integer]}]}
|
||
|
||
# Should be equivalent to:
|
||
# (integer & atom) | (integer & integer) | (tuple & atom) | (tuple & integer)
|
||
# which simplifies to:
|
||
# :none | :integer | :none | :none
|
||
# which is just :integer
|
||
Debug.print_tdd_graph(Compiler.spec_to_id(spec1))
|
||
assert_equivalent_specs(spec1, :integer)
|
||
end
|
||
|
||
@doc "Tests A | (B & C) versus (A | B) & (A | C) -- they are NOT always equivalent"
|
||
test "subtyping with distributivity" do
|
||
# Let's test `A | (B & C) <: (A | B) & (A | C)`
|
||
spec_left = {:union, [:atom, {:intersect, [:integer, {:integer_range, 0, :pos_inf}]}]}
|
||
|
||
spec_right =
|
||
{:intersect,
|
||
[{:union, [:atom, :integer]}, {:union, [:atom, {:integer_range, 0, :pos_inf}]}]}
|
||
|
||
# `spec_left` normalizes to `atom | positive_integer`
|
||
# `spec_right` normalizes to `(atom | integer) & (atom | positive_integer)`
|
||
# Since `atom | positive_integer` is a subtype of `atom | integer`, the intersection on the right
|
||
# simplifies to `atom | positive_integer`. Therefore, they are equivalent in this case.
|
||
assert_equivalent_specs(spec_left, spec_right)
|
||
|
||
spec_sub = {:union, [:integer, {:intersect, [:atom, :tuple]}]}
|
||
spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :tuple]}]}
|
||
assert_subtype(spec_sub, spec_super)
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Advanced Negation and Contradiction Tests
|
||
# ---
|
||
describe "Tdd.Compiler: Advanced Negation and Contradiction" do
|
||
@doc "Tests that a type and its negation correctly partition the universal set (:any)."
|
||
test "A | ¬A <=> :any" do
|
||
spec = {:union, [:integer, {:negation, :integer}]}
|
||
assert_equivalent_specs(spec, :any)
|
||
end
|
||
|
||
@doc "Tests that a subtype relationship holds against a negated supertype"
|
||
test "subtyping with negation: integer <: ¬atom" do
|
||
# An integer is never an atom, so it should be a subtype of "not atom".
|
||
assert_subtype(:integer, {:negation, :atom})
|
||
# The reverse is not true: `not atom` includes lists, integers, etc.
|
||
refute_subtype({:negation, :atom}, :integer)
|
||
end
|
||
|
||
@doc "A complex type that should resolve to :none"
|
||
test "complex contradiction involving subtype logic" do
|
||
# This is `(integer and not a integer)`. Since all integers are integers, this is impossible.
|
||
spec = {:intersect, [:integer, {:negation, :integer}]}
|
||
assert_equivalent_specs(spec, :none)
|
||
end
|
||
|
||
@doc "The type 'list of integers that are also atoms' should be impossible"
|
||
test "contradiction inside a recursive type structure" do
|
||
# list_of(integer & atom) is list_of(:none).
|
||
# A list of :none can only be the empty list, as no element can ever exist.
|
||
spec = {:list_of, {:intersect, [:integer, :atom]}}
|
||
Tdd.Store.init()
|
||
Debug.print_tdd_graph(Compiler.spec_to_id(spec))
|
||
Debug.print_tdd_graph(Compiler.spec_to_id({:literal, []}))
|
||
assert_equivalent_specs(spec, {:literal, []})
|
||
end
|
||
end
|
||
|
||
# ---
|
||
# Complex Recursive (μ) and Polymorphic (Λ, Apply) Tests
|
||
# These tests probe the interaction between recursion, polymorphism, and subtyping.
|
||
# ---
|
||
describe "Tdd.Compiler: Interplay of μ, Λ, and Subtyping" do
|
||
@doc "Tests subtyping between structurally similar, but not identical, recursive types."
|
||
test "subtyping of structural recursive types: list_of(1|2) <: list_of(integer)" do
|
||
list_of_1_or_2 = {:list_of, {:union, [{:literal, 1}, {:literal, 2}]}}
|
||
list_of_integer = {:list_of, :integer}
|
||
|
||
assert_subtype(list_of_1_or_2, list_of_integer)
|
||
refute_subtype(list_of_integer, list_of_1_or_2)
|
||
end
|
||
|
||
@doc "Tests a non-sensical recursion that should simplify away"
|
||
test "μ-types that should normalize to a non-recursive form" do
|
||
# A type defined as "a cons of an atom and itself, or none" should be equivalent to `list_of(atom)`.
|
||
# This tests if our manual mu-calculus definition matches the syntactic sugar.
|
||
manual_list_of_atom = {:mu, :L, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :L}}]}}
|
||
sugar_list_of_atom = {:list_of, :atom}
|
||
assert_equivalent_specs(manual_list_of_atom, sugar_list_of_atom)
|
||
end
|
||
|
||
test "infer termination of recursive types" do
|
||
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
|
||
assert_equivalent_specs(spec, :integer)
|
||
end
|
||
|
||
@doc "Tests polymorphism with multiple type parameters."
|
||
test "lambda with multiple parameters: (Λ(A,B). {A,B})(int, atom)" do
|
||
# λ(A, B). {A, B}
|
||
map_constructor = {:type_lambda, [:A, :B], {:tuple, [{:type_var, :A}, {:type_var, :B}]}}
|
||
# Apply it to integer and atom
|
||
applied_spec = {:type_apply, map_constructor, [:integer, :atom]}
|
||
# The result should be the concrete type {integer, atom}
|
||
expected_spec = {:tuple, [:integer, :atom]}
|
||
|
||
assert_equivalent_specs(applied_spec, expected_spec)
|
||
end
|
||
|
||
@doc "Tests that applying a lambda to a complex recursive type works correctly"
|
||
test "applying a polymorphic list constructor to a tree type" do
|
||
# First, define our tree type from a previous test
|
||
leaf_node = {:literal, :empty_tree}
|
||
|
||
tree_spec =
|
||
{:mu, :Tree,
|
||
{:union,
|
||
[
|
||
leaf_node,
|
||
{:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]}
|
||
]}}
|
||
|
||
# Now, apply the generic list lambda to this tree_spec
|
||
gen_list_lambda = {:type_lambda, [:T], {:list_of, {:type_var, :T}}}
|
||
list_of_trees = {:type_apply, gen_list_lambda, [tree_spec]}
|
||
|
||
# Check if a concrete instance is a subtype of this new complex type
|
||
tree_instance_1 = {:tuple, [{:literal, :a}, leaf_node, leaf_node]}
|
||
tree_instance_2 = {:tuple, [{:literal, :b}, leaf_node, leaf_node]}
|
||
list_of_trees_instance = {:cons, tree_instance_1, {:cons, tree_instance_2, {:literal, []}}}
|
||
|
||
assert_subtype(list_of_trees_instance, list_of_trees)
|
||
end
|
||
|
||
# failing
|
||
@doc "An 'ill-formed' recursive type that should evaluate to :none"
|
||
test "μ-types that are self-contradictory should be :none" do
|
||
# A type defined as `μX. cons(integer, X)`. This describes an infinite list
|
||
# of integers with no base case (`[]`). No finite value can ever satisfy this type.
|
||
infinite_list = {:mu, :X, {:cons, :integer, {:type_var, :X}}}
|
||
assert_equivalent_specs(infinite_list, :none)
|
||
end
|
||
end
|
||
end
|