cleanup comments
This commit is contained in:
Kacper Marzecki
parent
61e95be622
commit
214b4b06ac
47
lib/til.ex
47
lib/til.ex
@ -685,8 +685,6 @@ defmodule Tdd.TypeSpec do
|
||||
(min == :neg_inf or val >= min) and (max == :pos_inf or val <= max)
|
||||
|
||||
{{:mu, v1, b1_body}, {:mu, v2, b2_body}} ->
|
||||
# This logic is from the original file, which is correct in principle
|
||||
# but was failing due to the TDD layer bug.
|
||||
cond do
|
||||
is_list_mu_form(b1_body, v1) and is_list_mu_form(b2_body, v2) ->
|
||||
e1 = extract_list_mu_element(b1_body, v1)
|
||||
@ -798,8 +796,6 @@ defmodule Tdd.TypeSpec do
|
||||
end
|
||||
|
||||
defmodule Tdd.Store do
|
||||
# NOTE: This module remains unchanged.
|
||||
# The original provided code for this module is correct and complete.
|
||||
@moduledoc """
|
||||
Manages the state of the TDD system's node graph and operation cache.
|
||||
"""
|
||||
@ -848,7 +844,6 @@ defmodule Tdd.Store do
|
||||
def get_node(id) do
|
||||
case Process.get(@node_by_id_key, %{}) do
|
||||
%{^id => details} -> {:ok, details}
|
||||
# IMPROVEMENT: Handle placeholder details gracefully
|
||||
%{^id => {:placeholder, _spec}} -> {:ok, {:placeholder, "Knot-tying placeholder"}}
|
||||
%{} -> {:error, :not_found}
|
||||
end
|
||||
@ -910,7 +905,6 @@ defmodule Tdd.Store do
|
||||
"""
|
||||
@spec create_placeholder(TypeSpec.t()) :: non_neg_integer()
|
||||
def create_placeholder(spec) do
|
||||
# IMPROVEMENT: Correctly reserve an ID without creating a malformed node.
|
||||
next_id = Process.get(@next_id_key)
|
||||
node_by_id = Process.get(@node_by_id_key)
|
||||
|
||||
@ -937,7 +931,7 @@ defmodule Tdd.Store do
|
||||
nodes = Process.get(@nodes_key)
|
||||
node_by_id = Process.get(@node_by_id_key)
|
||||
|
||||
# This part is now safe. The old_details will be `{:placeholder, ...}`
|
||||
# The old_details will be `{:placeholder, ...}`
|
||||
# which does not exist as a key in the `nodes` map, so Map.delete is a no-op.
|
||||
old_details = Map.get(node_by_id, id)
|
||||
nodes = Map.delete(nodes, old_details)
|
||||
@ -959,8 +953,6 @@ end
|
||||
defmodule Tdd.Variable do
|
||||
@moduledoc """
|
||||
Defines the canonical structure for all Tdd predicate variables.
|
||||
REFAC: This module is unchanged, but its functions for recursive types will
|
||||
now be called with TDD IDs instead of TypeSpecs by the Tdd.Compiler.
|
||||
"""
|
||||
|
||||
# --- Category 0: Primary Type Discriminators ---
|
||||
@ -998,7 +990,6 @@ defmodule Tdd.Variable do
|
||||
@spec v_tuple_elem_pred(non_neg_integer(), sub_problem_tdd_id :: non_neg_integer()) :: term()
|
||||
def v_tuple_elem_pred(index, sub_problem_tdd_id)
|
||||
when is_integer(index) and index >= 0 and is_integer(sub_problem_tdd_id) do
|
||||
# REFAC: The nested term is now a TDD ID, not a spec or a variable.
|
||||
{4, :b_element, index, sub_problem_tdd_id}
|
||||
end
|
||||
|
||||
@ -1019,8 +1010,6 @@ defmodule Tdd.Variable do
|
||||
end
|
||||
|
||||
defmodule Tdd.Predicate.Info do
|
||||
# NOTE: This module remains largely unchanged. The traits for recursive variables
|
||||
# correctly identify them by structure, independent of what's inside.
|
||||
@moduledoc "A knowledge base for the properties of TDD predicate variables."
|
||||
alias Tdd.Variable
|
||||
|
||||
@ -1092,7 +1081,6 @@ defmodule Tdd.Predicate.Info do
|
||||
%{type: :tuple_prop, category: :tuple, implies: [{Variable.v_is_tuple(), true}]}
|
||||
end
|
||||
|
||||
# REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
|
||||
def get_traits({4, :b_element, index, _tdd_id}) do
|
||||
%{
|
||||
type: :tuple_recursive,
|
||||
@ -1106,7 +1094,6 @@ defmodule Tdd.Predicate.Info do
|
||||
%{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]}
|
||||
end
|
||||
|
||||
# REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
|
||||
def get_traits({5, :c_head, _tdd_id, _}) do
|
||||
%{
|
||||
type: :list_recursive,
|
||||
@ -1116,7 +1103,6 @@ defmodule Tdd.Predicate.Info do
|
||||
}
|
||||
end
|
||||
|
||||
# REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
|
||||
def get_traits({5, :d_tail, _tdd_id, _}) do
|
||||
%{
|
||||
type: :list_recursive,
|
||||
@ -1132,8 +1118,6 @@ end
|
||||
defmodule Tdd.Consistency.Engine do
|
||||
@moduledoc """
|
||||
A rule-based engine for checking the semantic consistency of a set of assumptions.
|
||||
REFAC: This module is largely unchanged, but we now make `remap_sub_problem_vars`
|
||||
and `unwrap_var` public so they can be shared with Tdd.Algo.
|
||||
"""
|
||||
alias Tdd.Predicate.Info
|
||||
alias Tdd.Variable
|
||||
@ -1186,8 +1170,6 @@ defmodule Tdd.Consistency.Engine do
|
||||
@spec unwrap_var(term()) :: term()
|
||||
def unwrap_var(var) do
|
||||
case var do
|
||||
# REFAC: These variables now contain TDD IDs, but this function just extracts
|
||||
# whatever is inside. The consumer (`handle_recursive_subproblem`) will know it's an ID.
|
||||
{4, :b_element, _index, inner_content} -> inner_content
|
||||
{5, :c_head, inner_content, _} -> inner_content
|
||||
{5, :d_tail, inner_content, _} -> inner_content
|
||||
@ -1371,7 +1353,7 @@ defmodule Tdd.Algo do
|
||||
do: Store.true_node_id(),
|
||||
else: Store.false_node_id()
|
||||
|
||||
# FIX: Add cases to handle placeholder nodes co-inductively.
|
||||
# TODO: Add cases to handle placeholder nodes co-inductively.
|
||||
# Treat the placeholder as `any`.
|
||||
match?({:ok, {:placeholder, _}}, {:ok, u1_details}) ->
|
||||
# op(placeholder, u2) -> op(any, u2)
|
||||
@ -1448,7 +1430,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
# --- Unary Operation: Negation ---
|
||||
# This function is correct and does not need to be changed.
|
||||
@spec negate(non_neg_integer) :: non_neg_integer
|
||||
def negate(tdd_id) do
|
||||
cache_key = {:negate, tdd_id}
|
||||
@ -1469,7 +1450,7 @@ defmodule Tdd.Algo do
|
||||
{:ok, {var, y, n, d}} ->
|
||||
Store.find_or_create_node(var, negate(y), negate(n), negate(d))
|
||||
|
||||
# FIX: Handle placeholder nodes encountered during co-inductive simplification.
|
||||
# TODO: Handle placeholder nodes encountered during co-inductive simplification.
|
||||
# A placeholder is treated as `any` for the check, so its negation is `none`.
|
||||
{:ok, {:placeholder, _spec}} ->
|
||||
Store.false_node_id()
|
||||
@ -1481,7 +1462,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
# --- Unary Operation: Semantic Simplification ---
|
||||
# This function is correct and does not need to be changed.
|
||||
@spec simplify(non_neg_integer(), map()) :: non_neg_integer
|
||||
def simplify(tdd_id, assumptions \\ %{}) do
|
||||
sorted_assumptions = Enum.sort(assumptions)
|
||||
@ -1505,7 +1485,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
end
|
||||
|
||||
# This function is correct and does not need to be changed.
|
||||
defp do_simplify(tdd_id, sorted_assumptions, context) do
|
||||
current_state = {tdd_id, sorted_assumptions}
|
||||
|
||||
@ -1559,7 +1538,6 @@ defmodule Tdd.Algo do
|
||||
)
|
||||
|
||||
_ ->
|
||||
# The rest of the logic for standard variables is unchanged.
|
||||
case Map.get(assumptions, var) do
|
||||
true ->
|
||||
do_simplify(y, sorted_assumptions, new_context)
|
||||
@ -1607,7 +1585,7 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
# --- Unary Operation: Substitute ---
|
||||
# FIX: The implementation of substitute needs to change.
|
||||
# TODO: does the implementation of substitute need to change?
|
||||
|
||||
@spec substitute(non_neg_integer(), non_neg_integer(), non_neg_integer()) :: non_neg_integer()
|
||||
def substitute(root_id, from_id, to_id) do
|
||||
@ -1641,7 +1619,6 @@ defmodule Tdd.Algo do
|
||||
Store.false_node_id()
|
||||
|
||||
{:ok, {var, y, n, d}} ->
|
||||
# FIX: Substitute within the variable term itself.
|
||||
new_var = substitute_in_var(var, from_id, to_id)
|
||||
new_y = substitute(y, from_id, to_id)
|
||||
new_n = substitute(n, from_id, to_id)
|
||||
@ -1658,7 +1635,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
|
||||
# --- Coinductive Emptiness Check ---
|
||||
# This function is correct and does not need to be changed.
|
||||
@spec check_emptiness(non_neg_integer()) :: non_neg_integer()
|
||||
def check_emptiness(tdd_id) do
|
||||
cache_key = {:check_emptiness, tdd_id}
|
||||
@ -1675,7 +1651,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
end
|
||||
|
||||
# This function is correct and does not need to be changed.
|
||||
defp do_check_emptiness(tdd_id, sorted_assumptions, context) do
|
||||
current_state = {tdd_id, sorted_assumptions}
|
||||
|
||||
@ -1688,7 +1663,7 @@ defmodule Tdd.Algo do
|
||||
if Engine.check(assumptions) == :contradiction do
|
||||
Store.false_node_id()
|
||||
else
|
||||
IO.inspect(tdd_id, label: "Fetching node in do_check_emptiness")
|
||||
# IO.inspect(tdd_id, label: "Fetching node in do_check_emptiness")
|
||||
# Debug.print_tdd_graph(tdd_id)
|
||||
|
||||
case Store.get_node(tdd_id) do
|
||||
@ -1799,7 +1774,6 @@ defmodule Tdd.Algo do
|
||||
end
|
||||
end
|
||||
|
||||
# This function, containing our previous fix, is correct and does not need to be changed.
|
||||
defp handle_recursive_subproblem(
|
||||
algo_type,
|
||||
sub_key,
|
||||
@ -1920,8 +1894,6 @@ end
|
||||
defmodule Tdd.Compiler do
|
||||
@moduledoc """
|
||||
Compiles a `TypeSpec` into a canonical TDD ID.
|
||||
REFAC: This module now embeds TDD IDs into recursive predicate variables
|
||||
instead of raw TypeSpecs, a key part of the architectural decoupling.
|
||||
"""
|
||||
alias Tdd.TypeSpec
|
||||
alias Tdd.Variable
|
||||
@ -1932,13 +1904,10 @@ defmodule Tdd.Compiler do
|
||||
@doc "The main public entry point. Takes a spec and returns its TDD ID."
|
||||
@spec spec_to_id(TypeSpec.t()) :: non_neg_integer()
|
||||
def spec_to_id(spec) do
|
||||
# FIX: State initialization is moved to the public API boundary (`is_subtype/2`),
|
||||
# making this function a pure compiler component.
|
||||
normalized_spec = TypeSpec.normalize(spec)
|
||||
compile_normalized_spec(normalized_spec, %{})
|
||||
end
|
||||
|
||||
# This context-aware compilation function from the previous fix remains correct.
|
||||
defp compile_normalized_spec(normalized_spec, context) do
|
||||
sorted_context = Enum.sort(context)
|
||||
cache_key = {:compile_spec_with_context, normalized_spec, sorted_context}
|
||||
@ -2115,9 +2084,6 @@ defmodule Tdd.Compiler do
|
||||
@doc "Checks if spec1 is a subtype of spec2 using TDDs."
|
||||
@spec is_subtype(TypeSpec.t(), TypeSpec.t()) :: boolean
|
||||
def is_subtype(spec1, spec2) do
|
||||
# FIX: Each subtyping check is an independent, top-level operation.
|
||||
# It must initialize the store to guarantee a clean slate and prevent
|
||||
# state from leaking between unrelated checks.
|
||||
Store.init()
|
||||
|
||||
id1 = spec_to_id(spec1)
|
||||
@ -2129,9 +2095,6 @@ defmodule Tdd.Compiler do
|
||||
intersect_id = Algo.apply(:intersect, &op_intersect_terminals/2, id1, neg_id2)
|
||||
Debug.print_tdd_graph(intersect_id, "IS_SUBTYPE intersect")
|
||||
|
||||
# The crash was because `intersect_id` was not an integer, which should not
|
||||
# happen if `apply` works correctly on valid IDs. By fixing the state
|
||||
# initialization, `id1` and `id2` will now be valid in the same store context.
|
||||
final_id = Algo.check_emptiness(intersect_id)
|
||||
final_id == Store.false_node_id()
|
||||
end
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user