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

heckpoint

Browse Source
This commit is contained in:
Kacper Marzecki 2025-06-15 20:19:25 +02:00
parent eb2e8855ac
commit bb08fbe078
1 changed files with 121 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

214
test.exs
View File

@ -45,7 +45,7 @@ defmodule Tdd do
Process.put(:op_cache, new_state.op_cache)
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
# Basic reduction: if all children are identical, this node is redundant.
@ -61,11 +61,13 @@ defmodule Tdd do
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
@ -79,71 +81,82 @@ defmodule Tdd do
end
# --- Semantic Constraint Checking ---
# assumptions_map is {variable_id => value (true, false, :dc)}
defp check_assumptions_consistency(assumptions_map) do
# Primary type mutual exclusivity:
# Check if more than one primary type (category 0) is assumed to be true.
primary_true_predicates =
Enum.reduce(assumptions_map, MapSet.new(), fn
({{0, predicate_name}, true}, acc_set) -> MapSet.put(acc_set, predicate_name)
# ({var, false}, acc_set) -> # If is_atom is false, that's fine with is_tuple being true.
# Check if var is a primary type and its assumed value contradicts another assumed primary type.
# E.g. assumptions_map has { {0, :is_atom}, true } and we are checking an assumption for { {0, :is_tuple}, true }
# This is implicitly handled by iterating through assumptions_map.
{{0, predicate_name}, true}, acc_set -> MapSet.put(acc_set, predicate_name)
_otherwise, acc_set -> acc_set
end)
if MapSet.size(primary_true_predicates) > 1 do
# IO.puts "Debug: Contradiction! Assumptions: #{inspect assumptions_map}, True primary types: #{inspect primary_true_predicates}"
:contradiction
else
# Add other semantic checks here, e.g.:
# - If assumptions include `{v_int_lt_N, true}` and `{v_int_gt_M, true}` where N <= M.
# - If assumptions include `{v_tuple_size_eq_2, true}` and `{v_tuple_size_eq_3, true}`.
# 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 ---
# Simplifies a TDD given a map of assumptions {variable => value}.
# Value can be true, false, or :dc (if we want to model "don't care" assumptions).
# --- Semantic Simplification (Memoized) ---
defp simplify_with_constraints(tdd_id, assumptions_map) do
state = get_state()
# Canonicalize assumptions_map for cache key: sort map by variable
# Convert map to sorted list of tuples for stable cache key
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 ->
# If assumptions are contradictory, the entire path is impossible.
# update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)}) # Cache this finding
# Path is semantically impossible
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
true -> # Current var is assumed true, follow yes branch with same assumptions
# Current var is assumed true in path, follow yes branch
true ->
simplify_with_constraints(y, assumptions_map)
false -> # Current var is assumed false, follow no branch with same assumptions
# Current var is assumed false in path, follow no branch
false ->
simplify_with_constraints(n, assumptions_map)
:dc -> # Current var is assumed don't care, follow dc branch
# Current var is assumed don't care in path, follow dc branch
:dc ->
simplify_with_constraints(d, assumptions_map)
nil -> # Current var is not in assumptions, so it's a decision point.
# 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))
simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc)) # Assuming :dc can be an assumption value
make_node_raw(var, simplified_y, simplified_n, simplified_d) # Use raw, as children are now simplified
# 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
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
@ -164,34 +177,41 @@ defmodule Tdd do
def type_none, do: @false_node_id
def type_atom do
make_node(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
# 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(var_eq, @true_node_id, @false_node_id, @false_node_id)
make_node(@v_is_atom, atom_val_node, @false_node_id, @false_node_id)
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(@v_is_tuple, @true_node_id, @false_node_id, @false_node_id)
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(var_size_0, @true_node_id, @false_node_id, @false_node_id)
make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
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(var_size, @true_node_id, @false_node_id, @false_node_id)
make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
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 (uses make_node, which is currently make_node_raw) ---
def apply(op_name, op_lambda, u1_id, u2_id) do
# --- 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
@ -202,66 +222,65 @@ defmodule Tdd do
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 -> # Recursive case
true ->
u1_details = get_node_details(u1_id)
u2_details = get_node_details(u2_id)
result_id =
cond do
# Case: u1 is terminal, u2 is not
u1_details == :true_terminal or u1_details == :false_terminal ->
{var2, y2, n2, d2} = u2_details
res_y = apply(op_name, op_lambda, u1_id, y2)
res_n = apply(op_name, op_lambda, u1_id, n2)
res_d = apply(op_name, op_lambda, u1_id, d2)
make_node(var2, res_y, res_n, res_d) # make_node is make_node_raw
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)
# Case: u2 is terminal, u1 is not
u2_details == :true_terminal or u2_details == :false_terminal ->
{var1, y1, n1, d1} = u1_details
res_y = apply(op_name, op_lambda, y1, u2_id)
res_n = apply(op_name, op_lambda, n1, u2_id)
res_d = apply(op_name, op_lambda, d1, u2_id)
make_node(var1, res_y, res_n, res_d) # make_node is make_node_raw
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)
# Case: Both u1 and u2 are non-terminal nodes
true ->
{var1, y1, n1, d1} = u1_details
{var2, y2, n2, d2} = u2_details
# Elixir tuple comparison
top_var = Enum.min([var1, var2])
top_var =
cond do
var1 == var2 -> var1
var1 < var2 -> var1
true -> var2 # var2 < var1
end
# Recursive calls based on top_var
res_y =
cond do
top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, y1, y2)
top_var == var1 -> apply(op_name, op_lambda, y1, u2_id) # u2_id passed through
true -> apply(op_name, op_lambda, u1_id, y2) # u1_id passed through
end
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 =
cond do
top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, n1, n2)
top_var == var1 -> apply(op_name, op_lambda, n1, u2_id)
true -> apply(op_name, op_lambda, u1_id, n2)
end
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 =
cond do
top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, d1, d2)
top_var == var1 -> apply(op_name, op_lambda, d1, u2_id)
true -> apply(op_name, op_lambda, u1_id, d2)
end
make_node(top_var, res_y, res_n, res_d) # make_node is make_node_raw
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
@ -270,83 +289,78 @@ defmodule Tdd do
t1_val, :false_terminal -> t1_val
end
apply(:sum, op_lambda_sum, tdd1_id, tdd2_id)
raw_result_id = apply_raw(:sum, op_lambda_sum, tdd1_id, tdd2_id)
simplify_with_constraints(raw_result_id, %{})
end
# --- Intersection ---
def intersect(tdd1_id, tdd2_id) do
op_lambda_intersect = fn
# AND logic for terminals
# false and X = false
:false_terminal, _ -> :false_terminal
# X and false = false
_, :false_terminal -> :false_terminal
# true and X = X (e.g. true and true = true, true and false = false)
:true_terminal, t2_val -> t2_val
# X and true = X
t1_val, :true_terminal -> t1_val
end
apply(:intersect, op_lambda_intersect, tdd1_id, tdd2_id)
raw_result_id = apply_raw(:intersect, op_lambda_intersect, tdd1_id, tdd2_id)
simplify_with_constraints(raw_result_id, %{})
end
# --- Negation ---
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()
# Unary operation cache key
cache_key = {:negate, tdd_id}
cache_key = {:negate_raw, tdd_id}
cond do
# Handle terminals directly, no caching needed for these simple cases.
tdd_id == @true_node_id ->
@false_node_id
tdd_id == @false_node_id ->
@true_node_id
# Check cache for non-terminal IDs
Map.has_key?(state.op_cache, cache_key) ->
state.op_cache[cache_key]
# Compute for non-terminal ID if not in cache
true ->
case get_node_details(tdd_id) do
{var, y, n, d} ->
{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(var, res_y, res_n, res_d)
# Cache the computed result for this non-terminal tdd_id
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
nil ->
# This should ideally not be reached if IDs are managed correctly
raise "Tdd.negate: Unknown node ID #{inspect(tdd_id)} during get_node_details. State: #{inspect(state.node_by_id)}"
end
end
end
# --- Subtyping ---
# A <: B (A is a subtype of B)
# --- Subtyping (API) ---
def is_subtype(sub_type_id, super_type_id) do
cond do
# Optimization: A is always a subtype of A
sub_type_id == super_type_id ->
true
# Optimization: `none` is a subtype of anything
# none is subtype of anything
sub_type_id == @false_node_id ->
true
# Optimization: Anything is a subtype of `any`
# anything is subtype of any
super_type_id == @true_node_id ->
true
true ->
# Definition: A <: B <=> A ∩ (¬B) == ∅ (type_none / @false_node_id)
# 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