Skip to content

Commit 415cd20

Browse files
josevalimjosevalim
committed
Allow difference formulas to apply across unions
1 parent 5979c42 commit 415cd20

1 file changed

Lines changed: 71 additions & 82 deletions

File tree

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

Lines changed: 71 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -5878,107 +5878,96 @@ defmodule Module.Types.Descr do
58785878

58795879
## Optimize differences
58805880

5881-
# For the right-side being a leaf, we have:
5881+
# We have two formulas for differences.
58825882
#
5883-
# ((a1 and C1) or U1 or (not a1 and D1)) and not a2
5883+
# ## When D1 = bottom
58845884
#
5885-
# If disjoint?(a1, a2), we end up with:
5885+
# (((a_diff and not D2) or (a_int and not C2)) and C1 and not U2) or (U1 and not B2)
58865886
#
5887-
# (a1 and C1) or (U1 and not a2) or (not a1 and D1 and not a2)
5887+
# If disjoint, a_diff is a1 and a_int is none:
58885888
#
5889-
# If subtype?(a1, a2), we end up with:
5889+
# (a1 and C1 and not D2 and not U2) or (U1 and not B2)
58905890
#
5891-
# (U1 and not a2) or (D1 and not a2)
5891+
# If subtype, a_diff is none and a_int is a1:
58925892
#
5893-
# If one key difference, then we compute the difference
5894-
# and the union of said keys, returning a_union and a_diff:
5893+
# (a1 and C1 and not C2 and not U2) or (U1 and not B2)
58955894
#
5896-
# ((a1 and C1) or U1 or (not a1 and D1)) and not a2
5897-
# (a_diff and C1) or (U1 and not a2) or (not a_union and D1)
5895+
# In the snippet below we also enforce that C1 is top for simplicity.
58985896
#
5899-
defp bdd_difference({a1, c1, u1, d1} = bdd1, bdd_leaf(_, _) = bdd2, leaf_compare)
5900-
when is_tuple(bdd2) do
5901-
case leaf_compare.(a1, bdd2, :union) do
5902-
:disjoint ->
5903-
res =
5904-
bdd_union(
5905-
bdd_difference(u1, bdd2, leaf_compare),
5906-
bdd_difference({a1, :bdd_bot, :bdd_bot, d1}, bdd2)
5907-
)
5908-
5909-
if c1 == :bdd_bot, do: res, else: bdd_union(res, {a1, c1, :bdd_bot, :bdd_bot})
5910-
5911-
{:one_key_difference, a_diff, a_union} ->
5912-
bdd_intersection(a_diff, c1)
5913-
|> bdd_union(bdd_difference(u1, bdd2, leaf_compare))
5914-
|> bdd_union(bdd_difference(d1, a_union, leaf_compare))
5915-
5916-
:subtype ->
5917-
bdd_union(bdd_difference(u1, bdd2, leaf_compare), bdd_difference(d1, bdd2, leaf_compare))
5918-
5919-
:none ->
5920-
bdd_difference(bdd1, bdd2)
5921-
end
5922-
end
5923-
5924-
# For the left-side being a leaf, we have:
5925-
#
5926-
# a1 and not ((a2 and C2) or U2 or (not a2 and D2))
5927-
# a1 and not (a2 and C2) and not U2 and (a2 or not D2)
5928-
#
5929-
# If disjoint?(a1, a2):
5930-
#
5931-
# a1 and not (a2 and C2) = a1 (a2 and C2 is subset of a2, disjoint from a1)
5932-
# a1 and (a2 or not D2) = a1 and not D2 (a1 and a2 = bottom)
5933-
#
5934-
# Result: a1 and not D2 and not U2
5935-
#
5936-
# If subtype?(a1, a2):
5937-
#
5938-
# a1 and not (a2 and C2) = a1 and not C2 (a1 and not a2 = bottom)
5939-
# a1 and (a2 or not D2) = a1 (a1 and a2 = a1)
5940-
#
5941-
# Result: a1 and not C2 and not U2
5897+
# ## When C2 = top
59425898
#
5943-
# If one key difference, then we compute the difference
5944-
# and the intersection of said keys, returning a_int and a_diff:
5899+
# ((a_diff and C1) or (U1 and not a2) or (not a_union and D1)) and not U2 and not D2
59455900
#
5946-
# a1 and not (a2 and C2) and not U2 and (a2 or not D2)
5947-
# ((a1 and not a2) or (a1 and not C2)) and not U2 and (a2 or not D2)
5948-
# (a_diff or (a1 and not C2)) and not U2 and (a2 or not D2)
5901+
# If disjoint, a_diff is a1 and a_union is a1 or a2:
59495902
#
5950-
# Now distribute into (a2 or not D2):
5903+
# ((a1 and C1) or (U1 and not a2) or (not a1 and D1 and not a2)) and not U2 and not D2
59515904
#
5952-
# ((a_diff and (a2 or not D2)) or
5953-
# ((a1 and not C2) and (a2 or not D2))) and not U2
5954-
# ((a_diff and not D2) or
5955-
# (a_int and not C2) or
5956-
# (a1 and not C2 and not D2)) and not U2
5905+
# If subtype, a_diff is none and a_union is a2:
59575906
#
5958-
# Now, we know that a1 is a_diff or a_int, which means
5959-
# (a1 and not C2 and not D2) is a subset of the other two
5960-
# expressions, so we end up with:
5907+
# ((U1 and not a2) or (D1 and not D2)) and not U2 and not D2
59615908
#
5962-
# ((a_diff and not D2) or (a_int and not C2)) and not U2
5963-
#
5964-
defp bdd_difference(bdd_leaf(_, _) = bdd1, bdd2, leaf_compare) when is_tuple(bdd2) do
5909+
defp bdd_difference(bdd1, bdd2, leaf_compare) when is_tuple(bdd1) and is_tuple(bdd2) do
5910+
{a1, c1, u1, d1} = bdd_expand(bdd1)
59655911
{a2, c2, u2, d2} = bdd_expand(bdd2)
5966-
type = if c2 == :bdd_top, do: :none, else: :intersection
59675912

