Fix optimizations for closed map checking (#14813)
This commit is contained in:
@@ -3363,10 +3363,10 @@ defmodule Module.Types.Descr do
|
||||
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.
|
||||
# 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)
|
||||
is_optional_static(neg_type) or throw(:closed)
|
||||
|
||||
# There may be value in common
|
||||
tag == :open ->
|
||||
@@ -3391,6 +3391,9 @@ defmodule Module.Types.Descr do
|
||||
neg_tag == :open ->
|
||||
true
|
||||
|
||||
neg_tag == :closed and not is_optional_static(type) ->
|
||||
throw(:closed)
|
||||
|
||||
true ->
|
||||
# an absent key in a open negative map can be ignored
|
||||
diff = difference(type, neg_atom_default)
|
||||
@@ -3401,6 +3404,8 @@ defmodule Module.Types.Descr do
|
||||
else
|
||||
map_line_empty?(tag, fields, negs)
|
||||
end
|
||||
catch
|
||||
:closed -> map_line_empty?(tag, fields, negs)
|
||||
end
|
||||
|
||||
# Verify the domain condition from equation (22) in paper ICFP'23 https://www.irif.fr/~gc/papers/icfp23.pdf
|
||||
|
||||
@@ -2505,5 +2505,96 @@ defmodule Module.Types.DescrTest do
|
||||
refute subtype?(map1, map2)
|
||||
assert subtype?(map2, map1)
|
||||
end
|
||||
|
||||
test "struct difference" do
|
||||
entries =
|
||||
[
|
||||
closed_map(__struct__: atom([MapSet]), map: term()),
|
||||
closed_map(__struct__: atom([Jason.OrderedObject]), values: term()),
|
||||
closed_map(__struct__: atom([GenEvent.Stream]), timeout: term(), manager: term()),
|
||||
closed_map(__struct__: atom([HashDict]), size: term(), root: term()),
|
||||
closed_map(__struct__: atom([HashSet]), size: term(), root: term()),
|
||||
closed_map(
|
||||
__struct__: atom([IO.Stream]),
|
||||
raw: term(),
|
||||
device: term(),
|
||||
line_or_bytes: term()
|
||||
),
|
||||
closed_map(__struct__: atom([Range]), first: term(), last: term(), step: term()),
|
||||
closed_map(
|
||||
__struct__: atom([Stream]),
|
||||
enum: term(),
|
||||
done: term(),
|
||||
funs: term(),
|
||||
accs: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([Req.Response.Async]),
|
||||
pid: term(),
|
||||
ref: term(),
|
||||
stream_fun: term(),
|
||||
cancel_fun: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([Postgrex.Stream]),
|
||||
options: term(),
|
||||
params: term(),
|
||||
query: term(),
|
||||
conn: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([DBConnection.PrepareStream]),
|
||||
opts: term(),
|
||||
params: term(),
|
||||
query: term(),
|
||||
conn: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([DBConnection.Stream]),
|
||||
opts: term(),
|
||||
params: term(),
|
||||
query: term(),
|
||||
conn: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([Ecto.Adapters.SQL.Stream]),
|
||||
meta: term(),
|
||||
opts: term(),
|
||||
params: term(),
|
||||
statement: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([Date.Range]),
|
||||
first: term(),
|
||||
last: term(),
|
||||
step: term(),
|
||||
first_in_iso_days: term(),
|
||||
last_in_iso_days: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([File.Stream]),
|
||||
node: term(),
|
||||
raw: term(),
|
||||
path: term(),
|
||||
modes: term(),
|
||||
line_or_bytes: term()
|
||||
),
|
||||
closed_map(
|
||||
__struct__: atom([Phoenix.LiveView.LiveStream]),
|
||||
name: term(),
|
||||
ref: term(),
|
||||
inserts: term(),
|
||||
deletes: term(),
|
||||
reset?: term(),
|
||||
dom_id: term(),
|
||||
consumable?: term()
|
||||
)
|
||||
]
|
||||
|
||||
range =
|
||||
closed_map(__struct__: atom([Range]), first: integer(), last: integer(), step: integer())
|
||||
|
||||
assert subtype?(range, Enum.reduce(entries, &union/2))
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
Reference in New Issue
Block a user