checkpoioint before refactor
This commit is contained in:
Kacper Marzecki
parent
cc62c5ce8e
commit
1ede4de72c
88
test.exs
88
test.exs
@ -331,7 +331,7 @@ defmodule Tdd do
|
||||
end
|
||||
|
||||
defp check_assumptions_consistency(assumptions_map, ambient_constraints \\ %{}) do
|
||||
# 1. Merge ambient constraints into the main map.
|
||||
# 1. Merge ambient constraints into the main map.
|
||||
# This ensures, for example, that if we are checking the `head` of a `list(X)`,
|
||||
# the constraint `is_subtype(head, X)` is enforced.
|
||||
assumptions_map = Map.merge(ambient_constraints, assumptions_map)
|
||||
@ -498,7 +498,7 @@ defmodule Tdd do
|
||||
end
|
||||
|
||||
# (The original integer checking logic is moved into this helper)
|
||||
defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
has_true_integer_specific_pred =
|
||||
Enum.any?(assumptions_map, fn {var_id, truth_value} ->
|
||||
elem(var_id, 0) == 2 && truth_value == true
|
||||
@ -584,8 +584,10 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
|
||||
:alt ->
|
||||
is_integer(current_interval_max) && current_interval_max < n_val
|
||||
|
||||
:cgt ->
|
||||
is_integer(current_interval_min) && current_interval_min > n_val
|
||||
|
||||
_ ->
|
||||
false
|
||||
end
|
||||
@ -595,10 +597,13 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
:beq ->
|
||||
(is_integer(current_interval_min) && current_interval_min > n_val) ||
|
||||
(is_integer(current_interval_max) && current_interval_max < n_val)
|
||||
|
||||
:alt ->
|
||||
is_integer(current_interval_min) && current_interval_min >= n_val
|
||||
|
||||
:cgt ->
|
||||
is_integer(current_interval_max) && current_interval_max <= n_val
|
||||
|
||||
_ ->
|
||||
false
|
||||
end
|
||||
@ -636,8 +641,10 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
|
||||
# A predicate on head or tail exists, e.g. {{5, :head, _}, _}
|
||||
has_head_or_tail_pred =
|
||||
Enum.any?(assumptions_map, fn {{_cat, ptype, _}, _} -> ptype == :head or ptype == :tail
|
||||
_ -> false end)
|
||||
Enum.any?(assumptions_map, fn
|
||||
{{_cat, ptype, _}, _} -> ptype == :head or ptype == :tail
|
||||
_ -> false
|
||||
end)
|
||||
|
||||
cond do
|
||||
# Contradiction: list-specific rule is assumed, but type is not a list.
|
||||
@ -926,20 +933,29 @@ defp check_integer_logic(assumptions_map, primary_true_predicates) do
|
||||
# 5. Simplify the final result.
|
||||
simplify_with_constraints(raw_final_tdd, %{})
|
||||
end
|
||||
def type_list_of(element_type_id) when is_integer(element_type_id) do
|
||||
# An empty list satisfies any list_of constraint vacuously.
|
||||
# The type is effectively `[] | [X | list(X)]`
|
||||
# We can't build this recursively, so we use a specialized predicate.
|
||||
|
||||
# This type is trivially `any` if element type is `any`
|
||||
if element_type_id == type_any() do
|
||||
type_list()
|
||||
else
|
||||
all_elems_check = make_node_raw(v_list_all_elements_are(element_type_id), @true_node_id, @false_node_id, @false_node_id)
|
||||
raw_node = make_node_raw(v_is_list(), all_elems_check, @false_node_id, @false_node_id)
|
||||
simplify_with_constraints(raw_node, %{})
|
||||
def type_list_of(element_type_id) when is_integer(element_type_id) do
|
||||
# An empty list satisfies any list_of constraint vacuously.
|
||||
# The type is effectively `[] | [X | list(X)]`
|
||||
# We can't build this recursively, so we use a specialized predicate.
|
||||
|
||||
# This type is trivially `any` if element type is `any`
|
||||
if element_type_id == type_any() do
|
||||
type_list()
|
||||
else
|
||||
all_elems_check =
|
||||
make_node_raw(
|
||||
v_list_all_elements_are(element_type_id),
|
||||
@true_node_id,
|
||||
@false_node_id,
|
||||
@false_node_id
|
||||
)
|
||||
|
||||
raw_node = make_node_raw(v_is_list(), all_elems_check, @false_node_id, @false_node_id)
|
||||
simplify_with_constraints(raw_node, %{})
|
||||
end
|
||||
end
|
||||
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)
|
||||
@ -1843,6 +1859,7 @@ defmodule ListTests do
|
||||
IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
|
||||
end
|
||||
end
|
||||
|
||||
defmodule ListOfTests do
|
||||
import Tdd
|
||||
|
||||
@ -1865,9 +1882,12 @@ defmodule ListOfTests do
|
||||
# --- Specific List Types ---
|
||||
t_list = type_list()
|
||||
t_empty_list = type_empty_list()
|
||||
t_list_one_int = type_cons(t_int_5, t_empty_list) # [5]
|
||||
t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list) # [:foo]
|
||||
t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list)) # [5, :foo]
|
||||
# [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))
|
||||
@ -1876,16 +1896,36 @@ defmodule ListOfTests do
|
||||
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())))
|
||||
|
||||
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))
|
||||
|
||||
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)
|
||||
|
||||
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.
|
||||
@ -1896,7 +1936,6 @@ defmodule ListOfTests do
|
||||
# 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)
|
||||
@ -1913,6 +1952,7 @@ defmodule ListOfTests do
|
||||
IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
|
||||
end
|
||||
end
|
||||
|
||||
test_all.()
|
||||
IntegerTests.run(test)
|
||||
TupleTests.run(test)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user