From 42f53650c0fc966cb4009181b7ef436fc75aab84 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Tue, 22 Jul 2025 14:55:17 +0200 Subject: [PATCH 01/32] Refactor BDD list type handling in Module.Types.Descr - Updated the representation of non-empty lists and empty intersections/differences to use BDD structures. - Introduced new functions for BDD operations including list_get, list_get_pos, and list_all? for better handling of BDD paths. - Modified list normalization and difference functions to work with BDDs --- lib/elixir/lib/module/types/descr.ex | 385 +++++++++++++----- .../test/elixir/module/types/descr_test.exs | 8 +- 2 files changed, 276 insertions(+), 117 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 765e076467b..a508f9be4f3 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -46,7 +46,7 @@ defmodule Module.Types.Descr do @fun_top :fun_top @atom_top {:negation, :sets.new(version: 2)} @map_top [{:open, %{}, []}] - @non_empty_list_top [{:term, :term, []}] + @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot} @tuple_top [{:open, []}] @map_empty [{:closed, %{}, []}] @@ -68,8 +68,8 @@ defmodule Module.Types.Descr do @term_or_dynamic_optional Map.put(@term, :dynamic, %{optional: 1}) @not_atom_or_optional Map.delete(@term_or_optional, :atom) - @empty_intersection [0, []] - @empty_difference [0, []] + @empty_intersection [0, [], :bdd_bot] + @empty_difference [0, [], :bdd_bot] defguard is_descr(descr) when is_map(descr) or descr == :term @@ -1831,17 +1831,30 @@ defmodule Module.Types.Descr do :error -> list_new(list_type, last_type) - {dnf, last_type} -> + {bdd, last_type} -> # It is safe to discard the negations for the tail because # `list(term()) and not list(integer())` means a list # of all terms except lists where all of them are integer, # which means the head is still a term(). - {list_type, last_type} = - Enum.reduce(dnf, {list_type, last_type}, fn {head, tail, _}, {acc_head, acc_tail} -> + {list_type, _} = + list_get_pos(bdd) + |> Enum.reduce({list_type, last_type}, fn {head, tail}, {acc_head, acc_tail} -> {union(head, acc_head), union(tail, acc_tail)} end) - list_new(list_type, last_type) + # So for instance if i give term() and `term() and not (list(term())` + # what happens? + # list_type starts with term() and does not change + # last_type starts with everything but :list and [] + # then we iterate over the bdd, which contains... what? it contains + # {:term, :term} and not {:term, %{bitmap: 2}} + # what is bitmap: 2? it is empty_list() + # we only add the positive {:term, :term} to both things + # so we get {:term, :term} lol... that seems wrong, i should not add back the + # empty_list() + # maybe i should get tl on the bdd? + + list_new(list_type, Map.delete(last_type, :list)) end end @@ -1855,7 +1868,72 @@ defmodule Module.Types.Descr do end defp list_new(list_type, last_type) do - [{list_type, last_type, []}] + {{list_type, last_type}, :bdd_top, :bdd_bot} + end + + # Takes all the paths from the root to the leaves finishing with a 1, + # and compile into tuples of positive and negative nodes. Positive nodes are + # those followed by a left path, negative nodes are those followed by a right path. + defp list_get(bdd), do: list_get([], {:term, :term}, [], bdd) + + defp list_get(acc, {list_acc, tail_acc} = pos, negs, bdd) do + case bdd do + :bdd_bot -> + acc + + :bdd_top -> + [{pos, negs} | acc] + + {{list, tail} = list_type, left, right} -> + new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} + list_get(list_get(acc, new_pos, negs, left), pos, [list_type | negs], right) + end + end + + # Takes all the paths from the root to the leaves finishing with a 1, + # and compile into tuples of positive and negative nodes. Keep only the non-empty positives. + defp list_get_pos(bdd), do: list_get_pos([], {:term, :term}, [], bdd) + + defp list_get_pos(acc, {list_acc, tail_acc} = pos, negs, bdd) do + case bdd do + :bdd_bot -> + acc + + :bdd_top -> + if list_empty_line?(list_acc, tail_acc, negs) do + acc + else + [pos | acc] + end + + {{list, tail} = list_type, left, right} -> + new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} + list_get_pos(list_get_pos(acc, new_pos, negs, left), pos, [list_type | negs], right) + end + end + + # Takes all the paths from the root to the leaves finishing with a 1, computes the intersection + # of the positives, and calls the condition on the result. Checks it is true for all of them. + # As if calling Enum.all? on all the paths of the bdd. + defp list_all?(bdd, condition), do: list_all?({:term, :term}, [], bdd, condition) + + defp list_all?({list_acc, tail_acc} = pos, negs, bdd, condition) do + case bdd do + :bdd_bot -> + true + + :bdd_top -> + condition.(list_acc, tail_acc, negs) + + {{list, tail} = list_type, left, right} -> + list_all?( + {intersection(list_acc, list), intersection(tail_acc, tail)}, + negs, + left, + condition + ) and + list_all?(pos, [list_type | negs], right, condition) + end end defp list_pop_dynamic(:term), do: {false, :term} @@ -1870,86 +1948,148 @@ defmodule Module.Types.Descr do defp list_tail_unfold(:term), do: @not_non_empty_list defp list_tail_unfold(other), do: Map.delete(other, :list) - defp list_union(dnf1, dnf2), do: dnf1 ++ (dnf2 -- dnf1) + defp list_union(bdd1, bdd2) do + case {bdd1, bdd2} do + {:bdd_top, _} -> :bdd_top + {_, :bdd_top} -> :bdd_top + {:bdd_bot, bdd} -> bdd + {bdd, :bdd_bot} -> bdd + {{list, l1, r1}, {list, l2, r2}} -> {list, list_union(l1, l2), list_union(r1, r2)} + # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. + # It is the same as going down bdd1 to insert bdd1 into it. + # Possible opti: insert into the bdd with smallest height + {{list, l, r}, bdd} -> {list, list_union(l, bdd), list_union(r, bdd)} + end + end - defp list_intersection(dnf1, dnf2) do - for {list_type1, last_type1, negs1} <- dnf1, - {list_type2, last_type2, negs2} <- dnf2, - reduce: [] do - acc -> - inter = intersection(list_type1, list_type2) - last = intersection(last_type1, last_type2) - negs = negs1 ++ negs2 + defp list_intersection(bdd1, bdd2) do + case {bdd1, bdd2} do + {bdd, {{list, tail}, :bdd_top, :bdd_bot}} when is_tuple(bdd) -> + if list == :term and tail == :term do + bdd + else + list_intersection_recur(bdd1, bdd2) + end - cond do - :lists.member({inter, last}, negs) -> acc - empty?(inter) or empty?(last) -> acc - true -> [{inter, last, negs} | acc] + {{{list, tail}, :bdd_top, :bdd_bot}, bdd} when is_tuple(bdd) -> + if list == :term and tail == :term do + bdd + else + list_intersection_recur(bdd1, bdd2) end + + _ -> + list_intersection_recur(bdd1, bdd2) + end + |> case do + {_, :bdd_bot, :bdd_bot} -> :bdd_bot + bdd -> bdd end end - # Computes the difference between two DNF (Disjunctive Normal Form) list types. - # It progressively subtracts each type in dnf2 from all types in dnf1. - # The algorithm handles three cases: - # 1. Disjoint types: keeps the original type from dnf1 - # 2. Subtype relationship: - # a) If dnf2 type is a supertype, keeps only the negations - # b) If only the last type differs, subtracts it - # 3. Base case: adds dnf2 type to negations of dnf1 type - # The result may be larger than the initial dnf1, which is maintained in the accumulator. - defp list_difference(_, dnf) when dnf == @non_empty_list_top do - [] - end + defp list_intersection_recur(bdd1, bdd2) do + case {bdd1, bdd2} do + # Base cases + {_, :bdd_bot} -> + :bdd_bot - defp list_difference(dnf1, dnf2) do - Enum.reduce(dnf2, dnf1, fn {t2, last2, negs2}, acc_dnf1 -> - last2 = list_tail_unfold(last2) + {:bdd_bot, _} -> + :bdd_bot - Enum.flat_map(acc_dnf1, fn {t1, last1, negs1} -> - last1 = list_tail_unfold(last1) + {:bdd_top, bdd} -> + bdd - new_negs = - Enum.reduce(negs2, [], fn {nt, nlast}, nacc -> - t = intersection(t1, nt) - last = intersection(last1, nlast) + {bdd, :bdd_top} -> + bdd - cond do - :lists.member({t, last}, negs1) -> nacc - empty?(t) or empty?(last) -> nacc - true -> [{t, last, negs1} | nacc] - end - end) + # Optimizations + # If intersecting with a single positive or negative function, we insert + # it at the root instead of merging the trees (this avoids going down the + # whole bdd). + # Note: instead of inserting the bdd at the root, we decided to intersect with + # every atom in the bdd. If empty, then replace with the right tree. + {bdd, {list, :bdd_top, :bdd_bot}} -> + intersect_bdd_with_list(bdd, list) - i = intersection(t1, t2) - l = intersection(last1, last2) + {bdd, {list, :bdd_bottom, :bdd_top}} -> + {list, :bdd_bottom, bdd} - cond do - empty?(i) or empty?(l) -> [{t1, last1, negs1}] - subtype?(t1, t2) and subtype?(last1, last2) -> new_negs - subtype?(t1, t2) -> [{t1, difference(last1, last2), negs1} | new_negs] - true -> [{t1, last1, [{t2, last2} | negs1]} | new_negs] + {{list, :bdd_top, :bdd_bottom}, bdd} -> + intersect_bdd_with_list(bdd, list) + + {{list, :bdd_bottom, :bdd_top}, bdd} -> + {list, :bdd_bottom, bdd} + + # General cases + {{list, l1, r1}, {list, l2, r2}} -> + {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)} + + {{list, l, r}, bdd} -> + {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)} + end + end + + # We can only do this if the bdd has :bdd_bot as right child. Otherwise, if `a` is the root, + # it contains both formulas `a and left`, and `not a and right`. Thus, intersecting `not a` + # with a `{list, last}` is a wrong formula. Then, if the intersection is empty, the whole + # bdd is empty. + defp intersect_bdd_with_list(bdd, {list, last}) do + case bdd do + {{bdd_list, bdd_last}, left, :bdd_bot} -> + list = intersection(bdd_list, list) + last = intersection(bdd_last, last) + + if empty?(list) or empty?(last) do + :bdd_bot + else + {{list, last}, left, :bdd_bot} end - end) - end) + + _ -> + # Otherwise, we simply put the positive list at the root. + {{list, last}, bdd, :bdd_bot} + end + end + + # Computes the difference between two BDD (Binary Decision Diagram) list types. + # It progressively subtracts each type in bdd2 from all types in bdd1. + # The algorithm handles three cases: + # 1. Disjoint types: keeps the original type from bdd1 + # 2. Subtype relationship: + # a) If bdd2 type is a supertype, keeps only the negations + # b) If only the last type differs, subtracts it + # 3. Base case: adds bdd2 type to negations of bdd1 type + # The result may be larger than the initial bdd1, which is maintained in the accumulator. + defp list_difference(bdd1, bdd2) do + case {bdd1, bdd2} do + {:bdd_bot, _} -> :bdd_bot + {_, :bdd_top} -> :bdd_bot + {bdd, :bdd_bot} -> bdd + {:bdd_top, {lst, l, r}} -> {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)} + {{lst, l1, r1}, {lst, l2, r2}} -> {lst, list_difference(l1, l2), list_difference(r1, r2)} + {{lst, l, r}, bdd} -> {lst, list_difference(l, bdd), list_difference(r, bdd)} + end + |> case do + {_, :bdd_bot, :bdd_bot} -> :bdd_bot + bdd -> bdd + end end defp list_empty?(@non_empty_list_top), do: false + defp list_empty?(bdd), do: list_all?(bdd, &list_empty_line?/3) - defp list_empty?(dnf) do - Enum.all?(dnf, fn {list_type, last_type, negs} -> - last_type = list_tail_unfold(last_type) + defp list_empty_line?(list_type, last_type, negs) do + last_type = list_tail_unfold(last_type) - empty?(list_type) or empty?(last_type) or - Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type -> - if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do - {:halt, nil} - else - {:cont, difference(acc_last_type, neg_last)} - end - end) - |> is_nil() - end) + empty?(list_type) or empty?(last_type) or + Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type -> + if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do + {:halt, nil} + else + {:cont, difference(acc_last_type, neg_last)} + end + end) + |> is_nil() end defp non_empty_list_only?(descr), do: empty?(Map.delete(descr, :list)) @@ -1987,19 +2127,15 @@ defmodule Module.Types.Descr do defp list_hd_static(:term), do: :term - defp list_hd_static(descr) do - case descr do - %{list: [{type, _last, _negs}]} -> - type - - %{list: dnf} -> - Enum.reduce(dnf, none(), fn {type, _, _}, acc -> union(type, acc) end) - - %{} -> - none() - end + defp list_hd_static(%{list: bdd}) do + list_get_pos(bdd) + |> Enum.reduce(none(), fn {list, _}, acc -> + union(list, acc) + end) end + defp list_hd_static(%{}), do: none() + @doc """ Returns the tail of a list. @@ -2034,19 +2170,17 @@ defmodule Module.Types.Descr do defp list_tl_static(:term), do: :term - defp list_tl_static(%{list: dnf} = descr) do + defp list_tl_static(%{list: bdd} = descr) do initial = case descr do %{bitmap: bitmap} when (bitmap &&& @bit_empty_list) != 0 -> - %{list: dnf, bitmap: @bit_empty_list} + %{list: bdd, bitmap: @bit_empty_list} %{} -> - %{list: dnf} + %{list: bdd} end - Enum.reduce(dnf, initial, fn {_, last, _}, acc -> - union(last, acc) - end) + list_get_pos(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) end defp list_tl_static(%{}), do: none() @@ -2055,11 +2189,12 @@ defmodule Module.Types.Descr do defp list_improper_static?(%{bitmap: bitmap}) when (bitmap &&& @bit_empty_list) != 0, do: false defp list_improper_static?(term), do: equal?(term, @not_list) - defp list_to_quoted(dnf, empty?, opts) do - dnf = list_normalize(dnf) + defp list_to_quoted(bdd, empty?, opts) do + dnf = list_normalize(bdd) {unions, list_rendered?} = - Enum.reduce(dnf, {[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} -> + dnf + |> Enum.reduce({[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} -> {name, arguments, list_rendered?} = cond do list_type == term() and list_improper_static?(last_type) -> @@ -2109,37 +2244,61 @@ defmodule Module.Types.Descr do # Eliminate empty lists from the union, and redundant types (that are subtypes of others, # or that can be merged with others). - defp list_normalize(dnf) do - Enum.reduce(dnf, [], fn {lt, last, negs}, acc -> - if list_literal_empty?(lt, last, negs), - do: acc, - else: add_to_list_normalize(acc, lt, last, negs) + defp list_normalize(bdd) do + list_get(bdd) + |> Enum.reduce([], fn {{list, last}, negs}, acc -> + if list_empty_line?(list, last, negs) do + acc + else + # First, try to eliminate the negations from the existing type. + {list, last, negs} = + Enum.uniq(negs) + |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} -> + last = list_tail_unfold(last) + new_list = intersection(list, nlist) + new_last = intersection(last, nlast) + + cond do + # No intersection between the list and the negative + empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs} + subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs} + true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]} + end + end) + + add_to_list_normalize(acc, list, last, negs |> Enum.reverse()) + end end) end - defp list_literal_empty?(list_type, last_type, negations) do - empty?(list_type) or empty?(last_type) or - Enum.any?(negations, fn {neg_type, neg_last} -> - subtype?(list_type, neg_type) and subtype?(last_type, neg_last) - end) + # List of possible union merges: + # Case 1: when a list is a subtype of another + # Case 2: when two lists have the same list type, then the last types are united + defp add_to_list_normalize([{t, l, []} = cur | rest], list, last, []) do + cond do + subtype?(list, t) and subtype?(last, l) -> [cur | rest] + subtype?(t, list) and subtype?(l, last) -> [{list, last, []} | rest] + equal?(t, list) -> [{t, union(l, last), []} | rest] + true -> [cur | add_to_list_normalize(rest, list, last, [])] + end end - # Inserts a list type into a list of non-subtype list types. - # If the {list_type, last_type} is a subtype of an existing type, the negs - # are added to that type. - # If one list member is a subtype of {list_type, last_type}, it is replaced - # and its negations are added to the new type. - # If the type of elements are the same, the last types are merged. - defp add_to_list_normalize([{t, l, n} | rest], list, last, negs) do - cond do - subtype?(list, t) and subtype?(last, l) -> [{t, l, n ++ negs} | rest] - subtype?(t, list) and subtype?(l, last) -> [{list, last, n ++ negs} | rest] - equal?(t, list) -> [{t, union(l, last), n ++ negs} | rest] - true -> [{t, l, n} | add_to_list_normalize(rest, list, last, negs)] + # Case 3: when a list with negations is united with one of its negations + defp add_to_list_normalize([{t, l, n} = cur | rest], list, last, []) do + case pop_elem({list, last}, n) do + {true, n1} -> [{t, l, n1} | rest] + {false, _} -> [cur | add_to_list_normalize(rest, list, last, n)] end end - defp add_to_list_normalize([], list, last, negs), do: [{list, last, negs}] + defp add_to_list_normalize(rest, list, last, negs), do: [{list, last, negs} | rest] + + defp pop_elem(elem, list) do + case :lists.delete(elem, list) do + ^list -> {false, list} + new_list -> {true, new_list} + end + end ## Dynamic # diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index 74d561e5de2..17a6746c4d0 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -587,7 +587,7 @@ defmodule Module.Types.DescrTest do test "list" do # Basic list type differences assert difference(list(term()), empty_list()) == non_empty_list(term()) - assert difference(list(integer()), list(term())) == none() + assert difference(list(integer()), list(term())) |> empty?() assert difference(list(integer()), list(float())) |> equal?(non_empty_list(integer())) @@ -609,7 +609,7 @@ defmodule Module.Types.DescrTest do refute difference(list(union(atom(), binary())), list(atom())) == list(binary()) # Tests for list with last element - assert difference(list(integer(), atom()), list(number(), term())) == none() + assert difference(list(integer(), atom()), list(number(), term())) |> empty?() assert difference( list(atom(), term()), @@ -657,8 +657,8 @@ defmodule Module.Types.DescrTest do ) # Difference with proper list - assert difference(list(integer(), atom()), list(integer())) == - non_empty_list(integer(), atom()) + assert difference(list(integer(), atom()), list(integer())) + |> equal?(non_empty_list(integer(), atom())) end test "fun" do From d3fc8b2f6016155249b290a7216bc2a8a1c5c627 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 24 Jul 2025 15:02:55 +0200 Subject: [PATCH 02/32] Fix list_get_pos bug --- lib/elixir/lib/module/types/descr.ex | 77 +++++++++++++------ .../test/elixir/module/types/expr_test.exs | 24 ++++++ 2 files changed, 78 insertions(+), 23 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index a508f9be4f3..74981dcb207 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1831,14 +1831,22 @@ defmodule Module.Types.Descr do :error -> list_new(list_type, last_type) - {bdd, last_type} -> - # It is safe to discard the negations for the tail because - # `list(term()) and not list(integer())` means a list - # of all terms except lists where all of them are integer, - # which means the head is still a term(). - {list_type, _} = + {bdd, last_type_no_list} -> + # The argument last_type may include list types; in this case, we aim to add + # those to the main list type, only to keep the type of the final element (which may + # be either the empty list, or some non-list value). + # To do so, we go through the list types in last_type, but since those are stored + # as a bdd of list types, we take care to include the effect of negations on computing + # each last type. + # To see if a negation changes the last type or the list type, we just need to check + # if the negative list type is a supertype of the positive list type. In that case, + # we can remove the negative last type from the positive one. + # (If this subtracted type was empty, the whole type would be empty) + {list_type, last_type} = list_get_pos(bdd) - |> Enum.reduce({list_type, last_type}, fn {head, tail}, {acc_head, acc_tail} -> + |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail}, + {acc_head, acc_tail} -> + tail = list_tail_unfold(tail) {union(head, acc_head), union(tail, acc_tail)} end) @@ -1854,7 +1862,13 @@ defmodule Module.Types.Descr do # empty_list() # maybe i should get tl on the bdd? - list_new(list_type, Map.delete(last_type, :list)) + last_type = + case last_type do + :term -> @not_non_empty_list + other -> Map.delete(other, :list) + end + + list_new(list_type, last_type) end end @@ -1871,7 +1885,7 @@ defmodule Module.Types.Descr do {{list_type, last_type}, :bdd_top, :bdd_bot} end - # Takes all the paths from the root to the leaves finishing with a 1, + # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. defp list_get(bdd), do: list_get([], {:term, :term}, [], bdd) @@ -1890,31 +1904,48 @@ defmodule Module.Types.Descr do end end - # Takes all the paths from the root to the leaves finishing with a 1, - # and compile into tuples of positive and negative nodes. Keep only the non-empty positives. - defp list_get_pos(bdd), do: list_get_pos([], {:term, :term}, [], bdd) + # Takes all the lines from the root to the leaves finishing with a 1, + # and compile into tuples of positive and negative nodes. Keep only the non-empty positives, + # and include the impact of negations on the last type. + # To see if a negation changes the last type or the list type, we just need to check + # if the negative list type is a supertype of the positive list type. In that case, + # we can remove the negative last type from the positive one. + # (If this subtracted type was empty, the whole type would be empty) + defp list_get_pos(bdd), do: list_get_pos(:term, :term, bdd, []) - defp list_get_pos(acc, {list_acc, tail_acc} = pos, negs, bdd) do + defp list_get_pos(list_acc, last_acc, bdd, lines_acc) do case bdd do :bdd_bot -> - acc + lines_acc :bdd_top -> - if list_empty_line?(list_acc, tail_acc, negs) do - acc + [{list_acc, last_acc} | lines_acc] + + {{list, last}, left, right} -> + # Case 1: count the list_type negatively. Check condition when it affects the positive one. + lines_acc = + if subtype?(list_acc, list) do + last = difference(last_acc, last) + if empty?(last), do: lines_acc, else: list_get_pos(list_acc, last, right, lines_acc) + else + list_get_pos(list_acc, last_acc, right, lines_acc) + end + + # Case 2: count the list_type positively. + list_acc = intersection(list_acc, list) + last_acc = intersection(last_acc, last) + + if empty?(list_acc) or empty?(last_acc) do + lines_acc else - [pos | acc] + list_get_pos(list_acc, last_acc, left, lines_acc) end - - {{list, tail} = list_type, left, right} -> - new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} - list_get_pos(list_get_pos(acc, new_pos, negs, left), pos, [list_type | negs], right) end end - # Takes all the paths from the root to the leaves finishing with a 1, computes the intersection + # Takes all the lines from the root to the leaves finishing with a 1, computes the intersection # of the positives, and calls the condition on the result. Checks it is true for all of them. - # As if calling Enum.all? on all the paths of the bdd. + # As if calling Enum.all? on all the lines of the bdd. defp list_all?(bdd, condition), do: list_all?({:term, :term}, [], bdd, condition) defp list_all?({list_acc, tail_acc} = pos, negs, bdd, condition) do diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 53b4362906a..3c85a390f0a 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2031,6 +2031,30 @@ defmodule Module.Types.ExprTest do ) ) == dynamic(integer()) end + + # test "regressions – duplicate-key list pattern" do + # assert typecheck!( + # # HEAD PATTERN LIST + # [ + # # first tuple + # [ + # {key, _} + # # second tuple + rest + # | [{key, _} | _] = rest + # ] + # ], + # # BODY – we just return the tail we captured + # rest + # ) == + # dynamic( + # non_empty_list( + # # every element is {term, term} + # tuple([term(), term()]), + # # the tail can be anything + # term() + # ) + # ) + # end end describe "info" do From 09a859948d22a30c67bb6bc00f61f46b3f1c7118 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 24 Jul 2025 16:54:24 +0200 Subject: [PATCH 03/32] Add test --- .../test/elixir/module/types/expr_test.exs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 3c85a390f0a..5e1a7e7e572 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2055,6 +2055,25 @@ defmodule Module.Types.ExprTest do # ) # ) # end + + test "Oban.Telemetry pattern matching does not time-out" do + assert typecheck!(fn + [:oban, :job, _event], _measure, _meta, _opts -> :ok + # [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok + [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok + [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok + [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok + # [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok + # [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok + _event, _measure, _meta, _opts -> :ok + end) + |> equal?( + fun( + [term(), term(), term(), term()], + dynamic(atom([:ok])) + ) + ) + end end describe "info" do From 5a6519090a55c3c4e07edca1f88c59a9e5d5946a Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 24 Jul 2025 17:10:48 +0200 Subject: [PATCH 04/32] Add test --- .../test/elixir/module/types/expr_test.exs | 47 ++++++++++++------- 1 file changed, 30 insertions(+), 17 deletions(-) diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 5e1a7e7e572..4c24c59deca 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2056,23 +2056,36 @@ defmodule Module.Types.ExprTest do # ) # end - test "Oban.Telemetry pattern matching does not time-out" do - assert typecheck!(fn - [:oban, :job, _event], _measure, _meta, _opts -> :ok - # [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok - [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok - [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok - [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok - # [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok - # [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok - _event, _measure, _meta, _opts -> :ok - end) - |> equal?( - fun( - [term(), term(), term(), term()], - dynamic(atom([:ok])) - ) - ) + test "typecheck! finishes within 200 ms for Oban-style pattern match" do + timeout_ms = 200 + + task = + Task.async(fn -> + typecheck!(fn + [:oban, :job, _event], _measure, _meta, _opts -> :ok + [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok + [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok + [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok + [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok + [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok + [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok + _event, _measure, _meta, _opts -> :ok + end) + end) + + case Task.yield(task, timeout_ms) || Task.shutdown(task, :brutal_kill) do + {:ok, type} -> + assert type + |> equal?( + fun( + [term(), term(), term(), term()], + dynamic(atom([:ok])) + ) + ) + + nil -> + flunk("typecheck! did not finish within #{timeout_ms} ms") + end end end From b03ed2336477f0311e8791f0ed7da0df9945771b Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Tue, 29 Jul 2025 19:20:43 +0200 Subject: [PATCH 05/32] Functioning map BDDs --- lib/elixir/lib/module/types/descr.ex | 943 ++++++++++++++---- .../test/elixir/module/types/descr_test.exs | 56 +- 2 files changed, 780 insertions(+), 219 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 74981dcb207..ce9bb8ce1f0 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -26,6 +26,9 @@ defmodule Module.Types.Descr do @bit_top (1 <<< 7) - 1 @bit_number @bit_integer ||| @bit_float + defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot]} + defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot]} + defmacrop domain_key(key), do: {:domain_key, key} @domain_key_types [ @@ -45,10 +48,10 @@ defmodule Module.Types.Descr do @fun_top :fun_top @atom_top {:negation, :sets.new(version: 2)} - @map_top [{:open, %{}, []}] + @map_top {{:open, %{}}, :bdd_top, :bdd_bot} @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot} @tuple_top [{:open, []}] - @map_empty [{:closed, %{}, []}] + @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot} @none %{} @term %{ @@ -544,6 +547,52 @@ defmodule Module.Types.Descr do (bitmap, atom) are checked first for speed since, if they are present, the type is non-empty as we normalize then during construction. """ + + # defguardp is_descr(d) + # when d == :term or + # (is_map(d) and + # (Map.has_key?(d, :atom) or Map.has_key?(d, :bitmap) or + # Map.has_key?(d, :list) or Map.has_key?(d, :map) or + # Map.has_key?(d, :tuple) or Map.has_key?(d, :fun))) + + # defp bdd_size({{tag, fields = %{}}, l, r}) when tag in [:open, :closed] do + # bdd_size(l) + bdd_size(r) + 1 + Enum.reduce(fields, 0, fn d, acc -> descr_size(d) + acc end) + # end + + # defp bdd_size({{list = %{}, last = %{}}, l, r}) do + # bdd_size(l) + bdd_size(r) + 1 + descr_or_domain_size(list) + descr_or_fields_size(last) + # end + + defp bdd_size({lit, l, r}), do: bdd_size(l) + bdd_size(r) + 1 + + defp bdd_size(bdd), do: 0 + + defp dnf_structural_size(dnf) do + Enum.reduce(dnf, 0, fn {_tag, pos}, acc -> + 1 + acc + length(pos) + end) + end + + defp dnf_size(dnf) do + Enum.reduce(dnf, 0, fn {_tag, pos}, acc -> + 1 + acc + Enum.reduce(pos, 0, fn d, acc -> descr_size(d) + acc end) + end) + end + + def descr_size(:term), do: 1 + + def descr_size(%{} = descr) do + Enum.reduce(Map.to_list(descr), 0, fn {key, value}, acc -> + acc + descr_size(key, value) + end) + end + + def descr_size(:tuple, dnf), do: dnf_size(dnf) + def descr_size(:fun, bdd), do: bdd_size(bdd) + def descr_size(:map, bdd), do: bdd_size(bdd) + def descr_size(:list, bdd), do: bdd_size(bdd) + def descr_size(_, _), do: 1 + def empty?(:term), do: false def empty?(%{} = descr) do @@ -555,6 +604,46 @@ defmodule Module.Types.Descr do true descr -> + # IO.puts("Woooh") + d = descr_size(descr) + + if d > 100 do + IO.puts("descr_size(descr): #{d}") + IO.puts("The decomposition is:") + + if Map.has_key?(descr, :atom), + do: IO.puts("Atom size: #{descr_size(:atom, descr.atom)}") + + if Map.has_key?(descr, :list) do + IO.puts("List size: #{descr_size(:list, descr.list)}") + else + IO.puts("List size: 0") + end + + if Map.has_key?(descr, :map) do + IO.puts("Map size: #{descr_size(:map, descr.map)}") + else + IO.puts("Map size: 0") + end + + if Map.has_key?(descr, :tuple) do + IO.puts("Tuple size: #{descr_size(:tuple, descr.tuple)}") + IO.puts("Tuple structural size: #{dnf_structural_size(descr.tuple)}") + else + IO.puts("Tuple size: 0") + end + + if Map.has_key?(descr, :fun) do + IO.puts("Fun size: #{descr_size(:fun, descr.fun)}") + else + IO.puts("Fun size: 0") + end + + # dbg(descr) + end + + # dbg(descr, limit: :infinity, printable_limit: :infinity, width: :infinity) + not Map.has_key?(descr, :atom) and not Map.has_key?(descr, :bitmap) and not Map.has_key?(descr, :optional) and @@ -1979,38 +2068,54 @@ defmodule Module.Types.Descr do defp list_tail_unfold(:term), do: @not_non_empty_list defp list_tail_unfold(other), do: Map.delete(other, :list) - defp list_union(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_top, _} -> :bdd_top - {_, :bdd_top} -> :bdd_top - {:bdd_bot, bdd} -> bdd - {bdd, :bdd_bot} -> bdd - {{list, l1, r1}, {list, l2, r2}} -> {list, list_union(l1, l2), list_union(r1, r2)} - # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. - # It is the same as going down bdd1 to insert bdd1 into it. - # Possible opti: insert into the bdd with smallest height - {{list, l, r}, bdd} -> {list, list_union(l, bdd), list_union(r, bdd)} + # Attempt a merge, if the union is between two single lists. + defp list_union(list_literal(list1, last1), list_literal(list2, last2)) do + cond do + subtype?(list1, list2) and subtype?(last1, last2) -> list_literal(list2, last2) + subtype?(list2, list1) and subtype?(last2, last1) -> list_literal(list1, last1) + equal?(list1, list2) -> list_literal(list1, union(last1, last2)) + true -> list_union_recur(list_literal(list1, last1), list_literal(list2, last2)) end end - defp list_intersection(bdd1, bdd2) do + defp list_union(bdd1, bdd2), do: list_union_recur(bdd1, bdd2) + + defp list_union_recur(bdd1, bdd2) do case {bdd1, bdd2} do - {bdd, {{list, tail}, :bdd_top, :bdd_bot}} when is_tuple(bdd) -> - if list == :term and tail == :term do - bdd - else - list_intersection_recur(bdd1, bdd2) - end + {:bdd_top, _} -> + :bdd_top - {{{list, tail}, :bdd_top, :bdd_bot}, bdd} when is_tuple(bdd) -> - if list == :term and tail == :term do - bdd - else - list_intersection_recur(bdd1, bdd2) - end + {_, :bdd_top} -> + :bdd_top - _ -> - list_intersection_recur(bdd1, bdd2) + {:bdd_bot, bdd} -> + bdd + + {bdd, :bdd_bot} -> + bdd + + {{list, l1, r1}, {list, l2, r2}} -> + {list, list_union(l1, l2), list_union(r1, r2)} + + {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 -> + {list1, list_union(l1, bdd2), list_union(r1, bdd2)} + + {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 -> + {list2, list_union(bdd1, l2), list_union(bdd1, r2)} + end + end + + defp is_list_top?({{list, tail}, :bdd_top, :bdd_bot}) do + list == :term and tail == :term + end + + defp is_list_top?(_), do: false + + defp list_intersection(bdd1, bdd2) do + cond do + is_list_top?(bdd1) and is_tuple(bdd2) -> bdd2 + is_list_top?(bdd2) and is_tuple(bdd1) -> bdd1 + true -> list_intersection_recur(bdd1, bdd2) end |> case do {_, :bdd_bot, :bdd_bot} -> :bdd_bot @@ -2039,24 +2144,38 @@ defmodule Module.Types.Descr do # whole bdd). # Note: instead of inserting the bdd at the root, we decided to intersect with # every atom in the bdd. If empty, then replace with the right tree. - {bdd, {list, :bdd_top, :bdd_bot}} -> - intersect_bdd_with_list(bdd, list) + # {bdd, {list, :bdd_top, :bdd_bot}} -> + # intersect_bdd_with_list(bdd, list) - {bdd, {list, :bdd_bottom, :bdd_top}} -> - {list, :bdd_bottom, bdd} + # {bdd, {list, :bdd_bottom, :bdd_top}} -> + # {list, :bdd_bottom, bdd} - {{list, :bdd_top, :bdd_bottom}, bdd} -> - intersect_bdd_with_list(bdd, list) + # {{list, :bdd_top, :bdd_bottom}, bdd} -> + # intersect_bdd_with_list(bdd, list) - {{list, :bdd_bottom, :bdd_top}, bdd} -> - {list, :bdd_bottom, bdd} + # {{list, :bdd_bottom, :bdd_top}, bdd} -> + # {list, :bdd_bottom, bdd} + {list_literal(list1, last1), list_literal(list2, last2)} -> + try do + list1 = non_empty_intersection!(list1, list2) + last1 = non_empty_intersection!(last1, last2) + list_literal(list1, last1) + catch + :empty -> :bdd_bot + end # General cases {{list, l1, r1}, {list, l2, r2}} -> {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)} - {{list, l, r}, bdd} -> - {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)} + {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 -> + {list1, list_intersection_recur(l1, bdd2), list_intersection_recur(r1, bdd2)} + + {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 -> + {list2, list_intersection_recur(bdd1, l2), list_intersection_recur(bdd1, r2)} + + # {{list, l, r}, bdd} -> + # {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)} end end @@ -2093,12 +2212,29 @@ defmodule Module.Types.Descr do # The result may be larger than the initial bdd1, which is maintained in the accumulator. defp list_difference(bdd1, bdd2) do case {bdd1, bdd2} do - {:bdd_bot, _} -> :bdd_bot - {_, :bdd_top} -> :bdd_bot - {bdd, :bdd_bot} -> bdd - {:bdd_top, {lst, l, r}} -> {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)} - {{lst, l1, r1}, {lst, l2, r2}} -> {lst, list_difference(l1, l2), list_difference(r1, r2)} - {{lst, l, r}, bdd} -> {lst, list_difference(l, bdd), list_difference(r, bdd)} + {:bdd_bot, _} -> + :bdd_bot + + {_, :bdd_top} -> + :bdd_bot + + {bdd, :bdd_bot} -> + bdd + + {:bdd_top, {lst, l, r}} -> + {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)} + + {{lst, l1, r1}, {lst, l2, r2}} -> + {lst, list_difference(l1, l2), list_difference(r1, r2)} + + {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 < lst2 -> + {lst1, list_difference(l1, bdd2), list_difference(r1, bdd2)} + + {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 > lst2 -> + {lst2, list_difference(bdd1, l2), list_difference(bdd1, r2)} + + # {{lst, l, r}, bdd} -> + # {lst, list_difference(l, bdd), list_difference(r, bdd)} end |> case do {_, :bdd_bot, :bdd_bot} -> :bdd_bot @@ -2449,6 +2585,239 @@ defmodule Module.Types.Descr do # and other keys bound to any type. It will be represented using a map domain that maps # atom to `if_set(integer())`, and every other domain key to `term_or_optional()`. + # ## TESTING + # def map_merge(%{map: bdd1} = d1, %{map: bdd2} = d2) do + # # Starting accumulator: the empty map type + # res = %{map: :bdd_bot} + + # # Recursive auxiliary function + # aux = fn aux, accu, bdd1, bdd2 -> + # case {map_first_label(bdd1), map_first_label(bdd2)} do + # {:dummy, :dummy} -> + # {some1, none1} = map_empty_cases(bdd1) + # {some2, none2} = map_empty_cases(bdd2) + + # some = some1 or some2 + # none = none1 and none2 + + # # Approximation if some and not none + # if some do + # fields = :maps.from_list(accu) + # map_union(res, %{map: map_new(:open, fields)}) + # else + # res + # end + + # {l1, l2} -> + # l = min_label(l1, l2) + + # # Split along label l + # split1 = map_split(bdd1, l) + # split2 = map_split(bdd2, l) + + # Enum.reduce(split1, res, fn {t1, d1_next}, acc -> + # Enum.reduce(split2, acc, fn {t2, d2_next}, acc2 -> + # t = + # if Map.has_key?(t2, :optional) and t2.optional do + # union(t1, remove_optional(t2)) + # else + # t2 + # end + + # aux.(aux, [{l, t} | accu], d1_next.map, d2_next.map) + # end) + # end) + # end + # end + + # aux.(aux, [], bdd1, bdd2) + # end + + # defp map_first_label(:bdd_top), do: :dummy + # defp map_first_label(:bdd_bot), do: :dummy + + # defp map_first_label({{tag, fields}, :bdd_top, :bdd_bot}) do + # case :maps.next(:maps.iterator(fields)) do + # :none -> :dummy + # {key, _value, _iter} -> key + # end + # end + + # defp map_first_label({{_tag, _fields}, l, _r}), do: map_first_label(l) + + # # Returns {some, none} + # defp map_empty_cases(bdd) do + # map_bdd_get(bdd) + # |> Enum.reduce({false, true}, fn + # {:open, fields, _negs}, {some, none} -> + # some = some or map_size(fields) > 0 + # none = none and map_size(fields) == 0 + # {some, none} + + # {:closed, fields, _negs}, {some, none} -> + # some = some or map_size(fields) > 0 + # none = none and map_size(fields) == 0 + # {some, none} + # end) + # end + + # # Split a BDD into a list of {type_for_label, rest_of_map} + # defp map_split(bdd, label) do + # map_bdd_get(bdd) + # |> Enum.map(fn {tag, fields, negs} -> + # case :maps.take(label, fields) do + # {value, fields_rest} -> + # {remove_optional(value), %{map: map_new(tag, fields_rest)}} + + # :error -> + # # If absent + # type_for_label = + # case tag do + # :open -> term_or_optional() + # :closed -> not_set() + # domains = %{} -> Map.get(domains, domain_key(:atom), not_set()) + # end + + # {type_for_label, %{map: map_new(tag, fields)}} + # end + # end) + # end + + # defp min_label(:dummy, :dummy), do: :dummy + # defp min_label(:dummy, l), do: l + # defp min_label(l, :dummy), do: l + # defp min_label(l1, l2), do: if(l1 <= l2, do: l1, else: l2) + + @doc """ + Type-level merge for maps (like `Map.merge/2`). + + Semantics per OCaml code: + - For each key `l`, if the right map's type for `l` **may be absent**, + the merged type for `l` is `left(l) ∪ present(right(l))`; + otherwise it is `right(l)` (right-biased override). + - Domains are merged with the same rule (component-wise). + - If either side is `:open`, the result is effectively open (via domains). + + Returns `{:ok, merged_descr}` or `:badmap` if either input is not a (possibly dynamic) map type. + """ + def map_merge(:term, _), do: :badmap + def map_merge(_, :term), do: :badmap + + def map_merge(%{} = descr1, %{} = descr2) do + case {:maps.take(:dynamic, descr1), :maps.take(:dynamic, descr2)} do + {:error, :error} -> + with {:ok, m} <- map_merge_static(descr1, descr2) do + {:ok, m} + else + :badmap -> :badmap + end + + {{dyn1, stat1}, :error} -> + with {:ok, stat_stat} <- map_merge_static(stat1, descr2), + {:ok, dyn_stat} <- map_merge_static(dynamic(dyn1), descr2) do + {:ok, union(stat_stat, dynamic(dyn_stat))} + else + :badmap -> :badmap + end + + {:error, {dyn2, stat2}} -> + with {:ok, stat_stat} <- map_merge_static(descr1, stat2), + {:ok, stat_dyn} <- map_merge_static(descr1, dynamic(dyn2)) do + {:ok, union(stat_stat, dynamic(stat_dyn))} + else + :badmap -> :badmap + end + + {{dyn1, stat1}, {dyn2, stat2}} -> + with {:ok, ss} <- map_merge_static(stat1, stat2), + {:ok, sd} <- map_merge_static(stat1, dynamic(dyn2)), + {:ok, ds} <- map_merge_static(dynamic(dyn1), stat2), + {:ok, dd} <- map_merge_static(dynamic(dyn1), dynamic(dyn2)) do + {:ok, union(ss, union(dynamic(sd), union(dynamic(ds), dynamic(dd))))} + else + :badmap -> :badmap + end + end + end + + # --- Core static merger on the BDDs --------------------------------------- + + defp map_merge_static(%{map: bdd1} = d1, %{map: bdd2} = d2) do + # both inputs must be exclusively map (no extra components) + if map_only?(d1) and map_only?(d2) do + # Build the result by taking the cross-product of positive literals + # (DNF lines) and unioning merged literals. + merged_bdd = + map_bdd_get(bdd1) + |> Enum.reduce(:bdd_bot, fn {tag1, fields1, _negs1}, acc1 -> + Enum.reduce(map_bdd_get(bdd2), acc1, fn {tag2, fields2, _negs2}, acc2 -> + {new_tag_or_domains, new_fields} = + map_literal_merge(tag1, fields1, tag2, fields2) + + map_union(acc2, {{new_tag_or_domains, new_fields}, :bdd_top, :bdd_bot}) + end) + end) + + {:ok, %{map: merged_bdd}} + else + :badmap + end + end + + defp map_merge_static(_, _), do: :badmap + + # --- Literal / domain merge (right-biased with "optional means fallback") -- + + # Merge two map literals (tag-or-domains + fields) into one literal. + defp map_literal_merge(tag_or_domains1, fields1, tag_or_domains2, fields2) do + default1 = map_key_tag_to_type(tag_or_domains1) + default2 = map_key_tag_to_type(tag_or_domains2) + + # Merge domains first (handles openness and all non-atom key domains) + new_tag_or_domains = map_domain_merge(tag_or_domains1, tag_or_domains2) + + # For explicit atom keys: symmetrical merge with defaults for missing keys + new_fields = + symmetrical_merge(fields1, default1, fields2, default2, fn _key, v1, v2 -> + map_merge_value(v1, v2) + end) + + {new_tag_or_domains, new_fields} + end + + # Component-wise merge of domains. For every domain key dk in @domain_key_types: + # result(dk) = merge_value( domain1(dk), domain2(dk) ). + # If all resulting domain entries are empty/optional, collapse to :closed. + defp map_domain_merge(tag_or_domains1, tag_or_domains2) do + new_domains = + for domain_key(_) = dk <- @domain_key_types, reduce: %{} do + acc -> + v1 = map_domain_default(tag_or_domains1, dk) + v2 = map_domain_default(tag_or_domains2, dk) + v = map_merge_value(v1, v2) + + if empty_or_optional?(v) do + acc + else + Map.put(acc, dk, v) + end + end + + if map_size(new_domains) == 0, do: :closed, else: new_domains + end + + # Default value for a domain when not explicitly present in the literal. + defp map_domain_default(:open, _dk), do: term_or_optional() + defp map_domain_default(:closed, _dk), do: not_set() + defp map_domain_default(domains = %{}, dk), do: Map.get(domains, dk, not_set()) + + # Merge the two value types for a key, per OCaml's rule: + # if right may be absent, use left ∪ present(right), else right. + defp map_merge_value(left, right) do + {optional?, right_present} = pop_optional_static(right) + if optional?, do: union(left, right_present), else: right + end + defp map_descr(tag, pairs, default, force?) do {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false) @@ -2513,25 +2882,73 @@ defmodule Module.Types.Descr do defguardp is_optional_static(map) when is_map(map) and is_map_key(map, :optional) - defp map_new(tag, fields = %{}), do: [{tag, fields, []}] + defp map_new(tag, fields = %{}), do: {{tag, fields}, :bdd_top, :bdd_bot} defp map_only?(descr), do: empty?(Map.delete(descr, :map)) - defp map_union(dnf1, dnf2) do - # Union is just concatenation, but we rely on some optimization strategies to - # avoid the list to grow when possible + defp map_union(bdd1, bdd2) do + case {bdd1, bdd2} do + {:bdd_top, _} -> + :bdd_top - # first pass trying to identify patterns where two maps can be fused as one - with [map1] <- dnf1, - [map2] <- dnf2, - optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do - [optimized] - else - # otherwise we just concatenate and remove structural duplicates - _ -> dnf1 ++ (dnf2 -- dnf1) + {_, :bdd_top} -> + :bdd_top + + {:bdd_bot, bdd} -> + bdd + + {bdd, :bdd_bot} -> + bdd + + {map_literal(tag1, fields1), map_literal(tag2, fields2)} -> + case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do + {tag, fields, []} -> + {{tag, fields}, :bdd_top, :bdd_bot} + + nil -> + lit1 = {tag1, fields1} + lit2 = {tag2, fields2} + + cond do + lit1 == lit2 -> {lit1, :bdd_top, :bdd_bot} + lit1 < lit2 -> {lit1, :bdd_top, {lit2, :bdd_top, :bdd_bot}} + lit1 > lit2 -> {lit2, :bdd_top, {lit1, :bdd_top, :bdd_bot}} + end + end + + {{map, l1, r1}, {map, l2, r2}} -> + {map, map_union(l1, l2), map_union(r1, r2)} + + # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. + # It is the same as going down bdd1 to insert bdd1 into it. + # Possible opti: insert into the bdd with smallest height + {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 -> + {map1, map_union(l1, bdd2), map_union(r1, bdd2)} + + {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 -> + {map2, map_union(bdd1, l2), map_union(bdd1, r2)} + + # {{map, l, r}, bdd} -> + # {map, map_union(l, bdd), map_union(r, bdd)} end end + # defp map_union(dnf1, dnf2) do + # # Union is just concatenation, but we rely on some optimization strategies to + # # avoid the list to grow when possible + + # # first pass trying to identify patterns where two maps can be fused as one + # with [map1] <- dnf1, + # [map2] <- dnf2, + # optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do + # [optimized] + # else + # # otherwise we just concatenate and remove structural duplicates + # _ -> dnf1 ++ (dnf2 -- dnf1) + # end + # end + # defp maybe_optimize_map_union(map, map), do: map + defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do :all_equal -> @@ -2555,7 +2972,8 @@ defmodule Module.Types.Descr do end end - defp maybe_optimize_map_union(_, _), do: nil + defp maybe_optimize_map_union(map1, map2), + do: raise("I should not be there: see inputs #{inspect(map1)} and #{inspect(map2)}") defp map_union_optimization_strategy(tag1, pos1, tag2, pos2) defp map_union_optimization_strategy(tag, pos, tag, pos), do: :all_equal @@ -2627,21 +3045,111 @@ defmodule Module.Types.Descr do if subtype?(v2, v1), do: :right_subtype_of_left end - # Given two unions of maps, intersects each pair of maps. - defp map_intersection(dnf1, dnf2) do - for {tag1, pos1, negs1} <- dnf1, - {tag2, pos2, negs2} <- dnf2, - reduce: [] do - acc -> + defp is_map_top?({{tag, fields}, :bdd_top, :bdd_bot}) do + tag == :open and map_size(fields) == 0 + end + + defp is_map_top?(_), do: false + + defp map_intersection(bdd1, bdd2) do + # If intersecting with the top map type, no-op + cond do + is_map_top?(bdd1) and is_tuple(bdd2) -> bdd2 + is_map_top?(bdd2) and is_tuple(bdd1) -> bdd1 + true -> map_intersection_recur(bdd1, bdd2) + end + end + + defp map_intersection_recur(bdd1, bdd2) do + case {bdd1, bdd2} do + # Base cases + {_, :bdd_bot} -> + :bdd_bot + + {:bdd_bot, _} -> + :bdd_bot + + {:bdd_top, bdd} -> + bdd + + {bdd, :bdd_top} -> + bdd + + {map_literal(tag1, fields1), map_literal(tag2, fields2)} -> try do - {tag, fields} = map_literal_intersection(tag1, pos1, tag2, pos2) - prepend_to_map_dnf(tag, fields, negs1 ++ (negs2 -- negs1), acc) + map = map_literal_intersection(tag1, fields1, tag2, fields2) + {map, :bdd_top, :bdd_bot} catch - :empty -> acc + :empty -> :bdd_bot end + + # Optimizations + # If intersecting with a single positive or negative function, we insert + # it at the root instead of merging the trees (this avoids going down the + # whole bdd). + # No: bc we want to have increasing order of literals. + # {bdd, {map, :bdd_top, :bdd_bot}} -> + # {map, bdd, :bdd_bot} + + # {bdd, {map, :bdd_bot, :bdd_top}} -> + # {map, :bdd_bot, bdd} + + # {{map, :bdd_top, :bdd_bot}, bdd} -> + # {map, bdd, :bdd_bot} + + # {{map, :bdd_bot, :bdd_top}, bdd} -> + # {map, :bdd_bot, bdd} + + # General cases + {{map, l1, r1}, {map, l2, r2}} -> + {map, map_intersection_recur(l1, l2), map_intersection_recur(r1, r2)} + + {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 -> + {map1, map_intersection_recur(l1, bdd2), map_intersection_recur(r1, bdd2)} + + {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 -> + {map2, map_intersection_recur(bdd1, l2), map_intersection_recur(bdd1, r2)} + + # {{map, l, r}, bdd} -> + # {map, map_intersection_recur(l, bdd), map_intersection_recur(r, bdd)} end end + defp map_difference(bdd1, bdd2) do + case {bdd1, bdd2} do + {:bdd_bot, _} -> + :bdd_bot + + {_, :bdd_top} -> + :bdd_bot + + {bdd, :bdd_bot} -> + bdd + + {:bdd_top, {map, l, r}} -> + {map, map_difference(:bdd_top, l), map_difference(:bdd_top, r)} + + {{map, l1, r1}, {map, l2, r2}} -> + {map, map_difference(l1, l2), map_difference(r1, r2)} + + {{map1, l1, r1}, {map2, _l2, _r2}} when map1 < map2 -> + {map1, map_difference(l1, bdd2), map_difference(r1, bdd2)} + + {{map1, _l1, _r1}, {map2, l2, r2}} when map1 > map2 -> + {map2, map_difference(bdd1, l2), map_difference(bdd1, r2)} + + # {{map, l, r}, bdd} -> {map, map_difference(l, bdd), map_difference(r, bdd)} + end + end + + # defp map_negation(bdd) do + # case bdd do + # :bdd_bot -> :bdd_top + # :bdd_top -> :bdd_bot + # {map, l, r} -> {map, map_negation(l), map_negation(r)} + # end + # end + # Intersects two map literals; throws if their intersection is empty. # Both open: the result is open. defp map_literal_intersection(:open, map1, :open, map2) do @@ -2750,61 +3258,90 @@ defmodule Module.Types.Descr do if empty?(type), do: throw(:empty), else: type end - defp map_difference(_, dnf) when dnf == @map_top, do: [] - defp map_difference(dnf, dnf), do: [] - - defp map_difference(dnf1, dnf2) do - Enum.reduce(dnf2, dnf1, fn - {:open, fields2, []}, current_dnf when map_size(fields2) == 1 -> - # Optimization: we are removing an open map with one field. - Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> - {key, value, _rest} = :maps.next(:maps.iterator(fields2)) - t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value) + # defp map_difference(_, dnf) when dnf == @map_top, do: [] + # defp map_difference(dnf, dnf), do: [] + + # defp map_difference(dnf1, dnf2) do + # Enum.reduce(dnf2, dnf1, fn + # {:open, fields2, []}, current_dnf when map_size(fields2) == 1 -> + # # Optimization: we are removing an open map with one field. + # Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> + # {key, value, _rest} = :maps.next(:maps.iterator(fields2)) + # t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value) + + # if empty?(t_diff) do + # acc + # else + # {tag, pos} = {tag1, Map.put(fields1, key, t_diff)} + # entry = {tag, pos, negs1} + + # cond do + # :lists.member({tag, pos}, negs1) -> acc + # :lists.member(entry, acc) -> acc + # true -> [entry | acc] + # end + # end + # end) + + # {tag2, fields2, negs2}, current_dnf -> + # Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> + # negs = + # if :lists.member({tag2, fields2}, negs1) do + # negs1 + # else + # [{tag2, fields2} | negs1] + # end + + # acc = prepend_to_map_dnf(tag1, fields1, negs, acc) + + # Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc -> + # try do + # {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2) + # prepend_to_map_dnf(tag, fields, negs1, acc) + # catch + # :empty -> acc + # end + # end) + # end) + # end) + # end + + # defp prepend_to_map_dnf(tag, fields, negs, acc) do + # entry = {tag, fields, negs} + + # cond do + # :lists.member({tag, fields}, negs) -> acc + # :lists.member(entry, acc) -> acc + # true -> [entry | acc] + # end + # end - if empty?(t_diff) do - acc - else - {tag, pos} = {tag1, Map.put(fields1, key, t_diff)} - entry = {tag, pos, negs1} - - cond do - :lists.member({tag, pos}, negs1) -> acc - :lists.member(entry, acc) -> acc - true -> [entry | acc] - end - end - end) - - {tag2, fields2, negs2}, current_dnf -> - Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> - negs = - if :lists.member({tag2, fields2}, negs1) do - negs1 - else - [{tag2, fields2} | negs1] - end + # Takes all the lines from the root to the leaves finishing with a 1, + # and compile into tuples of positive and negative nodes. Positive nodes are + # those followed by a left path, negative nodes are those followed by a right path. + def map_bdd_get(bdd) do + # dbg(bdd) + map_bdd_get([], {:open, %{}}, [], bdd) + end - acc = prepend_to_map_dnf(tag1, fields1, negs, acc) + defp map_bdd_get(acc, {tag, fields} = map, negs, bdd) do + case bdd do + :bdd_bot -> + acc - Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc -> - try do - {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2) - prepend_to_map_dnf(tag, fields, negs1, acc) - catch - :empty -> acc - end - end) - end) - end) - end + :bdd_top -> + if map_empty?(tag, fields, negs), do: acc, else: [{tag, fields, negs} | acc] - defp prepend_to_map_dnf(tag, fields, negs, acc) do - entry = {tag, fields, negs} + {{next_tag, next_fields} = next_map, left, right} -> + acc = + try do + new_pos = map_literal_intersection(tag, fields, next_tag, next_fields) + map_bdd_get(acc, new_pos, negs, left) + catch + :empty -> acc + end - cond do - :lists.member({tag, fields}, negs) -> acc - :lists.member(entry, acc) -> acc - true -> [entry | acc] + map_bdd_get(acc, map, [next_map | negs], right) end end @@ -2851,15 +3388,15 @@ defmodule Module.Types.Descr do # Optimization: if the key does not exist in the map, avoid building # if_set/not_set pairs and return the popped value directly. - defp map_fetch_static(%{map: [{tag_or_domains, fields, []}]}, key) + defp map_fetch_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key) when not is_map_key(fields, key) do map_key_tag_to_type(tag_or_domains) |> pop_optional_static() end # Takes a map dnf and returns the union of types it can take for a given key. # If the key may be undefined, it will contain the `not_set()` type. - defp map_fetch_static(%{map: dnf}, key) do - dnf + defp map_fetch_static(%{map: bdd}, key) do + map_bdd_get(bdd) |> Enum.reduce(none(), fn # Optimization: if there are no negatives and key exists, return its value {_tag, %{^key => value}, []}, acc -> @@ -3022,28 +3559,20 @@ defmodule Module.Types.Descr do end end - def map_refresh_domain(%{map: [{tag, fields, []}]}, domain, type) do - %{map: [{map_refresh_tag(tag, domain, type), fields, []}]} + def map_refresh_domain(%{map: {{tag, fields}, :bdd_top, :bdd_bot}}, domain, type) do + %{map: {{map_refresh_tag(tag, domain, type), fields}, :bdd_top, :bdd_bot}} end - def map_refresh_domain(%{map: dnf}, domain, type) do - Enum.map(dnf, fn - {tag, fields, []} -> - {map_refresh_tag(tag, domain, type), fields, []} - - {tag, fields, negs} -> - # For negations, we count on the idea that a negation will not remove any - # type from a domain unless it completely cancels out the type. - # So for any non-empty map dnf, we just update the domain with the new type, - # as well as its negations to keep them accurate. - {map_refresh_tag(tag, domain, type), fields, - Enum.map(negs, fn {neg_tag, neg_fields} -> - {map_refresh_tag(neg_tag, domain, type), neg_fields} - end)} - end) + # TODO: TEST THIS (previous implem was wrong) + def map_refresh_domain(%{map: bdd}, domain, type) do + # For negations, we count on the idea that a negation will not remove any + # type from a domain unless it completely cancels out the type. + # So for any non-empty map dnf, we just update the domain with the new type, + # as well as its negations to keep them accurate. + %{map: bdd_map(bdd, fn {tag, fields} -> {map_refresh_tag(tag, domain, type), fields} end)} end - def map_refresh_atom(descr = %{map: dnf}, atom_key, type) do + def map_refresh_atom(descr = %{map: bdd}, atom_key, type) do case atom_key do {:union, keys} -> keys @@ -3051,10 +3580,9 @@ defmodule Module.Types.Descr do |> Enum.reduce(descr, fn key, acc -> map_refresh_key(acc, key, type) end) {:negation, keys} -> - # 1) Fetch all the possible keys in the dnf + # 1) Fetch all the possible keys in the bdd # 2) Get them all, except the ones in neg_atoms - possible_keys = map_fetch_all_key_names(dnf) - considered_keys = :sets.subtract(possible_keys, keys) + considered_keys = map_fetch_all_key_names(bdd) |> :sets.subtract(keys) considered_keys |> :sets.to_list() @@ -3078,20 +3606,22 @@ defmodule Module.Types.Descr do end # Directly inserts a key of a given type into every positive and negative map. - defp map_put_static(%{map: dnf} = descr, key, type) do - dnf = - Enum.map(dnf, fn {tag, fields, negs} -> - {tag, Map.put(fields, key, type), - Enum.map(negs, fn {neg_tag, neg_fields} -> - {neg_tag, Map.put(neg_fields, key, type)} - end)} - end) + defp map_put_static(%{map: bdd} = descr, key, type) do + bdd = bdd_map(bdd, fn {tag, fields} -> {tag, Map.put(fields, key, type)} end) - %{descr | map: dnf} + %{descr | map: bdd} end defp map_put_static(descr, _key, _type), do: descr + defp bdd_map(bdd, fun) do + case bdd do + :bdd_bot -> :bdd_bot + :bdd_top -> :bdd_top + {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)} + end + end + @doc """ Removes a key from a map type. """ @@ -3222,7 +3752,7 @@ defmodule Module.Types.Descr do defp unfold_domains(domains = %{}), do: domains - defp map_get_static(%{map: [{tag_or_domains, fields, []}]}, key_descr) do + defp map_get_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key_descr) do # For each non-empty kind of type in the key_descr, we add the corresponding key domain in a union. domains = unfold_domains(tag_or_domains) @@ -3230,20 +3760,23 @@ defmodule Module.Types.Descr do |> covered_key_types() |> Enum.reduce(none(), fn # Note: we could stop if we reach term_or_optional() - {:atom, atom_type}, acc -> map_get_atom([{domains, fields, []}], atom_type) |> union(acc) - key_type, acc -> Map.get(domains, key_type, not_set()) |> union(acc) + {:atom, atom_type}, acc -> + map_get_atom(map_literal(domains, fields), atom_type) |> union(acc) + + key_type, acc -> + Map.get(domains, key_type, not_set()) |> union(acc) end) end - defp map_get_static(%{map: dnf}, key_descr) do + defp map_get_static(%{map: bdd}, key_descr) do key_descr |> covered_key_types() |> Enum.reduce(none(), fn {:atom, atom_type}, acc -> - map_get_atom(dnf, atom_type) |> union(acc) + map_get_atom(bdd, atom_type) |> union(acc) domain_key, acc -> - map_get_domain(dnf, domain_key) |> union(acc) + map_get_domain(bdd, domain_key) |> union(acc) end) end @@ -3264,13 +3797,13 @@ defmodule Module.Types.Descr do # Fetching a key of type `atom() and not (:a)` from a map of type # `%{a: atom(), b: float(), atom() => pid()}` # would return either `nil` or `float()` (key `:b`) or `pid()` (key `atom()`), but not `atom()` (key `:a`). - defp map_get_atom(dnf, atom_type) do + defp map_get_atom(bdd, atom_type) do case atom_type do {:union, atoms} -> atoms |> :sets.to_list() |> Enum.reduce(none(), fn atom, acc -> - {static_optional?, type} = map_fetch_static(%{map: dnf}, atom) + {static_optional?, type} = map_fetch_static(%{map: bdd}, atom) if static_optional? do union(type, acc) |> nil_or_type() |> if_set() @@ -3280,15 +3813,15 @@ defmodule Module.Types.Descr do end) {:negation, atoms} -> - # 1) Fetch all the possible keys in the dnf + # 1) Fetch all the possible keys in the bdd # 2) Get them all, except the ones in neg_atoms - possible_keys = map_fetch_all_key_names(dnf) + possible_keys = map_fetch_all_key_names(bdd) considered_keys = :sets.subtract(possible_keys, atoms) considered_keys |> :sets.to_list() |> Enum.reduce(none(), fn atom, acc -> - {static_optional?, type} = map_fetch_static(%{map: dnf}, atom) + {static_optional?, type} = map_fetch_static(%{map: bdd}, atom) if static_optional? do union(type, acc) |> nil_or_type() |> if_set() @@ -3296,13 +3829,13 @@ defmodule Module.Types.Descr do union(type, acc) end end) - |> union(map_get_domain(dnf, domain_key(:atom))) + |> union(map_get_domain(bdd, domain_key(:atom))) end end # Fetch all present keys in a map dnf (including negated ones). - defp map_fetch_all_key_names(dnf) do - dnf + defp map_fetch_all_key_names(bdd) do + map_bdd_get(bdd) |> Enum.reduce(:sets.new(version: 2), fn {_tag, fields, negs}, acc -> keys = :sets.from_list(Map.keys(fields)) @@ -3316,8 +3849,8 @@ defmodule Module.Types.Descr do end # Take a map dnf and return the union of types for the given key domain. - defp map_get_domain(dnf, domain_key(_) = domain_key) do - dnf + defp map_get_domain(bdd, domain_key(_) = domain_key) do + map_bdd_get(bdd) |> Enum.reduce(none(), fn {tag, _fields, []}, acc when is_atom(tag) -> map_key_tag_to_type(tag) |> union(acc) @@ -3368,7 +3901,8 @@ defmodule Module.Types.Descr do case :maps.take(:dynamic, descr) do :error -> if descr_key?(descr, :map) and map_only?(descr) do - {optional?, taken, result} = map_take_static(descr, key, initial) + {optional?, taken, result} = + map_take_static(descr, key, initial) cond do taken == nil -> {nil, updater.(result)} @@ -3386,9 +3920,14 @@ defmodule Module.Types.Descr do result = union(dynamic(updater.(dynamic_result)), updater.(static_result)) cond do - static_taken == nil and dynamic_taken == nil -> {nil, result} - static_optional? or empty?(dynamic_taken) -> :badkey - true -> {union(dynamic(dynamic_taken), static_taken), result} + static_taken == nil and dynamic_taken == nil -> + {nil, result} + + static_optional? or empty?(dynamic_taken) -> + :badkey + + true -> + {union(dynamic(dynamic_taken), static_taken), result} end else :badmap @@ -3398,7 +3937,7 @@ defmodule Module.Types.Descr do # Takes a static map type and removes a key from it. # This allows the key to be put or deleted later on. - defp map_take_static(%{map: [{tag, fields, []}]} = descr, key, initial) + defp map_take_static(%{map: {{tag, fields}, :bdd_top, :bdd_bot}} = descr, key, initial) when not is_map_key(fields, key) do case tag do :open -> {true, maybe_union(initial, fn -> term() end), descr} @@ -3406,9 +3945,10 @@ defmodule Module.Types.Descr do end end - defp map_take_static(%{map: dnf}, key, initial) do + defp map_take_static(%{map: bdd}, key, initial) do {value, map} = - Enum.reduce(dnf, {initial, none()}, fn + map_bdd_get(bdd) + |> Enum.reduce({initial, none()}, fn # Optimization: if there are no negatives, we can directly remove the key. {tag, fields, []}, {value, map} -> {fst, snd} = map_pop_key(tag, fields, key) @@ -3447,9 +3987,7 @@ defmodule Module.Types.Descr do # Short-circuits if it finds a non-empty map literal in the union. # Since the algorithm is recursive, we implement the short-circuiting # as throw/catch. - defp map_empty?(dnf) do - Enum.all?(dnf, fn {tag, pos, negs} -> map_empty?(tag, pos, negs) end) - end + defp map_empty?(bdd), do: map_bdd_get(bdd) == [] defp map_empty?(_, pos, []), do: Enum.any?(Map.to_list(pos), fn {_, v} -> empty?(v) end) defp map_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true @@ -3460,7 +3998,7 @@ defmodule Module.Types.Descr do atom_default = map_key_tag_to_type(tag) neg_atom_default = map_key_tag_to_type(neg_tag) - (Enum.all?(neg_fields, fn {neg_key, neg_type} -> + (Enum.all?(Map.to_list(neg_fields), fn {neg_key, neg_type} -> cond do # Ignore keys present in both maps; will be handled below is_map_key(fields, neg_key) -> @@ -3481,7 +4019,7 @@ defmodule Module.Types.Descr do empty?(diff) or map_empty?(tag, Map.put(fields, neg_key, diff), negs) end end) and - Enum.all?(fields, fn {key, type} -> + Enum.all?(Map.to_list(fields), fn {key, type} -> case neg_fields do %{^key => neg_type} -> diff = difference(type, neg_type) @@ -3568,24 +4106,31 @@ defmodule Module.Types.Descr do end # Use heuristics to normalize a map dnf for pretty printing. - defp map_normalize(dnfs) do - for dnf <- dnfs, not map_empty?([dnf]) do - {tag, fields, negs} = dnf - + defp map_normalize(bdd) do + for {tag, fields, negs} <- map_bdd_get(bdd) do {fields, negs} = - Enum.reduce(negs, {fields, []}, fn neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} -> - if map_empty_negation?(tag, acc_fields, neg) do - {acc_fields, acc_negs} - else - case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do - {:one, diff_key} -> - {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])), - acc_negs} + Enum.reduce(negs, {fields, []}, fn + # Optimization: we are removing an open map with one field. + {:open, neg_fields}, {acc_fields, acc_negs} when map_size(neg_fields) == 1 -> + {key, value, _rest} = :maps.next(:maps.iterator(neg_fields)) + t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value) + + # If the difference was empty, then the whole line would be empty, which is not. + {Map.put(acc_fields, key, t_diff), acc_negs} + + neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} -> + if non_intersecting_negation?(tag, acc_fields, neg) do + {acc_fields, acc_negs} + else + case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do + {:one, diff_key} -> + {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])), + acc_negs} - _ -> - {acc_fields, [neg | acc_negs]} + _ -> + {acc_fields, [neg | acc_negs]} + end end - end end) {tag, fields, negs} @@ -3619,11 +4164,10 @@ defmodule Module.Types.Descr do defp map_fuse_with_first_fusible(map, []), do: [map] defp map_fuse_with_first_fusible(map, [candidate | rest]) do - if fused = maybe_optimize_map_union(map, candidate) do + case maybe_optimize_map_union(map, candidate) do + nil -> [candidate | map_fuse_with_first_fusible(map, rest)] # we found a fusible candidate, we're done - [fused | rest] - else - [candidate | map_fuse_with_first_fusible(map, rest)] + fused -> [fused | rest] end end @@ -3646,7 +4190,7 @@ defmodule Module.Types.Descr do end # Adapted from `map_empty?` to remove useless negations. - defp map_empty_negation?(tag, fields, {neg_tag, neg_fields}) do + defp non_intersecting_negation?(tag, fields, {neg_tag, neg_fields}) do (tag == :closed and Enum.any?(neg_fields, fn {neg_key, neg_type} -> not is_map_key(fields, neg_key) and not is_optional_static(neg_type) @@ -3657,9 +4201,8 @@ defmodule Module.Types.Descr do end)) end - defp map_to_quoted(dnf, opts) do - dnf - |> map_normalize() + defp map_to_quoted(bdd, opts) do + map_normalize(bdd) |> Enum.map(&map_each_to_quoted(&1, opts)) end diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index 17a6746c4d0..f406adb2969 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -129,10 +129,12 @@ defmodule Module.Types.DescrTest do assert union(empty_map(), open_map([{domain_key(:integer), atom()}])) |> equal?(open_map([{domain_key(:integer), atom()}])) - assert union(open_map(), open_map([{domain_key(:integer), atom()}])) == open_map() + assert union(open_map(), open_map([{domain_key(:integer), atom()}])) + |> equal?(open_map()) # Test union of open map and map with domain key - assert union(open_map(), open_map([{domain_key(:integer), atom()}])) == open_map() + assert union(open_map(), open_map([{domain_key(:integer), atom()}])) + |> equal?(open_map()) end test "list" do @@ -161,7 +163,8 @@ defmodule Module.Types.DescrTest do assert union( open_map(a: float(), b: atom()), open_map(a: integer(), b: atom()) - ) == open_map(a: union(float(), integer()), b: atom()) + ) + |> equal?(open_map(a: union(float(), integer()), b: atom())) assert union( closed_map(a: float(), b: atom()), @@ -279,11 +282,11 @@ defmodule Module.Types.DescrTest do closed_map(a: integer()) ) - assert intersection(closed_map(a: integer()), open_map(b: not_set())) == - closed_map(a: integer()) + assert intersection(closed_map(a: integer()), open_map(b: not_set())) + |> equal?(closed_map(a: integer())) - assert intersection(closed_map(a: integer()), open_map(b: if_set(integer()))) == - closed_map(a: integer()) + assert intersection(closed_map(a: integer()), open_map(b: if_set(integer()))) + |> equal?(closed_map(a: integer())) assert equal?( intersection(closed_map(a: integer()), closed_map(a: if_set(integer()))), @@ -541,6 +544,7 @@ defmodule Module.Types.DescrTest do # Non-overlapping domain keys t1 = closed_map([{domain_key(:integer), atom()}]) t2 = closed_map([{domain_key(:atom), binary()}]) + assert equal?(difference(t1, t2) |> union(empty_map()), t1) assert empty?(difference(t1, t1)) @@ -1724,15 +1728,21 @@ defmodule Module.Types.DescrTest do assert map_delete(term(), :a) == :badmap assert map_delete(integer(), :a) == :badmap assert map_delete(union(open_map(), integer()), :a) == :badmap - assert map_delete(closed_map(a: integer(), b: atom()), :a) == {:ok, closed_map(b: atom())} - assert map_delete(empty_map(), :a) == {:ok, empty_map()} - assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a) == - {:ok, closed_map(b: atom())} + assert map_delete(closed_map(a: integer(), b: atom()), :a) + |> elem(1) + |> equal?(closed_map(b: atom())) + + assert map_delete(empty_map(), :a) |> elem(1) |> equal?(empty_map()) + + assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a) + |> elem(1) + |> equal?(closed_map(b: atom())) # Deleting a non-existent key - assert map_delete(closed_map(a: integer(), b: atom()), :c) == - {:ok, closed_map(a: integer(), b: atom())} + assert map_delete(closed_map(a: integer(), b: atom()), :c) + |> elem(1) + |> equal?(closed_map(a: integer(), b: atom())) # Deleting from a dynamic map assert map_delete(dynamic(), :a) == {:ok, dynamic(open_map(a: not_set()))} @@ -1770,9 +1780,10 @@ defmodule Module.Types.DescrTest do end test "map_delete with atom fallback" do - assert closed_map([{:a, integer()}, {:b, atom()}, {domain_key(:atom), pid()}]) - |> map_delete(:a) == - {:ok, closed_map([{:a, not_set()}, {:b, atom()}, {domain_key(:atom), pid()}])} + assert closed_map(a: integer(), b: atom(), atom: pid()) + |> map_delete(:a) + |> elem(1) + |> equal?(closed_map(a: not_set(), b: atom(), atom: pid())) end test "map_take" do @@ -1780,8 +1791,8 @@ defmodule Module.Types.DescrTest do assert map_take(integer(), :a) == :badmap assert map_take(union(open_map(), integer()), :a) == :badmap - assert map_take(closed_map(a: integer(), b: atom()), :a) == - {integer(), closed_map(b: atom())} + {took, rest} = map_take(closed_map(a: integer(), b: atom()), :a) + assert equal?(took, integer()) and equal?(rest, closed_map(b: atom())) # Deleting a non-existent key assert map_take(empty_map(), :a) == :badkey @@ -1880,6 +1891,13 @@ defmodule Module.Types.DescrTest do # Put a key-value pair in a difference of maps {:ok, type} = difference(open_map(), closed_map(a: integer())) |> map_put(:b, atom()) + + type2 = difference(open_map(b: atom()), closed_map(a: integer())) + diff = difference(type, type2) + assert empty?(diff) + assert subtype?(type, type2) + assert subtype?(type2, type) + assert equal?(type, difference(open_map(b: atom()), closed_map(a: integer()))) # Put a new key-value pair with dynamic type @@ -2034,7 +2052,7 @@ defmodule Module.Types.DescrTest do |> difference(list(integer())) |> difference(list(atom())) |> to_quoted_string() == - "non_empty_list(term()) and not (non_empty_list(atom()) or non_empty_list(integer()))" + "non_empty_list(term()) and not (non_empty_list(integer()) or non_empty_list(atom()))" assert list(term(), integer()) |> to_quoted_string() == "empty_list() or non_empty_list(term(), integer())" From d6f0217f4c0042bf669afceff5069bb180ffb995 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Sun, 3 Aug 2025 20:52:03 +0200 Subject: [PATCH 06/32] Rewrite of every type as bdd --- lib/elixir/lib/module/types/descr.ex | 1500 +++++++---------- .../test/elixir/module/types/descr_test.exs | 23 +- .../test/elixir/module/types/expr_test.exs | 55 +- 3 files changed, 684 insertions(+), 894 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index ce9bb8ce1f0..09c0faa4ce8 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -12,6 +12,7 @@ defmodule Module.Types.Descr do # Vocabulary: # # * DNF - disjunctive normal form which is a pair of unions and negations. + # * BDD - binary decision diagram which is a set-theoretic representation of types as a tree. # In the case of maps, we augment each pair with the open/closed tag. import Bitwise @@ -27,6 +28,7 @@ defmodule Module.Types.Descr do @bit_number @bit_integer ||| @bit_float defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot]} + defmacrop tuple_literal(tag, elements), do: {:{}, [], [{tag, elements}, :bdd_top, :bdd_bot]} defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot]} defmacrop domain_key(key), do: {:domain_key, key} @@ -50,7 +52,7 @@ defmodule Module.Types.Descr do @atom_top {:negation, :sets.new(version: 2)} @map_top {{:open, %{}}, :bdd_top, :bdd_bot} @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot} - @tuple_top [{:open, []}] + @tuple_top {{:open, []}, :bdd_top, :bdd_bot} @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot} @none %{} @@ -176,15 +178,28 @@ defmodule Module.Types.Descr do Enum.reduce(funs, &intersection/2) end + # This is an insertion of an arrow {domain, return} into a list of non-overlapping arrows. + # If no arrow overlaps with the new arrow, it will be inserted at the end. + # For any arrow that overlaps, we split this arrow into two: one where the domains intersect, + # and one where the domains differ. Then we continue the recursion with the domain subtracted + # from the one of the overlapping arrow. defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do common = intersection(domain, acc_domain) if empty?(common) do [{acc_domain, acc_return} | pivot_overlapping_clause(domain, return, acc)] else - [{common, union(return, acc_return)} | acc] - |> prepend_to_unless_empty(difference(domain, common), return) - |> prepend_to_unless_empty(difference(acc_domain, common), acc_return) + diff = difference(domain, acc_domain) + + rest = + if empty?(diff) do + [] + else + pivot_overlapping_clause(diff, return, acc) + end + + [{common, union(return, acc_return)} | rest] + |> prepend_to_unless_empty(difference(acc_domain, domain), acc_return) end end @@ -233,8 +248,8 @@ defmodule Module.Types.Descr do end end - defp unwrap_domain_tuple(%{tuple: dnf} = descr, transform) when map_size(descr) == 1 do - Enum.map(dnf, transform) + defp unwrap_domain_tuple(%{tuple: bdd} = descr, transform) when map_size(descr) == 1 do + tuple_bdd_to_dnf_no_negations(bdd) |> Enum.map(transform) end defp unwrap_domain_tuple(descr, _transform) when descr == %{}, do: [] @@ -456,9 +471,11 @@ defmodule Module.Types.Descr do {right_dynamic, right_static} = Map.pop(right, :dynamic, right) dynamic_part = difference_static(left_dynamic, right_static) - if empty?(dynamic_part), - do: none(), - else: Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part) + # This might be the worst place possible to check for emptiness. + # if empty?(dynamic_part), + # do: none(), + # else: + Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part) else difference_static(left, right) end @@ -547,52 +564,6 @@ defmodule Module.Types.Descr do (bitmap, atom) are checked first for speed since, if they are present, the type is non-empty as we normalize then during construction. """ - - # defguardp is_descr(d) - # when d == :term or - # (is_map(d) and - # (Map.has_key?(d, :atom) or Map.has_key?(d, :bitmap) or - # Map.has_key?(d, :list) or Map.has_key?(d, :map) or - # Map.has_key?(d, :tuple) or Map.has_key?(d, :fun))) - - # defp bdd_size({{tag, fields = %{}}, l, r}) when tag in [:open, :closed] do - # bdd_size(l) + bdd_size(r) + 1 + Enum.reduce(fields, 0, fn d, acc -> descr_size(d) + acc end) - # end - - # defp bdd_size({{list = %{}, last = %{}}, l, r}) do - # bdd_size(l) + bdd_size(r) + 1 + descr_or_domain_size(list) + descr_or_fields_size(last) - # end - - defp bdd_size({lit, l, r}), do: bdd_size(l) + bdd_size(r) + 1 - - defp bdd_size(bdd), do: 0 - - defp dnf_structural_size(dnf) do - Enum.reduce(dnf, 0, fn {_tag, pos}, acc -> - 1 + acc + length(pos) - end) - end - - defp dnf_size(dnf) do - Enum.reduce(dnf, 0, fn {_tag, pos}, acc -> - 1 + acc + Enum.reduce(pos, 0, fn d, acc -> descr_size(d) + acc end) - end) - end - - def descr_size(:term), do: 1 - - def descr_size(%{} = descr) do - Enum.reduce(Map.to_list(descr), 0, fn {key, value}, acc -> - acc + descr_size(key, value) - end) - end - - def descr_size(:tuple, dnf), do: dnf_size(dnf) - def descr_size(:fun, bdd), do: bdd_size(bdd) - def descr_size(:map, bdd), do: bdd_size(bdd) - def descr_size(:list, bdd), do: bdd_size(bdd) - def descr_size(_, _), do: 1 - def empty?(:term), do: false def empty?(%{} = descr) do @@ -604,50 +575,10 @@ defmodule Module.Types.Descr do true descr -> - # IO.puts("Woooh") - d = descr_size(descr) - - if d > 100 do - IO.puts("descr_size(descr): #{d}") - IO.puts("The decomposition is:") - - if Map.has_key?(descr, :atom), - do: IO.puts("Atom size: #{descr_size(:atom, descr.atom)}") - - if Map.has_key?(descr, :list) do - IO.puts("List size: #{descr_size(:list, descr.list)}") - else - IO.puts("List size: 0") - end - - if Map.has_key?(descr, :map) do - IO.puts("Map size: #{descr_size(:map, descr.map)}") - else - IO.puts("Map size: 0") - end - - if Map.has_key?(descr, :tuple) do - IO.puts("Tuple size: #{descr_size(:tuple, descr.tuple)}") - IO.puts("Tuple structural size: #{dnf_structural_size(descr.tuple)}") - else - IO.puts("Tuple size: 0") - end - - if Map.has_key?(descr, :fun) do - IO.puts("Fun size: #{descr_size(:fun, descr.fun)}") - else - IO.puts("Fun size: 0") - end - - # dbg(descr) - end - - # dbg(descr, limit: :infinity, printable_limit: :infinity, width: :infinity) - not Map.has_key?(descr, :atom) and not Map.has_key?(descr, :bitmap) and not Map.has_key?(descr, :optional) and - not Map.has_key?(descr, :tuple) and + (not Map.has_key?(descr, :tuple) or tuple_empty?(descr.tuple)) and (not Map.has_key?(descr, :map) or map_empty?(descr.map)) and (not Map.has_key?(descr, :list) or list_empty?(descr.list)) and (not Map.has_key?(descr, :fun) or fun_empty?(descr.fun)) @@ -661,6 +592,7 @@ defmodule Module.Types.Descr do defp empty_key?(:fun, value), do: fun_empty?(value) defp empty_key?(:map, value), do: map_empty?(value) defp empty_key?(:list, value), do: list_empty?(value) + defp empty_key?(:tuple, value), do: tuple_empty?(value) defp empty_key?(_, _value), do: false @doc """ @@ -732,9 +664,9 @@ defmodule Module.Types.Descr do defp to_quoted(:atom, val, _opts), do: atom_to_quoted(val) defp to_quoted(:bitmap, val, _opts), do: bitmap_to_quoted(val) defp to_quoted(:dynamic, descr, opts), do: dynamic_to_quoted(descr, opts) - defp to_quoted(:map, dnf, opts), do: map_to_quoted(dnf, opts) - defp to_quoted(:list, dnf, opts), do: list_to_quoted(dnf, false, opts) - defp to_quoted(:tuple, dnf, opts), do: tuple_to_quoted(dnf, opts) + defp to_quoted(:map, bdd, opts), do: map_to_quoted(bdd, opts) + defp to_quoted(:list, bdd, opts), do: list_to_quoted(bdd, false, opts) + defp to_quoted(:tuple, bdd, opts), do: tuple_to_quoted(bdd, opts) defp to_quoted(:fun, bdd, opts), do: fun_to_quoted(bdd, opts) @doc """ @@ -1417,7 +1349,22 @@ defmodule Module.Types.Descr do type_args = args_to_domain(arguments) Enum.reduce(arrows, none(), fn intersection_of_arrows, acc -> - aux_apply(acc, type_args, term(), intersection_of_arrows) + {x, _cache} = aux_apply(acc, type_args, term(), intersection_of_arrows, %{}) + x + end) + end + + defp apply_disjoint(arguments, arrows) do + type_args = args_to_domain(arguments) + + Enum.reduce(arrows, none(), fn {args, ret}, acc_return -> + dom = args_to_domain(args) + + if empty?(intersection(dom, type_args)) do + acc_return + else + union(acc_return, ret) + end end) end @@ -1435,39 +1382,67 @@ defmodule Module.Types.Descr do # - arrow_intersections: The list of function arrows to process # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf - defp aux_apply(result, _input, rets_reached, []) do - if subtype?(rets_reached, result), do: result, else: union(result, rets_reached) + defp aux_apply(result, input, rets_reached, [], cache) do + cache_key = {result, input, rets_reached, []} + res = union(result, rets_reached) + {res, Map.put(cache, cache_key, res)} end - defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do + defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections], cache) do # Calculate the part of the input not covered by this arrow's domain - dom_subtract = difference(input, args_to_domain(args)) - - # Refine the return type by intersecting with this arrow's return type - ret_refine = intersection(returns_reached, ret) - - # Phase 1: Domain partitioning - # If the input is not fully covered by the arrow's domain, then the result type should be - # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered - # parts of the domain. - # - # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite - # both atoms and pids in the result. - result = - if empty?(dom_subtract) do - result - else - aux_apply(result, dom_subtract, returns_reached, arrow_intersections) - end + cache_key = {result, input, returns_reached, [{args, ret} | arrow_intersections]} + + case cache do + %{^cache_key => value} -> + {value, cache} + + _ -> + dom = args_to_domain(args) + no_intersection? = empty?(intersection(dom, input)) + + cond do + # First: is there any intersection between the input and the arrow's domain? + # If not, we skip this arrow. + no_intersection? -> + {result, cache} = + aux_apply(result, input, returns_reached, arrow_intersections, cache) - # 2. Return type refinement - # The result type is also refined (intersected) in the sense that, if several arrows match - # the same part of the input, then the result type is an intersection of the return types of - # those arrows. + cache = Map.put(cache, cache_key, result) + {result, cache} - # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer() - # should result in (atom() ∩ pid()), which is none(). - aux_apply(result, input, ret_refine, arrow_intersections) + true -> + dom_subtract = difference(input, dom) + + # Refine the return type by intersecting with this arrow's return type + ret_refine = intersection(returns_reached, ret) + + # Phase 1: Domain partitioning + # If the input is not fully covered by the arrow's domain, then the result type should be + # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered + # parts of the domain. + # + # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite + # both atoms and pids in the result. + + {result, cache} = + if empty?(dom_subtract) do + {result, cache} + else + aux_apply(result, dom_subtract, returns_reached, arrow_intersections, cache) + end + + # 2. Return type refinement + # The result type is also refined (intersected) in the sense that, if several arrows match + # the same part of the input, then the result type is an intersection of the return types of + # those arrows. + + # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer() + # should result in (atom() ∩ pid()), which is none(). + {result, cache} = aux_apply(result, input, ret_refine, arrow_intersections, cache) + cache = Map.put(cache, cache_key, result) + {result, cache} + end + end end # Takes all the paths from the root to the leaves finishing with a 1, @@ -1497,9 +1472,15 @@ defmodule Module.Types.Descr do # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty defp fun_empty?(bdd) do case bdd do - :fun_bottom -> true - :fun_top -> false - bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end) + :fun_bottom -> + true + + :fun_top -> + false + + bdd -> + fun_get(bdd) + |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end) end end @@ -1536,8 +1517,10 @@ defmodule Module.Types.Descr do # Filter positives to only those with matching arity, then check if the negative # function's domain is a supertype of the positive domain and if the phi function # determines emptiness. + neg_dom = args_to_domain(neg_arguments) + length(neg_arguments) == positive_arity and - subtype?(args_to_domain(neg_arguments), positive_domain) and + subtype?(neg_dom, positive_domain) and phi_starter(neg_arguments, neg_return, positives) end) end @@ -1580,26 +1563,32 @@ defmodule Module.Types.Descr do # we can simplify the phi function check to a direct subtyping test. # This avoids the expensive recursive phi computation by checking only that applying the # input to the positive intersection yields a subtype of the return - if all_non_empty_domains?([{arguments, return} | positives]) do - fun_apply_static(arguments, [positives]) - |> subtype?(return) - else - n = length(arguments) - # Arity mismatch: functions with different arities cannot be subtypes - # of the target function type (arguments -> return) - if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do - false - else - # Initialize memoization cache for the recursive phi computation - arguments = Enum.map(arguments, &{false, &1}) - {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{}) - result - end + case disjoint_non_empty_domains?({arguments, return}, positives) do + :disjoint_non_empty -> + apply_disjoint(arguments, positives) |> subtype?(return) + + :non_empty -> + fun_apply_static(arguments, [positives]) |> subtype?(return) + + _ -> + n = length(arguments) + # Arity mismatch: functions with different arities cannot be subtypes + # of the target function type (arguments -> return) + if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do + false + else + # Initialize memoization cache for the recursive phi computation + arguments = Enum.map(arguments, &{false, &1}) + {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{}) + result + end end end defp phi(args, {b, t}, [], cache) do - {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache} + result = Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)) + {result, Map.put(cache, {args, {b, t}, []}, result)} + # {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache} end defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do @@ -1640,12 +1629,49 @@ defmodule Module.Types.Descr do end end + defp disjoint_non_empty_domains?({arguments, return}, positives) do + b1 = all_disjoint_domains?(positives) + b2 = all_non_empty_domains?([{arguments, return} | positives]) + + cond do + b1 and b2 -> :disjoint_non_empty + b2 -> :non_empty + true -> nil + end + end + defp all_non_empty_domains?(positives) do Enum.all?(positives, fn {args, _ret} -> Enum.all?(args, fn arg -> not empty?(arg) end) end) end + # For two arguments to be disjoint, we need at least one of their types to be disjoint. + defp disjoint_arguments?(args1, args2) do + Enum.reduce_while(Enum.zip(args1, args2), false, fn {t1, t2}, acc -> + t = intersection(t1, t2) + + if empty?(t) do + {:halt, true} + else + {:cont, acc} + end + end) + end + + # Test that all positives are two to two disjoint. We iterate on the list to do so. + defp all_disjoint_domains?([]), do: true + + defp all_disjoint_domains?([{args, _} | rest]) do + Enum.reduce_while(rest, true, fn {args_rest, _}, _acc -> + if disjoint_arguments?(args, args_rest) do + {:cont, true} + else + {:halt, false} + end + end) + end + defp fun_union(bdd1, bdd2) do case {bdd1, bdd2} do {:fun_top, _} -> :fun_top @@ -1895,15 +1921,15 @@ defmodule Module.Types.Descr do ## List - # Represents both list and improper list simultaneously using a pair - # `{list_type, last_type}`. - # - # We compute if it is a proper or improper list based if the last_type - # is an empty_list() or a list(). In particular, the last_type may be - # stored as `:term` for optimization purposes. This is ok because operations - # like `tl` effectively return the list itself plus the union of the tail - # (and if the tail includes the list itself, they are equivalent). And, - # for other operations like difference, we expand the tail_type back into + # Represents list and improper list simultaneously as a BDD with nodes of the form + # `{list_type, last_type}`, where `list_type` is the type of elements in the list, + # and `last_type` is the type of the last element (so `[]` if the list is proper, + # and anything else but a list if the list is improper). + + # The last_type may be stored as `:term` for optimization purposes. This is ok + # because operations like `tl` effectively return the list itself plus the union of + # the tail (and if the tail includes the list itself, they are equivalent). And, for other + # operations like difference, we expand the tail_type back into # `not non_empty_list()` via `list_tail_unfold/1`. Overall, this simplifies # the code because we don't need to special case `not non_empty_list()`. # @@ -2068,42 +2094,8 @@ defmodule Module.Types.Descr do defp list_tail_unfold(:term), do: @not_non_empty_list defp list_tail_unfold(other), do: Map.delete(other, :list) - # Attempt a merge, if the union is between two single lists. - defp list_union(list_literal(list1, last1), list_literal(list2, last2)) do - cond do - subtype?(list1, list2) and subtype?(last1, last2) -> list_literal(list2, last2) - subtype?(list2, list1) and subtype?(last2, last1) -> list_literal(list1, last1) - equal?(list1, list2) -> list_literal(list1, union(last1, last2)) - true -> list_union_recur(list_literal(list1, last1), list_literal(list2, last2)) - end - end - - defp list_union(bdd1, bdd2), do: list_union_recur(bdd1, bdd2) - - defp list_union_recur(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_top, _} -> - :bdd_top - - {_, :bdd_top} -> - :bdd_top - - {:bdd_bot, bdd} -> - bdd - - {bdd, :bdd_bot} -> - bdd - - {{list, l1, r1}, {list, l2, r2}} -> - {list, list_union(l1, l2), list_union(r1, r2)} - - {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 -> - {list1, list_union(l1, bdd2), list_union(r1, bdd2)} - - {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 -> - {list2, list_union(bdd1, l2), list_union(bdd1, r2)} - end - end + @compile {:inline, list_union: 2} + defp list_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2) defp is_list_top?({{list, tail}, :bdd_top, :bdd_bot}) do list == :term and tail == :term @@ -2111,11 +2103,21 @@ defmodule Module.Types.Descr do defp is_list_top?(_), do: false + defp list_intersection(list_literal(list1, last1), list_literal(list2, last2)) do + try do + list = non_empty_intersection!(list1, list2) + last = non_empty_intersection!(last1, last2) + list_literal(list, last) + catch + :empty -> :bdd_bot + end + end + defp list_intersection(bdd1, bdd2) do cond do is_list_top?(bdd1) and is_tuple(bdd2) -> bdd2 is_list_top?(bdd2) and is_tuple(bdd1) -> bdd1 - true -> list_intersection_recur(bdd1, bdd2) + true -> bdd_intersection(bdd1, bdd2) end |> case do {_, :bdd_bot, :bdd_bot} -> :bdd_bot @@ -2123,84 +2125,6 @@ defmodule Module.Types.Descr do end end - defp list_intersection_recur(bdd1, bdd2) do - case {bdd1, bdd2} do - # Base cases - {_, :bdd_bot} -> - :bdd_bot - - {:bdd_bot, _} -> - :bdd_bot - - {:bdd_top, bdd} -> - bdd - - {bdd, :bdd_top} -> - bdd - - # Optimizations - # If intersecting with a single positive or negative function, we insert - # it at the root instead of merging the trees (this avoids going down the - # whole bdd). - # Note: instead of inserting the bdd at the root, we decided to intersect with - # every atom in the bdd. If empty, then replace with the right tree. - # {bdd, {list, :bdd_top, :bdd_bot}} -> - # intersect_bdd_with_list(bdd, list) - - # {bdd, {list, :bdd_bottom, :bdd_top}} -> - # {list, :bdd_bottom, bdd} - - # {{list, :bdd_top, :bdd_bottom}, bdd} -> - # intersect_bdd_with_list(bdd, list) - - # {{list, :bdd_bottom, :bdd_top}, bdd} -> - # {list, :bdd_bottom, bdd} - {list_literal(list1, last1), list_literal(list2, last2)} -> - try do - list1 = non_empty_intersection!(list1, list2) - last1 = non_empty_intersection!(last1, last2) - list_literal(list1, last1) - catch - :empty -> :bdd_bot - end - - # General cases - {{list, l1, r1}, {list, l2, r2}} -> - {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)} - - {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 -> - {list1, list_intersection_recur(l1, bdd2), list_intersection_recur(r1, bdd2)} - - {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 -> - {list2, list_intersection_recur(bdd1, l2), list_intersection_recur(bdd1, r2)} - - # {{list, l, r}, bdd} -> - # {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)} - end - end - - # We can only do this if the bdd has :bdd_bot as right child. Otherwise, if `a` is the root, - # it contains both formulas `a and left`, and `not a and right`. Thus, intersecting `not a` - # with a `{list, last}` is a wrong formula. Then, if the intersection is empty, the whole - # bdd is empty. - defp intersect_bdd_with_list(bdd, {list, last}) do - case bdd do - {{bdd_list, bdd_last}, left, :bdd_bot} -> - list = intersection(bdd_list, list) - last = intersection(bdd_last, last) - - if empty?(list) or empty?(last) do - :bdd_bot - else - {{list, last}, left, :bdd_bot} - end - - _ -> - # Otherwise, we simply put the positive list at the root. - {{list, last}, bdd, :bdd_bot} - end - end - # Computes the difference between two BDD (Binary Decision Diagram) list types. # It progressively subtracts each type in bdd2 from all types in bdd1. # The algorithm handles three cases: @@ -2210,32 +2134,24 @@ defmodule Module.Types.Descr do # b) If only the last type differs, subtracts it # 3. Base case: adds bdd2 type to negations of bdd1 type # The result may be larger than the initial bdd1, which is maintained in the accumulator. - defp list_difference(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_bot, _} -> - :bdd_bot + defp list_difference(list_literal(list1, last1) = bdd1, list_literal(list2, last2) = bdd2) do + cond do + empty?(intersection(list1, list2)) or empty?(intersection(last1, last2)) -> + list_literal(list1, last1) - {_, :bdd_top} -> + subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot - {bdd, :bdd_bot} -> - bdd - - {:bdd_top, {lst, l, r}} -> - {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)} - - {{lst, l1, r1}, {lst, l2, r2}} -> - {lst, list_difference(l1, l2), list_difference(r1, r2)} - - {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 < lst2 -> - {lst1, list_difference(l1, bdd2), list_difference(r1, bdd2)} - - {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 > lst2 -> - {lst2, list_difference(bdd1, l2), list_difference(bdd1, r2)} + equal?(list1, list2) -> + list_literal(list1, difference(last1, last2)) - # {{lst, l, r}, bdd} -> - # {lst, list_difference(l, bdd), list_difference(r, bdd)} + true -> + bdd_difference(bdd1, bdd2) end + end + + defp list_difference(bdd1, bdd2) do + bdd_difference(bdd1, bdd2) |> case do {_, :bdd_bot, :bdd_bot} -> :bdd_bot bdd -> bdd @@ -2247,13 +2163,23 @@ defmodule Module.Types.Descr do defp list_empty_line?(list_type, last_type, negs) do last_type = list_tail_unfold(last_type) - + # To make a list {list, last} empty with some negative lists: + # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one. + # 2. Each of the list supertypes: + # a. either completely covers the type, if its last type is a supertype of the positive one, + # b. or it removes part of the last type. empty?(list_type) or empty?(last_type) or Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type -> - if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do - {:halt, nil} + if subtype?(list_type, neg_type) do + d = difference(acc_last_type, neg_last) + + if empty?(d) do + {:halt, nil} + else + {:cont, d} + end else - {:cont, difference(acc_last_type, neg_last)} + {:cont, acc_last_type} end end) |> is_nil() @@ -2554,17 +2480,30 @@ defmodule Module.Types.Descr do ## Map # - # Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs - # `{map_literal, negated_literals}` where `map_literal` is a map type literal - # and `negated_literals` is a list of map type literals that are negated from it. - # Each pair is augmented with the :open or :closed tag. + # Maps are represented as BDDs, that is, a tree of pairs `{tag_or_domain, fields}` + # where `tag_or_domain` is either :closed or :open, or a map from domain keys + # (@domain_key_types) to types, and `fields` is a map of atom keys (:foo, :bar, ...) + # to types. # # For instance, the type `%{..., a: integer()} and not %{b: atom()}` can be represented - # by the DNF containing one pair of shape: + # by the BDD containing one pair of shape: + # + # {{:open, %{:a => integer()}}, {{:closed, %{:b => atom()}}, :bdd_bot, :bdd_top}, :bdd_bot} + # + # which can be seen as: + # + # └─ %{..., a: integer()} + # ├─ %{b: atom()} + # │ ├─ :bdd_bot + # │ └─ :bdd_top + # └─ :bdd_bot # - # {:open, %{a => integer()}, [{:closed, %{b => atom()}}]} + # and is interpreted as the intersection of `%{..., a: integer()}` with + # `not %{b: atom()}`, since the only path from the root to the leaves which + # ends with `:bdd_top` is the one which takes the first (left) branch after + # `%{..., a: integer()}`, and the second (right) branch after `%{b: atom()}`. # - # The goal of keeping symbolic negations is to avoid distributing difference on + # This representation keeps negations symbolic, and avoids distributing difference on # every member of a union which creates a lot of map literals in the union and # requires emptiness checks to avoid creating empty maps. # @@ -2573,7 +2512,7 @@ defmodule Module.Types.Descr do # `%{..., a: if_set(not atom()), b: integer()}`. For maps with more keys, # each key in a negated literal may create a new union when eliminated. # - # Instead of a tag :open or :closed, we can also use a map of domains which + # Instead of a tag :open or :closed, we can use a map of domains which # specifies for each defined key domain (@domain_key_types) the type associated with # those keys. # @@ -2585,239 +2524,6 @@ defmodule Module.Types.Descr do # and other keys bound to any type. It will be represented using a map domain that maps # atom to `if_set(integer())`, and every other domain key to `term_or_optional()`. - # ## TESTING - # def map_merge(%{map: bdd1} = d1, %{map: bdd2} = d2) do - # # Starting accumulator: the empty map type - # res = %{map: :bdd_bot} - - # # Recursive auxiliary function - # aux = fn aux, accu, bdd1, bdd2 -> - # case {map_first_label(bdd1), map_first_label(bdd2)} do - # {:dummy, :dummy} -> - # {some1, none1} = map_empty_cases(bdd1) - # {some2, none2} = map_empty_cases(bdd2) - - # some = some1 or some2 - # none = none1 and none2 - - # # Approximation if some and not none - # if some do - # fields = :maps.from_list(accu) - # map_union(res, %{map: map_new(:open, fields)}) - # else - # res - # end - - # {l1, l2} -> - # l = min_label(l1, l2) - - # # Split along label l - # split1 = map_split(bdd1, l) - # split2 = map_split(bdd2, l) - - # Enum.reduce(split1, res, fn {t1, d1_next}, acc -> - # Enum.reduce(split2, acc, fn {t2, d2_next}, acc2 -> - # t = - # if Map.has_key?(t2, :optional) and t2.optional do - # union(t1, remove_optional(t2)) - # else - # t2 - # end - - # aux.(aux, [{l, t} | accu], d1_next.map, d2_next.map) - # end) - # end) - # end - # end - - # aux.(aux, [], bdd1, bdd2) - # end - - # defp map_first_label(:bdd_top), do: :dummy - # defp map_first_label(:bdd_bot), do: :dummy - - # defp map_first_label({{tag, fields}, :bdd_top, :bdd_bot}) do - # case :maps.next(:maps.iterator(fields)) do - # :none -> :dummy - # {key, _value, _iter} -> key - # end - # end - - # defp map_first_label({{_tag, _fields}, l, _r}), do: map_first_label(l) - - # # Returns {some, none} - # defp map_empty_cases(bdd) do - # map_bdd_get(bdd) - # |> Enum.reduce({false, true}, fn - # {:open, fields, _negs}, {some, none} -> - # some = some or map_size(fields) > 0 - # none = none and map_size(fields) == 0 - # {some, none} - - # {:closed, fields, _negs}, {some, none} -> - # some = some or map_size(fields) > 0 - # none = none and map_size(fields) == 0 - # {some, none} - # end) - # end - - # # Split a BDD into a list of {type_for_label, rest_of_map} - # defp map_split(bdd, label) do - # map_bdd_get(bdd) - # |> Enum.map(fn {tag, fields, negs} -> - # case :maps.take(label, fields) do - # {value, fields_rest} -> - # {remove_optional(value), %{map: map_new(tag, fields_rest)}} - - # :error -> - # # If absent - # type_for_label = - # case tag do - # :open -> term_or_optional() - # :closed -> not_set() - # domains = %{} -> Map.get(domains, domain_key(:atom), not_set()) - # end - - # {type_for_label, %{map: map_new(tag, fields)}} - # end - # end) - # end - - # defp min_label(:dummy, :dummy), do: :dummy - # defp min_label(:dummy, l), do: l - # defp min_label(l, :dummy), do: l - # defp min_label(l1, l2), do: if(l1 <= l2, do: l1, else: l2) - - @doc """ - Type-level merge for maps (like `Map.merge/2`). - - Semantics per OCaml code: - - For each key `l`, if the right map's type for `l` **may be absent**, - the merged type for `l` is `left(l) ∪ present(right(l))`; - otherwise it is `right(l)` (right-biased override). - - Domains are merged with the same rule (component-wise). - - If either side is `:open`, the result is effectively open (via domains). - - Returns `{:ok, merged_descr}` or `:badmap` if either input is not a (possibly dynamic) map type. - """ - def map_merge(:term, _), do: :badmap - def map_merge(_, :term), do: :badmap - - def map_merge(%{} = descr1, %{} = descr2) do - case {:maps.take(:dynamic, descr1), :maps.take(:dynamic, descr2)} do - {:error, :error} -> - with {:ok, m} <- map_merge_static(descr1, descr2) do - {:ok, m} - else - :badmap -> :badmap - end - - {{dyn1, stat1}, :error} -> - with {:ok, stat_stat} <- map_merge_static(stat1, descr2), - {:ok, dyn_stat} <- map_merge_static(dynamic(dyn1), descr2) do - {:ok, union(stat_stat, dynamic(dyn_stat))} - else - :badmap -> :badmap - end - - {:error, {dyn2, stat2}} -> - with {:ok, stat_stat} <- map_merge_static(descr1, stat2), - {:ok, stat_dyn} <- map_merge_static(descr1, dynamic(dyn2)) do - {:ok, union(stat_stat, dynamic(stat_dyn))} - else - :badmap -> :badmap - end - - {{dyn1, stat1}, {dyn2, stat2}} -> - with {:ok, ss} <- map_merge_static(stat1, stat2), - {:ok, sd} <- map_merge_static(stat1, dynamic(dyn2)), - {:ok, ds} <- map_merge_static(dynamic(dyn1), stat2), - {:ok, dd} <- map_merge_static(dynamic(dyn1), dynamic(dyn2)) do - {:ok, union(ss, union(dynamic(sd), union(dynamic(ds), dynamic(dd))))} - else - :badmap -> :badmap - end - end - end - - # --- Core static merger on the BDDs --------------------------------------- - - defp map_merge_static(%{map: bdd1} = d1, %{map: bdd2} = d2) do - # both inputs must be exclusively map (no extra components) - if map_only?(d1) and map_only?(d2) do - # Build the result by taking the cross-product of positive literals - # (DNF lines) and unioning merged literals. - merged_bdd = - map_bdd_get(bdd1) - |> Enum.reduce(:bdd_bot, fn {tag1, fields1, _negs1}, acc1 -> - Enum.reduce(map_bdd_get(bdd2), acc1, fn {tag2, fields2, _negs2}, acc2 -> - {new_tag_or_domains, new_fields} = - map_literal_merge(tag1, fields1, tag2, fields2) - - map_union(acc2, {{new_tag_or_domains, new_fields}, :bdd_top, :bdd_bot}) - end) - end) - - {:ok, %{map: merged_bdd}} - else - :badmap - end - end - - defp map_merge_static(_, _), do: :badmap - - # --- Literal / domain merge (right-biased with "optional means fallback") -- - - # Merge two map literals (tag-or-domains + fields) into one literal. - defp map_literal_merge(tag_or_domains1, fields1, tag_or_domains2, fields2) do - default1 = map_key_tag_to_type(tag_or_domains1) - default2 = map_key_tag_to_type(tag_or_domains2) - - # Merge domains first (handles openness and all non-atom key domains) - new_tag_or_domains = map_domain_merge(tag_or_domains1, tag_or_domains2) - - # For explicit atom keys: symmetrical merge with defaults for missing keys - new_fields = - symmetrical_merge(fields1, default1, fields2, default2, fn _key, v1, v2 -> - map_merge_value(v1, v2) - end) - - {new_tag_or_domains, new_fields} - end - - # Component-wise merge of domains. For every domain key dk in @domain_key_types: - # result(dk) = merge_value( domain1(dk), domain2(dk) ). - # If all resulting domain entries are empty/optional, collapse to :closed. - defp map_domain_merge(tag_or_domains1, tag_or_domains2) do - new_domains = - for domain_key(_) = dk <- @domain_key_types, reduce: %{} do - acc -> - v1 = map_domain_default(tag_or_domains1, dk) - v2 = map_domain_default(tag_or_domains2, dk) - v = map_merge_value(v1, v2) - - if empty_or_optional?(v) do - acc - else - Map.put(acc, dk, v) - end - end - - if map_size(new_domains) == 0, do: :closed, else: new_domains - end - - # Default value for a domain when not explicitly present in the literal. - defp map_domain_default(:open, _dk), do: term_or_optional() - defp map_domain_default(:closed, _dk), do: not_set() - defp map_domain_default(domains = %{}, dk), do: Map.get(domains, dk, not_set()) - - # Merge the two value types for a key, per OCaml's rule: - # if right may be absent, use left ∪ present(right), else right. - defp map_merge_value(left, right) do - {optional?, right_present} = pop_optional_static(right) - if optional?, do: union(left, right_present), else: right - end - defp map_descr(tag, pairs, default, force?) do {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false) @@ -2886,68 +2592,21 @@ defmodule Module.Types.Descr do defp map_only?(descr), do: empty?(Map.delete(descr, :map)) - defp map_union(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_top, _} -> - :bdd_top - - {_, :bdd_top} -> - :bdd_top - - {:bdd_bot, bdd} -> - bdd - - {bdd, :bdd_bot} -> - bdd - - {map_literal(tag1, fields1), map_literal(tag2, fields2)} -> - case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do - {tag, fields, []} -> - {{tag, fields}, :bdd_top, :bdd_bot} - - nil -> - lit1 = {tag1, fields1} - lit2 = {tag2, fields2} - - cond do - lit1 == lit2 -> {lit1, :bdd_top, :bdd_bot} - lit1 < lit2 -> {lit1, :bdd_top, {lit2, :bdd_top, :bdd_bot}} - lit1 > lit2 -> {lit2, :bdd_top, {lit1, :bdd_top, :bdd_bot}} - end - end - - {{map, l1, r1}, {map, l2, r2}} -> - {map, map_union(l1, l2), map_union(r1, r2)} - - # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. - # It is the same as going down bdd1 to insert bdd1 into it. - # Possible opti: insert into the bdd with smallest height - {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 -> - {map1, map_union(l1, bdd2), map_union(r1, bdd2)} - - {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 -> - {map2, map_union(bdd1, l2), map_union(bdd1, r2)} - - # {{map, l, r}, bdd} -> - # {map, map_union(l, bdd), map_union(r, bdd)} + defp non_empty_map_only?(descr) do + case :maps.take(:map, descr) do + :error -> false + {map_bdd, rest} -> empty?(rest) and not map_empty?(map_bdd) end end - # defp map_union(dnf1, dnf2) do - # # Union is just concatenation, but we rely on some optimization strategies to - # # avoid the list to grow when possible + def map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do + case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do + {tag, fields, []} -> map_literal(tag, fields) + nil -> {{tag1, fields1}, :bdd_top, {{tag2, fields2}, :bdd_top, :bdd_bot}} + end + end - # # first pass trying to identify patterns where two maps can be fused as one - # with [map1] <- dnf1, - # [map2] <- dnf2, - # optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do - # [optimized] - # else - # # otherwise we just concatenate and remove structural duplicates - # _ -> dnf1 ++ (dnf2 -- dnf1) - # end - # end - # defp maybe_optimize_map_union(map, map), do: map + def map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2) defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do @@ -3045,110 +2704,52 @@ defmodule Module.Types.Descr do if subtype?(v2, v1), do: :right_subtype_of_left end - defp is_map_top?({{tag, fields}, :bdd_top, :bdd_bot}) do - tag == :open and map_size(fields) == 0 - end - + defp is_map_top?(map_literal(:open, fields)) when map_size(fields) == 0, do: true defp is_map_top?(_), do: false + defp map_intersection(map_literal(tag1, fields1), map_literal(tag2, fields2)) do + try do + map = map_literal_intersection(tag1, fields1, tag2, fields2) + {map, :bdd_top, :bdd_bot} + catch + :empty -> :bdd_bot + end + end + defp map_intersection(bdd1, bdd2) do # If intersecting with the top map type, no-op cond do is_map_top?(bdd1) and is_tuple(bdd2) -> bdd2 is_map_top?(bdd2) and is_tuple(bdd1) -> bdd1 - true -> map_intersection_recur(bdd1, bdd2) - end - end - - defp map_intersection_recur(bdd1, bdd2) do - case {bdd1, bdd2} do - # Base cases - {_, :bdd_bot} -> - :bdd_bot - - {:bdd_bot, _} -> - :bdd_bot - - {:bdd_top, bdd} -> - bdd - - {bdd, :bdd_top} -> - bdd - - {map_literal(tag1, fields1), map_literal(tag2, fields2)} -> - try do - map = map_literal_intersection(tag1, fields1, tag2, fields2) - {map, :bdd_top, :bdd_bot} - catch - :empty -> :bdd_bot - end - - # Optimizations - # If intersecting with a single positive or negative function, we insert - # it at the root instead of merging the trees (this avoids going down the - # whole bdd). - # No: bc we want to have increasing order of literals. - # {bdd, {map, :bdd_top, :bdd_bot}} -> - # {map, bdd, :bdd_bot} - - # {bdd, {map, :bdd_bot, :bdd_top}} -> - # {map, :bdd_bot, bdd} - - # {{map, :bdd_top, :bdd_bot}, bdd} -> - # {map, bdd, :bdd_bot} - - # {{map, :bdd_bot, :bdd_top}, bdd} -> - # {map, :bdd_bot, bdd} - - # General cases - {{map, l1, r1}, {map, l2, r2}} -> - {map, map_intersection_recur(l1, l2), map_intersection_recur(r1, r2)} - - {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 -> - {map1, map_intersection_recur(l1, bdd2), map_intersection_recur(r1, bdd2)} - - {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 -> - {map2, map_intersection_recur(bdd1, l2), map_intersection_recur(bdd1, r2)} - - # {{map, l, r}, bdd} -> - # {map, map_intersection_recur(l, bdd), map_intersection_recur(r, bdd)} + true -> bdd_intersection(bdd1, bdd2) end end - defp map_difference(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_bot, _} -> - :bdd_bot + # Optimizations on single maps. + defp map_difference(map_literal(tag, fields) = map1, map_literal(neg_tag, neg_fields) = map2) do + # Case 1: we are removing an open map with one field. Just do the difference of that field. + if neg_tag == :open and map_size(neg_fields) == 1 do + {key, value, _rest} = :maps.next(:maps.iterator(neg_fields)) + t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value) - {_, :bdd_top} -> + if empty?(t_diff) do :bdd_bot + else + map_literal(tag, Map.put(fields, key, t_diff)) + end + else + # Case 2: the maps have all but one key in common. Do the difference of that key. + case map_all_but_one(tag, fields, neg_tag, neg_fields) do + {:one, diff_key} -> + map_literal(tag, Map.update!(fields, diff_key, &difference(&1, neg_fields[diff_key]))) - {bdd, :bdd_bot} -> - bdd - - {:bdd_top, {map, l, r}} -> - {map, map_difference(:bdd_top, l), map_difference(:bdd_top, r)} - - {{map, l1, r1}, {map, l2, r2}} -> - {map, map_difference(l1, l2), map_difference(r1, r2)} - - {{map1, l1, r1}, {map2, _l2, _r2}} when map1 < map2 -> - {map1, map_difference(l1, bdd2), map_difference(r1, bdd2)} - - {{map1, _l1, _r1}, {map2, l2, r2}} when map1 > map2 -> - {map2, map_difference(bdd1, l2), map_difference(bdd1, r2)} - - # {{map, l, r}, bdd} -> {map, map_difference(l, bdd), map_difference(r, bdd)} + _ -> + bdd_difference(map1, map2) + end end end - # defp map_negation(bdd) do - # case bdd do - # :bdd_bot -> :bdd_top - # :bdd_top -> :bdd_bot - # {map, l, r} -> {map, map_negation(l), map_negation(r)} - # end - # end + defp map_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2) # Intersects two map literals; throws if their intersection is empty. # Both open: the result is open. @@ -3258,71 +2859,10 @@ defmodule Module.Types.Descr do if empty?(type), do: throw(:empty), else: type end - # defp map_difference(_, dnf) when dnf == @map_top, do: [] - # defp map_difference(dnf, dnf), do: [] - - # defp map_difference(dnf1, dnf2) do - # Enum.reduce(dnf2, dnf1, fn - # {:open, fields2, []}, current_dnf when map_size(fields2) == 1 -> - # # Optimization: we are removing an open map with one field. - # Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> - # {key, value, _rest} = :maps.next(:maps.iterator(fields2)) - # t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value) - - # if empty?(t_diff) do - # acc - # else - # {tag, pos} = {tag1, Map.put(fields1, key, t_diff)} - # entry = {tag, pos, negs1} - - # cond do - # :lists.member({tag, pos}, negs1) -> acc - # :lists.member(entry, acc) -> acc - # true -> [entry | acc] - # end - # end - # end) - - # {tag2, fields2, negs2}, current_dnf -> - # Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc -> - # negs = - # if :lists.member({tag2, fields2}, negs1) do - # negs1 - # else - # [{tag2, fields2} | negs1] - # end - - # acc = prepend_to_map_dnf(tag1, fields1, negs, acc) - - # Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc -> - # try do - # {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2) - # prepend_to_map_dnf(tag, fields, negs1, acc) - # catch - # :empty -> acc - # end - # end) - # end) - # end) - # end - - # defp prepend_to_map_dnf(tag, fields, negs, acc) do - # entry = {tag, fields, negs} - - # cond do - # :lists.member({tag, fields}, negs) -> acc - # :lists.member(entry, acc) -> acc - # true -> [entry | acc] - # end - # end - # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - def map_bdd_get(bdd) do - # dbg(bdd) - map_bdd_get([], {:open, %{}}, [], bdd) - end + def map_bdd_get(bdd), do: map_bdd_get([], {:open, %{}}, [], bdd) defp map_bdd_get(acc, {tag, fields} = map, negs, bdd) do case bdd do @@ -3358,7 +2898,7 @@ defmodule Module.Types.Descr do def map_fetch(%{} = descr, key) when is_atom(key) do case :maps.take(:dynamic, descr) do :error -> - if descr_key?(descr, :map) and map_only?(descr) do + if descr_key?(descr, :map) and non_empty_map_only?(descr) do {static_optional?, static_type} = map_fetch_static(descr, key) if static_optional? or empty?(static_type) do @@ -3614,14 +3154,6 @@ defmodule Module.Types.Descr do defp map_put_static(descr, _key, _type), do: descr - defp bdd_map(bdd, fun) do - case bdd do - :bdd_bot -> :bdd_bot - :bdd_top -> :bdd_top - {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)} - end - end - @doc """ Removes a key from a map type. """ @@ -4107,35 +3639,50 @@ defmodule Module.Types.Descr do # Use heuristics to normalize a map dnf for pretty printing. defp map_normalize(bdd) do - for {tag, fields, negs} <- map_bdd_get(bdd) do - {fields, negs} = - Enum.reduce(negs, {fields, []}, fn - # Optimization: we are removing an open map with one field. - {:open, neg_fields}, {acc_fields, acc_negs} when map_size(neg_fields) == 1 -> - {key, value, _rest} = :maps.next(:maps.iterator(neg_fields)) - t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value) - - # If the difference was empty, then the whole line would be empty, which is not. - {Map.put(acc_fields, key, t_diff), acc_negs} - - neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} -> - if non_intersecting_negation?(tag, acc_fields, neg) do - {acc_fields, acc_negs} - else - case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do - {:one, diff_key} -> - {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])), - acc_negs} - - _ -> - {acc_fields, [neg | acc_negs]} - end - end - end) + map_bdd_get(bdd) + |> Enum.map(fn {tag, fields, negs} -> + map_eliminate_while_negs_decrease(tag, fields, negs) + end) + |> map_fusion() + end + # Continue to eliminate negations while length of list of negs decreases + defp map_eliminate_while_negs_decrease(tag, fields, []), do: {tag, fields, []} + + defp map_eliminate_while_negs_decrease(tag, fields, negs) do + n = length(negs) + {fields, negs} = maybe_eliminate_map_negations(tag, fields, negs) + + if length(negs) < n do + map_eliminate_while_negs_decrease(tag, fields, negs) + else {tag, fields, negs} end - |> map_fusion() + end + + defp maybe_eliminate_map_negations(tag, fields, negs) do + Enum.reduce(negs, {fields, []}, fn neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} -> + # If the intersection with the negative is empty, we can remove the negative. + empty_intersection? = + try do + _ = map_literal_intersection(tag, acc_fields, neg_tag, neg_fields) + false + catch + :empty -> true + end + + if empty_intersection? do + {acc_fields, acc_negs} + else + case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do + {:one, diff_key} -> + {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])), acc_negs} + + _ -> + {acc_fields, [neg | acc_negs]} + end + end + end) end # Given a dnf, fuse maps when possible @@ -4189,18 +3736,6 @@ defmodule Module.Types.Descr do end end - # Adapted from `map_empty?` to remove useless negations. - defp non_intersecting_negation?(tag, fields, {neg_tag, neg_fields}) do - (tag == :closed and - Enum.any?(neg_fields, fn {neg_key, neg_type} -> - not is_map_key(fields, neg_key) and not is_optional_static(neg_type) - end)) or - (neg_tag == :closed and - Enum.any?(fields, fn {key, type} -> - not is_map_key(neg_fields, key) and not is_optional_static(type) - end)) - end - defp map_to_quoted(bdd, opts) do map_normalize(bdd) |> Enum.map(&map_each_to_quoted(&1, opts)) @@ -4317,7 +3852,7 @@ defmodule Module.Types.Descr do ## Tuple - # Represents tuple types in two forms: + # Represents tuple types as a BDD with nodes of the following forms: # 1. Closed tuples: Fixed-length tuples with specific element types # Example: {integer(), atom()} # 2. Open tuples: Variable-length tuples with a minimum set of element types @@ -4374,28 +3909,17 @@ defmodule Module.Types.Descr do {acc, dynamic?} end - defp tuple_new(tag, elements), do: [{tag, elements}] - - defp tuple_intersection(dnf1, dnf2) do - for {tag1, elements1} <- dnf1, - {tag2, elements2} <- dnf2, - reduce: [] do - acc -> - case tuple_literal_intersection(tag1, elements1, tag2, elements2) do - {tag, elements} -> - entry = {tag, elements} - - case :lists.member(entry, acc) do - true -> acc - false -> [entry | acc] - end + defp tuple_new(tag, elements), do: tuple_literal(tag, elements) - :empty -> - acc - end + defp tuple_intersection(tuple_literal(tag1, elements1), tuple_literal(tag2, elements2)) do + case tuple_literal_intersection(tag1, elements1, tag2, elements2) do + {tag, elements} -> tuple_literal(tag, elements) + :empty -> :bdd_bot end end + defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2) + defp tuple_literal_intersection(tag1, elements1, tag2, elements2) do n = length(elements1) m = length(elements2) @@ -4428,19 +3952,108 @@ defmodule Module.Types.Descr do zip_non_empty_intersection!(rest1, rest2, [non_empty_intersection!(type1, type2) | acc]) end - defp tuple_difference(_, dnf) when dnf == @tuple_top do - 0 + defp tuple_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2) + + defp tuple_empty?(bdd), do: tuple_bdd_to_dnf(bdd) == [] + + # No negations, so not empty unless there's an empty type + # Note: since the extraction from the BDD is done in a way that guarantees that + # the elements are non-empty, we can avoid checking for empty types there. + # Otherwise, tuple_empty?(_, elements, []) would be Enum.any?(elements, &empty?/1) + defp tuple_empty?(_, _, []), do: false + # Open empty negation makes it empty + defp tuple_empty?(_, _, [{:open, []} | _]), do: true + # Open positive can't be emptied by a single closed negative + defp tuple_empty?(:open, _pos, [{:closed, _}]), do: false + + defp tuple_empty?(tag, elements, [{neg_tag, neg_elements} | negs]) do + n = length(elements) + m = length(neg_elements) + + # Scenarios where the difference is guaranteed to be empty: + # 1. When removing larger tuples from a fixed-size positive tuple + # 2. When removing smaller tuples from larger tuples + if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do + tuple_empty?(tag, elements, negs) + else + case element_intersection(elements, neg_elements) do + :empty -> + tuple_empty?(tag, elements, negs) + + _ -> + tuple_elements_empty?([], tag, elements, neg_elements, negs) and + tuple_compatibility(n, m, tag, elements, neg_tag, negs) + end + end + end + + # Recursively check elements for emptiness + defp tuple_elements_empty?(_, _, _, [], _), do: true + + defp tuple_elements_empty?(acc_meet, tag, elements, [neg_type | neg_elements], negs) do + # Handles the case where {tag, elements} is an open tuple, like {:open, []} + {ty, elements} = List.pop_at(elements, 0, term()) + diff = difference(ty, neg_type) + meet = intersection(ty, neg_type) + + # In this case, there is no intersection between the positive and this negative. + # So we should just "go next" + (empty?(diff) or tuple_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and + tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs) + end + + # Function that, given two tuples {tag1, elements1} and {tag2, elements2}, computes the + # intersection of all their elements (with default term() if one is open). + # If any intersection is empty, it return :empty. Else, it should return the list of them. + defp element_intersection(elements1, elements2) do + elements1 = + if length(elements1) < length(elements2), + do: tuple_fill(elements1, length(elements2)), + else: elements1 + + elements2 = + if length(elements1) > length(elements2), + do: tuple_fill(elements2, length(elements1)), + else: elements2 + + Enum.reduce_while(Enum.zip(elements1, elements2), [], fn {type1, type2}, acc -> + case intersection(type1, type2) do + :empty -> {:halt, :empty} + meet -> {:cont, [meet | acc]} + end + end) + |> case do + :empty -> :empty + list -> Enum.reverse(list) + end end - defp tuple_difference(dnf1, dnf2) do - Enum.reduce(dnf2, dnf1, fn {tag2, elements2}, dnf1 -> - Enum.reduce(dnf1, [], fn {tag1, elements1}, acc -> - tuple_eliminate_single_negation(tag1, elements1, {tag2, elements2}) - |> tuple_union(acc) + # Determines if the set difference is empty when: + # - Positive tuple: {tag, elements} of size n + # - Negative tuple: open or closed tuples of size m + defp tuple_compatibility(n, m, tag, elements, neg_tag, negs) do + # The tuples to consider are all those of size n to m - 1, and if the negative tuple is + # closed, we also need to consider tuples of size greater than m + 1. + tag == :closed or + (Enum.all?(n..(m - 1)//1, &tuple_empty?(:closed, tuple_fill(elements, &1), negs)) and + (neg_tag == :open or tuple_empty?(:open, tuple_fill(elements, m + 1), negs))) + end + + defp tuple_eliminate_negations(tag, elements, negs) do + Enum.reduce(negs, [{tag, elements}], fn {neg_tag, neg_elements}, acc -> + Enum.flat_map(acc, fn {tag, elements} -> + tuple_eliminate_single_negation(tag, elements, {neg_tag, neg_elements}) end) end) end + defp empty_element_intersection?(elements1, elements2) do + Enum.any?(Enum.zip(elements1, elements2), fn {type1, type2} -> + empty?(intersection(type1, type2)) + end) + end + + # Important: this generates DISJOINT tuples. defp tuple_eliminate_single_negation(tag, elements, {neg_tag, neg_elements}) do n = length(elements) m = length(neg_elements) @@ -4448,34 +4061,67 @@ defmodule Module.Types.Descr do # Scenarios where the difference is guaranteed to be empty: # 1. When removing larger tuples from a fixed-size positive tuple # 2. When removing smaller tuples from larger tuples - if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do + # 3. When there is no intersection between the elements of the two tuples + if (tag == :closed and n < m) or (neg_tag == :closed and n > m) or + empty_element_intersection?(elements, neg_elements) do [{tag, elements}] else - tuple_union( + tuple_dnf_union( tuple_elim_content([], tag, elements, neg_elements), tuple_elim_size(n, m, tag, elements, neg_tag) ) end end - # Eliminates negations according to tuple content. - defp tuple_elim_content(_acc, _tag, _elements, []), do: [] - - # Subtracts each element of a negative tuple to build a new tuple with the difference. - # Example: {number(), atom()} and not {float(), :foo} contains types {integer(), :foo} - # as well as {float(), atom() and not :foo} - # Same process as tuple_elements_empty? + # Build a disjoint disjunction for {t1,...,tn} ∧ not {u1,...,un} + # by splitting on the *earliest* index where they differ. + # + # Invariant: + # - `acc` holds the prefix we've already forced to *match* the negative tuple, + # stored in reverse order (so we can `Enum.reverse/2` at the end when we emit). + # - `elements` are the yet-unprocessed positive tuple element types. + # - `neg_elements` are the corresponding negative tuple element types. + # + # For position i: + # - One branch mismatches here: (ti \ ui), with earlier positions fixed to intersection(tj, uj). + # - The other recursive path forces match here: intersection(ti, ui) and continues to i+1. + # + # This yields disjoint branches like: + # {t1∧¬u1, t2, t3, ...} OR {t1∧u1, t2∧¬u2, t3, ...} OR {t1∧u1, t2∧u2, t3∧¬u3, ...} ... defp tuple_elim_content(acc, tag, elements, [neg_type | neg_elements]) do - {ty, elements} = List.pop_at(elements, 0, term()) + # If `elements` is shorter, default to top type `term()` (as in your example). + {ty, rest} = List.pop_at(elements, 0, term()) + + # ti \ ui (i.e., ti ∧ ¬ui) diff = difference(ty, neg_type) + # ti ∧ ui + meet = intersection(ty, neg_type) + + # Branch where the earliest difference is *here*. + # Earlier positions are the accumulated matches in `acc`; + # later positions remain unconstrained (`rest` as-is). + here_branch = + if empty?(diff) do + [] + else + [{tag, Enum.reverse(acc, [diff | rest])}] + end - res = tuple_elim_content([ty | acc], tag, elements, neg_elements) + # Branches where we force equality here and defer the first difference to later positions. + later_branches = + if empty?(meet) do + [] + else + tuple_elim_content([meet | acc], tag, rest, neg_elements) + end - if empty?(diff) do - res - else - [{tag, Enum.reverse(acc, [diff | elements])} | res] - end + here_branch ++ later_branches + end + + # No more negative elements to process: there is no “all-equal” branch to add, + # because we’re constructing {t} ∧ ¬{u}, which must differ somewhere. + defp tuple_elim_content(_acc, _tag, _elements, []) do + [] end # Eliminates negations according to size @@ -4498,8 +4144,8 @@ defmodule Module.Types.Descr do ) end - defp tuple_union(dnf1, dnf2) do - # Union is just concatenation, but we rely on some optimization strategies to + defp tuple_dnf_union(dnf1, dnf2) do + # Union of tuple DNFs is just concatenation, but we rely on some optimization strategies to # avoid the list to grow when possible # first pass trying to identify patterns where two maps can be fused as one @@ -4513,6 +4159,18 @@ defmodule Module.Types.Descr do end end + defp tuple_union( + tuple_literal(tag1, elements1) = tuple1, + tuple_literal(tag2, elements2) = tuple2 + ) do + case maybe_optimize_tuple_union({tag1, elements1}, {tag2, elements2}) do + {tag, elements} -> tuple_literal(tag, elements) + nil -> bdd_union(tuple1, tuple2) + end + end + + defp tuple_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2) + defp maybe_optimize_tuple_union({tag1, pos1} = tuple1, {tag2, pos2} = tuple2) do case tuple_union_optimization_strategy(tag1, pos1, tag2, pos2) do :all_equal -> @@ -4599,22 +4257,57 @@ defmodule Module.Types.Descr do if subtype?(v2, v1), do: :right_subtype_of_left end - defp tuple_to_quoted(dnf, opts) do - dnf + defp tuple_to_quoted(bdd, opts) do + tuple_bdd_to_dnf_no_negations(bdd) |> tuple_fusion() |> Enum.map(&tuple_literal_to_quoted(&1, opts)) end - # Given a dnf of tuples, fuses the tuple unions when possible, + # Transforms a bdd into a dnf (union of tuples with negations) + def tuple_bdd_to_dnf(bdd), + do: tuple_bdd_get([], {:open, []}, [], bdd, &{&1, &2, &3}, &[&1 | &2]) + + # Transforms a bdd into a positive normal form (union of tuples with no negations) + # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates + defp tuple_bdd_to_dnf_no_negations(bdd), + do: tuple_bdd_get([], {:open, []}, [], bdd, &tuple_eliminate_negations/3, &tuple_dnf_union/2) + + defp tuple_bdd_get(acc, {tag, elements} = tuple, negs, bdd, transform, compose) do + case bdd do + :bdd_bot -> + acc + + :bdd_top -> + if tuple_empty?(tag, elements, negs) do + acc + else + compose.(transform.(tag, elements, negs), acc) + end + + {{next_tag, next_elements} = next_tuple, left, right} -> + acc = + case tuple_literal_intersection(tag, elements, next_tag, next_elements) do + :empty -> + acc + + new_tuple -> + tuple_bdd_get(acc, new_tuple, negs, left, transform, compose) + end + + tuple_bdd_get(acc, tuple, [next_tuple | negs], right, transform, compose) + end + end + + # Given a union of tuples, fuses the tuple unions when possible, # e.g. {integer(), atom()} or {float(), atom()} into {number(), atom()} # The negations of two fused tuples are just concatenated. - defp tuple_fusion(dnf) do + defp tuple_fusion(dnf_no_negations) do # Steps: # 1. Consider tuples without negations apart from those with # 2. Group tuples by size and tag # 3. Try fusions for each group until no fusion is found # 4. Merge the groups back into a dnf - dnf + dnf_no_negations |> Enum.group_by(fn {tag, elems} -> {tag, length(elems)} end) |> Enum.flat_map(fn {_, tuples} -> tuple_non_negated_fuse(tuples) end) end @@ -4688,7 +4381,7 @@ defmodule Module.Types.Descr do def tuple_fetch(%{} = descr, key) when is_integer(key) do case :maps.take(:dynamic, descr) do :error -> - if descr_key?(descr, :tuple) and tuple_only?(descr) do + if descr_key?(descr, :tuple) and non_empty_tuple_only?(descr) do {static_optional?, static_type} = tuple_fetch_static(descr, key) # If I access a static tuple at a "open position", we have two options: @@ -4732,6 +4425,13 @@ defmodule Module.Types.Descr do defp tuple_only?(descr), do: empty?(Map.delete(descr, :tuple)) + defp non_empty_tuple_only?(descr) do + case :maps.take(:tuple, descr) do + :error -> false + {tuple_bdd, rest} -> empty?(rest) and not tuple_empty?(tuple_bdd) + end + end + defp tuple_fetch_static(descr, index) when is_integer(index) do case descr do :term -> {true, term()} @@ -4740,8 +4440,9 @@ defmodule Module.Types.Descr do end end - defp tuple_get(dnf, index) do - Enum.reduce(dnf, none(), fn + defp tuple_get(bdd, index) do + tuple_bdd_to_dnf_no_negations(bdd) + |> Enum.reduce(none(), fn {tag, elements}, acc -> Enum.at(elements, index, tuple_tag_to_type(tag)) |> union(acc) end) end @@ -4755,23 +4456,24 @@ defmodule Module.Types.Descr do case :maps.take(:dynamic, descr) do :error -> if tuple_only?(descr) do - process_tuples_values(Map.get(descr, :tuple, [])) + process_tuples_values(Map.get(descr, :tuple, :bdd_bot)) else :badtuple end {dynamic, static} -> if tuple_only?(static) and descr_key?(dynamic, :tuple) do - dynamic(process_tuples_values(Map.get(dynamic, :tuple, []))) - |> union(process_tuples_values(Map.get(static, :tuple, []))) + dynamic(process_tuples_values(Map.get(dynamic, :tuple, :bdd_bot))) + |> union(process_tuples_values(Map.get(static, :tuple, :bdd_bot))) else :badtuple end end end - defp process_tuples_values(dnf) do - Enum.reduce(dnf, none(), fn {tag, elements}, acc -> + defp process_tuples_values(bdd) do + tuple_bdd_to_dnf_no_negations(bdd) + |> Enum.reduce(none(), fn {tag, elements}, acc -> cond do Enum.any?(elements, &empty?/1) -> none() tag == :open -> term() @@ -4830,8 +4532,8 @@ defmodule Module.Types.Descr do def tuple_delete_at(_, _), do: :badindex # Takes a static map type and removes an index from it. - defp tuple_delete_static(%{tuple: dnf}, index) do - %{tuple: Enum.map(dnf, fn {tag, elements} -> {tag, List.delete_at(elements, index)} end)} + defp tuple_delete_static(%{tuple: bdd}, index) do + %{tuple: bdd_map(bdd, fn {tag, elements} -> {tag, List.delete_at(elements, index)} end)} end # If there is no map part to this static type, there is nothing to delete. @@ -4894,8 +4596,8 @@ defmodule Module.Types.Descr do defp tuple_insert_static(descr, _, _) when descr == @none, do: none() defp tuple_insert_static(descr, index, type) do - Map.update!(descr, :tuple, fn dnf -> - Enum.map(dnf, fn {tag, elements} -> + Map.update!(descr, :tuple, fn bdd -> + bdd_map(bdd, fn {tag, elements} -> {tag, List.insert_at(elements, index, type)} end) end) @@ -4907,16 +4609,98 @@ defmodule Module.Types.Descr do defp tuple_of_size_at_least_static?(descr, index) do case descr do - %{tuple: dnf} -> - Enum.all?(dnf, fn - {_, elements} -> length(elements) >= index - end) + %{tuple: bdd} -> + tuple_bdd_to_dnf_no_negations(bdd) + |> Enum.all?(fn {_, elements} -> length(elements) >= index end) %{} -> true end end + ## BDD helpers + + # Leaf cases + defp bdd_intersection(_, :bdd_bot), do: :bdd_bot + defp bdd_intersection(:bdd_bot, _), do: :bdd_bot + defp bdd_intersection(:bdd_top, other), do: other + defp bdd_intersection(other, :bdd_top), do: other + + # Internal-node cases + # Keeping the invariant that literals are ordered ensures nodes are not duplicated down + defp bdd_intersection({lit, l1, r1}, {lit, l2, r2}), + do: {lit, bdd_intersection(l1, l2), bdd_intersection(r1, r2)} + + defp bdd_intersection({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2, + do: {lit1, bdd_intersection(l1, bdd2), bdd_intersection(r1, bdd2)} + + defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, + do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)} + + defp bdd_difference(bdd1, bdd2) do + case {bdd1, bdd2} do + {:bdd_bot, _} -> + :bdd_bot + + {other, :bdd_bot} -> + other + + {:bdd_top, {lit, l, r}} -> + {lit, bdd_difference(:bdd_top, l), bdd_difference(:bdd_top, r)} + + {_, :bdd_top} -> + :bdd_bot + + {{lit, l1, r1}, {lit, l2, r2}} -> + {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)} + + {{lit1, l1, r1}, {lit2, _, _} = bdd2} when lit1 < lit2 -> + {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)} + + {{lit1, _, _} = bdd1, {lit2, l2, r2}} when lit1 > lit2 -> + {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)} + end + end + + # defp bdd_difference(:bdd_bot, _), do: :bdd_bot + # defp bdd_difference(other, :bdd_bot), do: other + # defp bdd_difference(:bdd_top, other), do: bdd_negation(other) + # defp bdd_difference(_, :bdd_top), do: :bdd_bot + + # defp bdd_difference({lit, l1, r1}, {lit, l2, r2}), + # do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)} + + # defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2, + # do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)} + + # defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, + # do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)} + + # defp bdd_negation(:bdd_bot), do: :bdd_top + # defp bdd_negation(:bdd_top), do: :bdd_bot + # defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)} + + defp bdd_union(:bdd_top, _), do: :bdd_top + defp bdd_union(_, :bdd_top), do: :bdd_top + defp bdd_union(:bdd_bot, other), do: other + defp bdd_union(other, :bdd_bot), do: other + defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)} + + # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree + defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2, + do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)} + + defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, + do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)} + + defp bdd_map(bdd, fun) do + case bdd do + :bdd_bot -> :bdd_bot + :bdd_top -> :bdd_top + {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)} + end + end + ## Pairs # To simplify disjunctive normal forms of e.g., map types, it is useful to diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index f406adb2969..0383a2a17da 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -637,13 +637,14 @@ defmodule Module.Types.DescrTest do ) # Nested lists with last element + # "lists of (lists of integers), ending with atom" + # minus + # "lists of (lists of numbers), ending with boolean" + # gives: + # "non empty lists of (lists of integers), ending with (atom and not boolean)" + assert difference(list(list(integer()), atom()), list(list(number()), boolean())) - |> equal?( - union( - non_empty_list(list(integer()), difference(atom(), boolean())), - non_empty_list(difference(list(integer()), list(number())), atom()) - ) - ) + |> equal?(non_empty_list(list(integer()), difference(atom(), boolean()))) # Union types in last element assert difference(list(integer(), union(atom(), binary())), list(number(), atom())) @@ -1538,11 +1539,12 @@ defmodule Module.Types.DescrTest do test "map_fetch" do assert map_fetch(term(), :a) == :badmap assert map_fetch(union(open_map(), integer()), :a) == :badmap + assert map_fetch(difference(open_map(), open_map()), :a) == :badmap + assert map_fetch(difference(closed_map(a: integer()), closed_map(a: term())), :a) == :badmap assert map_fetch(open_map(), :a) == :badkey assert map_fetch(open_map(a: not_set()), :a) == :badkey assert map_fetch(union(closed_map(a: integer()), closed_map(b: atom())), :a) == :badkey - assert map_fetch(difference(closed_map(a: integer()), closed_map(a: term())), :a) == :badkey assert map_fetch(closed_map(a: integer()), :a) == {false, integer()} @@ -2361,7 +2363,7 @@ defmodule Module.Types.DescrTest do ) |> union(difference(open_map(x: atom()), open_map(x: boolean()))) |> to_quoted_string() == - "%{..., a: integer(), b: atom(), c: boolean()} or %{..., x: atom() and not boolean()}" + "%{..., a: integer(), b: atom(), c: boolean()} or\n (%{..., x: atom() and not boolean()} and not %{..., a: integer(), b: atom(), c: boolean()})" assert closed_map(a: number(), b: atom(), c: pid()) |> difference(closed_map(a: integer(), b: atom(), c: pid())) @@ -2375,6 +2377,11 @@ defmodule Module.Types.DescrTest do # Remark: this simplification is order dependent. Having the first difference # after the second gives a different result. + assert open_map(a: number(), b: atom(), c: union(pid(), port())) + |> difference(open_map(a: integer(), b: atom(), c: union(pid(), port()))) + |> difference(open_map(a: float(), b: atom(), c: pid())) + |> to_quoted_string() == "%{..., a: float(), b: atom(), c: port()}" + assert open_map(a: number(), b: atom(), c: union(pid(), port())) |> difference(open_map(a: float(), b: atom(), c: pid())) |> difference(open_map(a: integer(), b: atom(), c: union(pid(), port()))) diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 4c24c59deca..6ace9373191 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2056,36 +2056,35 @@ defmodule Module.Types.ExprTest do # ) # end - test "typecheck! finishes within 200 ms for Oban-style pattern match" do - timeout_ms = 200 - - task = - Task.async(fn -> - typecheck!(fn - [:oban, :job, _event], _measure, _meta, _opts -> :ok - [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok - [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok - [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok - [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok - [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok - [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok - _event, _measure, _meta, _opts -> :ok - end) - end) + test "typecheck! must finish fast for large pattern match" do + type = + typecheck!(fn + [:oban, :job, _event], _measure, _meta, _opts -> + :ok - case Task.yield(task, timeout_ms) || Task.shutdown(task, :brutal_kill) do - {:ok, type} -> - assert type - |> equal?( - fun( - [term(), term(), term(), term()], - dynamic(atom([:ok])) - ) - ) + [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> + :ok + + [:oban, :peer, :election, :stop], _measure, _meta, _opts -> + :ok + + [:oban, :plugin, :exception], _measure, _meta, _opts -> + :ok + + [:oban, :plugin, :stop], _measure, _meta, _opts -> + :ok + + [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> + :ok + + [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> + :ok + + _event, _measure, _meta, _opts -> + :ok + end) - nil -> - flunk("typecheck! did not finish within #{timeout_ms} ms") - end + assert subtype?(type, fun([term(), term(), term(), term()], atom([:ok]))) end end From 415a3a2ecf6eb525f854901c4058de708294ba38 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 4 Aug 2025 18:13:27 +0200 Subject: [PATCH 07/32] Cleanup --- lib/elixir/lib/module/types/descr.ex | 453 +++++++----------- .../test/elixir/module/types/expr_test.exs | 34 +- 2 files changed, 188 insertions(+), 299 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 09c0faa4ce8..3e335b01e71 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -48,7 +48,7 @@ defmodule Module.Types.Descr do {:domain_key, :list} ] - @fun_top :fun_top + @fun_top :bdd_top @atom_top {:negation, :sets.new(version: 2)} @map_top {{:open, %{}}, :bdd_top, :bdd_bot} @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot} @@ -178,11 +178,25 @@ defmodule Module.Types.Descr do Enum.reduce(funs, &intersection/2) end - # This is an insertion of an arrow {domain, return} into a list of non-overlapping arrows. - # If no arrow overlaps with the new arrow, it will be inserted at the end. - # For any arrow that overlaps, we split this arrow into two: one where the domains intersect, - # and one where the domains differ. Then we continue the recursion with the domain subtracted - # from the one of the overlapping arrow. + # Inserts a new arrow `{domain, return}` into `acc`, a list whose arrows + # have disjoint domains. + # + # To preserve that invariant we compare the new arrow with every function in + # the accumulator, `{acc_domain, acc_return}`: + # + # * If `intersection(domain, acc_domain)` is empty, the arrows do not overlap. + # We keep the current arrow and recurse on the tail. + # + # * Otherwise, the domains overlap. We partition them into: + # + # common = intersection(domain, acc_domain) # shared part + # diff = difference(domain, acc_domain) # only in new arrow + # left = difference(acc_domain, domain) # only in existing arrow + # + # We emit `{common, union(return, acc_return)}` for the shared part, + # keep `{left, acc_return}` (if any), and continue inserting `diff` + # into the remainder of the list to handle further overlaps. + defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do common = intersection(domain, acc_domain) @@ -449,7 +463,7 @@ defmodule Module.Types.Descr do defp intersection(:fun, v1, v2) do bdd = fun_intersection(v1, v2) - if bdd == :fun_bottom, do: 0, else: bdd + if bdd == :bdd_bot, do: 0, else: bdd end defp intersection(:dynamic, v1, v2) do @@ -471,10 +485,6 @@ defmodule Module.Types.Descr do {right_dynamic, right_static} = Map.pop(right, :dynamic, right) dynamic_part = difference_static(left_dynamic, right_static) - # This might be the worst place possible to check for emptiness. - # if empty?(dynamic_part), - # do: none(), - # else: Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part) else difference_static(left, right) @@ -547,7 +557,7 @@ defmodule Module.Types.Descr do defp difference(:fun, v1, v2) do bdd = fun_difference(v1, v2) - if bdd == :fun_bottom, do: 0, else: bdd + if bdd == :bdd_bot, do: 0, else: bdd end @doc """ @@ -1078,8 +1088,8 @@ defmodule Module.Types.Descr do ### Key concepts: - # * BDD structure: A tree with function nodes and :fun_top/:fun_bottom leaves. - # Paths to :fun_top represent valid function types. Nodes are positive when + # * BDD structure: A tree with function nodes and :bdd_top/:bdd_bot leaves. + # Paths to :bdd_top represent valid function types. Nodes are positive when # following a left branch (e.g. (int, float -> bool) and negative otherwise. # * Function variance: @@ -1098,7 +1108,7 @@ defmodule Module.Types.Descr do # Note: Function domains are expressed as tuple types. We use separate representations # rather than unary functions with tuple domains to handle special cases like representing # functions of a specific arity (e.g., (none,none->term) for arity 2). - defp fun_new(inputs, output), do: {{inputs, output}, :fun_top, :fun_bottom} + defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot} # Creates a function type from a list of inputs and an output # where the inputs and/or output may be dynamic. @@ -1349,8 +1359,7 @@ defmodule Module.Types.Descr do type_args = args_to_domain(arguments) Enum.reduce(arrows, none(), fn intersection_of_arrows, acc -> - {x, _cache} = aux_apply(acc, type_args, term(), intersection_of_arrows, %{}) - x + aux_apply(acc, type_args, term(), intersection_of_arrows) end) end @@ -1382,67 +1391,39 @@ defmodule Module.Types.Descr do # - arrow_intersections: The list of function arrows to process # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf - defp aux_apply(result, input, rets_reached, [], cache) do - cache_key = {result, input, rets_reached, []} - res = union(result, rets_reached) - {res, Map.put(cache, cache_key, res)} + defp aux_apply(result, _input, rets_reached, []) do + if subtype?(rets_reached, result), do: result, else: union(result, rets_reached) end - defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections], cache) do + defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do # Calculate the part of the input not covered by this arrow's domain - cache_key = {result, input, returns_reached, [{args, ret} | arrow_intersections]} - - case cache do - %{^cache_key => value} -> - {value, cache} - - _ -> - dom = args_to_domain(args) - no_intersection? = empty?(intersection(dom, input)) - - cond do - # First: is there any intersection between the input and the arrow's domain? - # If not, we skip this arrow. - no_intersection? -> - {result, cache} = - aux_apply(result, input, returns_reached, arrow_intersections, cache) - - cache = Map.put(cache, cache_key, result) - {result, cache} - - true -> - dom_subtract = difference(input, dom) - - # Refine the return type by intersecting with this arrow's return type - ret_refine = intersection(returns_reached, ret) - - # Phase 1: Domain partitioning - # If the input is not fully covered by the arrow's domain, then the result type should be - # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered - # parts of the domain. - # - # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite - # both atoms and pids in the result. + dom_subtract = difference(input, args_to_domain(args)) + + # Phase 1: Domain partitioning + # If the input is not fully covered by the arrow's domain, then the result type should be + # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered + # parts of the domain. + # + # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite + # both atoms and pids in the result. + result = + if empty?(dom_subtract) do + result + else + aux_apply(result, dom_subtract, returns_reached, arrow_intersections) + end - {result, cache} = - if empty?(dom_subtract) do - {result, cache} - else - aux_apply(result, dom_subtract, returns_reached, arrow_intersections, cache) - end + # 2. Return type refinement + # The result type is also refined (intersected) in the sense that, if several arrows match + # the same part of the input, then the result type is an intersection of the return types of + # those arrows. - # 2. Return type refinement - # The result type is also refined (intersected) in the sense that, if several arrows match - # the same part of the input, then the result type is an intersection of the return types of - # those arrows. + # Refine the return type by intersecting with this arrow's return type + ret_refine = intersection(returns_reached, ret) - # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer() - # should result in (atom() ∩ pid()), which is none(). - {result, cache} = aux_apply(result, input, ret_refine, arrow_intersections, cache) - cache = Map.put(cache, cache_key, result) - {result, cache} - end - end + # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer() + # should result in (atom() ∩ pid()), which is none(). + aux_apply(result, input, ret_refine, arrow_intersections) end # Takes all the paths from the root to the leaves finishing with a 1, @@ -1452,8 +1433,8 @@ defmodule Module.Types.Descr do defp fun_get(acc, pos, neg, bdd) do case bdd do - :fun_bottom -> acc - :fun_top -> [{pos, neg} | acc] + :bdd_bot -> acc + :bdd_top -> [{pos, neg} | acc] {fun, left, right} -> fun_get(fun_get(acc, [fun | pos], neg, left), pos, [fun | neg], right) end end @@ -1472,15 +1453,9 @@ defmodule Module.Types.Descr do # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty defp fun_empty?(bdd) do case bdd do - :fun_bottom -> - true - - :fun_top -> - false - - bdd -> - fun_get(bdd) - |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end) + :bdd_bot -> true + :bdd_top -> false + bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end) end end @@ -1517,10 +1492,8 @@ defmodule Module.Types.Descr do # Filter positives to only those with matching arity, then check if the negative # function's domain is a supertype of the positive domain and if the phi function # determines emptiness. - neg_dom = args_to_domain(neg_arguments) - length(neg_arguments) == positive_arity and - subtype?(neg_dom, positive_domain) and + subtype?(args_to_domain(neg_arguments), positive_domain) and phi_starter(neg_arguments, neg_return, positives) end) end @@ -1588,7 +1561,6 @@ defmodule Module.Types.Descr do defp phi(args, {b, t}, [], cache) do result = Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)) {result, Map.put(cache, {args, {b, t}, []}, result)} - # {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache} end defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do @@ -1630,8 +1602,8 @@ defmodule Module.Types.Descr do end defp disjoint_non_empty_domains?({arguments, return}, positives) do - b1 = all_disjoint_domains?(positives) - b2 = all_non_empty_domains?([{arguments, return} | positives]) + b1 = all_disjoint_arguments?(positives) + b2 = all_non_empty_arguments?([{arguments, return} | positives]) cond do b1 and b2 -> :disjoint_non_empty @@ -1640,44 +1612,30 @@ defmodule Module.Types.Descr do end end - defp all_non_empty_domains?(positives) do + defp all_non_empty_arguments?(positives) do Enum.all?(positives, fn {args, _ret} -> Enum.all?(args, fn arg -> not empty?(arg) end) end) end - # For two arguments to be disjoint, we need at least one of their types to be disjoint. + # For two arguments to be disjoint, one of their types must be disjoint. defp disjoint_arguments?(args1, args2) do - Enum.reduce_while(Enum.zip(args1, args2), false, fn {t1, t2}, acc -> - t = intersection(t1, t2) - - if empty?(t) do - {:halt, true} - else - {:cont, acc} - end - end) + Enum.any?(Enum.zip(args1, args2), fn {t1, t2} -> disjoint?(t1, t2) end) end - # Test that all positives are two to two disjoint. We iterate on the list to do so. - defp all_disjoint_domains?([]), do: true + defp all_disjoint_arguments?([]), do: true - defp all_disjoint_domains?([{args, _} | rest]) do - Enum.reduce_while(rest, true, fn {args_rest, _}, _acc -> - if disjoint_arguments?(args, args_rest) do - {:cont, true} - else - {:halt, false} - end - end) + defp all_disjoint_arguments?([{args, _} | rest]) do + Enum.all?(rest, fn {args_rest, _} -> disjoint_arguments?(args, args_rest) end) and + all_disjoint_arguments?(rest) end defp fun_union(bdd1, bdd2) do case {bdd1, bdd2} do - {:fun_top, _} -> :fun_top - {_, :fun_top} -> :fun_top - {:fun_bottom, bdd} -> bdd - {bdd, :fun_bottom} -> bdd + {:bdd_top, _} -> :bdd_top + {_, :bdd_top} -> :bdd_top + {:bdd_bot, bdd} -> bdd + {bdd, :bdd_bot} -> bdd {{fun, l1, r1}, {fun, l2, r2}} -> {fun, fun_union(l1, l2), fun_union(r1, r2)} # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. # It is the same as going down bdd1 to insert bdd1 into it. @@ -1686,93 +1644,76 @@ defmodule Module.Types.Descr do end end - defp fun_intersection(bdd1, bdd2) do - # If intersecting with the top type for that arity, no-op - case {bdd1, bdd2} do - {bdd, {{args, return} = fun, :fun_top, :fun_bottom}} when is_tuple(bdd) -> - if return == :term and Enum.all?(args, &(&1 == %{})) and - matching_arity_left?(bdd, length(args)) do - bdd - else - {fun, bdd, :fun_bottom} - end - - {{{args, return} = fun, :fun_top, :fun_bottom}, bdd} when is_tuple(bdd) -> - if return == :term and Enum.all?(args, &(&1 == %{})) and - matching_arity_left?(bdd, length(args)) do - bdd - else - {fun, bdd, :fun_bottom} - end - - _ -> - fun_intersection_recur(bdd1, bdd2) - end - end - - defp matching_arity_left?({{args, _return}, l, r}, arity) do - length(args) == arity and matching_arity_left?(l, arity) and matching_arity_right?(r, arity) + defp is_fun_top?(bdd, {{args, return}, :bdd_top, :bdd_bot}) do + return == :term and Enum.all?(args, &(&1 == %{})) and + matching_arity_left?(bdd, length(args)) end - defp matching_arity_left?(_, _arity), do: true + defp is_fun_top?(_, _), do: false - defp matching_arity_right?({_, l, r}, arity) do - matching_arity_left?(l, arity) and matching_arity_right?(r, arity) + defp fun_intersection(bdd1, bdd2) do + cond do + # If intersecting with the top type for that arity, no-op + is_tuple(bdd2) and is_fun_top?(bdd2, bdd1) -> bdd2 + is_tuple(bdd1) and is_fun_top?(bdd1, bdd2) -> bdd1 + true -> fun_bdd_intersection(bdd1, bdd2) + end end - defp matching_arity_right?(_, _arity), do: true - - defp fun_intersection_recur(bdd1, bdd2) do + defp fun_bdd_intersection(bdd1, bdd2) do case {bdd1, bdd2} do # Base cases - {_, :fun_bottom} -> - :fun_bottom + {_, :bdd_bot} -> + :bdd_bot - {:fun_bottom, _} -> - :fun_bottom + {:bdd_bot, _} -> + :bdd_bot - {:fun_top, bdd} -> + {:bdd_top, bdd} -> bdd - {bdd, :fun_top} -> + {bdd, :bdd_top} -> bdd # Optimizations # If intersecting with a single positive or negative function, we insert # it at the root instead of merging the trees (this avoids going down the # whole bdd). - {bdd, {fun, :fun_top, :fun_bottom}} -> - {fun, bdd, :fun_bottom} + {bdd, {fun, :bdd_top, :bdd_bot}} -> + {fun, bdd, :bdd_bot} - {bdd, {fun, :fun_bottom, :fun_top}} -> - {fun, :fun_bottom, bdd} + {bdd, {fun, :bdd_bot, :bdd_top}} -> + {fun, :bdd_bot, bdd} - {{fun, :fun_top, :fun_bottom}, bdd} -> - {fun, bdd, :fun_bottom} + {{fun, :bdd_top, :bdd_bot}, bdd} -> + {fun, bdd, :bdd_bot} - {{fun, :fun_bottom, :fun_top}, bdd} -> - {fun, :fun_bottom, bdd} + {{fun, :bdd_bot, :bdd_top}, bdd} -> + {fun, :bdd_bot, bdd} # General cases {{fun, l1, r1}, {fun, l2, r2}} -> - {fun, fun_intersection_recur(l1, l2), fun_intersection_recur(r1, r2)} + {fun, fun_bdd_intersection(l1, l2), fun_bdd_intersection(r1, r2)} {{fun, l, r}, bdd} -> - {fun, fun_intersection_recur(l, bdd), fun_intersection_recur(r, bdd)} + {fun, fun_bdd_intersection(l, bdd), fun_bdd_intersection(r, bdd)} end end - defp fun_difference(bdd1, bdd2) do - case {bdd1, bdd2} do - {:fun_bottom, _} -> :fun_bottom - {_, :fun_top} -> :fun_bottom - {bdd, :fun_bottom} -> bdd - {:fun_top, {fun, l, r}} -> {fun, fun_difference(:fun_top, l), fun_difference(:fun_top, r)} - {{fun, l1, r1}, {fun, l2, r2}} -> {fun, fun_difference(l1, l2), fun_difference(r1, r2)} - {{fun, l, r}, bdd} -> {fun, fun_difference(l, bdd), fun_difference(r, bdd)} - end + defp matching_arity_left?({{args, _return}, l, r}, arity) do + length(args) == arity and matching_arity_left?(l, arity) and matching_arity_right?(r, arity) + end + + defp matching_arity_left?(_, _arity), do: true + + defp matching_arity_right?({_, l, r}, arity) do + matching_arity_left?(l, arity) and matching_arity_right?(r, arity) end + defp matching_arity_right?(_, _arity), do: true + + defp fun_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2) + # Converts the static and dynamic parts of descr to its quoted # representation. The goal here is to the opposite of fun_descr # and put static and dynamic parts back together to improve @@ -1947,16 +1888,16 @@ defmodule Module.Types.Descr do list_new(list_type, last_type) {bdd, last_type_no_list} -> - # The argument last_type may include list types; in this case, we aim to add - # those to the main list type, only to keep the type of the final element (which may - # be either the empty list, or some non-list value). - # To do so, we go through the list types in last_type, but since those are stored - # as a bdd of list types, we take care to include the effect of negations on computing - # each last type. - # To see if a negation changes the last type or the list type, we just need to check - # if the negative list type is a supertype of the positive list type. In that case, - # we can remove the negative last type from the positive one. - # (If this subtracted type was empty, the whole type would be empty) + # `last_type` may itself represent one or more list types. + # Our goal is to fold those list types into `list_type` while retaining the + # possible type of the final element (which can be `[]` or any non-list value). + # + # The list types inside `last_type` are stored in a BDD that includes possible + # negations, so we must evaluate each node with its sign taken into account. + # + # A negation only matters when the negated list type is a supertype of the + # corresponding positive list type; in that case we subtract the negated + # variant from the positive one. {list_type, last_type} = list_get_pos(bdd) |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail}, @@ -1965,24 +1906,6 @@ defmodule Module.Types.Descr do {union(head, acc_head), union(tail, acc_tail)} end) - # So for instance if i give term() and `term() and not (list(term())` - # what happens? - # list_type starts with term() and does not change - # last_type starts with everything but :list and [] - # then we iterate over the bdd, which contains... what? it contains - # {:term, :term} and not {:term, %{bitmap: 2}} - # what is bitmap: 2? it is empty_list() - # we only add the positive {:term, :term} to both things - # so we get {:term, :term} lol... that seems wrong, i should not add back the - # empty_list() - # maybe i should get tl on the bdd? - - last_type = - case last_type do - :term -> @not_non_empty_list - other -> Map.delete(other, :list) - end - list_new(list_type, last_type) end end @@ -2011,7 +1934,7 @@ defmodule Module.Types.Descr do acc :bdd_top -> - [{pos, negs} | acc] + if list_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc] {{list, tail} = list_type, left, right} -> new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} @@ -2135,18 +2058,14 @@ defmodule Module.Types.Descr do # 3. Base case: adds bdd2 type to negations of bdd1 type # The result may be larger than the initial bdd1, which is maintained in the accumulator. defp list_difference(list_literal(list1, last1) = bdd1, list_literal(list2, last2) = bdd2) do - cond do - empty?(intersection(list1, list2)) or empty?(intersection(last1, last2)) -> - list_literal(list1, last1) - - subtype?(list1, list2) and subtype?(last1, last2) -> - :bdd_bot - - equal?(list1, list2) -> - list_literal(list1, difference(last1, last2)) + list = intersection(list1, list2) + last = intersection(last1, last2) - true -> - bdd_difference(bdd1, bdd2) + cond do + empty?(list) or empty?(last) -> list_literal(list1, last1) + subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot + equal?(list1, list2) -> list_literal(list1, difference(last1, last2)) + true -> bdd_difference(bdd1, bdd2) end end @@ -2159,9 +2078,9 @@ defmodule Module.Types.Descr do end defp list_empty?(@non_empty_list_top), do: false - defp list_empty?(bdd), do: list_all?(bdd, &list_empty_line?/3) + defp list_empty?(bdd), do: list_all?(bdd, &list_empty?/3) - defp list_empty_line?(list_type, last_type, negs) do + defp list_empty?(list_type, last_type, negs) do last_type = list_tail_unfold(last_type) # To make a list {list, last} empty with some negative lists: # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one. @@ -2172,12 +2091,7 @@ defmodule Module.Types.Descr do Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type -> if subtype?(list_type, neg_type) do d = difference(acc_last_type, neg_last) - - if empty?(d) do - {:halt, nil} - else - {:cont, d} - end + if empty?(d), do: {:halt, nil}, else: {:cont, d} else {:cont, acc_last_type} end @@ -2340,27 +2254,23 @@ defmodule Module.Types.Descr do defp list_normalize(bdd) do list_get(bdd) |> Enum.reduce([], fn {{list, last}, negs}, acc -> - if list_empty_line?(list, last, negs) do - acc - else - # First, try to eliminate the negations from the existing type. - {list, last, negs} = - Enum.uniq(negs) - |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} -> - last = list_tail_unfold(last) - new_list = intersection(list, nlist) - new_last = intersection(last, nlast) - - cond do - # No intersection between the list and the negative - empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs} - subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs} - true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]} - end - end) + # First, try to eliminate the negations from the existing type. + {list, last, negs} = + Enum.uniq(negs) + |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} -> + last = list_tail_unfold(last) + new_list = intersection(list, nlist) + new_last = intersection(last, nlast) - add_to_list_normalize(acc, list, last, negs |> Enum.reverse()) - end + cond do + # No intersection between the list and the negative + empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs} + subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs} + true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]} + end + end) + + add_to_list_normalize(acc, list, last, negs |> Enum.reverse()) end) end @@ -2631,9 +2541,6 @@ defmodule Module.Types.Descr do end end - defp maybe_optimize_map_union(map1, map2), - do: raise("I should not be there: see inputs #{inspect(map1)} and #{inspect(map2)}") - defp map_union_optimization_strategy(tag1, pos1, tag2, pos2) defp map_union_optimization_strategy(tag, pos, tag, pos), do: :all_equal defp map_union_optimization_strategy(:open, empty, _, _) when empty == %{}, do: :any_map @@ -3103,7 +3010,6 @@ defmodule Module.Types.Descr do %{map: {{map_refresh_tag(tag, domain, type), fields}, :bdd_top, :bdd_bot}} end - # TODO: TEST THIS (previous implem was wrong) def map_refresh_domain(%{map: bdd}, domain, type) do # For negations, we count on the idea that a negation will not remove any # type from a domain unless it completely cancels out the type. @@ -4073,7 +3979,7 @@ defmodule Module.Types.Descr do end end - # Build a disjoint disjunction for {t1,...,tn} ∧ not {u1,...,un} + # Build a disjoint disjunction for {t1,...,tn} /\ not {u1,...,un} # by splitting on the *earliest* index where they differ. # # Invariant: @@ -4087,14 +3993,14 @@ defmodule Module.Types.Descr do # - The other recursive path forces match here: intersection(ti, ui) and continues to i+1. # # This yields disjoint branches like: - # {t1∧¬u1, t2, t3, ...} OR {t1∧u1, t2∧¬u2, t3, ...} OR {t1∧u1, t2∧u2, t3∧¬u3, ...} ... + # {t1 /\ not u1, t2, t3, ...} OR {t1 /\ u1, t2 /\ not u2, t3, ...} OR {t1/\u1, t2/\u2, t3/\ not u3, ...} ... defp tuple_elim_content(acc, tag, elements, [neg_type | neg_elements]) do # If `elements` is shorter, default to top type `term()` (as in your example). {ty, rest} = List.pop_at(elements, 0, term()) - # ti \ ui (i.e., ti ∧ ¬ui) + # ti \ ui (i.e., ti and not ui) diff = difference(ty, neg_type) - # ti ∧ ui + # ti /\ ui meet = intersection(ty, neg_type) # Branch where the earliest difference is *here*. @@ -4119,7 +4025,7 @@ defmodule Module.Types.Descr do end # No more negative elements to process: there is no “all-equal” branch to add, - # because we’re constructing {t} ∧ ¬{u}, which must differ somewhere. + # because we’re constructing {t} ant not {u}, which must differ somewhere. defp tuple_elim_content(_acc, _tag, _elements, []) do [] end @@ -4637,48 +4543,23 @@ defmodule Module.Types.Descr do defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)} - defp bdd_difference(bdd1, bdd2) do - case {bdd1, bdd2} do - {:bdd_bot, _} -> - :bdd_bot - - {other, :bdd_bot} -> - other - - {:bdd_top, {lit, l, r}} -> - {lit, bdd_difference(:bdd_top, l), bdd_difference(:bdd_top, r)} - - {_, :bdd_top} -> - :bdd_bot - - {{lit, l1, r1}, {lit, l2, r2}} -> - {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)} - - {{lit1, l1, r1}, {lit2, _, _} = bdd2} when lit1 < lit2 -> - {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)} - - {{lit1, _, _} = bdd1, {lit2, l2, r2}} when lit1 > lit2 -> - {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)} - end - end - - # defp bdd_difference(:bdd_bot, _), do: :bdd_bot - # defp bdd_difference(other, :bdd_bot), do: other - # defp bdd_difference(:bdd_top, other), do: bdd_negation(other) - # defp bdd_difference(_, :bdd_top), do: :bdd_bot + defp bdd_difference(:bdd_bot, _), do: :bdd_bot + defp bdd_difference(other, :bdd_bot), do: other + defp bdd_difference(:bdd_top, other), do: bdd_negation(other) + defp bdd_difference(_, :bdd_top), do: :bdd_bot - # defp bdd_difference({lit, l1, r1}, {lit, l2, r2}), - # do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)} + defp bdd_difference({lit, l1, r1}, {lit, l2, r2}), + do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)} - # defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2, - # do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)} + defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2, + do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)} - # defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, - # do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)} + defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2, + do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)} - # defp bdd_negation(:bdd_bot), do: :bdd_top - # defp bdd_negation(:bdd_top), do: :bdd_bot - # defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)} + defp bdd_negation(:bdd_bot), do: :bdd_top + defp bdd_negation(:bdd_top), do: :bdd_bot + defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)} defp bdd_union(:bdd_top, _), do: :bdd_top defp bdd_union(_, :bdd_top), do: :bdd_top diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 6ace9373191..26c9610736e 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2033,19 +2033,26 @@ defmodule Module.Types.ExprTest do end # test "regressions – duplicate-key list pattern" do - # assert typecheck!( - # # HEAD PATTERN LIST - # [ - # # first tuple - # [ - # {key, _} - # # second tuple + rest - # | [{key, _} | _] = rest - # ] - # ], - # # BODY – we just return the tail we captured - # rest - # ) == + # x = + # typecheck!( + # # HEAD PATTERN LIST + # [ + # # first tuple + # [ + # {key, _} + # # second tuple + rest + # | [{key, _} | _] = rest + # ] + # ], + # # BODY – we just return the tail we captured + # rest + # ) + + # IO.puts("x: #{to_quoted_string(x)}") + # IO.puts("x: #{inspect(x)}") + + # assert x + # |> equal?( # dynamic( # non_empty_list( # # every element is {term, term} @@ -2054,6 +2061,7 @@ defmodule Module.Types.ExprTest do # term() # ) # ) + # ) # end test "typecheck! must finish fast for large pattern match" do From ec5906ba8ccc0740ba548686b45b285e27bea511 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 4 Aug 2025 18:26:07 +0200 Subject: [PATCH 08/32] Updated the handling of positive and negative functions in `fun_normalize` and `fun_get` --- lib/elixir/lib/module/types/descr.ex | 36 +++++++++++----------------- 1 file changed, 14 insertions(+), 22 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 3e335b01e71..400d4cb72ff 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -196,7 +196,6 @@ defmodule Module.Types.Descr do # We emit `{common, union(return, acc_return)}` for the shared part, # keep `{left, acc_return}` (if any), and continue inserting `diff` # into the remainder of the list to handle further overlaps. - defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do common = intersection(domain, acc_domain) @@ -1314,7 +1313,7 @@ defmodule Module.Types.Descr do defp fun_normalize(%{fun: bdd}, arity, mode) do {domain, arrows, bad_arities} = Enum.reduce(fun_get(bdd), {term(), [], []}, fn - {pos_funs, neg_funs}, {domain, arrows, bad_arities} -> + {pos_funs, _neg_funs}, {domain, arrows, bad_arities} -> arrow_arity = case pos_funs do [{args, _} | _] -> length(args) @@ -1325,9 +1324,6 @@ defmodule Module.Types.Descr do arrow_arity != arity -> {domain, arrows, [arrow_arity | bad_arities]} - fun_empty?(pos_funs, neg_funs) -> - {domain, arrows, bad_arities} - true -> # Calculate domain from all positive functions path_domain = @@ -1363,13 +1359,13 @@ defmodule Module.Types.Descr do end) end - defp apply_disjoint(arguments, arrows) do - type_args = args_to_domain(arguments) + # A fast way to do function application when the arguments of the function are disjoint. + # Just build the union of all the return types of arrows that match the input. + defp apply_disjoint(input_arguments, arrows) do + type_input = args_to_domain(input_arguments) Enum.reduce(arrows, none(), fn {args, ret}, acc_return -> - dom = args_to_domain(args) - - if empty?(intersection(dom, type_args)) do + if empty?(intersection(args_to_domain(args), type_input)) do acc_return else union(acc_return, ret) @@ -1399,6 +1395,9 @@ defmodule Module.Types.Descr do # Calculate the part of the input not covered by this arrow's domain dom_subtract = difference(input, args_to_domain(args)) + # Refine the return type by intersecting with this arrow's return type + ret_refine = intersection(returns_reached, ret) + # Phase 1: Domain partitioning # If the input is not fully covered by the arrow's domain, then the result type should be # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered @@ -1418,9 +1417,6 @@ defmodule Module.Types.Descr do # the same part of the input, then the result type is an intersection of the return types of # those arrows. - # Refine the return type by intersecting with this arrow's return type - ret_refine = intersection(returns_reached, ret) - # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer() # should result in (atom() ∩ pid()), which is none(). aux_apply(result, input, ret_refine, arrow_intersections) @@ -1434,7 +1430,7 @@ defmodule Module.Types.Descr do defp fun_get(acc, pos, neg, bdd) do case bdd do :bdd_bot -> acc - :bdd_top -> [{pos, neg} | acc] + :bdd_top -> if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] {fun, left, right} -> fun_get(fun_get(acc, [fun | pos], neg, left), pos, [fun | neg], right) end end @@ -1451,13 +1447,7 @@ defmodule Module.Types.Descr do # - `fun(1) and not fun(1)` is empty # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty - defp fun_empty?(bdd) do - case bdd do - :bdd_bot -> true - :bdd_top -> false - bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end) - end - end + defp fun_empty?(bdd), do: fun_get(bdd) == [] # Checks if a function type represented by positive and negative function literals is empty. @@ -1660,6 +1650,8 @@ defmodule Module.Types.Descr do end end + # Note: using this for functions instead of bdd_intersection because the printing + # fun_denormalize relies on the order of functions in the bdd. defp fun_bdd_intersection(bdd1, bdd2) do case {bdd1, bdd2} do # Base cases @@ -1817,7 +1809,7 @@ defmodule Module.Types.Descr do end defp fun_get_pos(bdd) do - for {pos, negs} <- fun_get(bdd), not fun_empty?(pos, negs) do + for {pos, _negs} <- fun_get(bdd) do fun_filter_subset(pos, []) end end From f933a16843d932f61057f7975d04dacf949134ee Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 4 Aug 2025 18:38:38 +0200 Subject: [PATCH 09/32] Remove commented-out test --- .../test/elixir/module/types/expr_test.exs | 32 ------------------- 1 file changed, 32 deletions(-) diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 26c9610736e..7d19fbb73a3 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -2032,38 +2032,6 @@ defmodule Module.Types.ExprTest do ) == dynamic(integer()) end - # test "regressions – duplicate-key list pattern" do - # x = - # typecheck!( - # # HEAD PATTERN LIST - # [ - # # first tuple - # [ - # {key, _} - # # second tuple + rest - # | [{key, _} | _] = rest - # ] - # ], - # # BODY – we just return the tail we captured - # rest - # ) - - # IO.puts("x: #{to_quoted_string(x)}") - # IO.puts("x: #{inspect(x)}") - - # assert x - # |> equal?( - # dynamic( - # non_empty_list( - # # every element is {term, term} - # tuple([term(), term()]), - # # the tail can be anything - # term() - # ) - # ) - # ) - # end - test "typecheck! must finish fast for large pattern match" do type = typecheck!(fn From 654b2b526bca5a0bd5624f8724b3f6d69462c47c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Mon, 1 Sep 2025 15:35:43 +0200 Subject: [PATCH 10/32] Move test to proper clause --- .../test/elixir/module/types/expr_test.exs | 62 +++++++++---------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs index 7d19fbb73a3..cdd70f60f07 100644 --- a/lib/elixir/test/elixir/module/types/expr_test.exs +++ b/lib/elixir/test/elixir/module/types/expr_test.exs @@ -291,6 +291,37 @@ defmodule Module.Types.ExprTest do (term() -> dynamic({:ok, term()})) """ end + + test "works when there are multiple clauses with lists and maps" do + type = + typecheck!(fn + [:oban, :job, _event], _measure, _meta, _opts -> + :ok + + [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> + :ok + + [:oban, :peer, :election, :stop], _measure, _meta, _opts -> + :ok + + [:oban, :plugin, :exception], _measure, _meta, _opts -> + :ok + + [:oban, :plugin, :stop], _measure, _meta, _opts -> + :ok + + [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> + :ok + + [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> + :ok + + _event, _measure, _meta, _opts -> + :ok + end) + + assert subtype?(type, fun([term(), term(), term(), term()], atom([:ok]))) + end end describe "remotes" do @@ -2031,37 +2062,6 @@ defmodule Module.Types.ExprTest do ) ) == dynamic(integer()) end - - test "typecheck! must finish fast for large pattern match" do - type = - typecheck!(fn - [:oban, :job, _event], _measure, _meta, _opts -> - :ok - - [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> - :ok - - [:oban, :peer, :election, :stop], _measure, _meta, _opts -> - :ok - - [:oban, :plugin, :exception], _measure, _meta, _opts -> - :ok - - [:oban, :plugin, :stop], _measure, _meta, _opts -> - :ok - - [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> - :ok - - [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> - :ok - - _event, _measure, _meta, _opts -> - :ok - end) - - assert subtype?(type, fun([term(), term(), term(), term()], atom([:ok]))) - end end describe "info" do From 67e8ab5951a166e424c9604f731c41f963223a77 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 1 Sep 2025 16:54:34 +0200 Subject: [PATCH 11/32] Fixed a bug on disjoint?\2 due to incorrect special cases --- lib/elixir/lib/module/types/descr.ex | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 400d4cb72ff..2d65cf0d1a5 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -754,24 +754,12 @@ defmodule Module.Types.Descr do def disjoint?(%{dynamic: :term}, other), do: empty?(remove_optional(other)) def disjoint?(other, %{dynamic: :term}), do: empty?(remove_optional(other)) + # Two gradual types are disjoint if their upper bounds are disjoint. def disjoint?(left, right) do - left = unfold(left) - right = unfold(right) - is_gradual_left = gradual?(left) - is_gradual_right = gradual?(right) + left_upper = unfold(left) |> Map.get(:dynamic, left) + right_upper = unfold(right) |> Map.get(:dynamic, right) - cond do - is_gradual_left and not is_gradual_right -> - right_with_dynamic = Map.put(right, :dynamic, right) - not non_disjoint_intersection?(left, right_with_dynamic) - - is_gradual_right and not is_gradual_left -> - left_with_dynamic = Map.put(left, :dynamic, left) - not non_disjoint_intersection?(left_with_dynamic, right) - - true -> - not non_disjoint_intersection?(left, right) - end + not non_disjoint_intersection?(left_upper, right_upper) end @doc """ From bc49349dd8684411e4c8fc7d7333553cc49da536 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 1 Sep 2025 19:00:09 +0200 Subject: [PATCH 12/32] Optimization suggested --- lib/elixir/lib/module/types/descr.ex | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 2d65cf0d1a5..5c1cae5fdd6 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2038,11 +2038,8 @@ defmodule Module.Types.Descr do # 3. Base case: adds bdd2 type to negations of bdd1 type # The result may be larger than the initial bdd1, which is maintained in the accumulator. defp list_difference(list_literal(list1, last1) = bdd1, list_literal(list2, last2) = bdd2) do - list = intersection(list1, list2) - last = intersection(last1, last2) - cond do - empty?(list) or empty?(last) -> list_literal(list1, last1) + disjoint?(list1, list2) or disjoint?(last1, last2) -> list_literal(list1, last1) subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot equal?(list1, list2) -> list_literal(list1, difference(last1, last2)) true -> bdd_difference(bdd1, bdd2) @@ -4171,13 +4168,11 @@ defmodule Module.Types.Descr do end {{next_tag, next_elements} = next_tuple, left, right} -> + # If an intersection of tuples is empty, the line is empty and we skip it. acc = case tuple_literal_intersection(tag, elements, next_tag, next_elements) do - :empty -> - acc - - new_tuple -> - tuple_bdd_get(acc, new_tuple, negs, left, transform, compose) + :empty -> acc + new_tuple -> tuple_bdd_get(acc, new_tuple, negs, left, transform, compose) end tuple_bdd_get(acc, tuple, [next_tuple | negs], right, transform, compose) From 92a541196aaed7c92142043408fe54600781a9e1 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Mon, 1 Sep 2025 19:18:36 +0200 Subject: [PATCH 13/32] Optimize `pop_elem` function --- lib/elixir/lib/module/types/descr.ex | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 5c1cae5fdd6..6b336e55020 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2265,7 +2265,7 @@ defmodule Module.Types.Descr do # Case 3: when a list with negations is united with one of its negations defp add_to_list_normalize([{t, l, n} = cur | rest], list, last, []) do - case pop_elem({list, last}, n) do + case pop_elem(n, {list, last}, []) do {true, n1} -> [{t, l, n1} | rest] {false, _} -> [cur | add_to_list_normalize(rest, list, last, n)] end @@ -2273,13 +2273,9 @@ defmodule Module.Types.Descr do defp add_to_list_normalize(rest, list, last, negs), do: [{list, last, negs} | rest] - defp pop_elem(elem, list) do - case :lists.delete(elem, list) do - ^list -> {false, list} - new_list -> {true, new_list} - end - end - + defp pop_elem([key | t], key, acc), do: {true, :lists.reverse(acc, t)} + defp pop_elem([h | t], key, acc), do: pop_elem(t, key, [h | acc]) + defp pop_elem([], _key, acc), do: {false, :lists.reverse(acc)} ## Dynamic # # A type with a dynamic component is a gradual type; without, it is a static From 8118ab425e29d8f6248bbf15bb8116807e9840b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Tue, 2 Sep 2025 18:32:58 +0200 Subject: [PATCH 14/32] Simplify element intersection --- lib/elixir/lib/module/types/descr.ex | 117 ++++++++++++--------------- 1 file changed, 50 insertions(+), 67 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 6b336e55020..88ea55deccc 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -3799,27 +3799,23 @@ defmodule Module.Types.Descr do defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2) + defp tuple_literal_intersection(:open, [], tag, elements), do: {tag, elements} + defp tuple_literal_intersection(tag1, elements1, tag2, elements2) do n = length(elements1) m = length(elements2) - cond do - (tag1 == :closed and n < m) or (tag2 == :closed and n > m) -> - :empty - - tag1 == :open and tag2 == :open -> - try do - {:open, zip_non_empty_intersection!(elements1, elements2, [])} - catch - :empty -> :empty - end - - true -> - try do - {:closed, zip_non_empty_intersection!(elements1, elements2, [])} - catch - :empty -> :empty - end + if (tag1 == :closed and n < m) or (tag2 == :closed and n > m) do + :empty + else + try do + zip_non_empty_intersection!(elements1, elements2, []) + catch + :empty -> :empty + else + elements when tag1 == :open and tag2 == :open -> {:open, elements} + elements -> {:closed, elements} + end end end @@ -3831,9 +3827,39 @@ defmodule Module.Types.Descr do zip_non_empty_intersection!(rest1, rest2, [non_empty_intersection!(type1, type2) | acc]) end + defp zip_empty_intersection?([], _types2), do: false + defp zip_empty_intersection?(_types1, []), do: false + + defp zip_empty_intersection?([type1 | rest1], [type2 | rest2]) do + case empty?(intersection(type1, type2)) do + true -> true + false -> zip_empty_intersection?(rest1, rest2) + end + end + defp tuple_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2) - defp tuple_empty?(bdd), do: tuple_bdd_to_dnf(bdd) == [] + defp tuple_empty?(bdd), do: tuple_bdd_empty?({:open, []}, [], bdd) + + defp tuple_bdd_empty?({tag, elements} = pos, negs, bdd) do + case bdd do + :bdd_bot -> + true + + :bdd_top -> + tuple_empty?(tag, elements, negs) + + {{next_tag, next_elements} = next_tuple, left, right} -> + case tuple_literal_intersection(tag, elements, next_tag, next_elements) do + :empty -> + tuple_bdd_empty?(pos, [next_tuple | negs], right) + + new_tuple -> + tuple_bdd_empty?(new_tuple, negs, left) and + tuple_bdd_empty?(pos, [next_tuple | negs], right) + end + end + end # No negations, so not empty unless there's an empty type # Note: since the extraction from the BDD is done in a way that guarantees that @@ -3855,14 +3881,8 @@ defmodule Module.Types.Descr do if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do tuple_empty?(tag, elements, negs) else - case element_intersection(elements, neg_elements) do - :empty -> - tuple_empty?(tag, elements, negs) - - _ -> - tuple_elements_empty?([], tag, elements, neg_elements, negs) and - tuple_compatibility(n, m, tag, elements, neg_tag, negs) - end + tuple_elements_empty?([], tag, elements, neg_elements, negs) and + tuple_empty_arity?(n, m, tag, elements, neg_tag, negs) end end @@ -3875,42 +3895,15 @@ defmodule Module.Types.Descr do diff = difference(ty, neg_type) meet = intersection(ty, neg_type) - # In this case, there is no intersection between the positive and this negative. - # So we should just "go next" + # In this case, there is no intersection between the positive and this negative (empty?(diff) or tuple_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and - tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs) - end - - # Function that, given two tuples {tag1, elements1} and {tag2, elements2}, computes the - # intersection of all their elements (with default term() if one is open). - # If any intersection is empty, it return :empty. Else, it should return the list of them. - defp element_intersection(elements1, elements2) do - elements1 = - if length(elements1) < length(elements2), - do: tuple_fill(elements1, length(elements2)), - else: elements1 - - elements2 = - if length(elements1) > length(elements2), - do: tuple_fill(elements2, length(elements1)), - else: elements2 - - Enum.reduce_while(Enum.zip(elements1, elements2), [], fn {type1, type2}, acc -> - case intersection(type1, type2) do - :empty -> {:halt, :empty} - meet -> {:cont, [meet | acc]} - end - end) - |> case do - :empty -> :empty - list -> Enum.reverse(list) - end + (empty?(meet) or tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs)) end # Determines if the set difference is empty when: # - Positive tuple: {tag, elements} of size n # - Negative tuple: open or closed tuples of size m - defp tuple_compatibility(n, m, tag, elements, neg_tag, negs) do + defp tuple_empty_arity?(n, m, tag, elements, neg_tag, negs) do # The tuples to consider are all those of size n to m - 1, and if the negative tuple is # closed, we also need to consider tuples of size greater than m + 1. tag == :closed or @@ -3926,12 +3919,6 @@ defmodule Module.Types.Descr do end) end - defp empty_element_intersection?(elements1, elements2) do - Enum.any?(Enum.zip(elements1, elements2), fn {type1, type2} -> - empty?(intersection(type1, type2)) - end) - end - # Important: this generates DISJOINT tuples. defp tuple_eliminate_single_negation(tag, elements, {neg_tag, neg_elements}) do n = length(elements) @@ -3942,7 +3929,7 @@ defmodule Module.Types.Descr do # 2. When removing smaller tuples from larger tuples # 3. When there is no intersection between the elements of the two tuples if (tag == :closed and n < m) or (neg_tag == :closed and n > m) or - empty_element_intersection?(elements, neg_elements) do + zip_empty_intersection?(elements, neg_elements) do [{tag, elements}] else tuple_dnf_union( @@ -4142,10 +4129,6 @@ defmodule Module.Types.Descr do |> Enum.map(&tuple_literal_to_quoted(&1, opts)) end - # Transforms a bdd into a dnf (union of tuples with negations) - def tuple_bdd_to_dnf(bdd), - do: tuple_bdd_get([], {:open, []}, [], bdd, &{&1, &2, &3}, &[&1 | &2]) - # Transforms a bdd into a positive normal form (union of tuples with no negations) # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates defp tuple_bdd_to_dnf_no_negations(bdd), From 1123a6f860ef34cdf211e704c20bf83db2e38860 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Tue, 2 Sep 2025 18:50:42 +0200 Subject: [PATCH 15/32] Remove empty list check on intersections/differences --- lib/elixir/lib/module/types/descr.ex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 88ea55deccc..06794e087a3 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -73,8 +73,8 @@ defmodule Module.Types.Descr do @term_or_dynamic_optional Map.put(@term, :dynamic, %{optional: 1}) @not_atom_or_optional Map.delete(@term_or_optional, :atom) - @empty_intersection [0, [], :bdd_bot] - @empty_difference [0, [], :bdd_bot] + @empty_intersection [0, :bdd_bot] + @empty_difference [0, :bdd_bot] defguard is_descr(descr) when is_map(descr) or descr == :term From d4c670b18c7d73d387a7613469795633c35fd1fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Wed, 3 Sep 2025 11:48:06 +0200 Subject: [PATCH 16/32] Use consistent naming --- lib/elixir/lib/module/types/descr.ex | 69 ++++++++++++++++------------ 1 file changed, 39 insertions(+), 30 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 06794e087a3..01e99b766a9 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1300,7 +1300,7 @@ defmodule Module.Types.Descr do defp fun_normalize(%{fun: bdd}, arity, mode) do {domain, arrows, bad_arities} = - Enum.reduce(fun_get(bdd), {term(), [], []}, fn + Enum.reduce(fun_bdd_get(bdd), {term(), [], []}, fn {pos_funs, _neg_funs}, {domain, arrows, bad_arities} -> arrow_arity = case pos_funs do @@ -1413,13 +1413,18 @@ defmodule Module.Types.Descr do # Takes all the paths from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - defp fun_get(bdd), do: fun_get([], [], [], bdd) + defp fun_bdd_get(bdd), do: fun_bdd_get([], [], [], bdd) - defp fun_get(acc, pos, neg, bdd) do + defp fun_bdd_get(acc, pos, neg, bdd) do case bdd do - :bdd_bot -> acc - :bdd_top -> if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] - {fun, left, right} -> fun_get(fun_get(acc, [fun | pos], neg, left), pos, [fun | neg], right) + :bdd_bot -> + acc + + :bdd_top -> + if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] + + {fun, left, right} -> + fun_bdd_get(fun_bdd_get(acc, [fun | pos], neg, left), pos, [fun | neg], right) end end @@ -1435,7 +1440,7 @@ defmodule Module.Types.Descr do # - `fun(1) and not fun(1)` is empty # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty - defp fun_empty?(bdd), do: fun_get(bdd) == [] + defp fun_empty?(bdd), do: fun_bdd_get(bdd) == [] # Checks if a function type represented by positive and negative function literals is empty. @@ -1699,8 +1704,8 @@ defmodule Module.Types.Descr do # and put static and dynamic parts back together to improve # pretty printing. defp fun_denormalize(%{fun: static_bdd} = static, %{fun: dynamic_bdd} = dynamic, opts) do - static_pos = fun_get_pos(static_bdd) - dynamic_pos = fun_get_pos(dynamic_bdd) + static_pos = fun_bdd_get_pos(static_bdd) + dynamic_pos = fun_bdd_get_pos(dynamic_bdd) if static_pos != [] and dynamic_pos != [] do {static_pos, dynamic_pos} = fun_denormalize_pos(static_pos, dynamic_pos) @@ -1790,14 +1795,14 @@ defmodule Module.Types.Descr do # Converts a function BDD (Binary Decision Diagram) to its quoted representation defp fun_to_quoted(bdd, opts) do - case fun_get_pos(bdd) do + case fun_bdd_get_pos(bdd) do [] -> [] pos -> [fun_pos_to_quoted(pos, opts)] end end - defp fun_get_pos(bdd) do - for {pos, _negs} <- fun_get(bdd) do + defp fun_bdd_get_pos(bdd) do + for {pos, _negs} <- fun_bdd_get(bdd) do fun_filter_subset(pos, []) end end @@ -1879,11 +1884,11 @@ defmodule Module.Types.Descr do # corresponding positive list type; in that case we subtract the negated # variant from the positive one. {list_type, last_type} = - list_get_pos(bdd) - |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail}, - {acc_head, acc_tail} -> - tail = list_tail_unfold(tail) - {union(head, acc_head), union(tail, acc_tail)} + list_bdd_get_pos(bdd) + |> Enum.reduce({list_type, last_type_no_list}, fn + {head, tail}, {acc_head, acc_tail} -> + tail = list_tail_unfold(tail) + {union(head, acc_head), union(tail, acc_tail)} end) list_new(list_type, last_type) @@ -1906,9 +1911,9 @@ defmodule Module.Types.Descr do # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - defp list_get(bdd), do: list_get([], {:term, :term}, [], bdd) + defp list_bdd_get(bdd), do: list_bdd_get([], {:term, :term}, [], bdd) - defp list_get(acc, {list_acc, tail_acc} = pos, negs, bdd) do + defp list_bdd_get(acc, {list_acc, tail_acc} = pos, negs, bdd) do case bdd do :bdd_bot -> acc @@ -1918,7 +1923,7 @@ defmodule Module.Types.Descr do {{list, tail} = list_type, left, right} -> new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} - list_get(list_get(acc, new_pos, negs, left), pos, [list_type | negs], right) + list_bdd_get(list_bdd_get(acc, new_pos, negs, left), pos, [list_type | negs], right) end end @@ -1929,9 +1934,9 @@ defmodule Module.Types.Descr do # if the negative list type is a supertype of the positive list type. In that case, # we can remove the negative last type from the positive one. # (If this subtracted type was empty, the whole type would be empty) - defp list_get_pos(bdd), do: list_get_pos(:term, :term, bdd, []) + defp list_bdd_get_pos(bdd), do: list_bdd_get_pos(:term, :term, bdd, []) - defp list_get_pos(list_acc, last_acc, bdd, lines_acc) do + defp list_bdd_get_pos(list_acc, last_acc, bdd, lines_acc) do case bdd do :bdd_bot -> lines_acc @@ -1944,9 +1949,12 @@ defmodule Module.Types.Descr do lines_acc = if subtype?(list_acc, list) do last = difference(last_acc, last) - if empty?(last), do: lines_acc, else: list_get_pos(list_acc, last, right, lines_acc) + + if empty?(last), + do: lines_acc, + else: list_bdd_get_pos(list_acc, last, right, lines_acc) else - list_get_pos(list_acc, last_acc, right, lines_acc) + list_bdd_get_pos(list_acc, last_acc, right, lines_acc) end # Case 2: count the list_type positively. @@ -1956,7 +1964,7 @@ defmodule Module.Types.Descr do if empty?(list_acc) or empty?(last_acc) do lines_acc else - list_get_pos(list_acc, last_acc, left, lines_acc) + list_bdd_get_pos(list_acc, last_acc, left, lines_acc) end end end @@ -2112,7 +2120,7 @@ defmodule Module.Types.Descr do defp list_hd_static(:term), do: :term defp list_hd_static(%{list: bdd}) do - list_get_pos(bdd) + list_bdd_get_pos(bdd) |> Enum.reduce(none(), fn {list, _}, acc -> union(list, acc) end) @@ -2164,7 +2172,7 @@ defmodule Module.Types.Descr do %{list: bdd} end - list_get_pos(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) + list_bdd_get_pos(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) end defp list_tl_static(%{}), do: none() @@ -2229,7 +2237,7 @@ defmodule Module.Types.Descr do # Eliminate empty lists from the union, and redundant types (that are subtypes of others, # or that can be merged with others). defp list_normalize(bdd) do - list_get(bdd) + list_bdd_get(bdd) |> Enum.reduce([], fn {{list, last}, negs}, acc -> # First, try to eliminate the negations from the existing type. {list, last, negs} = @@ -2276,6 +2284,7 @@ defmodule Module.Types.Descr do defp pop_elem([key | t], key, acc), do: {true, :lists.reverse(acc, t)} defp pop_elem([h | t], key, acc), do: pop_elem(t, key, [h | acc]) defp pop_elem([], _key, acc), do: {false, :lists.reverse(acc)} + ## Dynamic # # A type with a dynamic component is a gradual type; without, it is a static @@ -2609,7 +2618,7 @@ defmodule Module.Types.Descr do defp map_difference(map_literal(tag, fields) = map1, map_literal(neg_tag, neg_fields) = map2) do # Case 1: we are removing an open map with one field. Just do the difference of that field. if neg_tag == :open and map_size(neg_fields) == 1 do - {key, value, _rest} = :maps.next(:maps.iterator(neg_fields)) + [{key, value}] = Map.to_list(neg_fields) t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value) if empty?(t_diff) do @@ -2813,7 +2822,7 @@ defmodule Module.Types.Descr do map_key_tag_to_type(tag_or_domains) |> pop_optional_static() end - # Takes a map dnf and returns the union of types it can take for a given key. + # Takes a map and returns the union of types it can take for a given key. # If the key may be undefined, it will contain the `not_set()` type. defp map_fetch_static(%{map: bdd}, key) do map_bdd_get(bdd) From 3529577dfa242598a91df2b078845a89992ef5da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Wed, 17 Sep 2025 15:15:04 +0200 Subject: [PATCH 17/32] Bump checker version as representation changed --- lib/elixir/lib/module/parallel_checker.ex | 2 +- lib/elixir/src/elixir_erl.erl | 2 +- lib/elixir/test/elixir/module/types/integration_test.exs | 2 +- lib/elixir/test/elixir/protocol/consolidation_test.exs | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/elixir/lib/module/parallel_checker.ex b/lib/elixir/lib/module/parallel_checker.ex index 2fdd5c3d5d2..178f04e2845 100644 --- a/lib/elixir/lib/module/parallel_checker.ex +++ b/lib/elixir/lib/module/parallel_checker.ex @@ -423,7 +423,7 @@ defmodule Module.ParallelChecker do mode = with {^module, binary, _filename} <- object_code, {:ok, {^module, [{~c"ExCk", chunk}]}} <- :beam_lib.chunks(binary, [~c"ExCk"]), - {:elixir_checker_v2, contents} <- :erlang.binary_to_term(chunk) do + {:elixir_checker_v3, contents} <- :erlang.binary_to_term(chunk) do # The chunk has more information, so that's our preference cache_chunk(table, module, contents) else diff --git a/lib/elixir/src/elixir_erl.erl b/lib/elixir/src/elixir_erl.erl index 5a012050ff7..9630c3db117 100644 --- a/lib/elixir/src/elixir_erl.erl +++ b/lib/elixir/src/elixir_erl.erl @@ -662,7 +662,7 @@ checker_chunk(Map, Def, ChunkOpts) -> end }, - [{<<"ExCk">>, term_to_binary({elixir_checker_v2, Contents}, ChunkOpts)}]. + [{<<"ExCk">>, term_to_binary({elixir_checker_v3, Contents}, ChunkOpts)}]. prepend_behaviour_info(true, Def) -> [{{behaviour_info, 1}, []} | Def]; prepend_behaviour_info(false, Def) -> Def. diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs index 85ba20a8288..d9bde23d4bb 100644 --- a/lib/elixir/test/elixir/module/types/integration_test.exs +++ b/lib/elixir/test/elixir/module/types/integration_test.exs @@ -1538,7 +1538,7 @@ defmodule Module.Types.IntegrationTest do defp read_chunk(binary) do assert {:ok, {_module, [{~c"ExCk", chunk}]}} = :beam_lib.chunks(binary, [~c"ExCk"]) - assert {:elixir_checker_v2, map} = :erlang.binary_to_term(chunk) + assert {:elixir_checker_v3, map} = :erlang.binary_to_term(chunk) map end diff --git a/lib/elixir/test/elixir/protocol/consolidation_test.exs b/lib/elixir/test/elixir/protocol/consolidation_test.exs index 55d0efb612c..a32b309d6b9 100644 --- a/lib/elixir/test/elixir/protocol/consolidation_test.exs +++ b/lib/elixir/test/elixir/protocol/consolidation_test.exs @@ -165,7 +165,7 @@ defmodule Protocol.ConsolidationTest do defp exports(binary) do {:ok, {_, [{~c"ExCk", check_bin}]}} = :beam_lib.chunks(binary, [~c"ExCk"]) - assert {:elixir_checker_v2, contents} = :erlang.binary_to_term(check_bin) + assert {:elixir_checker_v3, contents} = :erlang.binary_to_term(check_bin) Map.new(contents.exports) end From 4a0c84bae11523819b277234b8b70301592e87f5 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:10:33 +0200 Subject: [PATCH 18/32] Remove unused function --- lib/elixir/lib/module/types/descr.ex | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 01e99b766a9..fa6a75de734 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -3856,7 +3856,7 @@ defmodule Module.Types.Descr do true :bdd_top -> - tuple_empty?(tag, elements, negs) + tuple_line_empty?(tag, elements, negs) {{next_tag, next_elements} = next_tuple, left, right} -> case tuple_literal_intersection(tag, elements, next_tag, next_elements) do @@ -3874,13 +3874,13 @@ defmodule Module.Types.Descr do # Note: since the extraction from the BDD is done in a way that guarantees that # the elements are non-empty, we can avoid checking for empty types there. # Otherwise, tuple_empty?(_, elements, []) would be Enum.any?(elements, &empty?/1) - defp tuple_empty?(_, _, []), do: false + defp tuple_line_empty?(_, _, []), do: false # Open empty negation makes it empty - defp tuple_empty?(_, _, [{:open, []} | _]), do: true + defp tuple_line_empty?(_, _, [{:open, []} | _]), do: true # Open positive can't be emptied by a single closed negative - defp tuple_empty?(:open, _pos, [{:closed, _}]), do: false + defp tuple_line_empty?(:open, _pos, [{:closed, _}]), do: false - defp tuple_empty?(tag, elements, [{neg_tag, neg_elements} | negs]) do + defp tuple_line_empty?(tag, elements, [{neg_tag, neg_elements} | negs]) do n = length(elements) m = length(neg_elements) @@ -3888,7 +3888,7 @@ defmodule Module.Types.Descr do # 1. When removing larger tuples from a fixed-size positive tuple # 2. When removing smaller tuples from larger tuples if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do - tuple_empty?(tag, elements, negs) + tuple_line_empty?(tag, elements, negs) else tuple_elements_empty?([], tag, elements, neg_elements, negs) and tuple_empty_arity?(n, m, tag, elements, neg_tag, negs) @@ -3904,8 +3904,9 @@ defmodule Module.Types.Descr do diff = difference(ty, neg_type) meet = intersection(ty, neg_type) - # In this case, there is no intersection between the positive and this negative - (empty?(diff) or tuple_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and + # In this case, there is no intersection between the positive and this negative. + # So we should just "go next" + (empty?(diff) or tuple_line_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and (empty?(meet) or tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs)) end @@ -3916,8 +3917,8 @@ defmodule Module.Types.Descr do # The tuples to consider are all those of size n to m - 1, and if the negative tuple is # closed, we also need to consider tuples of size greater than m + 1. tag == :closed or - (Enum.all?(n..(m - 1)//1, &tuple_empty?(:closed, tuple_fill(elements, &1), negs)) and - (neg_tag == :open or tuple_empty?(:open, tuple_fill(elements, m + 1), negs))) + (Enum.all?(n..(m - 1)//1, &tuple_line_empty?(:closed, tuple_fill(elements, &1), negs)) and + (neg_tag == :open or tuple_line_empty?(:open, tuple_fill(elements, m + 1), negs))) end defp tuple_eliminate_negations(tag, elements, negs) do @@ -4149,7 +4150,7 @@ defmodule Module.Types.Descr do acc :bdd_top -> - if tuple_empty?(tag, elements, negs) do + if tuple_line_empty?(tag, elements, negs) do acc else compose.(transform.(tag, elements, negs), acc) From 8664e7fd4ab3d76727e6ad8c1e725d2bb70a0bbb Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:21:15 +0200 Subject: [PATCH 19/32] Make map_empty? short-circuiting --- lib/elixir/lib/module/types/descr.ex | 42 ++++++++++++++++++++-------- 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index fa6a75de734..8f6012409c0 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2759,7 +2759,7 @@ defmodule Module.Types.Descr do acc :bdd_top -> - if map_empty?(tag, fields, negs), do: acc, else: [{tag, fields, negs} | acc] + if map_line_empty?(tag, fields, negs), do: acc, else: [{tag, fields, negs} | acc] {{next_tag, next_fields} = next_map, left, right} -> acc = @@ -3407,13 +3407,31 @@ defmodule Module.Types.Descr do # Short-circuits if it finds a non-empty map literal in the union. # Since the algorithm is recursive, we implement the short-circuiting # as throw/catch. - defp map_empty?(bdd), do: map_bdd_get(bdd) == [] + defp map_empty?(bdd), do: map_bdd_empty?({:open, %{}}, [], bdd) - defp map_empty?(_, pos, []), do: Enum.any?(Map.to_list(pos), fn {_, v} -> empty?(v) end) - defp map_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true - defp map_empty?(:open, fs, [{:closed, _} | negs]), do: map_empty?(:open, fs, negs) + defp map_bdd_empty?({tag, fields} = map, negs, bdd) do + case bdd do + :bdd_bot -> + true + + :bdd_top -> + map_line_empty?(tag, fields, negs) + + {{next_tag, next_fields} = next_map, left, right} -> + try do + new_map = map_literal_intersection(tag, fields, next_tag, next_fields) + map_bdd_empty?(new_map, negs, left) and map_bdd_empty?(map, [next_map | negs], right) + catch + :empty -> map_bdd_empty?(map, [next_map | negs], right) + end + end + end + + defp map_line_empty?(_, pos, []), do: Enum.any?(Map.to_list(pos), fn {_, v} -> empty?(v) end) + defp map_line_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true + defp map_line_empty?(:open, fs, [{:closed, _} | negs]), do: map_line_empty?(:open, fs, negs) - defp map_empty?(tag, fields, [{neg_tag, neg_fields} | negs]) do + defp map_line_empty?(tag, fields, [{neg_tag, neg_fields} | negs]) do if map_check_domain_keys(tag, neg_tag) do atom_default = map_key_tag_to_type(tag) neg_atom_default = map_key_tag_to_type(neg_tag) @@ -3432,18 +3450,18 @@ defmodule Module.Types.Descr do # There may be value in common tag == :open -> diff = difference(term_or_optional(), neg_type) - empty?(diff) or map_empty?(tag, Map.put(fields, neg_key, diff), negs) + empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) true -> diff = difference(atom_default, neg_type) - empty?(diff) or map_empty?(tag, Map.put(fields, neg_key, diff), negs) + empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) end end) and Enum.all?(Map.to_list(fields), fn {key, type} -> case neg_fields do %{^key => neg_type} -> diff = difference(type, neg_type) - empty?(diff) or map_empty?(tag, Map.put(fields, key, diff), negs) + empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) %{} -> cond do @@ -3456,12 +3474,12 @@ defmodule Module.Types.Descr do true -> # an absent key in a open negative map can be ignored diff = difference(type, neg_atom_default) - empty?(diff) or map_empty?(tag, Map.put(fields, key, diff), negs) + empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) end end - end)) or map_empty?(tag, fields, negs) + end)) or map_line_empty?(tag, fields, negs) else - map_empty?(tag, fields, negs) + map_line_empty?(tag, fields, negs) end end From fd486f7efeabc14e3a313700a9c6cdf3b89ceb3f Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:25:22 +0200 Subject: [PATCH 20/32] Sort map_union to preserve invariant Co-authored-by: Jean Klingler --- lib/elixir/lib/module/types/descr.ex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 8f6012409c0..b166e21b5d6 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2494,7 +2494,11 @@ defmodule Module.Types.Descr do def map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do {tag, fields, []} -> map_literal(tag, fields) - nil -> {{tag1, fields1}, :bdd_top, {{tag2, fields2}, :bdd_top, :bdd_bot}} + nil -> + case {{tag1, fields1}, {tag2, fields2}} do + {r, l} when l < r -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}} + {l, r} -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}} + end end end From 7765fead472b6afd5094ee50058c947ea34699f8 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:25:50 +0200 Subject: [PATCH 21/32] Update comment Co-authored-by: Jean Klingler --- lib/elixir/lib/module/types/descr.ex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index b166e21b5d6..e50c6170623 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -3547,7 +3547,7 @@ defmodule Module.Types.Descr do end) end - # Use heuristics to normalize a map dnf for pretty printing. + # Use heuristics to normalize a map bdd for pretty printing. defp map_normalize(bdd) do map_bdd_get(bdd) |> Enum.map(fn {tag, fields, negs} -> From f541e71db818c95fbdcede4263194aebcb97d190 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:42:25 +0200 Subject: [PATCH 22/32] Add test for map representation invariant --- lib/elixir/test/elixir/module/types/descr_test.exs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index 0383a2a17da..3eea72d64bf 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -135,6 +135,18 @@ defmodule Module.Types.DescrTest do # Test union of open map and map with domain key assert union(open_map(), open_map([{domain_key(:integer), atom()}])) |> equal?(open_map()) + + # Ensure no duplicate, no matter the order + assert union( + open_map(a: integer()), + open_map(a: number(), b: binary()) + ) + |> union(open_map(a: integer())) == + union( + open_map(a: number(), b: binary()), + open_map(a: integer()) + ) + |> union(open_map(a: integer())) end test "list" do From 272c4f0d43472375ef2b55c5447d54e3b6272f37 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Wed, 17 Sep 2025 15:42:48 +0200 Subject: [PATCH 23/32] Formatting --- lib/elixir/lib/module/types/descr.ex | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index e50c6170623..ea8a5baaf58 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2493,12 +2493,14 @@ defmodule Module.Types.Descr do def map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do - {tag, fields, []} -> map_literal(tag, fields) - nil -> + {tag, fields, []} -> + map_literal(tag, fields) + + nil -> case {{tag1, fields1}, {tag2, fields2}} do {r, l} when l < r -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}} {l, r} -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}} - end + end end end From c941281ff67979fb003678b56f133fcd5c559fbc Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 10:52:11 +0200 Subject: [PATCH 24/32] Fix test --- lib/elixir/test/elixir/module/types/descr_test.exs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index 3eea72d64bf..d45ed220dec 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -2375,7 +2375,7 @@ defmodule Module.Types.DescrTest do ) |> union(difference(open_map(x: atom()), open_map(x: boolean()))) |> to_quoted_string() == - "%{..., a: integer(), b: atom(), c: boolean()} or\n (%{..., x: atom() and not boolean()} and not %{..., a: integer(), b: atom(), c: boolean()})" + "%{..., x: atom() and not boolean()} or\n (%{..., a: integer(), b: atom(), c: boolean()} and not %{..., x: atom() and not boolean()})" assert closed_map(a: number(), b: atom(), c: pid()) |> difference(closed_map(a: integer(), b: atom(), c: pid())) From 95412fdfa62a3ae5fbb5dee9fcc50e2c053ad647 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 11:13:33 +0200 Subject: [PATCH 25/32] Remove higher order implementation for tuple_normalize --- lib/elixir/lib/module/types/descr.ex | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index ea8a5baaf58..26fb54a8dfa 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -262,7 +262,7 @@ defmodule Module.Types.Descr do end defp unwrap_domain_tuple(%{tuple: bdd} = descr, transform) when map_size(descr) == 1 do - tuple_bdd_to_dnf_no_negations(bdd) |> Enum.map(transform) + tuple_normalize(bdd) |> Enum.map(transform) end defp unwrap_domain_tuple(descr, _transform) when descr == %{}, do: [] @@ -4158,17 +4158,16 @@ defmodule Module.Types.Descr do end defp tuple_to_quoted(bdd, opts) do - tuple_bdd_to_dnf_no_negations(bdd) + tuple_normalize(bdd) |> tuple_fusion() |> Enum.map(&tuple_literal_to_quoted(&1, opts)) end - # Transforms a bdd into a positive normal form (union of tuples with no negations) + # Transforms a bdd into a union of tuples with no negations. # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates - defp tuple_bdd_to_dnf_no_negations(bdd), - do: tuple_bdd_get([], {:open, []}, [], bdd, &tuple_eliminate_negations/3, &tuple_dnf_union/2) + defp tuple_normalize(bdd), do: tuple_normalize([], {:open, []}, [], bdd) - defp tuple_bdd_get(acc, {tag, elements} = tuple, negs, bdd, transform, compose) do + defp tuple_normalize(acc, {tag, elements} = tuple, negs, bdd) do case bdd do :bdd_bot -> acc @@ -4177,7 +4176,7 @@ defmodule Module.Types.Descr do if tuple_line_empty?(tag, elements, negs) do acc else - compose.(transform.(tag, elements, negs), acc) + tuple_eliminate_negations(tag, elements, negs) |> tuple_dnf_union(acc) end {{next_tag, next_elements} = next_tuple, left, right} -> @@ -4185,10 +4184,10 @@ defmodule Module.Types.Descr do acc = case tuple_literal_intersection(tag, elements, next_tag, next_elements) do :empty -> acc - new_tuple -> tuple_bdd_get(acc, new_tuple, negs, left, transform, compose) + new_tuple -> tuple_normalize(acc, new_tuple, negs, left) end - tuple_bdd_get(acc, tuple, [next_tuple | negs], right, transform, compose) + tuple_normalize(acc, tuple, [next_tuple | negs], right) end end @@ -4335,7 +4334,7 @@ defmodule Module.Types.Descr do end defp tuple_get(bdd, index) do - tuple_bdd_to_dnf_no_negations(bdd) + tuple_normalize(bdd) |> Enum.reduce(none(), fn {tag, elements}, acc -> Enum.at(elements, index, tuple_tag_to_type(tag)) |> union(acc) end) @@ -4366,7 +4365,7 @@ defmodule Module.Types.Descr do end defp process_tuples_values(bdd) do - tuple_bdd_to_dnf_no_negations(bdd) + tuple_normalize(bdd) |> Enum.reduce(none(), fn {tag, elements}, acc -> cond do Enum.any?(elements, &empty?/1) -> none() @@ -4504,7 +4503,7 @@ defmodule Module.Types.Descr do defp tuple_of_size_at_least_static?(descr, index) do case descr do %{tuple: bdd} -> - tuple_bdd_to_dnf_no_negations(bdd) + tuple_normalize(bdd) |> Enum.all?(fn {_, elements} -> length(elements) >= index end) %{} -> From 13dedd4258228d98c7a6792d8e2a2349fa608986 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 11:48:05 +0200 Subject: [PATCH 26/32] Improve map_fetch static, removing circularity there is now map_dnf_fetch_static to avoid calling map_bdd_get in a loop. also, renamed map_bdd_get to map_bdd_to_dnf (avoids confusion with get operation on maps) --- lib/elixir/lib/module/types/descr.ex | 65 +++++++++++++++------------- 1 file changed, 34 insertions(+), 31 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 26fb54a8dfa..e7723bc2724 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -2757,9 +2757,9 @@ defmodule Module.Types.Descr do # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - def map_bdd_get(bdd), do: map_bdd_get([], {:open, %{}}, [], bdd) + def map_bdd_to_dnf(bdd), do: map_bdd_to_dnf([], {:open, %{}}, [], bdd) - defp map_bdd_get(acc, {tag, fields} = map, negs, bdd) do + defp map_bdd_to_dnf(acc, {tag, fields} = map, negs, bdd) do case bdd do :bdd_bot -> acc @@ -2771,12 +2771,12 @@ defmodule Module.Types.Descr do acc = try do new_pos = map_literal_intersection(tag, fields, next_tag, next_fields) - map_bdd_get(acc, new_pos, negs, left) + map_bdd_to_dnf(acc, new_pos, negs, left) catch :empty -> acc end - map_bdd_get(acc, map, [next_map | negs], right) + map_bdd_to_dnf(acc, map, [next_map | negs], right) end end @@ -2828,11 +2828,17 @@ defmodule Module.Types.Descr do map_key_tag_to_type(tag_or_domains) |> pop_optional_static() end - # Takes a map and returns the union of types it can take for a given key. - # If the key may be undefined, it will contain the `not_set()` type. defp map_fetch_static(%{map: bdd}, key) do - map_bdd_get(bdd) - |> Enum.reduce(none(), fn + map_bdd_to_dnf(bdd) |> map_dnf_fetch_static(key) + end + + defp map_fetch_static(%{}, _key), do: {false, none()} + defp map_fetch_static(:term, _key), do: {true, term()} + + # Takes a map DNF and returns the union of types it can take for a given key. + # If the key may be undefined, it will contain the `not_set()` type. + defp map_dnf_fetch_static(dnf, key) do + Enum.reduce(dnf, none(), fn # Optimization: if there are no negatives and key exists, return its value {_tag, %{^key => value}, []}, acc -> value |> union(acc) @@ -2858,9 +2864,6 @@ defmodule Module.Types.Descr do |> pop_optional_static() end - defp map_fetch_static(%{}, _key), do: {false, none()} - defp map_fetch_static(:term, _key), do: {true, term()} - @doc """ Fetches and puts a `key` of a given type, assuming that the descr is exclusively a map (or dynamic). @@ -3001,7 +3004,7 @@ defmodule Module.Types.Descr do def map_refresh_domain(%{map: bdd}, domain, type) do # For negations, we count on the idea that a negation will not remove any # type from a domain unless it completely cancels out the type. - # So for any non-empty map dnf, we just update the domain with the new type, + # So for any non-empty map bdd, we just update the domain with the new type, # as well as its negations to keep them accurate. %{map: bdd_map(bdd, fn {tag, fields} -> {map_refresh_tag(tag, domain, type), fields} end)} end @@ -3016,7 +3019,7 @@ defmodule Module.Types.Descr do {:negation, keys} -> # 1) Fetch all the possible keys in the bdd # 2) Get them all, except the ones in neg_atoms - considered_keys = map_fetch_all_key_names(bdd) |> :sets.subtract(keys) + considered_keys = map_bdd_to_dnf(bdd) |> map_fetch_all_key_names() |> :sets.subtract(keys) considered_keys |> :sets.to_list() @@ -3178,7 +3181,7 @@ defmodule Module.Types.Descr do defp unfold_domains(domains = %{}), do: domains - defp map_get_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key_descr) do + defp map_get_static(%{map: map_literal(tag_or_domains, fields)}, key_descr) do # For each non-empty kind of type in the key_descr, we add the corresponding key domain in a union. domains = unfold_domains(tag_or_domains) @@ -3187,7 +3190,7 @@ defmodule Module.Types.Descr do |> Enum.reduce(none(), fn # Note: we could stop if we reach term_or_optional() {:atom, atom_type}, acc -> - map_get_atom(map_literal(domains, fields), atom_type) |> union(acc) + map_get_atom([{domains, fields, []}], atom_type) |> union(acc) key_type, acc -> Map.get(domains, key_type, not_set()) |> union(acc) @@ -3195,14 +3198,16 @@ defmodule Module.Types.Descr do end defp map_get_static(%{map: bdd}, key_descr) do + dnf = map_bdd_to_dnf(bdd) + key_descr |> covered_key_types() |> Enum.reduce(none(), fn {:atom, atom_type}, acc -> - map_get_atom(bdd, atom_type) |> union(acc) + map_get_atom(dnf, atom_type) |> union(acc) domain_key, acc -> - map_get_domain(bdd, domain_key) |> union(acc) + map_get_domain(dnf, domain_key) |> union(acc) end) end @@ -3223,13 +3228,13 @@ defmodule Module.Types.Descr do # Fetching a key of type `atom() and not (:a)` from a map of type # `%{a: atom(), b: float(), atom() => pid()}` # would return either `nil` or `float()` (key `:b`) or `pid()` (key `atom()`), but not `atom()` (key `:a`). - defp map_get_atom(bdd, atom_type) do + defp map_get_atom(dnf, atom_type) do case atom_type do {:union, atoms} -> atoms |> :sets.to_list() |> Enum.reduce(none(), fn atom, acc -> - {static_optional?, type} = map_fetch_static(%{map: bdd}, atom) + {static_optional?, type} = map_dnf_fetch_static(dnf, atom) if static_optional? do union(type, acc) |> nil_or_type() |> if_set() @@ -3241,13 +3246,13 @@ defmodule Module.Types.Descr do {:negation, atoms} -> # 1) Fetch all the possible keys in the bdd # 2) Get them all, except the ones in neg_atoms - possible_keys = map_fetch_all_key_names(bdd) + possible_keys = map_fetch_all_key_names(dnf) considered_keys = :sets.subtract(possible_keys, atoms) considered_keys |> :sets.to_list() |> Enum.reduce(none(), fn atom, acc -> - {static_optional?, type} = map_fetch_static(%{map: bdd}, atom) + {static_optional?, type} = map_dnf_fetch_static(dnf, atom) if static_optional? do union(type, acc) |> nil_or_type() |> if_set() @@ -3255,14 +3260,13 @@ defmodule Module.Types.Descr do union(type, acc) end end) - |> union(map_get_domain(bdd, domain_key(:atom))) + |> union(map_get_domain(dnf, domain_key(:atom))) end end # Fetch all present keys in a map dnf (including negated ones). - defp map_fetch_all_key_names(bdd) do - map_bdd_get(bdd) - |> Enum.reduce(:sets.new(version: 2), fn {_tag, fields, negs}, acc -> + defp map_fetch_all_key_names(dnf) do + Enum.reduce(dnf, :sets.new(version: 2), fn {_tag, fields, negs}, acc -> keys = :sets.from_list(Map.keys(fields)) # Add all the negative keys @@ -3274,10 +3278,9 @@ defmodule Module.Types.Descr do end) end - # Take a map dnf and return the union of types for the given key domain. - defp map_get_domain(bdd, domain_key(_) = domain_key) do - map_bdd_get(bdd) - |> Enum.reduce(none(), fn + # Take a map bdd and return the union of types for the given key domain. + defp map_get_domain(dnf, domain_key(_) = domain_key) do + Enum.reduce(dnf, none(), fn {tag, _fields, []}, acc when is_atom(tag) -> map_key_tag_to_type(tag) |> union(acc) @@ -3373,7 +3376,7 @@ defmodule Module.Types.Descr do defp map_take_static(%{map: bdd}, key, initial) do {value, map} = - map_bdd_get(bdd) + map_bdd_to_dnf(bdd) |> Enum.reduce({initial, none()}, fn # Optimization: if there are no negatives, we can directly remove the key. {tag, fields, []}, {value, map} -> @@ -3551,7 +3554,7 @@ defmodule Module.Types.Descr do # Use heuristics to normalize a map bdd for pretty printing. defp map_normalize(bdd) do - map_bdd_get(bdd) + map_bdd_to_dnf(bdd) |> Enum.map(fn {tag, fields, negs} -> map_eliminate_while_negs_decrease(tag, fields, negs) end) From 4666d36da4ca873c539a357475e8657e3aa9852a Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 11:53:15 +0200 Subject: [PATCH 27/32] Unify renaming bdd_get to bdd_to_dnf --- lib/elixir/lib/module/types/descr.ex | 44 ++++++++++++++-------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index e7723bc2724..5b1736a2db2 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1300,7 +1300,7 @@ defmodule Module.Types.Descr do defp fun_normalize(%{fun: bdd}, arity, mode) do {domain, arrows, bad_arities} = - Enum.reduce(fun_bdd_get(bdd), {term(), [], []}, fn + Enum.reduce(fun_bdd_to_dnf(bdd), {term(), [], []}, fn {pos_funs, _neg_funs}, {domain, arrows, bad_arities} -> arrow_arity = case pos_funs do @@ -1413,9 +1413,9 @@ defmodule Module.Types.Descr do # Takes all the paths from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - defp fun_bdd_get(bdd), do: fun_bdd_get([], [], [], bdd) + defp fun_bdd_to_dnf(bdd), do: fun_bdd_to_dnf([], [], [], bdd) - defp fun_bdd_get(acc, pos, neg, bdd) do + defp fun_bdd_to_dnf(acc, pos, neg, bdd) do case bdd do :bdd_bot -> acc @@ -1424,7 +1424,7 @@ defmodule Module.Types.Descr do if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] {fun, left, right} -> - fun_bdd_get(fun_bdd_get(acc, [fun | pos], neg, left), pos, [fun | neg], right) + fun_bdd_to_dnf(fun_bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right) end end @@ -1440,7 +1440,7 @@ defmodule Module.Types.Descr do # - `fun(1) and not fun(1)` is empty # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty - defp fun_empty?(bdd), do: fun_bdd_get(bdd) == [] + defp fun_empty?(bdd), do: fun_bdd_to_dnf(bdd) == [] # Checks if a function type represented by positive and negative function literals is empty. @@ -1704,8 +1704,8 @@ defmodule Module.Types.Descr do # and put static and dynamic parts back together to improve # pretty printing. defp fun_denormalize(%{fun: static_bdd} = static, %{fun: dynamic_bdd} = dynamic, opts) do - static_pos = fun_bdd_get_pos(static_bdd) - dynamic_pos = fun_bdd_get_pos(dynamic_bdd) + static_pos = fun_bdd_to_pos_dnf(static_bdd) + dynamic_pos = fun_bdd_to_pos_dnf(dynamic_bdd) if static_pos != [] and dynamic_pos != [] do {static_pos, dynamic_pos} = fun_denormalize_pos(static_pos, dynamic_pos) @@ -1795,14 +1795,14 @@ defmodule Module.Types.Descr do # Converts a function BDD (Binary Decision Diagram) to its quoted representation defp fun_to_quoted(bdd, opts) do - case fun_bdd_get_pos(bdd) do + case fun_bdd_to_pos_dnf(bdd) do [] -> [] pos -> [fun_pos_to_quoted(pos, opts)] end end - defp fun_bdd_get_pos(bdd) do - for {pos, _negs} <- fun_bdd_get(bdd) do + defp fun_bdd_to_pos_dnf(bdd) do + for {pos, _negs} <- fun_bdd_to_dnf(bdd) do fun_filter_subset(pos, []) end end @@ -1884,7 +1884,7 @@ defmodule Module.Types.Descr do # corresponding positive list type; in that case we subtract the negated # variant from the positive one. {list_type, last_type} = - list_bdd_get_pos(bdd) + list_bdd_to_pos_dnf(bdd) |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail}, {acc_head, acc_tail} -> tail = list_tail_unfold(tail) @@ -1911,9 +1911,9 @@ defmodule Module.Types.Descr do # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - defp list_bdd_get(bdd), do: list_bdd_get([], {:term, :term}, [], bdd) + defp list_bdd_to_dnf(bdd), do: list_bdd_to_dnf([], {:term, :term}, [], bdd) - defp list_bdd_get(acc, {list_acc, tail_acc} = pos, negs, bdd) do + defp list_bdd_to_dnf(acc, {list_acc, tail_acc} = pos, negs, bdd) do case bdd do :bdd_bot -> acc @@ -1923,7 +1923,7 @@ defmodule Module.Types.Descr do {{list, tail} = list_type, left, right} -> new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} - list_bdd_get(list_bdd_get(acc, new_pos, negs, left), pos, [list_type | negs], right) + list_bdd_to_dnf(list_bdd_to_dnf(acc, new_pos, negs, left), pos, [list_type | negs], right) end end @@ -1934,9 +1934,9 @@ defmodule Module.Types.Descr do # if the negative list type is a supertype of the positive list type. In that case, # we can remove the negative last type from the positive one. # (If this subtracted type was empty, the whole type would be empty) - defp list_bdd_get_pos(bdd), do: list_bdd_get_pos(:term, :term, bdd, []) + defp list_bdd_to_pos_dnf(bdd), do: list_bdd_to_pos_dnf(:term, :term, bdd, []) - defp list_bdd_get_pos(list_acc, last_acc, bdd, lines_acc) do + defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do case bdd do :bdd_bot -> lines_acc @@ -1952,9 +1952,9 @@ defmodule Module.Types.Descr do if empty?(last), do: lines_acc, - else: list_bdd_get_pos(list_acc, last, right, lines_acc) + else: list_bdd_to_pos_dnf(list_acc, last, right, lines_acc) else - list_bdd_get_pos(list_acc, last_acc, right, lines_acc) + list_bdd_to_pos_dnf(list_acc, last_acc, right, lines_acc) end # Case 2: count the list_type positively. @@ -1964,7 +1964,7 @@ defmodule Module.Types.Descr do if empty?(list_acc) or empty?(last_acc) do lines_acc else - list_bdd_get_pos(list_acc, last_acc, left, lines_acc) + list_bdd_to_pos_dnf(list_acc, last_acc, left, lines_acc) end end end @@ -2120,7 +2120,7 @@ defmodule Module.Types.Descr do defp list_hd_static(:term), do: :term defp list_hd_static(%{list: bdd}) do - list_bdd_get_pos(bdd) + list_bdd_to_pos_dnf(bdd) |> Enum.reduce(none(), fn {list, _}, acc -> union(list, acc) end) @@ -2172,7 +2172,7 @@ defmodule Module.Types.Descr do %{list: bdd} end - list_bdd_get_pos(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) + list_bdd_to_pos_dnf(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) end defp list_tl_static(%{}), do: none() @@ -2237,7 +2237,7 @@ defmodule Module.Types.Descr do # Eliminate empty lists from the union, and redundant types (that are subtypes of others, # or that can be merged with others). defp list_normalize(bdd) do - list_bdd_get(bdd) + list_bdd_to_dnf(bdd) |> Enum.reduce([], fn {{list, last}, negs}, acc -> # First, try to eliminate the negations from the existing type. {list, last, negs} = From 7b780c1a6d5fe33a44466325fa1f097c9f86160d Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 11:57:24 +0200 Subject: [PATCH 28/32] Make fun_empty? short-circuiting --- lib/elixir/lib/module/types/descr.ex | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 5b1736a2db2..9a834c5ab4f 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1440,7 +1440,20 @@ defmodule Module.Types.Descr do # - `fun(1) and not fun(1)` is empty # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty - defp fun_empty?(bdd), do: fun_bdd_to_dnf(bdd) == [] + defp fun_empty?(bdd), do: fun_bdd_empty?([], [], bdd) + + defp fun_bdd_empty?(pos, neg, bdd) do + case bdd do + :bdd_bot -> + true + + :bdd_top -> + fun_empty?(pos, neg) + + {fun, left, right} -> + fun_bdd_empty?([fun | pos], neg, left) and fun_bdd_empty?(pos, [fun | neg], right) + end + end # Checks if a function type represented by positive and negative function literals is empty. From 8dfaa10da878b4e78ec84f47b3b6c957790ba6c0 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 11:58:37 +0200 Subject: [PATCH 29/32] Naming fun_line_empty? for precision --- lib/elixir/lib/module/types/descr.ex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 9a834c5ab4f..e0040cb1e78 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1421,7 +1421,7 @@ defmodule Module.Types.Descr do acc :bdd_top -> - if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] + if fun_line_empty?(pos, neg), do: acc, else: [{pos, neg} | acc] {fun, left, right} -> fun_bdd_to_dnf(fun_bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right) @@ -1448,7 +1448,7 @@ defmodule Module.Types.Descr do true :bdd_top -> - fun_empty?(pos, neg) + fun_line_empty?(pos, neg) {fun, left, right} -> fun_bdd_empty?([fun | pos], neg, left) and fun_bdd_empty?(pos, [fun | neg], right) @@ -1468,9 +1468,9 @@ defmodule Module.Types.Descr do # - `{[fun(integer() -> atom())], [fun(none() -> term())]}` is empty # - `{[], _}` (representing the top function type fun()) is never empty # - defp fun_empty?([], _), do: false + defp fun_line_empty?([], _), do: false - defp fun_empty?(positives, negatives) do + defp fun_line_empty?(positives, negatives) do case fetch_arity_and_domain(positives) do # If there are functions with different arities in positives, then the function type is empty {:empty, _} -> From 8221515e47364ecafb3a7eb06f24020a0a485947 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Thu, 18 Sep 2025 12:07:39 +0200 Subject: [PATCH 30/32] Remove high order list_empty? implem --- lib/elixir/lib/module/types/descr.ex | 64 +++++++++++++++------------- 1 file changed, 34 insertions(+), 30 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index e0040cb1e78..ac9f8d590f3 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1932,11 +1932,18 @@ defmodule Module.Types.Descr do acc :bdd_top -> - if list_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc] + if list_line_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc] - {{list, tail} = list_type, left, right} -> - new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)} - list_bdd_to_dnf(list_bdd_to_dnf(acc, new_pos, negs, left), pos, [list_type | negs], right) + {{list, tail} = next_list, left, right} -> + try do + li = non_empty_intersection!(list_acc, list) + la = non_empty_intersection!(tail_acc, tail) + + list_bdd_to_dnf(acc, {li, la}, negs, left) + |> list_bdd_to_dnf(pos, [next_list | negs], right) + catch + :empty -> list_bdd_to_dnf(acc, pos, [next_list | negs], right) + end end end @@ -1982,30 +1989,6 @@ defmodule Module.Types.Descr do end end - # Takes all the lines from the root to the leaves finishing with a 1, computes the intersection - # of the positives, and calls the condition on the result. Checks it is true for all of them. - # As if calling Enum.all? on all the lines of the bdd. - defp list_all?(bdd, condition), do: list_all?({:term, :term}, [], bdd, condition) - - defp list_all?({list_acc, tail_acc} = pos, negs, bdd, condition) do - case bdd do - :bdd_bot -> - true - - :bdd_top -> - condition.(list_acc, tail_acc, negs) - - {{list, tail} = list_type, left, right} -> - list_all?( - {intersection(list_acc, list), intersection(tail_acc, tail)}, - negs, - left, - condition - ) and - list_all?(pos, [list_type | negs], right, condition) - end - end - defp list_pop_dynamic(:term), do: {false, :term} defp list_pop_dynamic(descr) do @@ -2076,9 +2059,30 @@ defmodule Module.Types.Descr do end defp list_empty?(@non_empty_list_top), do: false - defp list_empty?(bdd), do: list_all?(bdd, &list_empty?/3) + defp list_empty?(bdd), do: list_bdd_empty?({:term, :term}, [], bdd) + + defp list_bdd_empty?({list_acc, tail_acc} = pos, negs, bdd) do + case bdd do + :bdd_bot -> + true + + :bdd_top -> + list_line_empty?(list_acc, tail_acc, negs) + + {{list, tail} = list_type, left, right} -> + try do + li = non_empty_intersection!(list_acc, list) + la = non_empty_intersection!(tail_acc, tail) + + list_bdd_empty?({li, la}, negs, left) and + list_bdd_empty?(pos, [list_type | negs], right) + catch + :empty -> list_bdd_empty?(pos, [list_type | negs], right) + end + end + end - defp list_empty?(list_type, last_type, negs) do + defp list_line_empty?(list_type, last_type, negs) do last_type = list_tail_unfold(last_type) # To make a list {list, last} empty with some negative lists: # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one. From d157f5fe8e444e324be7b7ea1ad57196c36f924b Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Sun, 28 Sep 2025 18:48:44 +0200 Subject: [PATCH 31/32] Improve map_line_empty and emptiness algoriths The key change is that map_line_empty was checking the whole tree no matter what, due to an or condition that should not be checked as the previous Enum.all? are enough to conclude. Also clarified the invariant that allows not to check the positives fields as a base case (still in map_line_empty?) --- lib/elixir/lib/module/types/descr.ex | 271 ++++++++++++++------------- 1 file changed, 142 insertions(+), 129 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index ac9f8d590f3..09bc3ad7eab 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1440,19 +1440,9 @@ defmodule Module.Types.Descr do # - `fun(1) and not fun(1)` is empty # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty - defp fun_empty?(bdd), do: fun_bdd_empty?([], [], bdd) - - defp fun_bdd_empty?(pos, neg, bdd) do - case bdd do - :bdd_bot -> - true - - :bdd_top -> - fun_line_empty?(pos, neg) - - {fun, left, right} -> - fun_bdd_empty?([fun | pos], neg, left) and fun_bdd_empty?(pos, [fun | neg], right) - end + defp fun_empty?(bdd) do + bdd_to_dnf(bdd) + |> Enum.all?(fn {pos, neg} -> fun_line_empty?(pos, neg) end) end # Checks if a function type represented by positive and negative function literals is empty. @@ -2058,28 +2048,26 @@ defmodule Module.Types.Descr do end end - defp list_empty?(@non_empty_list_top), do: false - defp list_empty?(bdd), do: list_bdd_empty?({:term, :term}, [], bdd) - - defp list_bdd_empty?({list_acc, tail_acc} = pos, negs, bdd) do - case bdd do - :bdd_bot -> - true - - :bdd_top -> - list_line_empty?(list_acc, tail_acc, negs) + defp non_empty_list_literals_intersection(list_literals) do + try do + Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} -> + {non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)} + end) + catch + :empty -> :empty + end + end - {{list, tail} = list_type, left, right} -> - try do - li = non_empty_intersection!(list_acc, list) - la = non_empty_intersection!(tail_acc, tail) + defp list_empty?(@non_empty_list_top), do: false - list_bdd_empty?({li, la}, negs, left) and - list_bdd_empty?(pos, [list_type | negs], right) - catch - :empty -> list_bdd_empty?(pos, [list_type | negs], right) - end - end + defp list_empty?(bdd) do + bdd_to_dnf(bdd) + |> Enum.all?(fn {pos, negs} -> + case non_empty_list_literals_intersection(pos) do + :empty -> true + {list, last} -> list_line_empty?(list, last, negs) + end + end) end defp list_line_empty?(list_type, last_type, negs) do @@ -2774,27 +2762,21 @@ defmodule Module.Types.Descr do # Takes all the lines from the root to the leaves finishing with a 1, # and compile into tuples of positive and negative nodes. Positive nodes are # those followed by a left path, negative nodes are those followed by a right path. - def map_bdd_to_dnf(bdd), do: map_bdd_to_dnf([], {:open, %{}}, [], bdd) - - defp map_bdd_to_dnf(acc, {tag, fields} = map, negs, bdd) do - case bdd do - :bdd_bot -> - acc - - :bdd_top -> - if map_line_empty?(tag, fields, negs), do: acc, else: [{tag, fields, negs} | acc] + def map_bdd_to_dnf(bdd) do + bdd_to_dnf(bdd) + |> Enum.reduce([], fn {pos, negs}, acc -> + case non_empty_map_literals_intersection(pos) do + :empty -> + acc - {{next_tag, next_fields} = next_map, left, right} -> - acc = - try do - new_pos = map_literal_intersection(tag, fields, next_tag, next_fields) - map_bdd_to_dnf(acc, new_pos, negs, left) - catch - :empty -> acc + {tag, fields} -> + if init_map_line_empty?(tag, fields, negs) do + acc + else + [{tag, fields, negs} | acc] end - - map_bdd_to_dnf(acc, map, [next_map | negs], right) - end + end + end) end @doc """ @@ -3430,30 +3412,44 @@ defmodule Module.Types.Descr do {true, maybe_union(initial, fn -> term() end), open_map()} end + defp non_empty_map_literals_intersection(maps) do + try do + Enum.reduce(maps, {:open, %{}}, fn {next_tag, next_fields}, {tag, fields} -> + map_literal_intersection(tag, fields, next_tag, next_fields) + end) + catch + :empty -> :empty + end + end + # Short-circuits if it finds a non-empty map literal in the union. # Since the algorithm is recursive, we implement the short-circuiting # as throw/catch. - defp map_empty?(bdd), do: map_bdd_empty?({:open, %{}}, [], bdd) - - defp map_bdd_empty?({tag, fields} = map, negs, bdd) do - case bdd do - :bdd_bot -> - true - - :bdd_top -> - map_line_empty?(tag, fields, negs) + defp map_empty?(bdd) do + bdd_to_dnf(bdd) + |> Enum.all?(fn {pos, negs} -> + case non_empty_map_literals_intersection(pos) do + :empty -> + true + + {tag, fields} when is_map(fields) -> + # We check the emptiness of the fields because non_empty_map_literal_intersection + # will not return :empty on fields that are set to none() and that exist + # just in one map, but not the other. + init_map_line_empty?(tag, fields, negs) + end + end) + end - {{next_tag, next_fields} = next_map, left, right} -> - try do - new_map = map_literal_intersection(tag, fields, next_tag, next_fields) - map_bdd_empty?(new_map, negs, left) and map_bdd_empty?(map, [next_map | negs], right) - catch - :empty -> map_bdd_empty?(map, [next_map | negs], right) - end - end + defp init_map_line_empty?(tag, fields, negs) do + Enum.any?(Map.to_list(fields), fn {_key, type} -> empty?(type) end) or + map_line_empty?(tag, fields, negs) end - defp map_line_empty?(_, pos, []), do: Enum.any?(Map.to_list(pos), fn {_, v} -> empty?(v) end) + # These positives get checked once when calling init_map_line_empty?, and then every time + # an intersection or difference is computed, its emptiness is checked again. + # So they are all necessarily non-empty. + defp map_line_empty?(_, _pos, []), do: false defp map_line_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true defp map_line_empty?(:open, fs, [{:closed, _} | negs]), do: map_line_empty?(:open, fs, negs) @@ -3462,48 +3458,49 @@ defmodule Module.Types.Descr do atom_default = map_key_tag_to_type(tag) neg_atom_default = map_key_tag_to_type(neg_tag) - (Enum.all?(Map.to_list(neg_fields), fn {neg_key, neg_type} -> - cond do - # Ignore keys present in both maps; will be handled below - is_map_key(fields, neg_key) -> - true - - # The key is not shared between positive and negative maps, - # if the negative type is optional, then there may be a value in common - tag == :closed -> - is_optional_static(neg_type) - - # There may be value in common - tag == :open -> - diff = difference(term_or_optional(), neg_type) - empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) - - true -> - diff = difference(atom_default, neg_type) - empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) - end - end) and - Enum.all?(Map.to_list(fields), fn {key, type} -> - case neg_fields do - %{^key => neg_type} -> - diff = difference(type, neg_type) - empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) - - %{} -> - cond do - neg_tag == :open -> - true - - neg_tag == :closed and not is_optional_static(type) -> - false - - true -> - # an absent key in a open negative map can be ignored - diff = difference(type, neg_atom_default) - empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) - end - end - end)) or map_line_empty?(tag, fields, negs) + Enum.all?(Map.to_list(neg_fields), fn {neg_key, neg_type} -> + cond do + # Ignore keys present in both maps; will be handled below + is_map_key(fields, neg_key) -> + true + + # The keys is only in the negative map, and the positive map is closed + # in that case, this field is not_set(), and its difference with the negative map type is empty iff + # the negative type is optional. + tag == :closed -> + is_optional_static(neg_type) or + map_line_empty?(tag, fields, negs) + + # There may be value in common + tag == :open -> + diff = difference(term_or_optional(), neg_type) + empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) + + true -> + diff = difference(atom_default, neg_type) + empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs) + end + end) and + Enum.all?(Map.to_list(fields), fn {key, type} -> + case neg_fields do + %{^key => neg_type} -> + diff = difference(type, neg_type) + empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) + + %{} -> + cond do + # The key is only in the positive map, while the negative map is open + # so this key is absorbed (e.g. %{a: integer} and not %{...}) + neg_tag == :open -> + true + + true -> + # an absent key in a open negative map can be ignored + diff = difference(type, neg_atom_default) + empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs) + end + end + end) else map_line_empty?(tag, fields, negs) end @@ -3892,28 +3889,29 @@ defmodule Module.Types.Descr do defp tuple_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2) - defp tuple_empty?(bdd), do: tuple_bdd_empty?({:open, []}, [], bdd) - - defp tuple_bdd_empty?({tag, elements} = pos, negs, bdd) do - case bdd do - :bdd_bot -> - true - - :bdd_top -> - tuple_line_empty?(tag, elements, negs) - - {{next_tag, next_elements} = next_tuple, left, right} -> + defp non_empty_tuple_literals_intersection(tuples) do + try do + Enum.reduce(tuples, {:open, []}, fn {next_tag, next_elements}, {tag, elements} -> case tuple_literal_intersection(tag, elements, next_tag, next_elements) do - :empty -> - tuple_bdd_empty?(pos, [next_tuple | negs], right) - - new_tuple -> - tuple_bdd_empty?(new_tuple, negs, left) and - tuple_bdd_empty?(pos, [next_tuple | negs], right) + :empty -> throw(:empty) + next -> next end + end) + catch + :empty -> :empty end end + defp tuple_empty?(bdd) do + bdd_to_dnf(bdd) + |> Enum.all?(fn {pos, negs} -> + case non_empty_tuple_literals_intersection(pos) do + :empty -> true + {tag, fields} -> tuple_line_empty?(tag, fields, negs) + end + end) + end + # No negations, so not empty unless there's an empty type # Note: since the extraction from the BDD is done in a way that guarantees that # the elements are non-empty, we can avoid checking for empty types there. @@ -4589,6 +4587,21 @@ defmodule Module.Types.Descr do end end + defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd) + + defp bdd_to_dnf(acc, pos, neg, bdd) do + case bdd do + :bdd_bot -> + acc + + :bdd_top -> + [{pos, neg} | acc] + + {fun, left, right} -> + bdd_to_dnf(bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right) + end + end + ## Pairs # To simplify disjunctive normal forms of e.g., map types, it is useful to From c1c7249d4b16991cf74147714323c0f3ab1b83de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Sun, 28 Sep 2025 18:49:25 +0200 Subject: [PATCH 32/32] Use simpler algorithm for inferred clauses --- lib/elixir/lib/module/types/descr.ex | 70 +++++++++---------- .../test/elixir/module/types/descr_test.exs | 49 +++++-------- 2 files changed, 48 insertions(+), 71 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 09bc3ad7eab..6fe1251aadd 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -167,61 +167,55 @@ defmodule Module.Types.Descr do domain_clauses = Enum.reduce(args_clauses, [], fn {args, return}, acc -> domain = args |> Enum.map(&upper_bound/1) |> args_to_domain() - pivot_overlapping_clause(domain, upper_bound(return), acc) + return = upper_bound(return) + pivot_overlapping_clause(domain, return, return, acc) end) funs = - for {domain, return} <- domain_clauses, + for {domain, _return, union} <- domain_clauses, args <- domain_to_args(domain), - do: fun(args, dynamic(return)) + do: fun(args, dynamic(union)) Enum.reduce(funs, &intersection/2) end - # Inserts a new arrow `{domain, return}` into `acc`, a list whose arrows - # have disjoint domains. + # If you have a function with multiple clauses, they may overlap, + # and we need to find the correct return type. This can be done + # in two different algorithms: a precise and a fast one. + # Consider the inferred clauses: # - # To preserve that invariant we compare the new arrow with every function in - # the accumulator, `{acc_domain, acc_return}`: + # (integer() or atom() -> :foo) and (integer() or float() -> :bar) # - # * If `intersection(domain, acc_domain)` is empty, the arrows do not overlap. - # We keep the current arrow and recurse on the tail. + # The precise algorithm works by finding the intersections between + # domains, assigning it the union, and then computing the leftovers + # on each side. The trouble of this approach is that it builds + # differences, which can be expensive, and can lead to several new + # clauses. For example, the clause above would emit: # - # * Otherwise, the domains overlap. We partition them into: + # (integer() -> :foo or :bar) and (atom() -> :foo) and (float() -> :bar) # - # common = intersection(domain, acc_domain) # shared part - # diff = difference(domain, acc_domain) # only in new arrow - # left = difference(acc_domain, domain) # only in existing arrow + # Due to performance constraints, we chose the fast approach, which + # leads to broad return types, but this is acceptable because we mark + # all return types as dynamic anyway. Therefore we infer the type: # - # We emit `{common, union(return, acc_return)}` for the shared part, - # keep `{left, acc_return}` (if any), and continue inserting `diff` - # into the remainder of the list to handle further overlaps. - defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do - common = intersection(domain, acc_domain) - - if empty?(common) do - [{acc_domain, acc_return} | pivot_overlapping_clause(domain, return, acc)] + # (integer() or atom() -> :foo or :bar) and (integer() or float() -> :foo or :bar) + # + defp pivot_overlapping_clause(domain, return, union, [{acc_domain, acc_return, acc_union} | acc]) do + if disjoint?(domain, acc_domain) do + [ + {acc_domain, acc_return, acc_union} + | pivot_overlapping_clause(domain, return, union, acc) + ] else - diff = difference(domain, acc_domain) - - rest = - if empty?(diff) do - [] - else - pivot_overlapping_clause(diff, return, acc) - end - - [{common, union(return, acc_return)} | rest] - |> prepend_to_unless_empty(difference(acc_domain, domain), acc_return) + [ + {acc_domain, acc_return, union(return, acc_union)} + | pivot_overlapping_clause(domain, return, union(acc_return, union), acc) + ] end end - defp pivot_overlapping_clause(domain, return, []) do - [{domain, return}] - end - - defp prepend_to_unless_empty(acc, domain, return) do - if empty?(domain), do: acc, else: [{domain, return} | acc] + defp pivot_overlapping_clause(domain, return, union, []) do + [{domain, return, union}] end @doc """ diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index d45ed220dec..205cacb4e9e 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -964,24 +964,18 @@ defmodule Module.Types.DescrTest do # Subsets assert fun_from_inferred_clauses([{[integer()], atom()}, {[number()], binary()}]) |> equal?( - intersection( - fun_from_non_overlapping_clauses([ - {[integer()], union(atom(), binary())}, - {[float()], binary()} - ]), - fun([number()], dynamic()) - ) + fun_from_non_overlapping_clauses([ + {[integer()], dynamic(union(atom(), binary()))}, + {[number()], dynamic(union(atom(), binary()))} + ]) ) assert fun_from_inferred_clauses([{[number()], binary()}, {[integer()], atom()}]) |> equal?( - intersection( - fun_from_non_overlapping_clauses([ - {[integer()], union(atom(), binary())}, - {[float()], binary()} - ]), - fun([number()], dynamic()) - ) + fun_from_non_overlapping_clauses([ + {[integer()], dynamic(union(atom(), binary()))}, + {[number()], dynamic(union(atom(), binary()))} + ]) ) # Partial @@ -990,14 +984,10 @@ defmodule Module.Types.DescrTest do {[union(float(), pid())], binary()} ]) |> equal?( - intersection( - fun_from_non_overlapping_clauses([ - {[integer()], atom()}, - {[float()], binary()}, - {[pid()], union(atom(), binary())} - ]), - fun([union(number(), pid())], dynamic()) - ) + fun_from_non_overlapping_clauses([ + {[union(integer(), pid())], dynamic(union(atom(), binary()))}, + {[union(float(), pid())], dynamic(union(atom(), binary()))} + ]) ) # Difference @@ -1006,17 +996,10 @@ defmodule Module.Types.DescrTest do {[number(), pid()], binary()} ]) |> equal?( - intersection( - fun_from_non_overlapping_clauses([ - {[float(), pid()], binary()}, - {[integer(), atom()], atom()}, - {[integer(), pid()], union(atom(), binary())} - ]), - fun_from_non_overlapping_clauses([ - {[integer(), union(pid(), atom())], dynamic()}, - {[number(), pid()], dynamic()} - ]) - ) + fun_from_non_overlapping_clauses([ + {[integer(), union(pid(), atom())], dynamic(union(atom(), binary()))}, + {[number(), pid()], dynamic(union(atom(), binary()))} + ]) ) end end