643 lines
23 KiB
Elixir
643 lines
23 KiB
Elixir
defmodule Tdd do
|
|
# --- Existing code from your previous version ---
|
|
# (init_tdd_system, get_state, update_state, make_node, get_node_details,
|
|
# variable definitions, basic type constructors, apply, sum, print_tdd)
|
|
# Ensure your `apply/4` function is the corrected version from the MatchError fix.
|
|
@moduledoc """
|
|
Ternary decision diagram for set-theoretic types.
|
|
"""
|
|
|
|
# --- Terminal Node IDs ---
|
|
@false_node_id 0
|
|
@true_node_id 1
|
|
|
|
defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id
|
|
|
|
def init_tdd_system do
|
|
Process.put(:nodes, %{})
|
|
|
|
Process.put(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal})
|
|
|
|
Process.put(:next_id, 2)
|
|
Process.put(:op_cache, %{})
|
|
IO.puts("TDD system initialized.")
|
|
end
|
|
|
|
defp get_state do
|
|
%{
|
|
nodes: Process.get(:nodes, %{}),
|
|
node_by_id:
|
|
Process.get(:node_by_id, %{
|
|
@false_node_id => :false_terminal,
|
|
@true_node_id => :true_terminal
|
|
}),
|
|
next_id: Process.get(:next_id, 2),
|
|
op_cache: Process.get(:op_cache, %{})
|
|
}
|
|
end
|
|
|
|
defp update_state(changes) do
|
|
current_state = get_state()
|
|
new_state = Map.merge(current_state, changes)
|
|
Process.put(:nodes, new_state.nodes)
|
|
Process.put(:node_by_id, new_state.node_by_id)
|
|
Process.put(:next_id, new_state.next_id)
|
|
Process.put(:op_cache, new_state.op_cache)
|
|
end
|
|
|
|
# --- Raw Node Creation (Structural) ---
|
|
# This is the original make_node, focused on structural uniqueness and basic reduction rule.
|
|
defp make_node_raw(variable, yes_id, no_id, dc_id) do
|
|
# Basic reduction: if all children are identical, this node is redundant.
|
|
if yes_id == no_id && yes_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
|
|
# Node already exists (structural sharing)
|
|
state.nodes[node_tuple]
|
|
else
|
|
# Create new node
|
|
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
|
|
|
|
# --- Public Node Creation (Currently same as raw, apply will handle context) ---
|
|
# The `apply` algorithm inherently creates the necessary structure.
|
|
# Semantic simplification is applied *after* `apply` completes.
|
|
def make_node(variable, yes_id, no_id, dc_id) do
|
|
make_node_raw(variable, yes_id, no_id, dc_id)
|
|
end
|
|
|
|
# --- Semantic Constraint Checking ---
|
|
# assumptions_map is {variable_id => value (true, false, :dc)}
|
|
defp check_assumptions_consistency(assumptions_map) do
|
|
primary_true_predicates =
|
|
Enum.reduce(assumptions_map, MapSet.new(), fn
|
|
{{0, predicate_name}, true}, acc_set -> MapSet.put(acc_set, predicate_name)
|
|
_otherwise, acc_set -> acc_set
|
|
end)
|
|
|
|
IO.inspect({assumptions_map, primary_true_predicates, MapSet.size(primary_true_predicates)},
|
|
label: "CheckConsistency"
|
|
)
|
|
|
|
if MapSet.size(primary_true_predicates) > 1 do
|
|
:contradiction
|
|
else
|
|
# TODO: Add more semantic checks here, e.g.:
|
|
# - {v_int_lt_N, true} and {v_int_gt_M, true} where N <= M.
|
|
# - {v_tuple_size_eq_2, true} and {v_tuple_size_eq_3, true}.
|
|
:consistent
|
|
end
|
|
end
|
|
|
|
# --- Semantic Simplification (Memoized) ---
|
|
defp simplify_with_constraints(tdd_id, assumptions_map) do
|
|
state = get_state()
|
|
sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
|
|
cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
|
|
|
|
cond do
|
|
is_terminal_id(tdd_id) ->
|
|
tdd_id
|
|
|
|
Map.has_key?(state.op_cache, cache_key) ->
|
|
state.op_cache[cache_key]
|
|
|
|
check_assumptions_consistency(assumptions_map) == :contradiction ->
|
|
# Path is semantically impossible
|
|
# Important
|
|
IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction")
|
|
update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
|
|
@false_node_id
|
|
|
|
true ->
|
|
{var, y, n, d} = get_node_details(tdd_id)
|
|
|
|
result_id =
|
|
case Map.get(assumptions_map, var) do
|
|
# Current var is assumed true in path, follow yes branch
|
|
true ->
|
|
simplify_with_constraints(y, assumptions_map)
|
|
|
|
# Current var is assumed false in path, follow no branch
|
|
false ->
|
|
simplify_with_constraints(n, assumptions_map)
|
|
|
|
# Current var is assumed don't care in path, follow dc branch
|
|
:dc ->
|
|
simplify_with_constraints(d, assumptions_map)
|
|
|
|
# Current var is not in assumptions, so it's a decision point.
|
|
nil ->
|
|
# Recursively simplify children by adding this var's assignment to assumptions.
|
|
simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
|
|
simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
|
|
# Assuming :dc can be an assumption value
|
|
simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
|
|
make_node_raw(var, simplified_y, simplified_n, simplified_d)
|
|
end
|
|
|
|
IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExit")
|
|
update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
|
|
result_id
|
|
end
|
|
end
|
|
|
|
# --- Public Node Creation (Used by Type Constructors) ---
|
|
# Type constructors will create a raw TDD and then simplify it.
|
|
defp make_node_for_constructors(variable, yes_id, no_id, dc_id) do
|
|
raw_id = make_node_raw(variable, yes_id, no_id, dc_id)
|
|
# Simplify with no initial assumptions
|
|
simplify_with_constraints(raw_id, %{})
|
|
end
|
|
|
|
def get_node_details(id) when is_terminal_id(id) do
|
|
if id == @true_node_id, do: :true_terminal, else: :false_terminal
|
|
end
|
|
|
|
def get_node_details(id) do
|
|
state = get_state()
|
|
state.node_by_id[id]
|
|
end
|
|
|
|
@v_is_atom {0, :is_atom}
|
|
@v_is_tuple {0, :is_tuple}
|
|
|
|
def v_atom_eq(atom_val), do: {1, :value, atom_val}
|
|
def v_tuple_size_eq(size), do: {4, :size, size}
|
|
def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}
|
|
|
|
def type_any, do: @true_node_id
|
|
def type_none, do: @false_node_id
|
|
|
|
def type_atom do
|
|
# Raw structure: if is_atom then True, else False, dc False
|
|
# This structure is already semantically simple.
|
|
make_node_for_constructors(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
|
|
end
|
|
|
|
def type_atom_literal(atom_val) do
|
|
var_eq = v_atom_eq(atom_val)
|
|
atom_val_node = make_node_raw(var_eq, @true_node_id, @false_node_id, @false_node_id)
|
|
raw_node = make_node_raw(@v_is_atom, atom_val_node, @false_node_id, @false_node_id)
|
|
simplify_with_constraints(raw_node, %{})
|
|
end
|
|
|
|
def type_tuple do
|
|
make_node_for_constructors(@v_is_tuple, @true_node_id, @false_node_id, @false_node_id)
|
|
end
|
|
|
|
def type_empty_tuple do
|
|
var_size_0 = v_tuple_size_eq(0)
|
|
tuple_size_node = make_node_raw(var_size_0, @true_node_id, @false_node_id, @false_node_id)
|
|
raw_node = make_node_raw(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
|
|
simplify_with_constraints(raw_node, %{})
|
|
end
|
|
|
|
def type_tuple_sized_any(size) do
|
|
var_size = v_tuple_size_eq(size)
|
|
tuple_size_node = make_node_raw(var_size, @true_node_id, @false_node_id, @false_node_id)
|
|
raw_node = make_node_raw(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
|
|
simplify_with_constraints(raw_node, %{})
|
|
end
|
|
|
|
# --- The APPLY Algorithm (Core Logic, uses make_node_raw) ---
|
|
# This function computes the raw structural result. Semantic simplification is applied by the caller.
|
|
defp apply_raw(op_name, op_lambda, u1_id, u2_id) do
|
|
state = get_state()
|
|
# apply_raw cache key
|
|
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_symbol = op_lambda.(get_node_details(u1_id), get_node_details(u2_id))
|
|
if res_terminal_symbol == :true_terminal, do: @true_node_id, else: @false_node_id
|
|
|
|
true ->
|
|
u1_details = get_node_details(u1_id)
|
|
u2_details = get_node_details(u2_id)
|
|
|
|
result_id =
|
|
cond do
|
|
u1_details == :true_terminal or u1_details == :false_terminal ->
|
|
{var2, y2, n2, d2} = u2_details
|
|
res_y = apply_raw(op_name, op_lambda, u1_id, y2)
|
|
res_n = apply_raw(op_name, op_lambda, u1_id, n2)
|
|
res_d = apply_raw(op_name, op_lambda, u1_id, d2)
|
|
make_node_raw(var2, res_y, res_n, res_d)
|
|
|
|
u2_details == :true_terminal or u2_details == :false_terminal ->
|
|
{var1, y1, n1, d1} = u1_details
|
|
res_y = apply_raw(op_name, op_lambda, y1, u2_id)
|
|
res_n = apply_raw(op_name, op_lambda, n1, u2_id)
|
|
res_d = apply_raw(op_name, op_lambda, d1, u2_id)
|
|
make_node_raw(var1, res_y, res_n, res_d)
|
|
|
|
true ->
|
|
{var1, y1, n1, d1} = u1_details
|
|
{var2, y2, n2, d2} = u2_details
|
|
# Elixir tuple comparison
|
|
top_var = Enum.min([var1, var2])
|
|
|
|
res_y =
|
|
apply_raw(
|
|
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_raw(
|
|
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_raw(
|
|
op_name,
|
|
op_lambda,
|
|
if(var1 == top_var, do: d1, else: u1_id),
|
|
if(var2 == top_var, do: d2, else: u2_id)
|
|
)
|
|
|
|
make_node_raw(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
|
|
|
|
# --- Public Set Operations (API) ---
|
|
def sum(tdd1_id, tdd2_id) do
|
|
op_lambda_sum = fn
|
|
:true_terminal, _ -> :true_terminal
|
|
_, :true_terminal -> :true_terminal
|
|
:false_terminal, t2_val -> t2_val
|
|
t1_val, :false_terminal -> t1_val
|
|
end
|
|
|
|
raw_result_id = apply_raw(:sum, op_lambda_sum, tdd1_id, tdd2_id)
|
|
simplify_with_constraints(raw_result_id, %{})
|
|
end
|
|
|
|
def intersect(tdd1_id, tdd2_id) do
|
|
op_lambda_intersect = fn
|
|
:false_terminal, _ -> :false_terminal
|
|
_, :false_terminal -> :false_terminal
|
|
:true_terminal, t2_val -> t2_val
|
|
t1_val, :true_terminal -> t1_val
|
|
end
|
|
|
|
raw_result_id = apply_raw(:intersect, op_lambda_intersect, tdd1_id, tdd2_id)
|
|
simplify_with_constraints(raw_result_id, %{})
|
|
end
|
|
|
|
def negate(tdd_id) do
|
|
# Negation also needs semantic simplification wrapper if it can create complex structures,
|
|
# but typically negation is structurally simple enough that raw ops are fine if children are simplified.
|
|
# However, to be safe and ensure canonical form for ¬(A & B) vs ¬A | ¬B.
|
|
raw_negated_id = negate_raw(tdd_id)
|
|
simplify_with_constraints(raw_negated_id, %{})
|
|
end
|
|
|
|
# Renamed original negate
|
|
defp negate_raw(tdd_id) do
|
|
state = get_state()
|
|
cache_key = {:negate_raw, tdd_id}
|
|
|
|
cond do
|
|
tdd_id == @true_node_id ->
|
|
@false_node_id
|
|
|
|
tdd_id == @false_node_id ->
|
|
@true_node_id
|
|
|
|
Map.has_key?(state.op_cache, cache_key) ->
|
|
state.op_cache[cache_key]
|
|
|
|
true ->
|
|
{var, y, n, d} = get_node_details(tdd_id)
|
|
# Negate children recursively using the public `negate` which includes simplification
|
|
# Public negate to ensure children are simplified
|
|
res_y = negate(y)
|
|
res_n = negate(n)
|
|
res_d = negate(d)
|
|
result_id = make_node_raw(var, res_y, res_n, res_d)
|
|
update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
|
|
result_id
|
|
end
|
|
end
|
|
|
|
# --- Subtyping (API) ---
|
|
def is_subtype(sub_type_id, super_type_id) do
|
|
cond do
|
|
sub_type_id == super_type_id ->
|
|
true
|
|
|
|
# none is subtype of anything
|
|
sub_type_id == @false_node_id ->
|
|
true
|
|
|
|
# anything is subtype of any
|
|
super_type_id == @true_node_id ->
|
|
true
|
|
|
|
true ->
|
|
# A <: B <=> A ∩ (¬B) == ∅
|
|
# All operations (intersect, negate) now produce semantically simplified results.
|
|
negated_super = negate(super_type_id)
|
|
intersection_result = intersect(sub_type_id, negated_super)
|
|
# Check against canonical false
|
|
intersection_result == @false_node_id
|
|
end
|
|
end
|
|
|
|
def print_tdd(id, indent \\ 0) do
|
|
prefix = String.duplicate(" ", indent)
|
|
details = get_node_details(id)
|
|
IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
|
|
|
|
case details do
|
|
{_var, y, n, d} ->
|
|
IO.puts("#{prefix} Yes ->")
|
|
print_tdd(y, indent + 1)
|
|
IO.puts("#{prefix} No ->")
|
|
print_tdd(n, indent + 1)
|
|
IO.puts("#{prefix} DC ->")
|
|
print_tdd(d, indent + 1)
|
|
|
|
:true_terminal ->
|
|
:ok
|
|
|
|
:false_terminal ->
|
|
:ok
|
|
|
|
nil ->
|
|
IO.puts("#{prefix} Error: Unknown ID #{id}")
|
|
end
|
|
end
|
|
end
|
|
|
|
# --- Example Usage ---
|
|
Tdd.init_tdd_system()
|
|
|
|
# Basic Types
|
|
tdd_foo = Tdd.type_atom_literal(:foo)
|
|
tdd_bar = Tdd.type_atom_literal(:bar)
|
|
tdd_atom = Tdd.type_atom()
|
|
tdd_empty_tuple = Tdd.type_empty_tuple()
|
|
tdd_any = Tdd.type_any()
|
|
tdd_none = Tdd.type_none()
|
|
|
|
test = fn name, expected, result ->
|
|
current_failures = Process.get(:test_failures, [])
|
|
|
|
if expected != result do
|
|
Process.put(:test_failures, [name | current_failures])
|
|
end
|
|
|
|
status = if expected == result, do: "PASSED", else: "FAILED"
|
|
IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
|
|
end
|
|
|
|
# Basic Types
|
|
tdd_foo = Tdd.type_atom_literal(:foo)
|
|
tdd_bar = Tdd.type_atom_literal(:bar)
|
|
tdd_baz = Tdd.type_atom_literal(:baz)
|
|
tdd_atom = Tdd.type_atom()
|
|
tdd_empty_tuple = Tdd.type_empty_tuple()
|
|
tdd_tuple = Tdd.type_tuple()
|
|
# Tuple of size 2, e.g. {any, any}
|
|
tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
|
|
tdd_any = Tdd.type_any()
|
|
tdd_none = Tdd.type_none()
|
|
|
|
test_all = fn ->
|
|
IO.puts("\n--- TDD for :foo ---")
|
|
Tdd.print_tdd(tdd_foo)
|
|
|
|
IO.puts("\n--- TDD for not :foo ---")
|
|
Tdd.print_tdd(Tdd.negate(tdd_foo))
|
|
|
|
IO.puts("\n--- TDD for atom ---")
|
|
Tdd.print_tdd(tdd_atom)
|
|
|
|
IO.puts("\n--- TDD for not atom ---")
|
|
# Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
|
|
# This represents "anything that is not an atom". The DC branch becomes true because if
|
|
# "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
|
|
Tdd.print_tdd(Tdd.negate(tdd_atom))
|
|
|
|
IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
|
|
tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
|
|
# Expected ID 0: :false_terminal
|
|
Tdd.print_tdd(tdd_foo_and_bar)
|
|
|
|
IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
|
|
tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
|
|
# Expected to be structurally identical to tdd_foo
|
|
Tdd.print_tdd(tdd_foo_and_atom)
|
|
IO.puts("\n--- Basic Subtyping Tests ---")
|
|
test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
|
|
test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
|
|
test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
|
|
test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
|
|
test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
|
|
test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
|
|
test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
|
|
test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
|
|
test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
|
|
test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))
|
|
|
|
IO.puts("\n--- Any/None Subtyping Tests ---")
|
|
test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
|
|
test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
|
|
test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
|
|
test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
|
|
test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
|
|
test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
|
|
test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
|
|
test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))
|
|
|
|
IO.puts("\n--- Union related Subtyping ---")
|
|
tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
|
|
tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)
|
|
|
|
test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
|
|
test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
|
|
test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
|
|
test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))
|
|
|
|
test.(
|
|
"(:foo | :bar) <: (:foo | :bar | :baz)",
|
|
true,
|
|
Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
|
|
)
|
|
|
|
test.(
|
|
"(:foo | :bar | :baz) <: (:foo | :bar)",
|
|
false,
|
|
Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
|
|
)
|
|
|
|
# Test against a non-member of the union
|
|
test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))
|
|
|
|
IO.puts("\n--- Intersection related Subtyping ---")
|
|
# Should be equivalent to tdd_foo
|
|
tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
|
|
# Should be tdd_none
|
|
tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
|
|
|
|
test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
|
|
test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
|
|
test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
|
|
test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
|
|
test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
|
|
# An intersection is a subtype of its components
|
|
test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
|
|
# (none <: atom)
|
|
test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
|
|
# (none <: tuple)
|
|
test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))
|
|
|
|
IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
|
|
# Reminder: ¬A <: ¬B is equivalent to B <: A (contrapositive)
|
|
|
|
# Test 1: ¬atom <: ¬:foo (Equivalent to :foo <: atom, which is true)
|
|
test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))
|
|
|
|
# Test 2: ¬:foo <: ¬atom (Equivalent to atom <: :foo, which is false)
|
|
test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))
|
|
|
|
# Double negation
|
|
test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
|
|
test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))
|
|
|
|
# Disjoint types
|
|
test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
|
|
test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
|
|
test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))
|
|
|
|
IO.puts("\n--- Mixed Types & Complex Subtyping ---")
|
|
tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
|
|
tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
|
|
|
|
test.(
|
|
"(:foo | {}) <: (atom | tuple)",
|
|
true,
|
|
Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
|
|
)
|
|
|
|
test.(
|
|
"(atom | tuple) <: (:foo | {})",
|
|
false,
|
|
Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
|
|
)
|
|
|
|
test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
|
|
test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))
|
|
|
|
# De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
|
|
# (:foo | :bar) <: ¬(¬:foo & ¬:bar)
|
|
tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))
|
|
|
|
test.(
|
|
"(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
|
|
true,
|
|
Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
|
|
)
|
|
|
|
test.(
|
|
"¬(¬:foo & ¬:bar) <: (:foo | :bar)",
|
|
true,
|
|
Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
|
|
)
|
|
|
|
# Type difference: atom - :foo (represented as atom & ¬:foo)
|
|
tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
|
|
test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
|
|
test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
|
|
# True if :bar is in (atom - :foo)
|
|
test.("(atom - :foo) <: :bar", true, 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
|
|
|
|
# Should be tdd_none
|
|
tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
|
|
test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
|
|
IO.inspect("tdd_atom_and_tuple")
|
|
Tdd.print_tdd(tdd_atom_and_tuple)
|
|
IO.inspect("tdd_none")
|
|
Tdd.print_tdd(tdd_none)
|