From 439747daf08c494e4f181098ad5454cf965ab76c Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Tue, 24 Jun 2025 00:43:41 +0200 Subject: [PATCH] dirty hack fix --- new.exs | 1410 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 856 insertions(+), 554 deletions(-) diff --git a/new.exs b/new.exs index 3c9dfc5..2b2c5d0 100644 --- a/new.exs +++ b/new.exs @@ -1,5 +1,6 @@ Code.require_file("./debug.exs") + defmodule Tdd.TypeSpec do @moduledoc """ Defines the `TypeSpec` structure and functions for its manipulation. @@ -35,50 +36,143 @@ defmodule Tdd.TypeSpec do """ @spec normalize(t()) :: t() def normalize(spec) do - # 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} = + {intermediate_normalized, _counter_after_pass1} = normalize_pass1(spec, %{}, 0) + {final_spec_before_subtype_redux, _mu_counter, _lambda_counter} = canonical_rename_pass(intermediate_normalized, %{}, 0, 0) - - final_spec + + apply_subtype_reduction(final_spec_before_subtype_redux) end + # Final pass for subtype-based reductions on fully canonical specs + defp apply_subtype_reduction(spec) do + case spec do + {:union, members} -> + recursively_reduced_members = Enum.map(members, &apply_subtype_reduction/1) + + flattened_members = + Enum.flat_map(recursively_reduced_members, fn + {:union, sub_members} -> sub_members + m -> [m] + end) + + unique_no_none = + flattened_members + |> Enum.reject(&(&1 == :none)) + |> Enum.uniq() + + if Enum.member?(unique_no_none, :any) do + :any + else + # Pass `true` for already_normalized flag to is_subtype? + final_members = + Enum.reject(unique_no_none, fn member_to_check -> + Enum.any?(unique_no_none, fn other_member -> + member_to_check != other_member and is_subtype?(member_to_check, other_member, true) + end) + end) + + case Enum.sort(final_members) do + [] -> :none + [single] -> single + list_members -> {:union, list_members} + end + end + + {:intersect, members} -> + recursively_reduced_members = Enum.map(members, &apply_subtype_reduction/1) + + expanded_flattened_members = + Enum.flat_map(recursively_reduced_members, fn + {:intersect, sub_members} -> sub_members + # get_supertypes expects normalized spec, and its output is also normalized + m -> get_supertypes(m, true) # Pass flag + end) + + unique_no_any = + expanded_flattened_members + |> Enum.reject(&(&1 == :any)) + |> Enum.uniq() + + if Enum.member?(unique_no_any, :none) do + :none + else + # Pass `true` for already_normalized flag to is_subtype? + final_members = + Enum.reject(unique_no_any, fn member_to_check -> + Enum.any?(unique_no_any, fn other_member -> + member_to_check != other_member and is_subtype?(other_member, member_to_check, true) + end) + end) + + case Enum.sort(final_members) do + [] -> :any + [single] -> single + list_members -> {:intersect, list_members} + end + end + + {:negation, body} -> {:negation, apply_subtype_reduction(body)} + {:tuple, elements} -> {:tuple, Enum.map(elements, &apply_subtype_reduction/1)} + {:cons, head, tail} -> {:cons, apply_subtype_reduction(head), apply_subtype_reduction(tail)} + {:mu, var_name, body} -> {:mu, var_name, apply_subtype_reduction(body)} + {:type_lambda, params, body} -> {:type_lambda, params, apply_subtype_reduction(body)} + {:type_apply, constructor, args} -> + {:type_apply, apply_subtype_reduction(constructor), Enum.map(args, &apply_subtype_reduction/1)} + atomic_or_literal -> atomic_or_literal + end + end # ------------------------------------------------------------------ # Pass 1: Structural Normalization, Beta-Reduction, Initial Alpha-Conversion - # (Formerly normalize/3) + # Returns: {normalized_spec, next_counter} # ------------------------------------------------------------------ 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) + res_tuple = case spec do + s when is_atom(s) and s in [:any, :none, :atom, :integer, :list, :tuple] -> {s, counter} + {:literal, _val} = lit_spec -> {lit_spec, counter} + {:type_var, name} -> {Map.get(env, name, spec), counter} + {: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 + + {:tuple, elements} -> + {normalized_elements, next_counter_after_elements} = + map_fold_counter_for_pass1(elements, env, counter, &normalize_pass1/3) + {{:tuple, normalized_elements}, next_counter_after_elements} + + {:cons, head, tail} -> + {normalized_head, counter_after_head} = normalize_pass1(head, env, counter) + {normalized_tail, counter_after_tail} = normalize_pass1(tail, env, counter_after_head) + {{:cons, normalized_head, normalized_tail}, counter_after_tail} + + {:integer_range, min, max} -> + range_spec = + if is_integer(min) and is_integer(max) and min > max do + :none + else + {:integer_range, min, max} + end + {range_spec, counter} + {: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$" + {normalized_element, counter_after_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) + normalize_pass1({:mu, internal_rec_var_name, list_body}, env, counter_after_element) + + {: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} + {normalized_body, next_counter_after_body} = normalize_pass1(body, body_env, counter + 1) + {{:mu, fresh_temp_name, normalized_body}, next_counter_after_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} -> @@ -86,43 +180,39 @@ defmodule Tdd.TypeSpec do {[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} + {normalized_body, final_counter} = normalize_pass1(body, body_env, next_counter_after_params) + {{:type_lambda, fresh_temp_param_names, normalized_body}, final_counter} + {: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_constructor, counter_after_constructor} = normalize_pass1(constructor_spec, env, counter) {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) + map_fold_counter_for_pass1(arg_specs, env, counter_after_constructor, &normalize_pass1/3) 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..." + raise "TypeSpec.normalize_pass1: Arity mismatch in application. Expected #{length(pass1_formal_params)} args, got #{length(normalized_arg_specs)}. Lambda: #{inspect(normalized_constructor)}, Args: #{inspect(normalized_arg_specs)}" 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) + normalize_pass1(substituted_body, env, counter_after_args) end - _other_constructor -> - {:type_apply, normalized_constructor, normalized_arg_specs} + _other_constructor -> + {{:type_apply, normalized_constructor, normalized_arg_specs}, counter_after_args} end - _other -> - raise "TypeSpec.normalize_pass1: Unhandled spec form: #{inspect(spec)}" + other_spec -> + raise "TypeSpec.normalize_pass1: Unhandled spec form: #{inspect(other_spec)}" end + res_tuple + end + + defp map_fold_counter_for_pass1(list, env, initial_counter, fun) do + Enum.map_reduce(list, initial_counter, fn item, acc_counter -> + fun.(item, env, acc_counter) + 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 @@ -130,11 +220,11 @@ defmodule Tdd.TypeSpec do else Map.get(substitutions, name, spec) end - {:mu, var_name, body} -> # var_name is a :p1_m_var here + {:mu, var_name, body} -> 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 + {:type_lambda, param_names, body} -> 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)} @@ -152,125 +242,106 @@ defmodule Tdd.TypeSpec do 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 - {:negation, inner_spec} -> inner_spec - :any -> :none - :none -> :any - _ -> {:negation, normalized_sub} - end - end - - 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 - {:integer_range, min, max} - end - end - - defp normalize_union_pass1(members, env, counter) do - normalized_and_flattened = - Enum.flat_map(members, fn member -> - 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 - - simplified_members = - sorted_members - |> Enum.reject(&(&1 == :none)) - |> MapSet.new() - - if MapSet.member?(simplified_members, :any) do - :any - else - reduced_members = - Enum.reject(simplified_members, fn member_to_check -> - Enum.any?(simplified_members, fn 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) - case reduced_members do - [] -> :none - [single_member] -> single_member - list -> {:union, Enum.sort(list)} # Final sort for canonical union form + {normalized_sub, next_counter} = normalize_pass1(sub_spec, env, counter) + res_spec = + case normalized_sub do + {:negation, inner_spec} -> inner_spec + :any -> :none + :none -> :any + _ -> {:negation, normalized_sub} end - end + {res_spec, next_counter} end - defp normalize_intersection_pass1(members, env, counter) do - normalized_and_flattened_with_supertypes = - Enum.flat_map(members, fn member -> - 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_pass1(normalized) # A pass1-aware or simple get_supertypes + defp normalize_union_pass1(members, env, initial_counter) do + {list_of_normalized_member_lists, final_counter_after_all_members} = + Enum.map_reduce(members, initial_counter, fn member_spec, current_processing_counter -> + {normalized_member_spec_term, counter_after_this_member_normalized} = + normalize_pass1(member_spec, env, current_processing_counter) + + members_to_add_to_overall_list = + case normalized_member_spec_term do + {:union, sub_members} -> sub_members + _ -> [normalized_member_spec_term] end - expanded + {members_to_add_to_overall_list, counter_after_this_member_normalized} end) - # Sort for stable processing - sorted_members = Enum.sort(normalized_and_flattened_with_supertypes) - simplified_members = - sorted_members - |> Enum.reject(&(&1 == :any)) - |> MapSet.new() + normalized_and_flattened = List.flatten(list_of_normalized_member_lists) - if MapSet.member?(simplified_members, :none) do - :none + unique_members = + normalized_and_flattened + |> Enum.reject(&(&1 == :none)) + |> Enum.uniq() + + if Enum.member?(unique_members, :any) do + {:any, final_counter_after_all_members} else - reduced_members = - Enum.reject(simplified_members, fn member_to_check -> - Enum.any?(simplified_members, fn other_member -> - member_to_check != other_member and Tdd.TypeSpec.is_subtype?(other_member, member_to_check) - end) - end) - case reduced_members do - [] -> :any # Empty intersection is 'any' - [single_member] -> single_member - list -> {:intersect, Enum.sort(list)} # Final sort - end + sorted_for_pass1 = Enum.sort(unique_members) + resulting_spec = + case sorted_for_pass1 do + [] -> :none + [single_member] -> single_member + list_members -> {:union, list_members} + end + {resulting_spec, final_counter_after_all_members} + end + end + + defp normalize_intersection_pass1(members, env, initial_counter) do + {list_of_member_groups, final_counter_after_all_members} = + Enum.map_reduce(members, initial_counter, fn member_spec, current_processing_counter -> + {normalized_member_spec_term, counter_after_this_member_normalized} = + normalize_pass1(member_spec, env, current_processing_counter) + + expanded_members = + case normalized_member_spec_term do + {:intersect, sub_members} -> sub_members + _ -> get_supertypes_pass1(normalized_member_spec_term) + end + {expanded_members, counter_after_this_member_normalized} + end) + + normalized_and_flattened_with_supertypes = List.flatten(list_of_member_groups) + + unique_members = + normalized_and_flattened_with_supertypes + |> Enum.reject(&(&1 == :any)) + |> Enum.uniq() + + if Enum.member?(unique_members, :none) do + {:none, final_counter_after_all_members} + else + sorted_for_pass1 = Enum.sort(unique_members) + resulting_spec = + case sorted_for_pass1 do + [] -> :any + [single_member] -> single_member + list_members -> {:intersect, list_members} + end + {resulting_spec, final_counter_after_all_members} end end - # 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 ... + {:literal, val} when is_integer(val) -> [:integer] + {:literal, val} when is_list(val) -> [:list] + {:literal, val} when is_tuple(val) -> [:tuple] + {:mu, _v, _body} -> [] + {:tuple, _} -> [:tuple] + {:integer_range, _, _} -> [:integer] _ -> [] end MapSet.to_list(MapSet.new([spec | supertypes])) end - - # ------------------------------------------------------------------ - # 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} = @@ -278,7 +349,6 @@ defmodule Tdd.TypeSpec do {{: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) @@ -290,18 +360,15 @@ defmodule Tdd.TypeSpec do {{: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) + map_foldl_counters_for_rename(elements, env, mu_c, lambda_c, &canonical_rename_pass/4) {{:tuple, renamed_elements}, next_mu_c, next_lambda_c} {:cons, head, tail} -> @@ -310,31 +377,27 @@ defmodule Tdd.TypeSpec do {{: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) + 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 + map_foldl_counters_for_rename(sorted_members, env, mu_c, lambda_c, &canonical_rename_pass/4) + {{:union, Enum.sort(renamed_members)}, next_mu_c, next_lambda_c} {: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 + map_foldl_counters_for_rename(sorted_members, env, mu_c, lambda_c, &canonical_rename_pass/4) + {{:intersect, Enum.sort(renamed_members)}, next_mu_c, next_lambda_c} {: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) + map_foldl_counters_for_rename(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. + s when is_atom(s) -> {s, mu_c, lambda_c} {: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)}" @@ -343,8 +406,7 @@ defmodule Tdd.TypeSpec do 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 + defp map_foldl_counters_for_rename(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) @@ -353,138 +415,161 @@ defmodule Tdd.TypeSpec do {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 + # Public API + @spec is_subtype?(t(), t()) :: boolean + def is_subtype?(spec1, spec2), do: is_subtype?(spec1, spec2, false) + + # Internal helper with already_normalized flag + @spec is_subtype?(t(), t(), boolean) :: boolean + def is_subtype?(spec1, spec2, already_normalized) do cond do spec1 == spec2 -> true spec1 == :none -> true spec2 == :any -> true - spec1 == :any and spec2 != :any -> false - spec2 == :none and spec1 != :none -> false + spec1 == :any and spec2 != :any -> false + spec2 == :none and spec1 != :none -> false true -> - norm_s1 = normalize(spec1) - norm_s2 = normalize(spec2) + {norm_s1, norm_s2} = + if already_normalized do + {spec1, spec2} + else + {normalize(spec1), normalize(spec2)} + end if norm_s1 == norm_s2 do true else - do_is_subtype_structural?(norm_s1, norm_s2) + do_is_subtype_structural?(norm_s1, norm_s2, MapSet.new()) end end end - defp do_is_subtype_structural?(spec1, spec2) do # spec1 and spec2 are fully normalized - case {spec1, spec2} do - # 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)) + defp do_is_subtype_structural?(spec1, spec2, visited) do + if MapSet.member?(visited, {spec1, spec2}) do + true + else + cond do + spec1 == :none -> true + spec2 == :any -> true + spec1 == :any and spec2 != :any -> false + spec2 == :none and spec1 != :none -> false + spec1 == spec2 -> true - # 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 + true -> + new_visited = MapSet.put(visited, {spec1, spec2}) - # Integer Range - {{:integer_range, _, _}, :integer} -> true - {{:integer_range, min1, max1}, {:integer_range, min2, 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) + case {spec1, spec2} do + {{:union, members1}, _} -> Enum.all?(members1, &do_is_subtype_structural?(&1, spec2, new_visited)) + {_, {:union, members2}} -> Enum.any?(members2, &do_is_subtype_structural?(spec1, &1, new_visited)) + {{:intersect, members1}, _} -> Enum.any?(members1, &do_is_subtype_structural?(&1, spec2, new_visited)) + {_, {:intersect, members2}} -> Enum.all?(members2, &do_is_subtype_structural?(spec1, &1, new_visited)) - # 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 + {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, elems1}, {:tuple, elems2}} when length(elems1) == length(elems2) -> + Enum.zip_with(elems1, elems2, &do_is_subtype_structural?(&1, &2, new_visited)) |> Enum.all?() + {{:tuple, _}, :tuple} -> true + + {{:integer_range, _, _}, :integer} -> true + {{:integer_range, min1, max1}, {:integer_range, min2, max2}} -> + min1_gte_min2 = case {min1, min2} do {:neg_inf, _} -> min2 == :neg_inf; {_, :neg_inf} -> true; {m1_v,m2_v} when is_integer(m1_v) and is_integer(m2_v) -> m1_v >= m2_v; _ -> false end + max1_lte_max2 = case {max1, max2} do {:pos_inf, _} -> max2 == :pos_inf; {_, :pos_inf} -> true; {m1_v,m2_v} when is_integer(m1_v) and is_integer(m2_v) -> m1_v <= m2_v; _ -> 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) + + {{: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) -> + e1 = extract_list_mu_element(b1_body, v1) + e2 = extract_list_mu_element(b2_body, v2) + do_is_subtype_structural?(e1, e2, new_visited) + v1 == v2 -> # Canonical vars are the same, implies types were structurally identical before renaming, or one unfolds to other + subst_map1 = %{v1 => spec1} # spec1 is the mu-type itself (μv1.b1_body) + subst_map2 = %{v2 => spec2} # spec2 is the mu-type itself (μv2.b2_body) + unfolded_b1 = substitute_vars_canonical(b1_body, subst_map1) + unfolded_b2 = substitute_vars_canonical(b2_body, subst_map2) + do_is_subtype_structural?(unfolded_b1, unfolded_b2, new_visited) + + true -> # Different canonical mu-variables, not list forms + # This path is taken for Mu_B_final vs Mu_C_final if spec1/spec2 were Mu_B_final/Mu_C_final *before* normalization. + # If they were normalized, they'd be identical if equivalent. + # If is_subtype? is called with already-canonical forms Mu_B_final and Mu_C_final, + # then v1 = :m_var1, v2 = :m_var2. So this `true` branch is taken. + false + end + + {{:mu, v_s1, body_s1}, :list} -> is_list_mu_form(body_s1, v_s1) + {{:negation, n_body1}, {:negation, n_body2}} -> + do_is_subtype_structural?(n_body2, n_body1, new_visited) + _ -> 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 end - # 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 + defp substitute_vars_canonical(spec, substitutions) do + case spec do + {:type_var, name} -> Map.get(substitutions, name, spec) + {:mu, var_name, body} -> + active_substitutions = Map.delete(substitutions, var_name) + {:mu, var_name, substitute_vars_canonical(body, active_substitutions)} + {:type_lambda, param_names, body} -> + active_substitutions = Enum.reduce(param_names, substitutions, &Map.delete(&2, &1)) + {:type_lambda, param_names, substitute_vars_canonical(body, active_substitutions)} + {:negation, sub} -> {:negation, substitute_vars_canonical(sub, substitutions)} + {:tuple, elements} -> {:tuple, Enum.map(elements, &substitute_vars_canonical(&1, substitutions))} + {:cons, h, t} -> {:cons, substitute_vars_canonical(h, substitutions), substitute_vars_canonical(t, substitutions)} + {:list_of, e} -> {:list_of, substitute_vars_canonical(e, substitutions)} + {:union, members} -> {:union, Enum.map(members, &substitute_vars_canonical(&1, substitutions))} + {:intersect, members} -> {:intersect, Enum.map(members, &substitute_vars_canonical(&1, substitutions))} + {:type_apply, con, args} -> + new_con = substitute_vars_canonical(con, substitutions) + new_args = Enum.map(args, &substitute_vars_canonical(&1, substitutions)) + {:type_apply, new_con, new_args} + _atomic_or_simple_spec -> spec + end + end + + defp is_list_mu_form({:union, members}, rec_var_name) do + sorted_members = Enum.sort(members) match?([{:literal, []}, {:cons, _elem, {:type_var, ^rec_var_name}}], sorted_members) or - match?([{:cons, _elem, {:type_var, ^rec_var_name}}, {:literal, []}], sorted_members) + 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 + Enum.find_value(members, fn + {:cons, elem_spec, {:type_var, ^rec_var_name}} -> elem_spec + _ -> nil + end) || :any end - defp get_supertypes(fully_normalized_spec) do + # Public API for get_supertypes + def get_supertypes(spec), do: get_supertypes(spec, false) + + # Internal helper for get_supertypes + defp get_supertypes(spec_input, already_normalized) do + fully_normalized_spec = if already_normalized, do: spec_input, else: normalize(spec_input) + supertypes = 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 list [] or [:a] is a list + {:literal, val} when is_list(val) -> [:list] {:literal, val} when is_tuple(val) -> [: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 + {:mu, v, body} -> if is_list_mu_form(body, v), do: [:list], else: [] + {:tuple, _} -> [: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 MapSet.to_list(MapSet.new([fully_normalized_spec | supertypes])) @@ -1577,7 +1662,7 @@ defmodule Tdd.TypeReconstructor do end defmodule Tdd.Compiler do - use Tdd.Debug + # use Tdd.Debug # Keep if you use it @moduledoc "Compiles a `TypeSpec` into a canonical TDD ID." alias Tdd.TypeSpec @@ -1587,284 +1672,272 @@ defmodule Tdd.Compiler do @doc """ The main public entry point. Takes a spec and returns its TDD ID. - This now delegates to a private function with a context for recursion. """ @spec spec_to_id(TypeSpec.t()) :: non_neg_integer() def spec_to_id(spec) do - # Start with an empty context map. - spec_to_id(spec, %{}) + normalized_spec = TypeSpec.normalize(spec) + # Context maps canonical var names from :mu (e.g. :m_var0) to placeholder TDD IDs. + compile_normalized_spec(normalized_spec, %{}) end - # This is the new core compilation function with a context map. - # The context tracks `{spec => placeholder_id}` for in-progress compilations. - defp spec_to_id(spec, context) do - normalized_spec = TypeSpec.normalize(spec) + # Internal function that expects a NORMALIZED spec. + # Handles caching, :mu binding, and :type_var resolution. + defp compile_normalized_spec(normalized_spec, context) do + # Cache key uses the normalized spec. Context is implicitly handled because + # type variables within normalized_spec are already canonical. + # If normalized_spec is a :type_var, its resolution depends on context, + # so it shouldn't hit the main cache directly if context is non-empty. cache_key = {:spec_to_id, normalized_spec} - case Store.get_op_cache(cache_key) do - {:ok, id} -> - id - - :not_found -> - # Check if we are in a recursive call for a spec we're already compiling. - case Map.get(context, normalized_spec) do - placeholder_id when is_integer(placeholder_id) -> - placeholder_id - + case normalized_spec do + {:type_var, var_name} -> + case Map.get(context, var_name) do nil -> - # This is a new spec. Decide which compilation path to take. - if is_recursive_spec?(normalized_spec) do - # Use the full knot-tying logic only for recursive types. - compile_recursive_spec(normalized_spec, context) - else - # Use the simple, direct path for all other types. - compile_non_recursive_spec(normalized_spec, context) - end + raise "Tdd.Compiler: Unbound type variable during TDD compilation: #{inspect(var_name)}. Full spec: #{inspect(normalized_spec)}. Context: #{inspect(context)}" + placeholder_id when is_integer(placeholder_id) -> + placeholder_id # This is a placeholder ID for a mu-bound variable + end + + _other_form -> # Not a top-level type variable, proceed with caching/compilation + case Store.get_op_cache(cache_key) do + {:ok, id} -> + id + :not_found -> + id_to_cache = + case normalized_spec do + {:mu, var_name, body_spec} -> + # var_name is canonical, e.g., :m_var0 + # Create a placeholder for this specific var_name's recursive usage. + # The placeholder itself needs a unique ID in the TDD store. + # Using {:recursive_var_placeholder, var_name} as the *variable* for the placeholder node. + placeholder_node_variable_tag = {:mu_placeholder_for_var, var_name} + placeholder_id = Store.create_placeholder(placeholder_node_variable_tag) + + new_context = Map.put(context, var_name, placeholder_id) + + # Recursively compile the body. body_spec is already normalized. + compiled_body_id = compile_normalized_spec(body_spec, new_context) + + # Knot-tying: + # The TDD graph rooted at `compiled_body_id` contains `placeholder_id` at recursive points. + # We want a new graph where these `placeholder_id`s now point to `compiled_body_id` itself. + # The result of this substitution is the TDD for the mu-type. + # + # If `update_node_in_place` is the chosen mechanism: + # Store.update_node_in_place(placeholder_id, Store.get_node(compiled_body_id)) + # final_id = placeholder_id # The placeholder ID becomes the ID of the mu-type + # + # If `Algo.substitute` is used (as in current `compile_recursive_spec`): + # This creates a new graph where occurrences of `placeholder_id` in `compiled_body_id`'s graph + # are replaced by `compiled_body_id` itself. + # The root of the mu-type's TDD is this new graph. + final_id = Algo.substitute(compiled_body_id, placeholder_id, compiled_body_id) + + Algo.simplify(final_id) + + # Atomic types, literals, and compound types (union, intersect, etc.) + _ -> + raw_id = do_structural_compile(normalized_spec, context) # Pass context for children's compilation + Algo.simplify(raw_id) + end + Store.put_op_cache(cache_key, id_to_cache) + id_to_cache end end end - defp is_recursive_spec?({:list_of, _a}), do: true - defp is_recursive_spec?(_a), do: false - - # NEW: The logic for simple, non-recursive types. - defp compile_non_recursive_spec(spec, context) do - # Just compile the body directly. Pass context in case it contains recursive children. - raw_id = do_spec_to_id(spec, context) - final_id = Algo.simplify(raw_id) - - # Cache and return. - Store.put_op_cache({:spec_to_id, spec}, final_id) - final_id - end - - # NEW: The full knot-tying logic, now isolated. - defp compile_recursive_spec(spec, context) do - # 1. Create a placeholder and update the context. - placeholder_id = Store.create_placeholder(spec) - new_context = Map.put(context, spec, placeholder_id) - - # 2. Compile the body. It will be built with pointers to the placeholder. - body_id = do_spec_to_id(spec, new_context) - - # 3. THIS IS THE CRUCIAL FIX: - # Instead of mutating the store, we create a NEW graph where all - # internal pointers to `placeholder_id` are replaced with `body_id`. - # This makes the graph point to its own root, creating the cycle. - final_id = Algo.substitute(body_id, placeholder_id, body_id) - - # 4. Simplify the resulting (now correctly cyclic) graph. - simplified_id = Algo.simplify(final_id) - - # 5. Cache the result and return it. - Store.put_op_cache({:spec_to_id, spec}, simplified_id) - simplified_id - end - - # This helper does the raw, structural compilation. - # It now takes and passes down the context. - defp do_spec_to_id(spec, context) do - case spec do - # Pass context on all recursive calls to spec_to_id/2 - :any -> - Store.true_node_id() - - :none -> - Store.false_node_id() - - :atom -> - create_base_type_tdd(Variable.v_is_atom()) - - :integer -> - create_base_type_tdd(Variable.v_is_integer()) - - :list -> - create_base_type_tdd(Variable.v_is_list()) - - :tuple -> - create_base_type_tdd(Variable.v_is_tuple()) + # This function compiles the actual structure of a normalized spec. + # It assumes `structural_spec` is NOT a top-level :mu or :type_var (those are handled by compile_normalized_spec). + # It calls `compile_normalized_spec` for its children to ensure they are properly cached and mu/type_var handled. + defp do_structural_compile(structural_spec, context) do + case structural_spec do + :any -> Store.true_node_id() + :none -> Store.false_node_id() + :atom -> create_base_type_tdd(Variable.v_is_atom()) + :integer -> create_base_type_tdd(Variable.v_is_integer()) + :list -> create_base_type_tdd(Variable.v_is_list()) + :tuple -> create_base_type_tdd(Variable.v_is_tuple()) {:literal, val} when is_atom(val) -> compile_value_equality(:atom, Variable.v_atom_eq(val), context) - {:literal, val} when is_integer(val) -> compile_value_equality(:integer, Variable.v_int_eq(val), context) - - {:literal, []} -> + {:literal, []} -> # Empty list compile_value_equality(:list, Variable.v_list_is_empty(), context) + # Add other literal types if necessary, e.g. literal tuples {:integer_range, min, max} -> compile_integer_range(min, max, context) {:union, specs} -> - Enum.map(specs, &spec_to_id(&1, context)) + Enum.map(specs, &compile_normalized_spec(&1, context)) |> Enum.reduce(Store.false_node_id(), fn id, acc -> Algo.apply(:sum, &op_union_terminals/2, id, acc) end) {:intersect, specs} -> - Enum.map(specs, &spec_to_id(&1, context)) + Enum.map(specs, &compile_normalized_spec(&1, context)) |> Enum.reduce(Store.true_node_id(), fn id, acc -> Algo.apply(:intersect, &op_intersect_terminals/2, id, acc) end) {:negation, sub_spec} -> - Algo.negate(spec_to_id(sub_spec, context)) + Algo.negate(compile_normalized_spec(sub_spec, context)) {:cons, head_spec, tail_spec} -> - id_head = spec_to_id(head_spec, context) - id_tail = spec_to_id(tail_spec, context) - compile_cons_from_ids(id_head, id_tail, context) + id_head = compile_normalized_spec(head_spec, context) + id_tail = compile_normalized_spec(tail_spec, context) + compile_cons_from_ids(id_head, id_tail, context) # context passed for sub_problem - {:tuple, elements} -> - compile_tuple(elements, context) + {:tuple, elements_specs} -> + compile_tuple_from_elements(elements_specs, context) # Renamed for clarity - # --- REMOVE THE SPECIAL CASE --- - # The main `spec_to_id/2` logic now handles ALL recursive types. - {:list_of, _element_spec} -> - # We need to compile the logical definition: [] | cons(E, list_of(E)) - # The TypeSpec normalizer doesn't do this expansion, so we do it here. - {:ok, {:list_of, element_spec}} = {:ok, spec} - recursive_def = {:union, [{:literal, []}, {:cons, element_spec, spec}]} - # Now compile this definition. The main `spec_to_id/2` will handle the knot-tying. - spec_to_id(recursive_def, context) + # These should not be encountered here if TypeSpec.normalize worked correctly for ground types. + {:type_lambda, _, _} -> + raise "Tdd.Compiler: Cannot compile :type_lambda directly. Spec should be ground. Spec: #{inspect(structural_spec)}" + {:type_apply, _, _} -> + raise "Tdd.Compiler: Cannot compile :type_apply directly. Spec should be ground and fully beta-reduced. Spec: #{inspect(structural_spec)}" + # :mu and :type_var are handled by compile_normalized_spec directly. + # :list_of is normalized to :mu by TypeSpec.normalize. + + # Catch-all for unexpected specs at this stage _ -> - raise "Tdd.Compiler: Cannot compile unknown spec: #{inspect(spec)}" + raise "Tdd.Compiler.do_structural_compile: Unhandled structural spec form: #{inspect(structural_spec)}" end end - # --- Private Helpers --- + # --- Private Helper Functions (mostly from old do_spec_to_id) --- + # Ensure they use `compile_normalized_spec` for sub-specs and pass `context`. defp create_base_type_tdd(var), - do: - Store.find_or_create_node( - var, - Store.true_node_id(), - Store.false_node_id(), - Store.false_node_id() - ) + do: Store.find_or_create_node(var, Store.true_node_id(), Store.false_node_id(), Store.false_node_id()) defp compile_value_equality(base_type_spec, value_var, context) do eq_node = create_base_type_tdd(value_var) - base_node_id = spec_to_id(base_type_spec, context) + # base_type_spec is an atom like :atom, :integer. It needs to be compiled. + base_node_id = compile_normalized_spec(base_type_spec, context) Algo.apply(:intersect, &op_intersect_terminals/2, base_node_id, eq_node) end defp compile_integer_range(min, max, context) do - base_id = spec_to_id(:integer, context) + base_id = compile_normalized_spec(:integer, context) # Ensure :integer is compiled via main path + lt_min_tdd = if min != :neg_inf, do: create_base_type_tdd(Variable.v_int_lt(min)) - gte_min_tdd = if lt_min_tdd, do: Algo.negate(lt_min_tdd), else: spec_to_id(:any) + gte_min_tdd = if lt_min_tdd, do: Algo.negate(lt_min_tdd), else: compile_normalized_spec(:any, context) # Use :any for unbounded id_with_min = Algo.apply(:intersect, &op_intersect_terminals/2, base_id, gte_min_tdd) if max == :pos_inf do id_with_min else + # x <= max is equivalent to x < max + 1 lt_max_plus_1_tdd = create_base_type_tdd(Variable.v_int_lt(max + 1)) Algo.apply(:intersect, &op_intersect_terminals/2, id_with_min, lt_max_plus_1_tdd) end end - # Pass context defp compile_cons_from_ids(h_id, t_id, context) do - # Build `list & !is_empty` manually and safely. - id_list = create_base_type_tdd(Variable.v_is_list()) + # TDD for `is_list & !is_empty` + id_list = compile_normalized_spec(:list, context) # Ensures :list is properly compiled id_is_empty = create_base_type_tdd(Variable.v_list_is_empty()) id_not_is_empty = Algo.negate(id_is_empty) + non_empty_list_id = Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty) - non_empty_list_id = - Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty) - - # Pass context head_checker = sub_problem(&Variable.v_list_head_pred/1, h_id, context) - # Pass context tail_checker = sub_problem(&Variable.v_list_tail_pred/1, t_id, context) [non_empty_list_id, head_checker, tail_checker] - |> Enum.reduce(Store.true_node_id(), fn id, acc -> + |> Enum.reduce(compile_normalized_spec(:any, context), fn id, acc -> # Start intersection with :any Algo.apply(:intersect, &op_intersect_terminals/2, id, acc) end) end - defp compile_tuple(elements, context) do - size = length(elements) - base_id = spec_to_id(:tuple, context) + defp compile_tuple_from_elements(elements_specs, context) do + size = length(elements_specs) + base_id = compile_normalized_spec(:tuple, context) # Ensures :tuple is properly compiled size_tdd = create_base_type_tdd(Variable.v_tuple_size_eq(size)) initial_id = Algo.apply(:intersect, &op_intersect_terminals/2, base_id, size_tdd) - elements + elements_specs |> Enum.with_index() |> Enum.reduce(initial_id, fn {elem_spec, index}, acc_id -> - elem_id = spec_to_id(elem_spec) + # Compile the element's spec using the main path + elem_id = compile_normalized_spec(elem_spec, context) elem_key_constructor = &Variable.v_tuple_elem_pred(index, &1) - # Pass context elem_checker = sub_problem(elem_key_constructor, elem_id, context) Algo.apply(:intersect, &op_intersect_terminals/2, acc_id, elem_checker) end) end + # sub_problem and do_sub_problem remain largely the same, + # but ensure `spec_to_id` called within `do_sub_problem` (for placeholder case) + # is `compile_normalized_spec`. defp do_sub_problem(sub_key_constructor, tdd_id, context) do - # The `if` block is now a standard multi-clause `cond` or `case` at the top. - # Let's use a `cond` to make the guard explicit. cond do - # Guard against invalid IDs from placeholder children. - tdd_id < 0 -> + tdd_id < 0 -> # Should not happen with valid placeholder IDs Store.false_node_id() - - # If it's a valid ID, proceed with the main logic. true -> case Store.get_node(tdd_id) do - {:ok, :true_terminal} -> - Store.true_node_id() + {:ok, :true_terminal} -> Store.true_node_id() + {:ok, :false_terminal} -> Store.false_node_id() + {:ok, {{:mu_placeholder_for_var, var_name_in_placeholder}, _, _, _}} -> + # This is a placeholder node encountered during sub_problem traversal. + # This means `tdd_id` is a `placeholder_id` for some `var_name`. + # We are creating a TDD for `sub_key_constructor(var_name = placeholder_id)`. + # This path is tricky. The `sub_problem` is meant to PUSH constraints inwards. + # Example: list_of(X) -> cons(X, list_of(X)). + # When compiling `list_of(X)`, head is `X`. `sub_problem(v_list_head_pred, compile(X), ...)` + # If `X` itself is `mu Y. ...`, then `compile(X)` becomes `P_Y`. + # So `sub_problem(v_list_head_pred, P_Y, ...)` + # Inside `do_sub_problem`, `tdd_id` is `P_Y`. Its node details are `mu_placeholder_for_var, Y`. + # This indicates that the sub-problem applies to whatever `Y` resolves to. + # This branch in do_sub_problem seems to handle if the *tdd_id itself* is a placeholder. + # The original logic for `{{:placeholder, spec}, _, _, _}`: + # dummy_var = sub_key_constructor.(:dummy) + # case dummy_var do ... uses spec ... + # This `spec` was the spec of the list_of/tuple that the placeholder represented. + # Now, placeholder is for `var_name`. `spec` is not directly available here. + # This part of `do_sub_problem` might need adjustment or may become less relevant + # if placeholders are simpler. + # For now, let's assume `tdd_id` passed to sub_problem is a fully compiled TDD (or terminal). + # If `tdd_id` *is* a placeholder ID, `Store.get_node(tdd_id)` will return its placeholder structure. + # The original `compile_recursive_spec`'s `substitute` call handles the cycles. + # `sub_problem` should operate on the structure of `tdd_id` *after* it's potentially resolved. + # The `substitute` call makes the graph cyclic. `sub_problem` might then traverse this cycle. + # `Algo.simplify`'s coinductive handling should manage this. + # This specific case `{{:mu_placeholder_for_var, ...}}` means tdd_id *is* a raw placeholder, + # which shouldn't happen if `substitute` was called correctly to make it point to a real structure. + # This suggests that `sub_problem` should perhaps not be called with raw placeholder_ids. + # + # Re-thinking: `sub_problem` constructs `Var(SubTDD)`. + # `Var` is `v_list_head_pred(InnerVar)`. `SubTDD` is the TDD for the head type. + # `sub_problem` is essentially `map(tdd_id, fn node_var -> sub_key_constructor.(node_var))`. + # If `tdd_id` is `P_Y`, then we are making `sub_key_constructor(P_Y_var)`. + # This seems correct. The placeholder variable in the store is `({:mu_placeholder_for_var, var_name}, 1,0,0)`. + # So `var` below would be `{:mu_placeholder_for_var, var_name_in_placeholder}`. + raise "Tdd.Compiler.do_sub_problem: Encountered raw placeholder node details. This path needs review. Details: #{inspect(Store.get_node(tdd_id))}" - {:ok, :false_terminal} -> - Store.false_node_id() - # Handle placeholders by operating on their spec, not their TDD structure. - {:ok, {{:placeholder, spec}, _, _, _}} -> - dummy_var = sub_key_constructor.(:dummy) - - case dummy_var do - {5, :c_head, :dummy, _} -> - {:list_of, element_spec} = spec - spec_to_id(element_spec, context) - - {5, :d_tail, :dummy, _} -> - tdd_id - - {4, :b_element, index, :dummy} -> - {:tuple, elements} = spec - spec_to_id(Enum.at(elements, index), context) - - _ -> - raise "sub_problem encountered an unhandled recursive predicate on a placeholder: #{inspect(dummy_var)}" - end - - # The normal, non-placeholder case - {:ok, {var, y, n, d}} -> + {:ok, {var, y, n, d}} -> # Normal node Store.find_or_create_node( sub_key_constructor.(var), - sub_problem(sub_key_constructor, y, context), - sub_problem(sub_key_constructor, n, context), - sub_problem(sub_key_constructor, d, context) + sub_problem(sub_key_constructor, y, context), # Pass context + sub_problem(sub_key_constructor, n, context), # Pass context + sub_problem(sub_key_constructor, d, context) # Pass context ) - - # This case should now be unreachable. - {:error, :not_found} -> - raise "sub_problem received an unknown tdd_id: #{tdd_id}" + {:error, reason} -> + raise "Tdd.Compiler.do_sub_problem: Error getting node for ID #{tdd_id}: #{reason}" end end end + # Memoization wrapper for sub_problem defp sub_problem(sub_key_constructor, tdd_id, context) do - cache_key = {:sub_problem, sub_key_constructor, tdd_id} - # Note: context is not part of the cache key. This is a simplification that - # assumes the result of a sub_problem is independent of the wider compilation - # context, which is true for our use case. + # Context is not part of cache key for sub_problem, as its effect is on how tdd_id was built. + # The structure of tdd_id is what matters for sub_problem's transformation. + cache_key = {:sub_problem,Atom.to_string(elem(sub_key_constructor.(:dummy_var_for_cache_key),1)), tdd_id} case Store.get_op_cache(cache_key) do - {:ok, result_id} -> - result_id - + {:ok, result_id} -> result_id :not_found -> result_id = do_sub_problem(sub_key_constructor, tdd_id, context) Store.put_op_cache(cache_key, result_id) @@ -1872,80 +1945,8 @@ defmodule Tdd.Compiler do end end - # defp compile_list_of(element_spec) do - # norm_elem_spec = TypeSpec.normalize(element_spec) - # cache_key = {:compile_list_of, norm_elem_spec} - # case Store.get_op_cache(cache_key) do - # {:ok, id} -> id - # :not_found -> - # id = do_compile_list_of(norm_elem_spec) - # Store.put_op_cache(cache_key, id) - # id - # end - # end - # - # defp do_compile_list_of(element_spec) do - # id_elem = spec_to_id(element_spec) - # id_empty_list = spec_to_id({:literal, []}) - # step_function = fn id_x -> - # id_cons = compile_cons_from_ids(id_elem, id_x) - # Algo.apply(:sum, &op_union_terminals/2, id_empty_list, id_cons) - # end - # loop_until_stable(Store.false_node_id(), step_function) - # end - # THIS IS THE FINAL, CORRECTED LOOP - defp loop_until_stable(prev_id, step_function, iteration \\ 0) do - IO.puts("\n--- Fixed-Point Iteration: #{iteration} ---") - IO.inspect(prev_id, label: "prev_id") - # Tdd.Debug.print(prev_id) # Optional: uncomment for full graph - - raw_next_id = step_function.(prev_id) - IO.inspect(raw_next_id, label: "raw_next_id (after step_function)") - # Let's see the raw graph - Tdd.Debug.print(raw_next_id) - - # Crucially, simplify after each step for canonical comparison. - next_id = Algo.simplify(raw_next_id) - IO.inspect(next_id, label: "next_id (after simplify)") - # Let's see the simplified graph - Tdd.Debug.print(next_id) - - if next_id == prev_id do - IO.puts("--- Fixed-Point Reached! ---") - next_id - else - # Add a safety break for debugging - if iteration > 2 do - IO.inspect(Process.info(self(), :current_stacktrace)) - raise "Fixed-point iteration did not converge after 2 steps. Halting." - end - - loop_until_stable(next_id, step_function, iteration + 1) - end - end - - 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`). - neg_id2 = Algo.negate(id2) - - op_intersect = fn - :false_terminal, _ -> :false_terminal - _, :false_terminal -> :false_terminal - t, :true_terminal -> t - :true_terminal, t -> t - # Default case for non-terminal nodes, though apply handles recursion - _t1, _t2 -> :non_terminal - end - - intersect_id = Algo.apply(:intersect, op_intersect, id1, neg_id2) - final_id = Algo.simplify(intersect_id) - final_id == Store.false_node_id() - end - - # --- Private Functions for Terminal Logic --- + # --- Terminal Logic Helpers (unchanged) --- defp op_union_terminals(:true_terminal, _), do: :true_terminal defp op_union_terminals(_, :true_terminal), do: :true_terminal defp op_union_terminals(t, :false_terminal), do: t @@ -1954,6 +1955,20 @@ defmodule Tdd.Compiler do defp op_intersect_terminals(_, :false_terminal), do: :false_terminal defp op_intersect_terminals(t, :true_terminal), do: t defp op_intersect_terminals(:true_terminal, t), do: t + + # --- Public Subtyping Check (from CompilerAlgoTests) --- + @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 + id1 = spec_to_id(spec1) + id2 = spec_to_id(spec2) + # A <: B <=> A & ~B == none + neg_id2 = Algo.negate(id2) + intersect_id = Algo.apply(:intersect, &op_intersect_terminals/2, id1, neg_id2) + # Simplify is crucial for coinductive reasoning with recursive types + final_id = Algo.simplify(intersect_id) + final_id == Store.false_node_id() + end end #### @@ -3313,53 +3328,67 @@ defmodule Tdd.TypeSpecAdvancedTests do end - def run() do - IO.puts("\n--- Running Tdd.TypeSpec Advanced Normalization Tests ---") +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, :m_var0, {:type_var, :m_var0}}, {: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 + "alpha-conversion with nested μ-variable (depth-first renaming)", + {:mu, :m_var0, {:mu, :m_var1, {:union, [{:type_var, :m_var0}, {:type_var, :m_var1}]}}}, # Body union already sorted by var name {: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]}} + "alpha-conversion order matters for canonical names (1)", + # With subtype reduction deferred, both branches should survive pass1 and get canonical names. + # The final apply_subtype_reduction will sort the outer union. + # Let's assume m1_spec sorts before m2_spec if they are different after canonical renaming. + # Expected: m0 ( union(m1(m0|m1) , m2(m0|m2)) ) - sort order of m1_spec and m2_spec depends on their full structure. + # Since :m_var1 and :m_var2 are the only difference, the one with :m_var1 comes first. + {:mu, :m_var0, {:union, [ + {:mu, :m_var1, {:union, [{:type_var, :m_var0}, {:type_var, :m_var1}]}}, # Inner union sorted + {:mu, :m_var2, {:union, [{:type_var, :m_var0}, {:type_var, :m_var2}]}} # Inner union sorted + ]}}, + {:mu, :A, {:union, [ + {:mu, :B, {:union, [{:type_var, :A}, {:type_var, :B}]}}, + {:mu, :C, {:union, [{:type_var, :A}, {:type_var, :C}]}} + ]}} ) 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 + "body of μ-type is normalized (sorted union, duplicates removed by final pass)", + # apply_subtype_reduction will sort and unique the union members. + {:mu, :m_var0, {:union, [:integer, {:type_var, :m_var0}]}}, # :integer then :type_var + {:mu, :Rec, {:union, [:integer, {:type_var, :Rec}, :integer, :none]}} + ) + + test( + "list_of(integer) normalizes to a μ-expression with canonical var", + # Expected: {:literal, []} sorts before {:cons, ...} + {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :integer, {:type_var, :m_var0}}]}}, {: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, []}, + {:literal, []}, # Sorted first {:cons, - {:mu, :m_var1, # Inner mu gets next canonical name - {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var1}}]}}, + {:mu, :m_var1, + {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var1}}]} # Inner sorted + }, {:type_var, :m_var0}} - ]}}, # CORRECTED EXPECTED + ]}}, {:list_of, {:list_of, :atom}} ) @@ -3367,31 +3396,47 @@ defmodule Tdd.TypeSpecAdvancedTests do 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, [:lambda_var0], {:type_var, :lambda_var0}}, {: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 + "multiple Λ-parameters alpha-converted (sorted by canonical name)", + {:type_lambda, [:lambda_var0, :lambda_var1], {:tuple, [{:type_var, :lambda_var0}, {:type_var, :lambda_var1}]}}, {: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]}} + # :integer then :type_var + {:type_lambda, [:lambda_var0], {:union, [:integer, {:type_var, :lambda_var0}]}}, + {:type_lambda, [:T], {:union, [:integer, {:type_var, :T}, :integer, :none]}} ) test( - "nested lambda alpha-conversion", - # Outer lambda -> params get :lambda_var0 - # Inner lambda (in body of outer) -> params get :lambda_var1 + "nested lambda alpha-conversion (depth-first renaming)", {:type_lambda, [:lambda_var0], {:type_lambda, [:lambda_var1], - {:tuple, [{:type_var, :lambda_var0}, {:type_var, :lambda_var1}]}}}, # CORRECTED EXPECTED + {:tuple, [{:type_var, :lambda_var0}, {:type_var, :lambda_var1}]}}}, {:type_lambda, [:X], {:type_lambda, [:Y], {:tuple, [{:type_var, :X}, {:type_var, :Y}]}}} ) + + test( + "lambda and mu interaction for canonical names", + # Union body: {:type_var, :lambda_var0} sorts before {:type_var, :m_var0} + {:type_lambda, [:lambda_var0], + {:mu, :m_var0, {:union, [{:type_var, :lambda_var0}, {:type_var, :m_var0}]}}}, + {:type_lambda, [:T], {:mu, :X, {:union, [{:type_var, :T}, {:type_var, :X}]}}} + ) + + test( + "mu and lambda interaction for canonical names", + # Union body: {:type_var, :lambda_var0} sorts before {:type_var, :m_var0} + {:mu, :m_var0, + {:type_lambda, [:lambda_var0], {:union, [{:type_var, :lambda_var0}, {:type_var, :m_var0}]}}}, + {:mu, :X, {:type_lambda, [:T], {:union, [{:type_var, :X}, {:type_var, :T}]}}} + ) + # --- Section: Type Application Normalization (Beta-Reduction) --- IO.puts("\n--- Section: Type Application Normalization (Beta-Reduction) ---") @@ -3401,10 +3446,10 @@ defmodule Tdd.TypeSpecAdvancedTests do {: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 + # Expected: normalized form of list_of(atom) + {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var0}}]}}, {:type_apply, {:type_lambda, [:T], {:list_of, {:type_var, :T}}}, [:atom]} ) @@ -3417,20 +3462,25 @@ defmodule Tdd.TypeSpecAdvancedTests do ) 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]} + "application resulting in a mu-type that needs further normalization after substitution", + # Union: :integer then :type_var + {:mu, :m_var0, {:union, [:integer, {:type_var, :m_var0}]}}, + {:type_apply, {:type_lambda, [:T], {:mu, :X, {:union, [{:type_var, :T}, {:type_var, :X}]}}}, [:integer]} ) test_raise( - "arity mismatch in application raises error", - RuntimeError, + "arity mismatch in application raises error (too many args)", + RuntimeError, ~r/Arity mismatch/, {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer, :atom]} ) + + test_raise( + "arity mismatch in application raises error (too few args)", + RuntimeError, + ~r/Arity mismatch/, + {:type_apply, {:type_lambda, [:T, :U], {:type_var, :T}}, [:integer]} + ) test( "application of non-lambda (e.g. type_var) remains unreduced", @@ -3440,10 +3490,7 @@ defmodule Tdd.TypeSpecAdvancedTests do 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 + {:type_lambda, [:lambda_var0], {:tuple, [{:type_var, :Y_free}, {:type_var, :lambda_var0}]}}, ( y_free_spec = {:type_var, :Y_free} inner_lambda = {:type_lambda, [:Y_bound], {:tuple, [{:type_var, :X}, {:type_var, :Y_bound}]}} @@ -3451,22 +3498,45 @@ defmodule Tdd.TypeSpecAdvancedTests do {:type_apply, outer_lambda, [y_free_spec]} ) ) + + test( + "application with nested lambdas and mus, complex substitution and renaming", + # Expected: list_of(atom) normalized + {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var0}}]}}, + ( + id_lambda = {:type_lambda, [:Tparam], {:type_var, :Tparam}} + list_lambda = {:type_lambda, [:Eparam], + {:list_of, {:type_var, :Eparam}} + } + id_applied_to_atom = {:type_apply, id_lambda, [:atom]} + {:type_apply, list_lambda, [id_applied_to_atom]} + ) + ) + # --- Section: Interaction with Union/Intersection --- IO.puts("\n--- Section: Interaction with Union/Intersection ---") test( - "union members are normalized with mu and apply", + "union members are normalized with mu and apply (sorted result)", + # :atom sorts before :integer {: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 will be {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :integer, {:type_var, :m_var0}}]}} 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])}, + # :atom sorts before {:mu, ...} + {:union, [:atom, list_of_int_normalized]}, {:union, [:atom, {:list_of, :integer}]} ) + + test( + "Normalization of type_apply within intersection, then intersection simplification", + :integer, + {:intersect, [:any, {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer]}]} + ) # Final Report @@ -3480,7 +3550,238 @@ defmodule Tdd.TypeSpecAdvancedTests do length(failures) == 0 end end +defmodule Tdd.CompilerAdvancedTests do + alias Tdd.Compiler + alias Tdd.Store + alias Tdd.TypeSpec # For constructing specs + # Helper to run tests + defp test(name, expected, actual_fun_call_result) do + # For subtyping, expected is boolean. For equivalence, compare TDD IDs. + if expected == actual_fun_call_result do + IO.puts("[PASS] #{name}") + else + IO.puts("[FAIL] #{name}") + IO.puts(" Expected: #{inspect(expected)}") + IO.puts(" Got: #{inspect(actual_fun_call_result)}") + Process.put(:test_failures, [name | Process.get(:test_failures, [])]) + end + end + + defp test_subtype(name, expected_bool, spec1, spec2) do + test(name, expected_bool, Tdd.Compiler.is_subtype(spec1, spec2)) + end + + defp test_equivalent_tdd(name, spec1, spec2) do + id1 = Tdd.Compiler.spec_to_id(spec1) + id2 = Tdd.Compiler.spec_to_id(spec2) + test(name, id1, id2) # Test that their TDD IDs are the same + end + + defp test_compiles_to_none(name, spec) do + id = Tdd.Compiler.spec_to_id(spec) + test(name, Tdd.Store.false_node_id(), id) + end + + defp test_compiles_to_any(name, spec) do + id = Tdd.Compiler.spec_to_id(spec) + test(name, Tdd.Store.true_node_id(), id) + end + + defp test_raise_compile(name, expected_error_struct, expected_message_regex, input_spec) do + current_failures = Process.get(:test_failures, []) + error_caught = + try do + Tdd.Compiler.spec_to_id(input_spec) + nil # No error + rescue + e -> + if is_struct(e, expected_error_struct) or + (is_tuple(e) and elem(e,0) == expected_error_struct and expected_error_struct == RuntimeError) do # RuntimeError is {RuntimeError, %{message: "..."}} + e + else + {: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 expected_error_struct == RuntimeError)) 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.Compiler Advanced Feature Tests (μ, Λ, Apply) ---") + Process.put(:test_failures, []) + Tdd.Store.init() # Ensure store is fresh for each run module if tests are separate + + # --- Section: Basic μ-type compilation (via list_of normalization) --- + IO.puts("\n--- Section: Basic μ-type (list_of) ---") + int_list = {:list_of, :integer} + any_list = {:list_of, :any} + atom_list = {:list_of, :atom} + + test_subtype("list_of(integer) <: list_of(any)", true, int_list, any_list) + test_subtype("list_of(any) <: list_of(integer)", false, any_list, int_list) + test_subtype("list_of(integer) <: list_of(atom)", false, int_list, atom_list) + + # Test equivalence of list_of(E) and its explicit μ unfolding + # TypeSpec.normalize will convert list_of to mu. So this tests mu compilation. + list_of_int_norm = TypeSpec.normalize(int_list) # This is already {:mu, :m_var0, ...} + test_equivalent_tdd("list_of(int) TDD is equivalent to its normalized mu-form TDD", int_list, list_of_int_norm) + + test_subtype("[] <: list_of(integer)", true, {:literal, []}, int_list) + test_subtype("cons(1, []) <: list_of(integer)", true, {:cons, {:literal, 1}, {:literal, []}}, int_list) + test_subtype("cons(:a, []) <: list_of(integer)", false, {:cons, {:literal, :a}, {:literal, []}}, int_list) + test_subtype("cons(1, cons(:a, [])) <: list_of(integer)", false, {:cons, {:literal, 1}, {:cons, {:literal, :a}, {:literal, []}}}, int_list) + + + # --- Section: Explicit μ-types --- + IO.puts("\n--- Section: Explicit μ-types ---") + # Binary Tree of Atoms: Tree = μX. (Empty | Node) + # Using :empty_tree for the literal leaf for clarity. + leaf_node = {:literal, :empty_tree} + tree_spec = {:mu, :Tree, {:union, [ + leaf_node, + {:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]} + ]}} + + # Check it compiles without error first + _tree_tdd_id = Tdd.Compiler.spec_to_id(tree_spec) + test("Explicit mu-type (atom tree) compiles", true, is_integer(_tree_tdd_id)) + + # An instance of the tree + simple_tree_instance = {:tuple, [:a, leaf_node, leaf_node]} + test_subtype("Simple atom tree instance <: AtomTree", true, simple_tree_instance, tree_spec) + + non_tree_instance = {:tuple, [123, leaf_node, leaf_node]} # Integer instead of atom + test_subtype("Non-atom tree instance ; Odd = Succ + # Let's use a simpler form: Stream = μS. cons(T, S) + int_stream_spec = {:mu, :S, {:cons, :integer, {:type_var, :S}}} + _int_stream_id = Tdd.Compiler.spec_to_id(int_stream_spec) + test("μ-type for int stream compiles", true, is_integer(_int_stream_id)) + + test_subtype("cons(1, cons(2, Stream)) <: Stream", true, + {:cons, {:literal, 1}, {:cons, {:literal, 2}, int_stream_spec}}, + int_stream_spec + ) + test_subtype("cons(:a, Stream) + # This should normalize to the same spec as list_of(integer) + list_of_int_from_apply = {:type_apply, gen_list_lambda, [:integer]} + test_equivalent_tdd( + "(ΛT. list_of(T)) TDD == list_of(integer) TDD", + list_of_int_from_apply, + int_list # which is {:list_of, :integer} + ) + + # Apply to atom: GenList + list_of_atom_from_apply = {:type_apply, gen_list_lambda, [:atom]} + test_equivalent_tdd( + "(ΛT. list_of(T)) TDD == list_of(atom) TDD", + list_of_atom_from_apply, + atom_list # which is {:list_of, :atom} + ) + + # Test subtyping between instantiated types + test_subtype( + "(ΛT. list_of(T)) <: (ΛT. list_of(T))", + true, + list_of_int_from_apply, + {:type_apply, gen_list_lambda, [:any]} + ) + + # Identity function: ID = ΛT. T + id_lambda = {:type_lambda, [:T], {:type_var, :T}} + id_applied_to_atom = {:type_apply, id_lambda, [:atom]} # Normalizes to :atom + test_equivalent_tdd("(ΛT.T) TDD == :atom TDD", id_applied_to_atom, :atom) + + # --- Section: Error Handling in Compiler --- + IO.puts("\n--- Section: Error Handling in Compiler ---") + + test_raise_compile( + "Compiling a raw :type_lambda errors", + RuntimeError, ~r/Cannot compile :type_lambda directly/, + {:type_lambda, [:T], {:type_var, :T}} # This is already normalized + ) + + # TypeSpec.normalize will leave this as is if F is free. + test_raise_compile( + "Compiling an unreduced :type_apply (with free constructor var) errors", + RuntimeError, ~r/Cannot compile :type_apply directly/, + {:type_apply, {:type_var, :F}, [:integer]} + ) + + # An unbound type variable not bound by any mu + # Normalization will keep {:type_var, :Unbound} as is if it's free. + # The error should come from `compile_normalized_spec` for the `{:type_var, name}` case. + test_raise_compile( + "Compiling an unbound :type_var errors", + RuntimeError, ~r/Unbound type variable/, + {:type_var, :SomeUnboundVar} + ) + + # A :type_var that is bound by a mu, but the mu is inside a lambda that isn't applied. + # e.g. ΛT. (μX. X) -- this is fine to normalize. Compiling it is an error. + spec_lambda_mu_var = {:type_lambda, [:T], {:mu, :X, {:type_var, :X}}} + test_raise_compile( + "Compiling lambda containing mu (still a lambda) errors", + RuntimeError, ~r/Cannot compile :type_lambda directly/, + spec_lambda_mu_var + ) + + + # Final Report + failures = Process.get(:test_failures, []) + if failures == [] do + IO.puts("\n✅ All Tdd.Compiler Advanced Feature tests passed!") + else + IO.puts("\n❌ Found #{length(failures)} Tdd.Compiler Advanced Feature test failures:") + Enum.each(Enum.reverse(failures), &IO.puts(" - #{&1}")) + end + length(failures) == 0 + end +end Process.sleep(100) TypeSpecTests.run() TddStoreTests.run() @@ -3491,6 +3792,7 @@ TypeReconstructorTests.run() CompilerAlgoTests.run() # TddCompilerRecursiveTests.run() Tdd.TypeSpecAdvancedTests.run() +Tdd.CompilerAdvancedTests.run() # Tdd.Compiler.is_subtype( # {:list_of, {:literal, 1}}, # {:list_of, :integer}