kacper/elipl
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

cleanup

Browse Source
This commit is contained in:
Kacper Marzecki 2025-06-16 01:07:42 +02:00
parent dddefdb7ac
commit de167ff5f3
1 changed files with 50 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

115
test.exs
View File

@ -256,7 +256,6 @@ defmodule Tdd do
end end
# --- Raw Node Creation (Structural) --- # --- 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 defp make_node_raw(variable, yes_id, no_id, dc_id) do
# Basic reduction: if all children are identical, this node is redundant. # Basic reduction: if all children are identical, this node is redundant.
if yes_id == no_id && yes_id == dc_id do if yes_id == no_id && yes_id == dc_id do
@ -269,7 +268,6 @@ defmodule Tdd do
# Node already exists (structural sharing) # Node already exists (structural sharing)
state.nodes[node_tuple] state.nodes[node_tuple]
else else
# Create new node
new_id = state.next_id new_id = state.next_id
update_state(%{ update_state(%{
@ -283,7 +281,7 @@ defmodule Tdd do
end end
end end
# --- Public Node Creation (Currently same as raw, apply will handle context) --- # --- Public Node Creation ---
# The `apply` algorithm inherently creates the necessary structure. # The `apply` algorithm inherently creates the necessary structure.
# Semantic simplification is applied *after* `apply` completes. # Semantic simplification is applied *after* `apply` completes.
def make_node(variable, yes_id, no_id, dc_id) do def make_node(variable, yes_id, no_id, dc_id) do
@ -545,17 +543,6 @@ defmodule Tdd do
# End else for atom_value_trues # End else for atom_value_trues
end end
# End true for atom_specific_pred
# The IO.inspect was here. For clarity, let's assign to result then inspect.
# result |> IO.inspect(label: "check_assumptions_consistency END assumptions_map = #{inspect(assumptions_map)}")
# For testing, you might want to remove or conditionalize this inspect:
# if System.get_env("DEBUG_CAC") do
# raw_result |> IO.inspect(label: "CAC END: #{inspect(assumptions_map)}")
# else
# raw_result
# end
# Return the consistency status
raw_result raw_result
end end
@ -568,11 +555,11 @@ defmodule Tdd do
defp max_opt(nil, x), do: x defp max_opt(nil, x), do: x
defp max_opt(x, nil), do: x defp max_opt(x, nil), do: x
defp max_opt(x, y), do: max(x, y) defp max_opt(x, y), do: max(x, y)
# --- Semantic Simplification (Memoized) --- # --- Semantic Simplification (Memoized) ---
defp simplify_with_constraints(tdd_id, assumptions_map) do defp simplify_with_constraints(tdd_id, assumptions_map) do
state = get_state() state = get_state()
# Sort assumptions for cache key consistency # Sort assumptions for cache key consistency
# Using Map.to_list and then sorting is more robust than Enum.sort_by if keys can be complex
sorted_assumptions_list = Enum.sort(Map.to_list(assumptions_map)) sorted_assumptions_list = Enum.sort(Map.to_list(assumptions_map))
cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list} cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
@ -625,16 +612,16 @@ defmodule Tdd do
# Note: We don't check for implies_var_dc here, as that's more complex. # Note: We don't check for implies_var_dc here, as that's more complex.
# The original recursion handles the DC case exploration. # The original recursion handles the DC case exploration.
IO.inspect( # IO.inspect(
%{ # %{
tdd_id: tdd_id, # tdd_id: tdd_id,
var: var, # var: var,
assumptions: assumptions_map, # assumptions: assumptions_map,
implies_var_true: implies_var_true, # implies_var_true: implies_var_true,
implies_var_false: implies_var_false # implies_var_false: implies_var_false
}, # },
label: "Simplify NIL branch" # label: "Simplify NIL branch"
) # )
cond do cond do
implies_var_true && implies_var_false -> implies_var_true && implies_var_false ->
@ -712,8 +699,6 @@ defmodule Tdd do
def type_none, do: @false_node_id def type_none, do: @false_node_id
def type_atom do 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) make_node_for_constructors(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
end end
@ -917,41 +902,41 @@ defmodule Tdd do
true -> true ->
# A <: B <=> A ∩ (¬B) == ∅ # A <: B <=> A ∩ (¬B) == ∅
# All operations (intersect, negate) now produce semantically simplified results. # All operations (intersect, negate) now produce semantically simplified results.
IO.puts("\n--- is_subtype debug ---") # IO.puts("\n--- is_subtype debug ---")
IO.inspect(sub_type_id, # IO.inspect(sub_type_id,
label: "is_subtype: sub_type_id (#{inspect(Tdd.get_node_details(sub_type_id))})" # label: "is_subtype: sub_type_id (#{inspect(Tdd.get_node_details(sub_type_id))})"
) # )
IO.inspect(super_type_id, # IO.inspect(super_type_id,
label: "is_subtype: super_type_id (#{inspect(Tdd.get_node_details(super_type_id))})" # label: "is_subtype: super_type_id (#{inspect(Tdd.get_node_details(super_type_id))})"
) # )
# Tdd.print_tdd(sub_type_id) # Tdd.print_tdd(sub_type_id)
# Tdd.print_tdd(super_type_id) # Tdd.print_tdd(super_type_id)
negated_super = negate(super_type_id) negated_super = negate(super_type_id)
IO.inspect(negated_super, # IO.inspect(negated_super,
label: "is_subtype: negated_super_id (#{inspect(Tdd.get_node_details(negated_super))})" # label: "is_subtype: negated_super_id (#{inspect(Tdd.get_node_details(negated_super))})"
) # )
# IO.puts("Structure of negated_super:") # IO.puts("Structure of negated_super:")
# Tdd.print_tdd(negated_super) # Tdd.print_tdd(negated_super)
intersection_result = intersect(sub_type_id, negated_super) intersection_result = intersect(sub_type_id, negated_super)
IO.inspect(intersection_result, # IO.inspect(intersection_result,
label: # label:
"is_subtype: intersection_result_id (#{inspect(Tdd.get_node_details(intersection_result))})" # "is_subtype: intersection_result_id (#{inspect(Tdd.get_node_details(intersection_result))})"
) # )
# IO.puts("Structure of intersection_result:") # IO.puts("Structure of intersection_result:")
# Tdd.print_tdd(intersection_result) # Tdd.print_tdd(intersection_result)
result = intersection_result == @false_node_id result = intersection_result == @false_node_id
IO.inspect(result, label: "is_subtype: final result") # IO.inspect(result, label: "is_subtype: final result")
IO.puts("--- end is_subtype debug ---\n") # IO.puts("--- end is_subtype debug ---\n")
result result
end end
end end
@ -1207,12 +1192,12 @@ test_all = fn ->
Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2) Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2)
) )
IO.puts("\n--- TDD structure for (atom - :foo) ---") # IO.puts("\n--- TDD structure for (atom - :foo) ---")
Tdd.print_tdd(tdd_atom_minus_foo) # Tdd.print_tdd(tdd_atom_minus_foo)
IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---") # IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
Tdd.print_tdd(tdd_recombined_atom) # Tdd.print_tdd(tdd_recombined_atom)
IO.puts("\n--- TDD structure for 'atom' for comparison ---") # IO.puts("\n--- TDD structure for 'atom' for comparison ---")
Tdd.print_tdd(tdd_atom) # Tdd.print_tdd(tdd_atom)
IO.inspect(Process.get(:test_failures, [])) IO.inspect(Process.get(:test_failures, []))
end end
@ -1236,14 +1221,14 @@ defmodule IntegerTests do
# x > 10 # x > 10
tdd_int_gt_10 = Tdd.type_int_gt(10) tdd_int_gt_10 = Tdd.type_int_gt(10)
tdd_atom_foo = Tdd.type_atom_literal(:foo) tdd_atom_foo = Tdd.type_atom_literal(:foo)
#
IO.puts("\n--- Integer Type Structures ---") # IO.puts("\n--- Integer Type Structures ---")
IO.puts("Integer:") # IO.puts("Integer:")
Tdd.print_tdd(tdd_int) # Tdd.print_tdd(tdd_int)
IO.puts("Int == 5:") # IO.puts("Int == 5:")
Tdd.print_tdd(tdd_int_5) # Tdd.print_tdd(tdd_int_5)
IO.puts("Int < 10:") # IO.puts("Int < 10:")
Tdd.print_tdd(tdd_int_lt_10) # Tdd.print_tdd(tdd_int_lt_10)
IO.puts("\n--- Integer Subtyping Tests ---") IO.puts("\n--- Integer Subtyping Tests ---")
test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int)) test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
@ -1273,20 +1258,20 @@ defmodule IntegerTests do
IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---") IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7) 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()) 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):") # IO.puts("Structure of int_5 & int_7 (should be ID 0):")
Tdd.print_tdd(intersect_5_7) # Tdd.print_tdd(intersect_5_7)
# x < 3 AND x > 10 # x < 3 AND x > 10
intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_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()) 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):") # IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
Tdd.print_tdd(intersect_lt3_gt10) # Tdd.print_tdd(intersect_lt3_gt10)
# x < 10 AND x > 3 (e.g. 4,5..9) # x < 10 AND x > 3 (e.g. 4,5..9)
intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3) 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()) 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):") # IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
Tdd.print_tdd(intersect_lt10_gt3) # Tdd.print_tdd(intersect_lt10_gt3)
# Test a value within this intersection # Test a value within this intersection
test_fn.( test_fn.(
"int_5 <: (int_lt_10 & int_gt_3)", "int_5 <: (int_lt_10 & int_gt_3)",
@ -1303,8 +1288,8 @@ defmodule IntegerTests do
test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_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_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)) 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:") # IO.puts("Structure of int_5 | int_7:")
Tdd.print_tdd(union_5_7) # Tdd.print_tdd(union_5_7)
# (int < 3) | (int > 10) # (int < 3) | (int > 10)
union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10) union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)