added more FAILING tests
This commit is contained in:
Kacper Marzecki
parent
3ea8d80801
commit
2854c4559c
@ -8,6 +8,7 @@ defmodule TddSystemTest do
|
||||
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.
|
||||
@ -165,7 +166,7 @@ defmodule TddSystemTest do
|
||||
assert_spec_normalized({:negation, :integer}, {:negation, :integer})
|
||||
end
|
||||
|
||||
@doc "Tests that an odd number of negations simplifies to a single negation."
|
||||
@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
|
||||
@ -433,4 +434,173 @@ defmodule TddSystemTest 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, :positive_integer]}]}
|
||||
|
||||
spec_right =
|
||||
{:intersect, [{:union, [:atom, :integer]}, {:union, [:atom, :positive_integer]}]}
|
||||
|
||||
# `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)
|
||||
|
||||
# However, let's create a case where it's only a subtype relationship
|
||||
# `integer | (atom & pid)` should be `integer | :none` which is `integer`.
|
||||
# `(integer | atom) & (integer | pid)` is a much larger type.
|
||||
# simplifies to :integer
|
||||
spec_sub = {:union, [:integer, {:intersect, [:atom, :pid]}]}
|
||||
spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :pid]}]}
|
||||
assert_subtype(spec_sub, spec_super)
|
||||
refute_subtype(spec_super, spec_sub)
|
||||
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]}}
|
||||
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 "itself or an integer" should be equivalent to just "integer",
|
||||
# because any finite instance of it must eventually terminate with an integer.
|
||||
spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
|
||||
assert_equivalent_specs(spec, :integer)
|
||||
|
||||
# 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
|
||||
|
||||
@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
|
||||
|
||||
@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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user