checkpoint integers
This commit is contained in:
Kacper Marzecki
parent
385ec666aa
commit
bc77e1f86b
223
test.exs
223
test.exs
@ -301,7 +301,7 @@ defmodule Tdd do
|
||||
end)
|
||||
|
||||
if MapSet.size(primary_true_predicates) > 1 do
|
||||
# IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
|
||||
IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
|
||||
:contradiction
|
||||
else
|
||||
# Check 2: Specific atom value conflicts, e.g. {1, :value, :foo} == true AND {1, :value, :bar} == true
|
||||
@ -312,7 +312,7 @@ defmodule Tdd do
|
||||
end)
|
||||
|
||||
if MapSet.size(atom_value_trues) > 1 do
|
||||
# IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
|
||||
IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
|
||||
:contradiction
|
||||
else
|
||||
# Check 3: Tuple size conflicts, e.g. {4, :size, 2} == true AND {4, :size, 3} == true
|
||||
@ -323,16 +323,67 @@ defmodule Tdd do
|
||||
end)
|
||||
|
||||
if MapSet.size(tuple_size_trues) > 1 do
|
||||
# IO.inspect(assumptions_map, label: "Contradiction: Tuple Sizes")
|
||||
:contradiction
|
||||
else
|
||||
# Add more checks as new variable types are introduced
|
||||
:consistent
|
||||
# Check 4: Integer predicate conflicts (New)
|
||||
# Collect all integer constraints assumed to be true
|
||||
# eq_val stores THE value if an :eq constraint is true. nil otherwise.
|
||||
# lt_bound stores the smallest N for which `val < N` is true (upper bound, exclusive). nil if none.
|
||||
# gt_bound stores the largest N for which `val > N` is true (lower bound, exclusive). nil if none.
|
||||
constraints =
|
||||
Enum.reduce(assumptions_map, %{eq_val: nil, lt_b: nil, gt_b: nil}, fn
|
||||
{{2, :eq, n}, true}, acc ->
|
||||
%{acc | eq_val: if(is_nil(acc.eq_val) or acc.eq_val == n, do: n, else: :conflict)}
|
||||
|
||||
{{2, :lt, n}, true}, acc ->
|
||||
%{acc | lt_b: min_opt(acc.lt_b, n)}
|
||||
|
||||
{{2, :gt, n}, true}, acc ->
|
||||
%{acc | gt_b: max_opt(acc.gt_b, n)}
|
||||
|
||||
_otherwise, acc ->
|
||||
acc
|
||||
end)
|
||||
|
||||
cond do
|
||||
# Multiple different equality constraints
|
||||
constraints.eq_val == :conflict ->
|
||||
:contradiction
|
||||
|
||||
# Check eq_val against lt_b and gt_b
|
||||
is_integer(constraints.eq_val) ->
|
||||
eq_v = constraints.eq_val
|
||||
lt_ok = is_nil(constraints.lt_b) || eq_v < constraints.lt_b
|
||||
gt_ok = is_nil(constraints.gt_b) || eq_v > constraints.gt_b
|
||||
if lt_ok && gt_ok, do: :consistent, else: :contradiction
|
||||
|
||||
# Check lt_b vs gt_b (if no specific eq_val)
|
||||
is_integer(constraints.lt_b) && is_integer(constraints.gt_b) &&
|
||||
constraints.lt_b <= constraints.gt_b + 1 ->
|
||||
# e.g., x < 5 AND x > 4 (no integer) OR x < 5 AND x > 3 (only x=4)
|
||||
# If lt_b <= gt_b + 1, it means there's no integer space or only one possible integer.
|
||||
# If lt_b == gt_b + 1, it implies x must be that one integer. This isn't a contradiction by itself yet.
|
||||
# If lt_b <= gt_b, it's a definite contradiction e.g. x < 5 and x > 5.
|
||||
if constraints.lt_b <= constraints.gt_b, do: :contradiction, else: :consistent
|
||||
|
||||
# No contradiction found from integer constraints alone
|
||||
true ->
|
||||
:consistent
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
# Helper for min, treating nil as infinity
|
||||
defp min_opt(nil, x), do: x
|
||||
defp min_opt(x, nil), do: x
|
||||
defp min_opt(x, y), do: min(x, y)
|
||||
|
||||
# Helper for max, treating nil as -infinity
|
||||
defp max_opt(nil, x), do: x
|
||||
defp max_opt(x, nil), do: x
|
||||
defp max_opt(x, y), do: max(x, y)
|
||||
# --- Semantic Simplification (Memoized) ---
|
||||
defp simplify_with_constraints(tdd_id, assumptions_map) do
|
||||
state = get_state()
|
||||
@ -410,11 +461,20 @@ defmodule Tdd do
|
||||
|
||||
@v_is_atom {0, :is_atom}
|
||||
@v_is_tuple {0, :is_tuple}
|
||||
# New primary type
|
||||
@v_is_integer {0, :is_integer}
|
||||
|
||||
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}
|
||||
|
||||
# Integer Predicates (Category 2)
|
||||
def v_int_eq(n) when is_integer(n), do: {2, :eq, n}
|
||||
# strictly less than n
|
||||
def v_int_lt(n) when is_integer(n), do: {2, :lt, n}
|
||||
# strictly greater than n
|
||||
def v_int_gt(n) when is_integer(n), do: {2, :gt, n}
|
||||
|
||||
def type_any, do: @true_node_id
|
||||
def type_none, do: @false_node_id
|
||||
|
||||
@ -449,6 +509,30 @@ defmodule Tdd do
|
||||
simplify_with_constraints(raw_node, %{})
|
||||
end
|
||||
|
||||
def type_integer do
|
||||
make_node_for_constructors(@v_is_integer, @true_node_id, @false_node_id, @false_node_id)
|
||||
end
|
||||
|
||||
def type_int_eq(n) do
|
||||
int_eq_node = make_node_raw(v_int_eq(n), @true_node_id, @false_node_id, @false_node_id)
|
||||
raw_node = make_node_raw(@v_is_integer, int_eq_node, @false_node_id, @false_node_id)
|
||||
simplify_with_constraints(raw_node, %{})
|
||||
end
|
||||
|
||||
# Represents integers x where x < n
|
||||
def type_int_lt(n) do
|
||||
int_lt_node = make_node_raw(v_int_lt(n), @true_node_id, @false_node_id, @false_node_id)
|
||||
raw_node = make_node_raw(@v_is_integer, int_lt_node, @false_node_id, @false_node_id)
|
||||
simplify_with_constraints(raw_node, %{})
|
||||
end
|
||||
|
||||
# Represents integers x where x > n
|
||||
def type_int_gt(n) do
|
||||
int_gt_node = make_node_raw(v_int_gt(n), @true_node_id, @false_node_id, @false_node_id)
|
||||
raw_node = make_node_raw(@v_is_integer, int_gt_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
|
||||
@ -868,4 +952,131 @@ test_all = fn ->
|
||||
IO.inspect(Process.get(:test_failures, []))
|
||||
end
|
||||
|
||||
test_all.()
|
||||
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
|
||||
|
||||
# test_all.()
|
||||
# IntegerTests.run(test)
|
||||
|
||||
# x < 3
|
||||
tdd_int_lt_3 = Tdd.type_int_lt(3)
|
||||
# x > 10
|
||||
tdd_int_gt_10 = Tdd.type_int_gt(10)
|
||||
union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
|
||||
|
||||
test.(
|
||||
"int_eq(12) <: (int < 3 | int > 10)",
|
||||
true,
|
||||
Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
|
||||
)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user