checkpoint
This commit is contained in:
Kacper Marzecki
parent
176a4c6a04
commit
ff557cb221
127
new.exs
127
new.exs
@ -1,3 +1,46 @@
|
||||
defmodule Tdd.Debug do
|
||||
@moduledoc "Helpers for debugging TDD structures."
|
||||
alias Tdd.Store
|
||||
|
||||
@doc "Prints a formatted representation of a TDD graph starting from an ID."
|
||||
def print(id) do
|
||||
IO.puts("--- TDD Graph (ID: #{id}) ---")
|
||||
do_print(id, 0, MapSet.new())
|
||||
IO.puts("------------------------")
|
||||
end
|
||||
|
||||
defp do_print(id, indent_level, visited) do
|
||||
prefix = String.duplicate(" ", indent_level)
|
||||
|
||||
if MapSet.member?(visited, id) do
|
||||
IO.puts("#{prefix}ID #{id} -> [Seen, recursive link]")
|
||||
:ok
|
||||
else
|
||||
new_visited = MapSet.put(visited, id)
|
||||
|
||||
case Store.get_node(id) do
|
||||
{:ok, :true_terminal} ->
|
||||
IO.puts("#{prefix}ID #{id} -> TRUE")
|
||||
|
||||
{:ok, :false_terminal} ->
|
||||
IO.puts("#{prefix}ID #{id} -> FALSE")
|
||||
|
||||
{:ok, {var, y, n, d}} ->
|
||||
IO.puts("#{prefix}ID #{id}: IF #{inspect(var)}")
|
||||
IO.puts("#{prefix} ├─ Yes:")
|
||||
do_print(y, indent_level + 2, new_visited)
|
||||
IO.puts("#{prefix} ├─ No:")
|
||||
do_print(n, indent_level + 2, new_visited)
|
||||
IO.puts("#{prefix} └─ DC:")
|
||||
do_print(d, indent_level + 2, new_visited)
|
||||
|
||||
{:error, reason} ->
|
||||
IO.puts("#{prefix}ID #{id}: ERROR - #{reason}")
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
defmodule Tdd.TypeSpec do
|
||||
@moduledoc """
|
||||
Defines the `TypeSpec` structure and functions for its manipulation.
|
||||
@ -529,15 +572,19 @@ defmodule Tdd.Variable do
|
||||
|
||||
# --- Category 5: List Properties ---
|
||||
# All are now 4-element tuples. The sorting will be correct.
|
||||
@spec v_list_all_elements_are(TypeSpec.t()) :: term()
|
||||
def v_list_all_elements_are(element_spec), do: {5, :a_all_elements, element_spec, nil}
|
||||
# @spec v_list_all_elements_are(TypeSpec.t()) :: term()
|
||||
# def v_list_all_elements_are(element_spec), do: {5, :a_all_elements, element_spec, nil}
|
||||
|
||||
|
||||
@doc "Predicate: The list is the empty list `[]`."
|
||||
@spec v_list_is_empty() :: term()
|
||||
def v_list_is_empty, do: {5, :b_is_empty, nil, nil}
|
||||
|
||||
@doc "Predicate: Applies a nested predicate to the head of a non-empty list."
|
||||
@spec v_list_head_pred(term()) :: term()
|
||||
def v_list_head_pred(nested_pred_var), do: {5, :c_head, nested_pred_var, nil}
|
||||
|
||||
@doc "Predicate: Applies a nested predicate to the tail of a non-empty list."
|
||||
@spec v_list_tail_pred(term()) :: term()
|
||||
def v_list_tail_pred(nested_pred_var), do: {5, :d_tail, nested_pred_var, nil}
|
||||
end
|
||||
@ -629,14 +676,14 @@ defmodule Tdd.Predicate.Info do
|
||||
}
|
||||
end
|
||||
|
||||
def get_traits({5, :a_all_elements, element_spec, _}) do
|
||||
%{
|
||||
type: :list_recursive_ambient,
|
||||
category: :list,
|
||||
ambient_constraint_spec: element_spec,
|
||||
implies: [{Variable.v_is_list(), true}]
|
||||
}
|
||||
end
|
||||
# def get_traits({5, :a_all_elements, element_spec, _}) do
|
||||
# %{
|
||||
# type: :list_recursive_ambient,
|
||||
# category: :list,
|
||||
# ambient_constraint_spec: element_spec,
|
||||
# implies: [{Variable.v_is_list(), true}]
|
||||
# }
|
||||
# end
|
||||
|
||||
def get_traits({5, :b_is_empty, _, _}) do
|
||||
%{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]}
|
||||
@ -694,6 +741,17 @@ defmodule Tdd.Consistency.Engine do
|
||||
do_check(assumptions)
|
||||
end
|
||||
|
||||
@doc """
|
||||
Expands a map of assumptions with all their logical implications.
|
||||
|
||||
Returns `{:ok, expanded_map}` or `{:error, :contradiction}`.
|
||||
"""
|
||||
@spec expand(map()) :: {:ok, map()} | {:error, :contradiction}
|
||||
def expand(assumptions) do
|
||||
# Just expose the internal helper.
|
||||
expand_with_implications(assumptions)
|
||||
end
|
||||
|
||||
# --- The Core Recursive Checker ---
|
||||
|
||||
defp do_check(assumptions) do
|
||||
@ -729,7 +787,7 @@ defmodule Tdd.Consistency.Engine do
|
||||
end
|
||||
else
|
||||
# `expand_with_implications` or `check_flat_consistency` failed.
|
||||
:error -> :contradiction
|
||||
{:error, _reason} -> :contradiction
|
||||
end
|
||||
end
|
||||
|
||||
@ -770,8 +828,8 @@ defmodule Tdd.Consistency.Engine do
|
||||
case Enum.reduce(implications, {:ok, %{}}, fn {implied_var, implied_val}, acc ->
|
||||
reduce_implication({implied_var, implied_val}, all_assumptions, acc)
|
||||
end) do
|
||||
{:error, :contradiction} ->
|
||||
:error
|
||||
{:error, :contradiction} = err ->
|
||||
err
|
||||
|
||||
{:ok, newly_added} when map_size(newly_added) == 0 ->
|
||||
{:ok, all_assumptions}
|
||||
@ -801,7 +859,7 @@ defmodule Tdd.Consistency.Engine do
|
||||
:ok <- check_tuple_consistency(assumptions) do
|
||||
:ok
|
||||
else
|
||||
:error -> :error
|
||||
:error -> {:error, :consistency_error}
|
||||
end
|
||||
end
|
||||
|
||||
@ -1018,7 +1076,6 @@ defmodule Tdd.Algo do
|
||||
@spec simplify(non_neg_integer(), map()) :: non_neg_integer
|
||||
def simplify(tdd_id, assumptions \\ %{}) do
|
||||
# The main cache uses a sorted list of assumptions for a canonical key.
|
||||
# The internal context set uses this same canonical form.
|
||||
sorted_assumptions = Enum.sort(assumptions)
|
||||
cache_key = {:simplify, tdd_id, sorted_assumptions}
|
||||
|
||||
@ -1288,8 +1345,8 @@ defmodule Tdd.TypeReconstructor do
|
||||
{5, :b_is_empty, _, _} -> {:literal, []}
|
||||
# --- THIS IS THE FIX ---
|
||||
# Correctly reconstruct a list_of spec from the ambient predicate.
|
||||
{5, :a_all_elements, element_spec, _} ->
|
||||
{:list_of, element_spec}
|
||||
# {5, :a_all_elements, element_spec, _} ->
|
||||
# {:list_of, element_spec}
|
||||
# Ignore recursive and ambient vars at this flat level
|
||||
_ -> :any
|
||||
end
|
||||
@ -1384,13 +1441,13 @@ defmodule Tdd.Compiler do
|
||||
|
||||
# --- RECURSIVE TYPES ---
|
||||
#
|
||||
{:list_of, element_spec} ->
|
||||
id_list = spec_to_id(:list)
|
||||
# The element_spec MUST be normalized to be a canonical part of the variable.
|
||||
# {:list_of, element_spec} ->
|
||||
# id_list = spec_to_id(:list)
|
||||
# # The element_spec MUST be normalized to be a canonical part of the variable.
|
||||
norm_elem_spec = TypeSpec.normalize(element_spec)
|
||||
var = Variable.v_list_all_elements_are(norm_elem_spec)
|
||||
id_check = create_base_type_tdd(var)
|
||||
Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
|
||||
# id_check = create_base_type_tdd(var)
|
||||
# Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
|
||||
{:cons, head_spec, tail_spec} ->
|
||||
id_head = spec_to_id(head_spec)
|
||||
id_tail = spec_to_id(tail_spec)
|
||||
@ -1917,11 +1974,11 @@ defmodule TddVariableTests do
|
||||
Variable.v_list_head_pred(Variable.v_is_atom())
|
||||
)
|
||||
|
||||
test(
|
||||
"v_list_all_elements_are nests a TypeSpec correctly",
|
||||
{5, :a_all_elements, {:union, [:atom, :integer]}, nil},
|
||||
Variable.v_list_all_elements_are(TypeSpec.normalize({:union, [:integer, :atom]}))
|
||||
)
|
||||
# test(
|
||||
# "v_list_all_elements_are nests a TypeSpec correctly",
|
||||
# {5, :a_all_elements, {:union, [:atom, :integer]}, nil},
|
||||
# Variable.v_list_all_elements_are(TypeSpec.normalize({:union, [:integer, :atom]}))
|
||||
# )
|
||||
|
||||
# --- Test Section: Global Ordering ---
|
||||
IO.puts("\n--- Section: Global Ordering (Based on Elixir Term Comparison) ---")
|
||||
@ -1968,17 +2025,17 @@ defmodule TddVariableTests do
|
||||
Variable.v_tuple_elem_pred(0, Variable.v_is_integer())
|
||||
)
|
||||
|
||||
IO.inspect(Variable.v_list_all_elements_are(:atom),
|
||||
label: "Variable.v_list_all_elements_are(:atom)"
|
||||
)
|
||||
# IO.inspect(Variable.v_list_all_elements_are(:atom),
|
||||
# label: "Variable.v_list_all_elements_are(:atom)"
|
||||
# )
|
||||
|
||||
IO.inspect(Variable.v_list_is_empty(), label: "Variable.v_list_is_empty()")
|
||||
|
||||
test(
|
||||
"List :a_all_elements var < List :b_is_empty var",
|
||||
true,
|
||||
Variable.v_list_all_elements_are(:atom) < Variable.v_list_is_empty()
|
||||
)
|
||||
# test(
|
||||
# "List :a_all_elements var < List :b_is_empty var",
|
||||
# true,
|
||||
# Variable.v_list_all_elements_are(:atom) < Variable.v_list_is_empty()
|
||||
# )
|
||||
|
||||
test(
|
||||
"List :b_is_empty var < List :c_head var",
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user