Skip to content

Commit 743fa8a

Browse files
committed
Propagate BDD leaf nodes down the tree on intersections
LazyBDDs allowed us to represent all operations lazily but the issue is that we want to propagate intersections eagerly, as they allow us to cut down the number of nodes in the tree. So whenever we have a leaf node, we propagate it throughout the whole tree, cutting down the number of nodes considerably and optimizing type checking. Before: [profile] Finished group pass check of 1765 modules in 13506ms After: [profile] Finished group pass check of 1765 modules in 2454ms
1 parent 995f7fc commit 743fa8a

File tree

1 file changed

+82
-33
lines changed

1 file changed

+82
-33
lines changed

lib/elixir/lib/module/types/descr.ex

Lines changed: 82 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1981,21 +1981,24 @@ defmodule Module.Types.Descr do
19811981
{empty_list, none()}
19821982
end
19831983

1984-
defp list_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
1985-
try do
1986-
list = non_empty_intersection!(list1, list2)
1987-
last = non_empty_intersection!(last1, last2)
1988-
bdd_leaf(list, last)
1989-
catch
1990-
:empty -> :bdd_bot
1991-
end
1992-
end
1993-
19941984
defp list_intersection(bdd1, bdd2) do
19951985
cond do
1996-
list_top?(bdd1) and is_tuple(bdd2) -> bdd2
1997-
list_top?(bdd2) and is_tuple(bdd1) -> bdd1
1998-
true -> bdd_intersection(bdd1, bdd2)
1986+
list_top?(bdd1) and is_tuple(bdd2) ->
1987+
bdd2
1988+
1989+
list_top?(bdd2) and is_tuple(bdd1) ->
1990+
bdd1
1991+
1992+
true ->
1993+
bdd_intersection(bdd1, bdd2, fn bdd_leaf(list1, last1), bdd_leaf(list2, last2) ->
1994+
try do
1995+
list = non_empty_intersection!(list1, list2)
1996+
last = non_empty_intersection!(last1, last2)
1997+
bdd_leaf(list, last)
1998+
catch
1999+
:empty -> :bdd_bot
2000+
end
2001+
end)
19992002
end
20002003
end
20012004

@@ -2594,21 +2597,23 @@ defmodule Module.Types.Descr do
25942597
defp map_top?(bdd_leaf(:open, fields)) when map_size(fields) == 0, do: true
25952598
defp map_top?(_), do: false
25962599

2597-
defp map_intersection(bdd_leaf(tag1, fields1), bdd_leaf(tag2, fields2)) do
2598-
try do
2599-
{tag, fields} = map_literal_intersection(tag1, fields1, tag2, fields2)
2600-
bdd_leaf(tag, fields)
2601-
catch
2602-
:empty -> :bdd_bot
2603-
end
2604-
end
2605-
26062600
defp map_intersection(bdd1, bdd2) do
2607-
# If intersecting with the top map type, no-op
26082601
cond do
2609-
map_top?(bdd1) and is_tuple(bdd2) -> bdd2
2610-
map_top?(bdd2) and is_tuple(bdd1) -> bdd1
2611-
true -> bdd_intersection(bdd1, bdd2)
2602+
map_top?(bdd1) and is_tuple(bdd2) ->
2603+
bdd2
2604+
2605+
map_top?(bdd2) and is_tuple(bdd1) ->
2606+
bdd1
2607+
2608+
true ->
2609+
bdd_intersection(bdd1, bdd2, fn bdd_leaf(tag1, fields1), bdd_leaf(tag2, fields2) ->
2610+
try do
2611+
{tag, fields} = map_literal_intersection(tag1, fields1, tag2, fields2)
2612+
bdd_leaf(tag, fields)
2613+
catch
2614+
:empty -> :bdd_bot
2615+
end
2616+
end)
26122617
end
26132618
end
26142619

@@ -4083,15 +4088,15 @@ defmodule Module.Types.Descr do
40834088

40844089
defp tuple_new(tag, elements), do: bdd_leaf(tag, elements)
40854090

4086-
defp tuple_intersection(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
4087-
case tuple_literal_intersection(tag1, elements1, tag2, elements2) do
4088-
{tag, elements} -> bdd_leaf(tag, elements)
4089-
:empty -> :bdd_bot
4090-
end
4091+
defp tuple_intersection(bdd1, bdd2) do
4092+
bdd_intersection(bdd1, bdd2, fn bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2) ->
4093+
case tuple_literal_intersection(tag1, elements1, tag2, elements2) do
4094+
{tag, elements} -> bdd_leaf(tag, elements)
4095+
:empty -> :bdd_bot
4096+
end
4097+
end)
40914098
end
40924099

4093-
defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2)
4094-
40954100
defp tuple_literal_intersection(:open, [], tag, elements), do: {tag, elements}
40964101

40974102
defp tuple_literal_intersection(tag1, elements1, tag2, elements2) do
@@ -4975,6 +4980,50 @@ defmodule Module.Types.Descr do
49754980
defp bdd_intersection_union(i, u1, u2),
49764981
do: bdd_intersection(i, bdd_union(u1, u2))
49774982

4983+
# Intersections are great because they allow us to cut down
4984+
# the number of nodes in the tree. So whenever we have a leaf,
4985+
# we actually propagate it throughout the whole tree, cutting
4986+
# down nodes.
4987+
defp bdd_intersection(bdd_leaf(_, _) = leaf, bdd, leaf_intersection) do
4988+
bdd_leaf_intersection(leaf, bdd, leaf_intersection)
4989+
end
4990+
4991+
defp bdd_intersection(bdd, bdd_leaf(_, _) = leaf, leaf_intersection) do
4992+
bdd_leaf_intersection(leaf, bdd, leaf_intersection)
4993+
end
4994+
4995+
defp bdd_intersection(bdd1, bdd2, _leaf_intersection) do
4996+
bdd_intersection(bdd1, bdd2)
4997+
end
4998+
4999+
defp bdd_leaf_intersection(leaf, bdd, intersection) do
5000+
case bdd do
5001+
:bdd_top ->
5002+
leaf
5003+
5004+
:bdd_bot ->
5005+
:bdd_bot
5006+
5007+
bdd_leaf(_, _) ->
5008+
intersection.(leaf, bdd)
5009+
5010+
{lit, _, _, _} when lit == leaf ->
5011+
bdd
5012+
5013+
{lit, c, u, d} ->
5014+
rest =
5015+
bdd_union(
5016+
bdd_leaf_intersection(leaf, u, intersection),
5017+
bdd_difference(bdd_leaf_intersection(leaf, d, intersection), lit)
5018+
)
5019+
5020+
case intersection.(leaf, lit) do
5021+
:bdd_bot -> rest
5022+
new_leaf -> bdd_union(bdd_leaf_intersection(new_leaf, c, intersection), rest)
5023+
end
5024+
end
5025+
end
5026+
49785027
# Lazy negation: eliminate the union, then perform normal negation (switching leaves)
49795028
def bdd_negation(:bdd_top), do: :bdd_bot
49805029
def bdd_negation(:bdd_bot), do: :bdd_top

0 commit comments

Comments
 (0)