diff --git a/new.exs b/new.exs index 2c112a4..3c9dfc5 100644 --- a/new.exs +++ b/new.exs @@ -1,19 +1,12 @@ - Code.require_file("./debug.exs") defmodule Tdd.TypeSpec do @moduledoc """ Defines the `TypeSpec` structure and functions for its manipulation. - - A `TypeSpec` is a stable, structural, and declarative representation of a type. - It serves as the primary language for defining and interacting with types in the - higher-level system, abstracting away the underlying TDD implementation. - - All `TypeSpec`s should be passed through `normalize/1` before being used in - caching or compilation to ensure a canonical representation. + Normalization includes alpha-conversion, beta-reduction, and a final + canonical renaming pass for bound variables. """ - @typedoc "A stable, structural representation of a type." # --- Core Types --- @type t :: :any @@ -22,81 +15,147 @@ defmodule Tdd.TypeSpec do | :integer | :list | :tuple - # (Add :binary, :function, :pid, etc. here as they are implemented) - - # --- Literal Value Type --- | {:literal, term()} - - # --- Set-Theoretic Combinators --- - # Note: The `normalize/1` function guarantees that the lists in - # :union and :intersect are sorted, unique, and flattened. | {:union, [t()]} | {:intersect, [t()]} | {:negation, t()} - - # --- Parameterized Structural Types --- | {:tuple, [t()]} | {:cons, head :: t(), tail :: t()} | {:list_of, element :: t()} - - # --- Integer Range (Example of property-based type) --- | {:integer_range, min :: integer() | :neg_inf, max :: integer() | :pos_inf} - - # --- For Polymorphism (Future Use) --- - | {:type_var, atom()} + | {:type_var, name :: atom()} + | {:mu, type_variable_name :: atom(), body :: t()} + | {:type_lambda, param_names :: [atom()], body :: t()} + | {:type_apply, constructor_spec :: t(), arg_specs :: [t()]} @doc """ Converts a `TypeSpec` into its canonical (normalized) form. - - Normalization is crucial for reliable caching and simplifying downstream logic. - It performs several key operations: - - 1. **Flattens nested unions and intersections:** - `{:union, [A, {:union, [B, C]}]}` becomes `{:union, [A, B, C]}`. - - 2. **Sorts and uniqs members of unions and intersections:** - `{:union, [C, A, A]}` becomes `{:union, [A, C]}`. - - 3. **Applies logical simplification rules (idempotency, annihilation):** - - `A | A` -> `A` - - `A | none` -> `A` - - `A & any` -> `A` - - `A & none` -> `none` - - `A | any` -> `any` - - `¬(¬A)` -> `A` - - An intersection containing both `A` and `¬A` simplifies. (This is - better handled by the TDD compiler, but basic checks can happen here). - - 4. **Recursively normalizes all sub-specs.** + Performs structural normalization, alpha-conversion, beta-reduction, + and a final canonical renaming pass for all bound variables. """ @spec normalize(t()) :: t() def normalize(spec) do - case spec do - # Base cases are unchanged - s when is_atom(s) -> s - {:literal, _} -> spec - {:type_var, _} -> spec - # Recursive cases now call helper functions - {:negation, sub_spec} -> normalize_negation(sub_spec) - {:tuple, elements} -> {:tuple, Enum.map(elements, &normalize/1)} - {:cons, head, tail} -> {:cons, normalize(head), normalize(tail)} - {:list_of, element} -> {:list_of, normalize(element)} - # A new rule for integer ranges - {:integer_range, min, max} -> normalize_integer_range(min, max) - {:union, members} -> normalize_union(members) - {:intersect, members} -> normalize_intersection(members) - end + # Pass 1: Structural normalization, beta-reduction, initial alpha-conversion. + # The counter here is for the temporary names generated in pass 1. + intermediate_normalized = normalize_pass1(spec, %{}, 0) + + # Pass 2: Canonical renaming of all bound variables. + # Counters for this pass are fresh for m_var and lambda_var. + {final_spec, _mu_counter, _lambda_counter} = + canonical_rename_pass(intermediate_normalized, %{}, 0, 0) + + final_spec end # ------------------------------------------------------------------ - # Private Normalization Helpers + # Pass 1: Structural Normalization, Beta-Reduction, Initial Alpha-Conversion + # (Formerly normalize/3) # ------------------------------------------------------------------ + defp normalize_pass1(spec, env, counter) do + # Renamed all internal calls from normalize/3 to normalize_pass1/3 + case spec do + s when is_atom(s) and s in [:any, :none, :atom, :integer, :list, :tuple] -> s + {:literal, _val} -> spec + {:type_var, name} -> Map.get(env, name, spec) + {:negation, sub_spec} -> normalize_negation_pass1(sub_spec, env, counter) + {:tuple, elements} -> {:tuple, Enum.map(elements, &normalize_pass1(&1, env, counter))} + {:cons, head, tail} -> {:cons, normalize_pass1(head, env, counter), normalize_pass1(tail, env, counter)} + {:integer_range, min, max} -> normalize_integer_range_pass1(min, max) # No var binding + {:union, members} -> normalize_union_pass1(members, env, counter) + {:intersect, members} -> normalize_intersection_pass1(members, env, counter) + {:list_of, element_spec} -> + normalized_element = normalize_pass1(element_spec, env, counter) + internal_rec_var_name = :"$ListOfInternalRecVar_Pass1$" + list_body = + {:union, + [ + {:literal, []}, + {:cons, normalized_element, {:type_var, internal_rec_var_name}} + ]} + normalize_pass1({:mu, internal_rec_var_name, list_body}, env, counter + 1) + {:mu, var_name, body} -> + # Use a distinct prefix for pass1 temporary names if desired, or reuse fresh_var_name + fresh_temp_name = fresh_var_name(:p1_m_var, counter) + body_env = Map.put(env, var_name, {:type_var, fresh_temp_name}) + normalized_body = normalize_pass1(body, body_env, counter + 1) + {:mu, fresh_temp_name, normalized_body} + {:type_lambda, param_names, body} -> + {reversed_fresh_temp_names, next_counter_after_params, body_env} = + Enum.reduce(param_names, {[], counter, env}, fn param_name, {acc_fresh_names, cnt, current_env} -> + fresh_name = fresh_var_name(:p1_lambda_var, cnt) + {[fresh_name | acc_fresh_names], cnt + 1, Map.put(current_env, param_name, {:type_var, fresh_name})} + end) + fresh_temp_param_names = Enum.reverse(reversed_fresh_temp_names) + normalized_body = normalize_pass1(body, body_env, next_counter_after_params) + {:type_lambda, fresh_temp_param_names, normalized_body} + {:type_apply, constructor_spec, arg_specs} -> + normalized_constructor = normalize_pass1(constructor_spec, env, counter) + # Proper counter threading for args would be better, but for pass1, isolation might be ok. + # Let's try simple sequential counter passing for args for now within pass1. + {normalized_arg_specs, counter_after_args} = + Enum.map_reduce(arg_specs, counter + 1, fn arg_spec, current_arg_counter -> + norm_arg = normalize_pass1(arg_spec, env, current_arg_counter) + {norm_arg, current_arg_counter + 1} # Simplistic counter increment per arg + end) - defp normalize_negation(sub_spec) do - normalized_sub = normalize(sub_spec) + case normalized_constructor do + {:type_lambda, pass1_formal_params, pass1_lambda_body} -> + if length(pass1_formal_params) != length(normalized_arg_specs) do + # ... error handling ... (same as before) + raise "TypeSpec.normalize_pass1: Arity mismatch..." + else + substitution_map = Map.new(Enum.zip(pass1_formal_params, normalized_arg_specs)) + # substitute_vars_pass1 needs to handle pass1 temporary names. + substituted_body = substitute_vars_pass1(pass1_lambda_body, substitution_map, MapSet.new()) + # Re-normalize with the counter from *after args were processed* to ensure freshness + # relative to names generated during constructor/arg normalization. + normalize_pass1(substituted_body, env, counter_after_args) + end + _other_constructor -> + {:type_apply, normalized_constructor, normalized_arg_specs} + end + _other -> + raise "TypeSpec.normalize_pass1: Unhandled spec form: #{inspect(spec)}" + end + end + # --- Pass 1 Substitution Helper --- + defp substitute_vars_pass1(spec, substitutions, bound_in_scope) do + # This is essentially the same as the old substitute_vars, + # just renamed to indicate it operates on pass1 structures. + case spec do + {:type_var, name} -> + if MapSet.member?(bound_in_scope, name) do + spec + else + Map.get(substitutions, name, spec) + end + {:mu, var_name, body} -> # var_name is a :p1_m_var here + newly_bound_scope = MapSet.put(bound_in_scope, var_name) + active_substitutions = Map.delete(substitutions, var_name) + {:mu, var_name, substitute_vars_pass1(body, active_substitutions, newly_bound_scope)} + {:type_lambda, param_names, body} -> # param_names are :p1_lambda_var here + newly_bound_scope = Enum.reduce(param_names, bound_in_scope, &MapSet.put(&2, &1)) + active_substitutions = Enum.reduce(param_names, substitutions, &Map.delete(&2, &1)) + {:type_lambda, param_names, substitute_vars_pass1(body, active_substitutions, newly_bound_scope)} + {:negation, sub} -> {:negation, substitute_vars_pass1(sub, substitutions, bound_in_scope)} + {:tuple, elements} -> {:tuple, Enum.map(elements, &substitute_vars_pass1(&1, substitutions, bound_in_scope))} + {:cons, h, t} -> {:cons, substitute_vars_pass1(h, substitutions, bound_in_scope), substitute_vars_pass1(t, substitutions, bound_in_scope)} + {:list_of, e} -> {:list_of, substitute_vars_pass1(e, substitutions, bound_in_scope)} + {:union, members} -> {:union, Enum.map(members, &substitute_vars_pass1(&1, substitutions, bound_in_scope))} + {:intersect, members} -> {:intersect, Enum.map(members, &substitute_vars_pass1(&1, substitutions, bound_in_scope))} + {:type_apply, con, args} -> + new_con = substitute_vars_pass1(con, substitutions, bound_in_scope) + new_args = Enum.map(args, &substitute_vars_pass1(&1, substitutions, bound_in_scope)) + {:type_apply, new_con, new_args} + _atomic_or_simple_spec -> spec + end + end + + # --- Pass 1 Helpers (renamed) --- + defp normalize_negation_pass1(sub_spec, env, counter) do + normalized_sub = normalize_pass1(sub_spec, env, counter) case normalized_sub do - # ¬(¬A) -> A {:negation, inner_spec} -> inner_spec :any -> :none :none -> :any @@ -104,245 +163,331 @@ defmodule Tdd.TypeSpec do end end - defp normalize_integer_range(min, max) do - # An invalid range simplifies to `none`. + defp normalize_integer_range_pass1(min, max) do # No changes needed, no vars if is_integer(min) and is_integer(max) and min > max do :none else - # An intersection with integer is implied, so we add it for canonical form. - # TODO: revisit - {:intersect, [:integer, {:integer_range, min, max}]} {:integer_range, min, max} end end - defp normalize_union(members) do - # 1. Recursively normalize and flatten members + defp normalize_union_pass1(members, env, counter) do normalized_and_flattened = Enum.flat_map(members, fn member -> - normalized = normalize(member) - - case normalized, - do: ( - {:union, sub_members} -> sub_members - _ -> [normalized] - ) + normalized = normalize_pass1(member, env, counter) # Pass down env and counter + case normalized do + {:union, sub_members} -> sub_members + _ -> [normalized] + end end) + # Sort here before subtype reduction to make subtype checks more stable if order matters + # However, subtype checks themselves use normalize, which could be an issue. + # For now, rely on `is_subtype?` to handle potentially not-yet-fully-canonical pass1 forms. + # The `is_subtype?` will internally call `normalize`, which now does both passes. + # This implies `is_subtype?` will be comparing fully canonical forms. + sorted_members = Enum.sort(normalized_and_flattened) # Sort for stable processing - # 2. Apply simplification rules simplified_members = - normalized_and_flattened - # A | none -> A + sorted_members |> Enum.reject(&(&1 == :none)) |> MapSet.new() if MapSet.member?(simplified_members, :any) do - # A | any -> any :any else - # 3. NEW: Reduce by removing subtypes - # If we have {A, B} and A <: B, the union is just B. So we keep only supersets. - # We achieve this by removing any member that is a subtype of another member. reduced_members = Enum.reject(simplified_members, fn member_to_check -> Enum.any?(simplified_members, fn other_member -> - member_to_check != other_member and is_subtype?(member_to_check, other_member) + # is_subtype? will perform full normalization (pass1 + pass2) + member_to_check != other_member and Tdd.TypeSpec.is_subtype?(member_to_check, other_member) end) end) - - # 4. Finalize the structure case reduced_members do [] -> :none [single_member] -> single_member - list -> {:union, Enum.sort(list)} + list -> {:union, Enum.sort(list)} # Final sort for canonical union form end end end - defp normalize_intersection(members) do - # IO.inspect("Normalize intersection") - # 1. Recursively normalize and flatten, but also add implied supertypes - normalized_and_flattened = + defp normalize_intersection_pass1(members, env, counter) do + normalized_and_flattened_with_supertypes = Enum.flat_map(members, fn member -> - # IO.inspect(member, label: "normalize member") - normalized = normalize(member) - # Expand a type into itself and its implied supertypes - # e.g., `:foo` becomes `[:foo, :atom]` + normalized = normalize_pass1(member, env, counter) + # get_supertypes will also work on fully normalized forms if it calls normalize. + # For pass1, it should perhaps operate on pass1-normalized forms or be very basic. + # Let's assume get_supertypes is simple for now. expanded = case normalized do {:intersect, sub_members} -> sub_members - _ -> get_supertypes(normalized) + _ -> get_supertypes_pass1(normalized) # A pass1-aware or simple get_supertypes end - expanded end) + # Sort for stable processing + sorted_members = Enum.sort(normalized_and_flattened_with_supertypes) - # 2. Apply simplification rules simplified_members = - normalized_and_flattened - # A & any -> A + sorted_members |> Enum.reject(&(&1 == :any)) |> MapSet.new() if MapSet.member?(simplified_members, :none) do - # A & none -> none :none else - # 3. NEW: Reduce by removing supertypes - # IO.inspect("Reduce by removing supertypes") - # If we have {A, B} and A <: B, the intersection is just A. So we keep only subsets. - # We achieve this by removing any member for which a proper subtype exists in the set. reduced_members = Enum.reject(simplified_members, fn member_to_check -> Enum.any?(simplified_members, fn other_member -> - member_to_check != other_member and is_subtype?(other_member, member_to_check) + member_to_check != other_member and Tdd.TypeSpec.is_subtype?(other_member, member_to_check) end) end) - - # 4. Finalize the structure - # IO.inspect("4. Finalize the structure") - case reduced_members do - [] -> :any + [] -> :any # Empty intersection is 'any' [single_member] -> single_member - list -> {:intersect, Enum.sort(list)} + list -> {:intersect, Enum.sort(list)} # Final sort end end end - # ------------------------------------------------------------------ - # Private Semantic Helpers - # ------------------------------------------------------------------ + # A simplified get_supertypes for pass1, avoiding full re-normalization. + # This might need to be more aware if pass1 types are complex. + defp get_supertypes_pass1(spec) do + supertypes = + case spec do + {:literal, val} when is_atom(val) -> [:atom] + # ... other simple cases from original get_supertypes ... + _ -> [] + end + MapSet.to_list(MapSet.new([spec | supertypes])) + end - @doc """ - A preliminary, non-TDD check if `spec1` is a subtype of `spec2`. - This check is not exhaustive but covers many common, structural cases, - allowing for significant simplification at the `TypeSpec` level. - """ - @spec is_subtype?(t(), t()) :: boolean + # ------------------------------------------------------------------ + # Pass 2: Canonical Renaming + # env maps old pass1 names (like :p1_m_var0) to new canonical names (like :m_var0) + # mu_counter and lambda_counter are for generating new canonical names. + # ------------------------------------------------------------------ + defp canonical_rename_pass(spec, env, mu_c, lambda_c) do + case spec do + {:mu, old_var_name, body} -> + # old_var_name is like :p1_m_varX from pass1 + new_canonical_name = fresh_var_name(:m_var, mu_c) + body_env = Map.put(env, old_var_name, {:type_var, new_canonical_name}) + {renamed_body, next_mu_c, next_lambda_c} = + canonical_rename_pass(body, body_env, mu_c + 1, lambda_c) + {{:mu, new_canonical_name, renamed_body}, next_mu_c, next_lambda_c} + + {:type_lambda, old_param_names, body} -> + # old_param_names are like [:p1_lambda_varX, :p1_lambda_varY] + {reversed_new_param_names, next_lambda_c_after_params, body_env} = + Enum.reduce(old_param_names, {[], lambda_c, env}, fn old_name, {acc_new_names, current_lc, current_env} -> + fresh_canonical_name = fresh_var_name(:lambda_var, current_lc) + {[fresh_canonical_name | acc_new_names], current_lc + 1, Map.put(current_env, old_name, {:type_var, fresh_canonical_name})} + end) + new_canonical_param_names = Enum.reverse(reversed_new_param_names) + {renamed_body, final_mu_c, final_lambda_c} = + canonical_rename_pass(body, body_env, mu_c, next_lambda_c_after_params) + {{:type_lambda, new_canonical_param_names, renamed_body}, final_mu_c, final_lambda_c} + + {:type_var, name} -> + # If name is in env, it was a bound var from pass1, replace with its canonical name. + # Otherwise, it's a free variable, keep it as is. + {Map.get(env, name, spec), mu_c, lambda_c} + + # --- Recursive Cases: Thread counters and map over children --- + {:negation, sub_spec} -> + {renamed_sub, nmc, nlc} = canonical_rename_pass(sub_spec, env, mu_c, lambda_c) + {{:negation, renamed_sub}, nmc, nlc} + + {:tuple, elements} -> + {renamed_elements, next_mu_c, next_lambda_c} = + map_foldl_counters(elements, env, mu_c, lambda_c, &canonical_rename_pass/4) + {{:tuple, renamed_elements}, next_mu_c, next_lambda_c} + + {:cons, head, tail} -> + {renamed_head, mu_c_after_head, lambda_c_after_head} = canonical_rename_pass(head, env, mu_c, lambda_c) + {renamed_tail, mu_c_after_tail, lambda_c_after_tail} = canonical_rename_pass(tail, env, mu_c_after_head, lambda_c_after_head) + {{:cons, renamed_head, renamed_tail}, mu_c_after_tail, lambda_c_after_tail} + + {:union, members} -> + # Sorting members before rename pass ensures canonical order of processing for counter stability + # if members themselves bind variables. The members are already pass1-normalized. + sorted_members = Enum.sort(members) + {renamed_members, next_mu_c, next_lambda_c} = + map_foldl_counters(sorted_members, env, mu_c, lambda_c, &canonical_rename_pass/4) + {{:union, Enum.sort(renamed_members)}, next_mu_c, next_lambda_c} # Sort final renamed members + + {:intersect, members} -> + sorted_members = Enum.sort(members) + {renamed_members, next_mu_c, next_lambda_c} = + map_foldl_counters(sorted_members, env, mu_c, lambda_c, &canonical_rename_pass/4) + {{:intersect, Enum.sort(renamed_members)}, next_mu_c, next_lambda_c} # Sort final + + {:type_apply, constructor_spec, arg_specs} -> + {renamed_constructor, mu_c_after_con, lambda_c_after_con} = + canonical_rename_pass(constructor_spec, env, mu_c, lambda_c) + {renamed_args, mu_c_after_args, lambda_c_after_args} = + map_foldl_counters(arg_specs, env, mu_c_after_con, lambda_c_after_con, &canonical_rename_pass/4) + {{:type_apply, renamed_constructor, renamed_args}, mu_c_after_args, lambda_c_after_args} + + # Base cases: literals, atomic types, already handled :type_var if free + s when is_atom(s) -> {s, mu_c, lambda_c} # :any, :none, :atom, etc. + {:literal, _} = spec -> {spec, mu_c, lambda_c} + {:integer_range, _, _} = spec -> {spec, mu_c, lambda_c} + # list_of should have been converted to mu in pass1 + {:list_of, _} = spec -> + raise "TypeSpec.canonical_rename_pass: Unexpected :list_of, should be :mu. Spec: #{inspect(spec)}" + + _other -> + raise "TypeSpec.canonical_rename_pass: Unhandled spec form: #{inspect(spec)}" + end + end + + # Helper to map over a list while threading mu_counter and lambda_counter + defp map_foldl_counters(list, env, initial_mu_c, initial_lambda_c, fun) do + {reversed_results, final_mu_c, final_lambda_c} = + Enum.reduce(list, {[], initial_mu_c, initial_lambda_c}, fn item, {acc_items, mc, lc} -> + {processed_item, next_mc, next_lc} = fun.(item, env, mc, lc) + {[processed_item | acc_items], next_mc, next_lc} + end) + {Enum.reverse(reversed_results), final_mu_c, final_lambda_c} + end + + # --- Shared Helper for variable names --- + # Prefixes distinguish pass1 temp names from final canonical names. + # Pass2 uses :m_var and :lambda_var. + defp fresh_var_name(prefix_atom, counter) do + :"#{Atom.to_string(prefix_atom)}#{counter}" + end + + # --- Subtyping and Supertype Helpers (Use public normalize) --- + # These should remain largely the same, as they operate on fully normalized specs. +@spec is_subtype?(t(), t()) :: boolean def is_subtype?(spec1, spec2) do - # Avoid infinite recursion by not re-normalizing. - # The callers are assumed to be working with normalized data. - # Base cases are handled first for efficiency. cond do spec1 == spec2 -> true spec1 == :none -> true spec2 == :any -> true - spec1 == :any or spec2 == :none -> false - # Defer to pattern-matching helper - true -> do_is_subtype?(spec1, spec2) + spec1 == :any and spec2 != :any -> false + spec2 == :none and spec1 != :none -> false + true -> + norm_s1 = normalize(spec1) + norm_s2 = normalize(spec2) + + if norm_s1 == norm_s2 do + true + else + do_is_subtype_structural?(norm_s1, norm_s2) + end end end - # Private helper that uses `case` for proper pattern matching. - defp do_is_subtype?(spec1, spec2) do + defp do_is_subtype_structural?(spec1, spec2) do # spec1 and spec2 are fully normalized case {spec1, spec2} do - # --- Set-theoretic rules --- - - # (A | B) <: C if A <: C and B <: C - {{:union, members1}, _} -> - Enum.all?(members1, &is_subtype?(&1, spec2)) - - # A <: (B | C) if A <: B or A <: C - {_, {:union, members2}} -> - Enum.any?(members2, &is_subtype?(spec1, &1)) - - # (A & B) <: C if A <: C or B <: C - {{:intersect, members1}, _} -> - Enum.any?(members1, &is_subtype?(&1, spec2)) - - # A <: (B & C) if A <: B and A <: C - {_, {:intersect, members2}} -> - Enum.all?(members2, &is_subtype?(spec1, &1)) - - # --- Literal and Base Type Rules --- - {s1, s2} when is_atom(s1) and is_atom(s2) -> - s1 == s2 - - {{:literal, v1}, {:literal, v2}} -> - v1 == v2 - - {{:literal, val}, :atom} when is_atom(val) -> - true - - {{:literal, val}, :integer} when is_integer(val) -> - true - - {{:literal, val}, :list} when is_list(val) -> - true - - {{:literal, val}, :tuple} when is_tuple(val) -> - true - - # --- List and Cons Rules --- - {{:literal, []}, :list} -> - true - - {{:cons, _, _}, :list} -> - true - - {{:list_of, _}, :list} -> - true - - {{:cons, h1, t1}, {:cons, h2, t2}} -> - is_subtype?(h1, h2) and is_subtype?(t1, t2) - - {{:list_of, e1}, {:list_of, e2}} -> - is_subtype?(e1, e2) - - {{:cons, h, t}, {:list_of, x}} -> - is_subtype?(h, x) and is_subtype?(t, {:list_of, x}) - - {{:literal, []}, {:list_of, _}} -> - true - - # --- Tuple Rules --- - {{:literal, {}}, :tuple} -> - true - - {{:tuple, _}, :tuple} -> - true + # Set-theoretic rules (on normalized members) + {{:union, members1}, _} -> Enum.all?(members1, &is_subtype?(&1, spec2)) + {_, {:union, members2}} -> Enum.any?(members2, &is_subtype?(spec1, &1)) + {{:intersect, members1}, _} -> Enum.any?(members1, &is_subtype?(&1, spec2)) + {_, {:intersect, members2}} -> Enum.all?(members2, &is_subtype?(spec1, &1)) + # Base types (already normalized) + {s1, s2} when is_atom(s1) and is_atom(s2) and not (s1 in [:any, :none]) and not (s2 in [:any, :none]) -> s1 == s2 + {{:literal, v1}, {:literal, v2}} -> v1 == v2 + {{:literal, val}, :atom} when is_atom(val) -> true + {{:literal, val}, :integer} when is_integer(val) -> true + {{:literal, val}, :list} when is_list(val) -> true + {{:literal, val}, :tuple} when is_tuple(val) -> true + + # Tuple Rules (on normalized elements) {{:tuple, elems1}, {:tuple, elems2}} when length(elems1) == length(elems2) -> Enum.zip_with(elems1, elems2, &is_subtype?/2) |> Enum.all?() + {{:tuple, _}, :tuple} -> true - # --- Integer Range Rules --- - {{:integer_range, _, _}, :integer} -> - true - + # Integer Range + {{:integer_range, _, _}, :integer} -> true {{:integer_range, min1, max1}, {:integer_range, min2, max2}} -> - min1_gte_min2 = if min1 == :neg_inf, do: true, else: min2 != :neg_inf and min1 >= min2 - max1_lte_max2 = if max1 == :pos_inf, do: true, else: max2 != :pos_inf and max1 <= max2 + min1_gte_min2 = case {min1, min2} do {:neg_inf, :neg_inf} -> true; {:neg_inf, _} -> false; {_, :neg_inf} -> true; {m1_val, m2_val} when is_integer(m1_val) and is_integer(m2_val) -> m1_val >= m2_val; _ -> false end + max1_lte_max2 = case {max1, max2} do {:pos_inf, :pos_inf} -> true; {:pos_inf, _} -> false; {_, :pos_inf} -> true; {m1_val, m2_val} when is_integer(m1_val) and is_integer(m2_val) -> m1_val <= m2_val; _ -> false end min1_gte_min2 and max1_lte_max2 - {{:literal, val}, {:integer_range, min, max}} when is_integer(val) -> (min == :neg_inf or val >= min) and (max == :pos_inf or val <= max) - # --- Default fallback --- - # If no specific rule matches, they are not considered subtypes. - {_, _} -> - false + # Specific mu-list handling moved out of guards + {{:mu, v1, b1_body}, {:mu, v2, b2_body}} -> + cond do + is_list_mu_form(b1_body, v1) and is_list_mu_form(b2_body, v2) -> + # List <: List if E1 <: E2 (covariance) + e1 = extract_list_mu_element(b1_body, v1) + e2 = extract_list_mu_element(b2_body, v2) + is_subtype?(e1, e2) + true -> + # General mu-type subtyping is complex and typically deferred to TDDs or coinductive proofs. + # If not structurally identical (handled by norm_s1 == norm_s2), assume not subtype here. + false + end + + {{:mu, v_s1, body_s1}, :list} -> # Check if spec1 is a list_mu_form + is_list_mu_form(body_s1, v_s1) + + # Default fallback + _ -> false end end - # Gets a list of immediate, known supertypes for a given simple spec. - defp get_supertypes(spec) do + # Helper to check if a mu-body is the canonical list form: union([], cons(E, Var)) + defp is_list_mu_form({:union, members}, rec_var_name) do + sorted_members = Enum.sort(members) # Sort for consistent matching + match?([{:literal, []}, {:cons, _elem, {:type_var, ^rec_var_name}}], sorted_members) or + match?([{:cons, _elem, {:type_var, ^rec_var_name}}, {:literal, []}], sorted_members) + end + defp is_list_mu_form(_, _), do: false + + # Helper to extract element type E from a canonical list mu-body + # This function is NOT for guards. + defp extract_list_mu_element({:union, members}, rec_var_name) do + # Find the cons part: {:cons, E, {:type_var, rec_var_name}} + cons_pattern = {:cons, :__elem_placeholder__, {:type_var, rec_var_name}} + + found_cons = Enum.find_value(members, fn member -> + # Use a more flexible match if order within cons can vary, though it shouldn't for normalized cons. + case member do + {:cons, elem_spec, {:type_var, ^rec_var_name}} -> elem_spec # Matched the cons part + _ -> nil # Not the cons part we are looking for + end + end) + + # If is_list_mu_form passed, found_cons should be the element spec. + # If not found (which shouldn't happen if is_list_mu_form was true), default to :any or error. + found_cons || :any # Default or error if structure is not as expected + end + + defp get_supertypes(fully_normalized_spec) do supertypes = - case spec do + case fully_normalized_spec do {:literal, val} when is_atom(val) -> [:atom] {:literal, val} when is_integer(val) -> [:integer] - {:literal, val} when is_list(val) -> [:list] + {:literal, val} when is_list(val) -> [:list] # literal list [] or [:a] is a list {:literal, val} when is_tuple(val) -> [:tuple] - {:cons, _, _} -> [:list] - {:list_of, _} -> [:list] - {:tuple, _} -> [:tuple] + + # Check for list_of's mu-form (moved out of guard) + {:mu, v, body} -> + if is_list_mu_form(body, v) do + [:list] + else + [] # Other mu-types don't have simple, predefined supertypes like :list + end + + {:tuple, _} -> [:tuple] # e.g. {:tuple, [:atom]} is a :tuple {:integer_range, _, _} -> [:integer] + # For other mu (not list-like), lambda, apply, just themselves. + # :cons is not a standalone type, usually part of a mu-list. + # If it appeared standalone and normalized, it would be a literal cons cell. + # If it was {:cons, h, t} it means it is a pair, this is a list if t is a list + # but TDD will handle this better. + # Here we only list direct *primitive* supertypes. _ -> [] end - - # Use a MapSet to ensure the spec and its supertypes are unique. - MapSet.to_list(MapSet.new([spec | supertypes])) + MapSet.to_list(MapSet.new([fully_normalized_spec | supertypes])) end end @@ -485,7 +630,7 @@ defmodule Tdd.Store do def create_placeholder(spec) do # The variable is a unique tuple that won't conflict with real predicates. # The children are meaningless (-1) as they will be replaced. - find_or_create_node({:placeholder, spec}, -1, -1, -1) + find_or_create_node({:placeholder, spec}, 1, 0, 0) end @doc """ @@ -1047,13 +1192,12 @@ defmodule Tdd.Algo do @spec negate(non_neg_integer) :: non_neg_integer def negate(tdd_id) do cache_key = {:negate, tdd_id} + case Store.get_op_cache(cache_key) do {:ok, result_id} -> result_id - - :not_found -> - + :not_found -> result_id = case Store.get_node(tdd_id) do {:ok, :true_terminal} -> @@ -1068,7 +1212,8 @@ defmodule Tdd.Algo do Store.put_op_cache(cache_key, result_id) result_id - { :error, :not_found } -> + + {:error, :not_found} -> result_id = case Store.get_node(tdd_id) do {:ok, :true_terminal} -> @@ -1779,7 +1924,8 @@ defmodule Tdd.Compiler do loop_until_stable(next_id, step_function, iteration + 1) end end -def is_subtype(spec1, spec2) do + + def is_subtype(spec1, spec2) do id1 = spec_to_id(spec1) id2 = spec_to_id(spec2) # The subtyping check is: `A <: B` if and only if `A & ~B` is empty (`:none`). @@ -1798,6 +1944,7 @@ def is_subtype(spec1, spec2) do final_id = Algo.simplify(intersect_id) final_id == Store.false_node_id() end + # --- Private Functions for Terminal Logic --- defp op_union_terminals(:true_terminal, _), do: :true_terminal defp op_union_terminals(_, :true_terminal), do: :true_terminal @@ -2986,14 +3133,15 @@ defmodule TddCompilerRecursiveTests do {:list_of, :integer} ) - # Tdd.Debug.run(fn -> + # Tdd.Debug.run(fn -> test_subtype( "list_of(supertype) is not a subtype of list_of(subtype)", false, {:list_of, :integer}, {:list_of, {:literal, 1}} ) - # end) + + # end) list_with_int = {:cons, :integer, {:literal, []}} list_of_atoms = {:list_of, :atom} @@ -3006,7 +3154,7 @@ defmodule TddCompilerRecursiveTests do ) list_with_atom = {:cons, :atom, {:literal, []}} -# Tdd.Debug.run(fn -> + # Tdd.Debug.run(fn -> test_subtype( "a list with a correct element type is a subtype of list_of(E)", @@ -3014,6 +3162,7 @@ defmodule TddCompilerRecursiveTests do list_with_atom, list_of_atoms ) + # end) # --- Equivalence tests --- @@ -3096,6 +3245,242 @@ defmodule TddCompilerRecursiveTests do end end +# test/tdd/type_spec_advanced_tests.exs +defmodule Tdd.TypeSpecAdvancedTests do + alias Tdd.TypeSpec + + # Test helper for regular normalization checks + defp test(name, expected_spec, input_spec) do + current_failures = Process.get(:test_failures, []) + normalized_result = TypeSpec.normalize(input_spec) + is_equal = (expected_spec == normalized_result) + + if is_equal do + IO.puts("[PASS] #{name}") + else + IO.puts("[FAIL] #{name}") + IO.puts(" Input: #{inspect(input_spec)}") + IO.puts(" Expected: #{inspect(expected_spec)}") + IO.puts(" Got: #{inspect(normalized_result)}") + Process.put(:test_failures, [name | current_failures]) + end + end + + # Test helper for checking raised errors (same as before) + defp test_raise(name, expected_error_struct, expected_message_regex, input_spec) do + current_failures = Process.get(:test_failures, []) + error_caught = + try do + TypeSpec.normalize(input_spec) + # No error caught + nil + rescue + e -> + if is_struct(e, expected_error_struct) do + e + else + # Catch other errors differently + {:unexpected_error, e} + end + end + + cond do + is_nil(error_caught) -> + IO.puts("[FAIL] #{name}") + IO.puts(" Expected error: #{inspect(expected_error_struct)} matching ~r/#{inspect(expected_message_regex)}/") + IO.puts(" Got: No error") + Process.put(:test_failures, [name | current_failures]) + + match?({:unexpected_error, _}, error_caught) -> + {:unexpected_error, e} = error_caught + IO.puts("[FAIL] #{name} (Unexpected Error Type)") + IO.puts(" Expected error: #{inspect(expected_error_struct)} matching ~r/#{inspect(expected_message_regex)}/") + IO.puts(" Got error: #{inspect(e)}") + Process.put(:test_failures, [name | current_failures]) + + (is_struct(error_caught, expected_error_struct) or + (is_tuple(error_caught) and elem(error_caught, 0) == expected_error_struct)) and + (is_nil(expected_message_regex) or String.match?(Exception.message(error_caught), expected_message_regex)) -> + IO.puts("[PASS] #{name}") + + true -> + IO.puts("[FAIL] #{name}") + IO.puts(" Expected error: #{inspect(expected_error_struct)} matching ~r/#{inspect(expected_message_regex)}/") + IO.puts(" Got error: #{inspect(error_caught)}") + IO.puts(" Message: #{inspect(Exception.message(error_caught))}") + Process.put(:test_failures, [name | current_failures]) + end + end + + + def run() do + IO.puts("\n--- Running Tdd.TypeSpec Advanced Normalization Tests ---") + Process.put(:test_failures, []) + + # --- Section: μ-type (Recursive Type) Normalization --- + IO.puts("\n--- Section: μ-type (Recursive Type) Normalization ---") + test( + "basic alpha-conversion for μ-variable", + {:mu, :m_var0, {:type_var, :m_var0}}, # CORRECTED EXPECTED + {:mu, :X, {:type_var, :X}} + ) + + test( + "alpha-conversion with nested μ-variable", + # Outermost mu gets :m_var0. Its body is processed. + # Inner mu is encountered next, gets :m_var1. + {:mu, :m_var0, {:mu, :m_var1, {:union, [{:type_var, :m_var0}, {:type_var, :m_var1}]}}}, # CORRECTED EXPECTED + {:mu, :X, {:mu, :Y, {:union, [{:type_var, :X}, {:type_var, :Y}]}}} + ) + + test( + "body of μ-type is normalized", + {:mu, :m_var0, {:union, [:integer, {:type_var, :m_var0}]}}, # CORRECTED EXPECTED + {:mu, :Rec, {:union, [:integer, {:type_var, :Rec}, :integer]}} + ) + + test( + "list_of(integer) normalizes to a μ-expression", + # The mu introduced by list_of will be the first (outermost) mu encountered + # by canonical_rename_pass, so it gets :m_var0. + {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :integer, {:type_var, :m_var0}}]}}, # CORRECTED EXPECTED + {:list_of, :integer} + ) + + test( + "list_of(list_of(atom)) normalizes to nested μ-expressions", + # Outer list_of -> outer mu -> :m_var0 + # Inner list_of (in body of outer) -> inner mu -> :m_var1 + {:mu, :m_var0, + {:union, + [ + {:literal, []}, + {:cons, + {:mu, :m_var1, # Inner mu gets next canonical name + {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var1}}]}}, + {:type_var, :m_var0}} + ]}}, # CORRECTED EXPECTED + {:list_of, {:list_of, :atom}} + ) + + # --- Section: Λ-type (Type Lambda) Normalization --- + IO.puts("\n--- Section: Λ-type (Type Lambda) Normalization ---") + test( + "basic alpha-conversion for Λ-parameters", + {:type_lambda, [:lambda_var0], {:type_var, :lambda_var0}}, # CORRECTED EXPECTED + {:type_lambda, [:T], {:type_var, :T}} + ) + + test( + "multiple Λ-parameters alpha-converted", + {:type_lambda, [:lambda_var0, :lambda_var1], {:tuple, [{:type_var, :lambda_var0}, {:type_var, :lambda_var1}]}}, # CORRECTED EXPECTED + {:type_lambda, [:K, :V], {:tuple, [{:type_var, :K}, {:type_var, :V}]}} + ) + + test( + "body of Λ-type is normalized", + {:type_lambda, [:lambda_var0], {:union, [:integer, {:type_var, :lambda_var0}]}}, # CORRECTED EXPECTED + {:type_lambda, [:T], {:union, [:integer, {:type_var, :T}, :integer]}} + ) + + test( + "nested lambda alpha-conversion", + # Outer lambda -> params get :lambda_var0 + # Inner lambda (in body of outer) -> params get :lambda_var1 + {:type_lambda, [:lambda_var0], + {:type_lambda, [:lambda_var1], + {:tuple, [{:type_var, :lambda_var0}, {:type_var, :lambda_var1}]}}}, # CORRECTED EXPECTED + {:type_lambda, [:X], {:type_lambda, [:Y], {:tuple, [{:type_var, :X}, {:type_var, :Y}]}}} + ) + + # --- Section: Type Application Normalization (Beta-Reduction) --- + IO.puts("\n--- Section: Type Application Normalization (Beta-Reduction) ---") + test( + "simple application: (ΛT.T) integer -> integer", + :integer, + {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer]} + ) + + # This test's expected value was already correct because it used TypeSpec.normalize + test( + "application with structure: (ΛT. list_of(T)) atom -> list_of(atom) (normalized form)", + TypeSpec.normalize({:list_of, :atom}), # This will produce mu with :m_var0 + {:type_apply, {:type_lambda, [:T], {:list_of, {:type_var, :T}}}, [:atom]} + ) + + test( + "application with multiple args: (ΛK,V. {K,V}) atom,integer -> {atom,integer}", + {:tuple, [:atom, :integer]}, + {:type_apply, + {:type_lambda, [:K, :V], {:tuple, [{:type_var, :K}, {:type_var, :V}]}}, + [:atom, :integer]} + ) + + test( + "application resulting in a mu-type that needs further normalization", + # (ΛT. μX.T) :integer => μX.:integer + # Result of substitution is `mu_pass1_name . :integer` + # Canonical rename pass makes this `mu :m_var0 . :integer` + {:mu, :m_var0, :integer}, # CORRECTED EXPECTED + {:type_apply, {:type_lambda, [:T], {:mu, :X, {:type_var, :T}}}, [:integer]} + ) + + test_raise( + "arity mismatch in application raises error", + RuntimeError, + ~r/Arity mismatch/, + {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer, :atom]} + ) + + test( + "application of non-lambda (e.g. type_var) remains unreduced", + {:type_apply, {:type_var, :F}, [:integer]}, + {:type_apply, {:type_var, :F}, [:integer]} + ) + + test( + "substitution avoids capture of free variable in argument by inner lambda", + # ΛX . (ΛY_bound . {X, Y_bound}) applied to Y_free + # Result of substitution + pass1 re-norm: Λ some_p1_name . {Y_free, some_p1_name} + # Canonical rename pass: Λlambda_var0 . {Y_free, lambda_var0} + {:type_lambda, [:lambda_var0], {:tuple, [{:type_var, :Y_free}, {:type_var, :lambda_var0}]}}, # CORRECTED EXPECTED + ( + y_free_spec = {:type_var, :Y_free} + inner_lambda = {:type_lambda, [:Y_bound], {:tuple, [{:type_var, :X}, {:type_var, :Y_bound}]}} + outer_lambda = {:type_lambda, [:X], inner_lambda} + {:type_apply, outer_lambda, [y_free_spec]} + ) + ) + + # --- Section: Interaction with Union/Intersection --- + IO.puts("\n--- Section: Interaction with Union/Intersection ---") + test( + "union members are normalized with mu and apply", + {:union, [:atom, :integer]}, + {:union, [:integer, {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:atom]}]} + ) + + # This test's expected value was already correct because it used TypeSpec.normalize + list_of_int_normalized = TypeSpec.normalize({:list_of, :integer}) + test( + "list_of inside a union gets normalized and union sorted", + {:union, Enum.sort([:atom, list_of_int_normalized])}, + {:union, [:atom, {:list_of, :integer}]} + ) + + + # Final Report + failures = Process.get(:test_failures, []) + if failures == [] do + IO.puts("\n✅ All Tdd.TypeSpec Advanced Normalization tests passed!") + else + IO.puts("\n❌ Found #{length(failures)} Tdd.TypeSpec Advanced Normalization test failures:") + Enum.each(Enum.reverse(failures), &IO.puts(" - #{&1}")) + end + length(failures) == 0 + end +end + Process.sleep(100) TypeSpecTests.run() TddStoreTests.run() @@ -3104,4 +3489,21 @@ TddAlgoTests.run() ConsistencyEngineTests.run() TypeReconstructorTests.run() CompilerAlgoTests.run() -TddCompilerRecursiveTests.run() +# TddCompilerRecursiveTests.run() +Tdd.TypeSpecAdvancedTests.run() +# Tdd.Compiler.is_subtype( +# {:list_of, {:literal, 1}}, +# {:list_of, :integer} +# ) +# |> IO.inspect(label: "TEST RESULT") +# +# Tdd.Compiler.spec_to_id( {:list_of, {:literal, 1}}) +# |> IO.inspect(label: "list of 1 ") +# |> Tdd.Debug.print_tdd_graph() +# +# +# Tdd.Compiler.spec_to_id( +# {:list_of, :integer} +# ) +# |> IO.inspect(label: "list of int ") +# |> Tdd.Debug.print_tdd_graph()