From bb08fbe07818c2fc944a70af98f7a2b01c2bc5c1 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Sun, 15 Jun 2025 20:19:25 +0200 Subject: [PATCH] heckpoint --- test.exs | 228 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 121 insertions(+), 107 deletions(-) diff --git a/test.exs b/test.exs index 4aceef2..f54a7e6 100644 --- a/test.exs +++ b/test.exs @@ -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 @@ -78,72 +80,83 @@ defmodule Tdd do make_node_raw(variable, yes_id, no_id, dc_id) end - # --- Semantic Constraint Checking --- + # --- 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. - # Recursively simplify children by adding this var's assignment to assumptions. + + # 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} -> - 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 - 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 + {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 --- - # 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