From 214b4b06acd6cb6534ed16754bc4d83dae2a371a Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Sat, 12 Jul 2025 12:29:31 +0200 Subject: [PATCH] cleanup comments --- lib/til.ex | 47 +++++------------------------------------------ 1 file changed, 5 insertions(+), 42 deletions(-) diff --git a/lib/til.ex b/lib/til.ex index 74403ba..680c486 100644 --- a/lib/til.ex +++ b/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