5968-
case leaf_compare.(bdd1, a2, type) do
5969-
:disjoint ->
5970-
bdd1 |> bdd_difference(d2, leaf_compare) |> bdd_difference(u2, leaf_compare)
5913+
cond do
5914+
d1 == :bdd_bot and c1 == :bdd_top ->
5915+
type = if c2 == :bdd_top, do: :none, else: :intersection
59715916

5972-
{:one_key_difference, a_diff, a_int} ->
5973-
bdd_union(
5974-
a_diff |> bdd_difference(d2, leaf_compare) |> bdd_difference(u2, leaf_compare),
5975-
a_int |> bdd_difference(c2, leaf_compare) |> bdd_difference(u2, leaf_compare)
5976-
)
5917+
case leaf_compare.(a1, a2, type) do
5918+
:disjoint ->
5919+
a1
5920+
|> bdd_difference(d2, leaf_compare)
5921+
|> bdd_difference(u2, leaf_compare)
5922+
|> bdd_union(bdd_difference(u1, bdd2, leaf_compare))
5923+
5924+
:subtype ->
5925+
a1
5926+
|> bdd_difference(c2, leaf_compare)
5927+
|> bdd_difference(u2, leaf_compare)
5928+
|> bdd_union(bdd_difference(u1, bdd2, leaf_compare))
5929+
5930+
{:one_key_difference, a_diff, a_int} ->
5931+
bdd_union(
5932+
a_diff |> bdd_difference(d2, leaf_compare) |> bdd_difference(u2, leaf_compare),
5933+
a_int |> bdd_difference(c2, leaf_compare) |> bdd_difference(u2, leaf_compare)
5934+
)
5935+
|> bdd_union(bdd_difference(u1, bdd2, leaf_compare))
59775936

5978-
:subtype ->
5979-
bdd1 |> bdd_difference(c2, leaf_compare) |> bdd_difference(u2, leaf_compare)
5937+
:none ->
5938+
bdd_difference(bdd1, bdd2)
5939+
end
59805940

5981-
:none ->
5941+
c2 == :bdd_top ->
5942+
type = if d1 == :bdd_bot, do: :none, else: :union
5943+
5944+
case leaf_compare.(a1, a2, type) do
5945+
:disjoint ->
5946+
bdd_difference(u1, a2, leaf_compare)
5947+
|> bdd_union(bdd_difference({a1, c1, :bdd_bot, d1}, a2))
5948+
|> bdd_difference(d2, leaf_compare)
5949+
|> bdd_difference(u2, leaf_compare)
5950+
5951+
:subtype ->
5952+
bdd_union(
5953+
bdd_difference(u1, a2, leaf_compare),
5954+
bdd_difference(d1, a2, leaf_compare)
5955+
)
5956+
|> bdd_difference(d2, leaf_compare)
5957+
|> bdd_difference(u2, leaf_compare)
5958+
5959+
{:one_key_difference, a_diff, a_union} ->
5960+
bdd_intersection(a_diff, c1)
5961+
|> bdd_union(bdd_difference(u1, a2, leaf_compare))
5962+
|> bdd_union(bdd_difference(d1, a_union, leaf_compare))
5963+
|> bdd_difference(d2, leaf_compare)
5964+
|> bdd_difference(u2, leaf_compare)
5965+
5966+
:none ->
5967+
bdd_difference(bdd1, bdd2)
5968+
end
5969+
5970+
true ->
59825971
bdd_difference(bdd1, bdd2)
59835972
end
59845973
end

0 commit comments

Comments
 (0)