diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 185e60dee2..1d857880ee 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -1795,13 +1795,12 @@ defmodule Module.Types.Descr do # # 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. + # variant from the positive one. This is done in list_bdd_to_pos_dnf/1. {list_type, last_type} = 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) - {union(head, acc_head), union(tail, acc_tail)} + {list, last, _negs}, {acc_list, acc_last} -> + {union(list, acc_list), union(last, acc_last)} end) list_new(list_type, last_type) @@ -1829,40 +1828,34 @@ defmodule Module.Types.Descr do 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. - defp list_bdd_to_dnf(bdd) do - bdd_to_dnf(bdd) - |> Enum.reduce([], fn {pos_list, neg_list}, acc -> - case non_empty_list_literals_intersection(pos_list) do - :empty -> - acc - - {list, last} -> - if list_line_empty?(list, last, neg_list), - do: acc, - else: [{{list, last}, neg_list} | acc] - end - 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. 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_bdd_to_pos_dnf(bdd) do bdd_to_dnf(bdd) - |> Enum.reduce([], fn {pos_list, neg_list}, acc -> + |> Enum.reduce([], fn {pos_list, negs}, acc -> case non_empty_list_literals_intersection(pos_list) do :empty -> acc {list, last} -> - if list_line_empty?(list, last, neg_list), do: acc, else: [{list, last} | acc] + Enum.reduce_while(negs, {last, []}, fn {neg_type, neg_last}, {acc_last, acc_negs} -> + if subtype?(list, neg_type) do + difference = difference(acc_last, neg_last) + if empty?(difference), do: {:halt, nil}, else: {:cont, {difference, acc_negs}} + else + {:cont, {acc_last, [{neg_type, neg_last} | acc_negs]}} + end + end) + |> case do + nil -> acc + {last, negs} -> [{list, last, Enum.reverse(negs)} | acc] + end end end) end @@ -1885,6 +1878,38 @@ defmodule Module.Types.Descr do defp list_top?(bdd_leaf(:term, :term)), do: true defp list_top?(_), do: false + @doc """ + Checks if a list type is a proper list (terminated by empty list). + """ + def list_proper?(:term), do: false + def list_proper?(%{} = descr), do: Map.get(descr, :dynamic, descr) |> list_proper_static?() + + defp list_proper_static?(:term), do: false + + defp list_proper_static?(%{} = descr) do + # A list is proper if it's either the empty list alone, or all non-empty + # list types have tails that are subtypes of empty list + case descr do + %{bitmap: bitmap, list: bdd} -> + (bitmap &&& @bit_empty_list) != 0 and empty?(Map.drop(descr, [:list, :bitmap])) and + list_bdd_proper?(bdd) + + %{bitmap: bitmap} -> + (bitmap &&& @bit_empty_list) != 0 and empty?(Map.delete(descr, :bitmap)) + + %{list: bdd} -> + empty?(Map.delete(descr, :list)) and list_bdd_proper?(bdd) + + %{} -> + empty?(descr) + end + end + + defp list_bdd_proper?(bdd) do + list_bdd_to_pos_dnf(bdd) + |> Enum.all?(fn {_list, last, _negs} -> subtype?(last, @empty_list) end) + end + defp list_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do try do list = non_empty_intersection!(list1, list2) @@ -1914,10 +1939,16 @@ defmodule Module.Types.Descr do # The result may be larger than the initial bdd1, which is maintained in the accumulator. defp list_difference(bdd_leaf(list1, last1) = bdd1, bdd_leaf(list2, last2) = bdd2) do cond do - disjoint?(list1, list2) or disjoint?(last1, last2) -> bdd_leaf(list1, last1) - subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot - equal?(list1, list2) -> bdd_leaf(list1, difference(last1, last2)) - true -> bdd_difference(bdd1, bdd2) + disjoint?(list1, list2) or disjoint?(last1, last2) -> + bdd_leaf(list1, last1) + + subtype?(list1, list2) -> + if subtype?(last1, last2), + do: :bdd_bot, + else: bdd_leaf(list1, difference(last1, last2)) + + true -> + bdd_difference(bdd1, bdd2) end end @@ -1991,20 +2022,17 @@ defmodule Module.Types.Descr do defp list_hd_static(%{list: bdd}) do list_bdd_to_pos_dnf(bdd) - |> Enum.reduce(none(), fn {list, _}, acc -> - union(list, acc) - end) + |> Enum.reduce(none(), fn {list, _last, _negs}, acc -> union(acc, list) end) end defp list_hd_static(%{}), do: none() @doc """ - Returns the tail of a list. + Returns the tail of a list. - Errors on a possibly empty list. - On a non empty list of integers, it returns a (possibly empty) list of integers. - On a non empty list of integers, with an atom tail element, it returns either an atom, - or a (possibly empty) list of integers with an atom tail element. + For a `non_empty_list(t)`, the tail type is `list(t)`. + For an improper list `non_empty_list(t, s)`, the tail type is + `list(t, s) or s` (either the rest of the list or the terminator) """ def list_tl(:term), do: :badnonemptylist @@ -2042,7 +2070,8 @@ defmodule Module.Types.Descr do %{list: bdd} end - list_bdd_to_pos_dnf(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end) + list_bdd_to_pos_dnf(bdd) + |> Enum.reduce(initial, fn {_list, last, _negs}, acc -> union(acc, last) end) end defp list_tl_static(%{}), do: none() @@ -2054,12 +2083,19 @@ defmodule Module.Types.Descr do dnf |> Enum.reduce({[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} -> {name, arguments, list_rendered?} = - if subtype?(last_type, @empty_list) do - name = if empty?, do: :list, else: :non_empty_list - {name, [to_quoted(list_type, opts)], empty?} - else - args = [to_quoted(list_type, opts), to_quoted(last_type, opts)] - {:non_empty_list, args, list_rendered?} + cond do + subtype?(last_type, @empty_list) -> + name = if empty?, do: :list, else: :non_empty_list + {name, [to_quoted(list_type, opts)], empty?} + + # Sugar: print the last type as term() if it only misses non empty lists. + subtype?(@not_non_empty_list, last_type) -> + args = [to_quoted(list_type, opts), {:term, [], []}] + {:non_empty_list, args, list_rendered?} + + true -> + args = [to_quoted(list_type, opts), to_quoted(last_type, opts)] + {:non_empty_list, args, list_rendered?} end acc = @@ -2096,27 +2132,19 @@ defmodule Module.Types.Descr do end # Eliminate empty lists from the union, and redundant types (that are subtypes of others, - # or that can be merged with others). + # or that can be merged with others). List_bdd_to_pos_dnf already takes into account the + # impact of negations on the last type. defp list_normalize(bdd) do - 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} = + list_bdd_to_pos_dnf(bdd) + |> Enum.reduce([], fn {list, last, negs}, acc -> + # Prune negations from those with empty intersections. + 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 + |> Enum.filter(fn {nlist, nlast} -> + not empty?(intersection(list, nlist)) and not empty?(intersection(last, nlast)) end) - add_to_list_normalize(acc, list, last, negs |> Enum.reverse()) + add_to_list_normalize(acc, list, last, negs) end) end diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs index 49d3eed89b..1ef9fb7818 100644 --- a/lib/elixir/test/elixir/module/types/descr_test.exs +++ b/lib/elixir/test/elixir/module/types/descr_test.exs @@ -1249,6 +1249,7 @@ defmodule Module.Types.DescrTest do assert list_hd(non_empty_list(term())) == {:ok, term()} assert list_hd(non_empty_list(integer())) == {:ok, integer()} assert list_hd(difference(list(number()), list(integer()))) == {:ok, number()} + assert list_hd(non_empty_list(atom(), float())) == {:ok, atom()} assert list_hd(dynamic()) == {:ok, dynamic()} assert list_hd(dynamic(list(integer()))) == {:ok, dynamic(integer())} @@ -1267,6 +1268,27 @@ defmodule Module.Types.DescrTest do assert list_hd(non_empty_list(atom(), negation(list(term(), term())))) == {:ok, atom()} end + test "list_proper?" do + assert list_proper?(term()) == false + assert list_proper?(none()) == true + assert list_proper?(empty_list()) == true + assert list_proper?(non_empty_list(integer())) == true + assert list_proper?(non_empty_list(integer(), atom())) == false + assert list_proper?(non_empty_list(integer(), term())) == false + assert list_proper?(non_empty_list(integer(), list(term()))) == true + assert list_proper?(list(integer()) |> union(list(integer(), integer()))) == false + assert list_proper?(dynamic(list(integer()))) == true + assert list_proper?(dynamic(list(integer(), atom()))) == false + + # An empty list + list_with_tail = + non_empty_list(atom(), union(integer(), empty_list())) + |> difference(non_empty_list(atom([:ok]), integer())) + |> difference(non_empty_list(atom(), term())) + + assert list_proper?(list_with_tail) == true + end + test "list_tl" do assert list_tl(none()) == :badnonemptylist assert list_tl(term()) == :badnonemptylist @@ -1284,11 +1306,9 @@ defmodule Module.Types.DescrTest do # integers with an atom tail, or a (possibly empty) list of tuples with a float tail. assert list_tl(union(non_empty_list(integer(), atom()), non_empty_list(tuple(), float()))) == {:ok, - atom() - |> union(float()) - |> union( - union(non_empty_list(integer(), atom()), non_empty_list(tuple(), float())) - )} + union(atom(), float()) + |> union(non_empty_list(integer(), atom())) + |> union(non_empty_list(tuple(), float()))} assert list_tl(dynamic()) == {:ok, dynamic()} assert list_tl(dynamic(list(integer()))) == {:ok, dynamic(list(integer()))} @@ -2391,6 +2411,14 @@ defmodule Module.Types.DescrTest do assert union(dynamic(list(integer(), float())), dynamic(list(integer(), pid()))) |> to_quoted_string() == "dynamic(empty_list() or non_empty_list(integer(), float() or pid()))" + + list_with_tail = + non_empty_list(atom(), union(integer(), empty_list())) + |> difference(non_empty_list(atom([:ok]), integer())) + |> difference(non_empty_list(atom(), integer())) + + # Check that simplifications occur. + assert to_quoted_string(list_with_tail) == "non_empty_list(atom())" end test "tuples" do