-
Notifications
You must be signed in to change notification settings - Fork 3.7k
numberize - rewrite only positive leaves, add map value numberization
#15801
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -584,22 +584,33 @@ defmodule Module.Types.Descr do | |||||||||||||||||
| defp numberize(:bitmap, bitmap), do: bitmap | ||||||||||||||||||
|
|
||||||||||||||||||
| defp numberize(:map, bdd) do | ||||||||||||||||||
| bdd_map(bdd, fn bdd_leaf(tag, fields) -> | ||||||||||||||||||
| bdd_map_positive(bdd, fn bdd_leaf(tag, fields) -> | ||||||||||||||||||
| bdd_leaf_new( | ||||||||||||||||||
| tag, | ||||||||||||||||||
| numberize_map_tag(tag), | ||||||||||||||||||
| fields_map(fn _key, {value, optional?} -> {numberize(value), optional?} end, fields) | ||||||||||||||||||
| ) | ||||||||||||||||||
| end) | ||||||||||||||||||
| end | ||||||||||||||||||
|
|
||||||||||||||||||
| defp numberize(:tuple, bdd) do | ||||||||||||||||||
| bdd_map(bdd, fn bdd_leaf(tag, fields) -> bdd_leaf_new(tag, Enum.map(fields, &numberize/1)) end) | ||||||||||||||||||
| bdd_map_positive(bdd, fn bdd_leaf(tag, fields) -> | ||||||||||||||||||
| bdd_leaf_new(tag, Enum.map(fields, &numberize/1)) | ||||||||||||||||||
| end) | ||||||||||||||||||
| end | ||||||||||||||||||
|
|
||||||||||||||||||
| defp numberize(:list, bdd) do | ||||||||||||||||||
| bdd_map(bdd, fn bdd_leaf(head, tail) -> bdd_leaf_new(numberize(head), numberize(tail)) end) | ||||||||||||||||||
| bdd_map_positive(bdd, fn bdd_leaf(head, tail) -> | ||||||||||||||||||
| bdd_leaf_new(numberize(head), numberize(tail)) | ||||||||||||||||||
| end) | ||||||||||||||||||
| end | ||||||||||||||||||
|
|
||||||||||||||||||
| # Map keys are compared exactly by `==`, only their values coerce, so the | ||||||||||||||||||
| # domain keys are kept as is and only the types they point to are widened. | ||||||||||||||||||
| defp numberize_map_tag(domains) when is_list(domains), | ||||||||||||||||||
| do: fields_map(fn _key, value -> numberize(value) end, domains) | ||||||||||||||||||
|
|
||||||||||||||||||
| defp numberize_map_tag(tag), do: tag | ||||||||||||||||||
|
|
||||||||||||||||||
| @doc """ | ||||||||||||||||||
| Returns if the type is a singleton. | ||||||||||||||||||
| """ | ||||||||||||||||||
|
|
@@ -6167,6 +6178,39 @@ defmodule Module.Types.Descr do | |||||||||||||||||
| end | ||||||||||||||||||
| end | ||||||||||||||||||
|
|
||||||||||||||||||
| # Like `bdd_map/2`, but only rewrites leaves in *positive* position. | ||||||||||||||||||
| # | ||||||||||||||||||
| # `bdd_map/2` is polarity-blind: on `A and not B` it rewrites `B` too, so a | ||||||||||||||||||
| # widening `fun` shrinks the result instead of enlarging it (`numberize/1` | ||||||||||||||||||
| # replacing `not {float()}` by `not {number()}` would drop `{1}` from the | ||||||||||||||||||
| # result even though `{1} == {1.0}`). Whenever `fun` changes a negated leaf, | ||||||||||||||||||
| # we drop the negation altogether: over-approximating is the safe direction | ||||||||||||||||||
| # for widening callers. Negations left untouched by `fun` are preserved, | ||||||||||||||||||
| # so the common negation-free case keeps its exact shape. | ||||||||||||||||||
| defp bdd_map_positive(bdd, fun) do | ||||||||||||||||||
| case bdd do | ||||||||||||||||||
| :bdd_bot -> | ||||||||||||||||||
| :bdd_bot | ||||||||||||||||||
|
|
||||||||||||||||||
| :bdd_top -> | ||||||||||||||||||
| :bdd_top | ||||||||||||||||||
|
|
||||||||||||||||||
| bdd_leaf(_, _) = leaf -> | ||||||||||||||||||
| fun.(leaf) | ||||||||||||||||||
|
|
||||||||||||||||||
| {_, leaf, left, union, right} -> | ||||||||||||||||||
| left = bdd_map_positive(left, fun) | ||||||||||||||||||
| union = bdd_map_positive(union, fun) | ||||||||||||||||||
| right = bdd_map_positive(right, fun) | ||||||||||||||||||
|
|
||||||||||||||||||
| case fun.(leaf) do | ||||||||||||||||||
| ^leaf -> bdd_node_new(leaf, left, union, right) | ||||||||||||||||||
| new_leaf when right == :bdd_bot -> bdd_node_new(new_leaf, left, union, :bdd_bot) | ||||||||||||||||||
| new_leaf -> bdd_union(bdd_intersection(new_leaf, left), bdd_union(union, right)) | ||||||||||||||||||
| end | ||||||||||||||||||
|
Comment on lines
+6206
to
+6210
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This above is more likely to be the correct formula. We rewrite only the leaf in positive position. |
||||||||||||||||||
| end | ||||||||||||||||||
| end | ||||||||||||||||||
|
|
||||||||||||||||||
| defp bdd_reduce(bdd, acc, fun) do | ||||||||||||||||||
| case bdd do | ||||||||||||||||||
| :bdd_bot -> | ||||||||||||||||||
|
|
||||||||||||||||||
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -2094,6 +2094,49 @@ defmodule Module.Types.ExprTest do | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| atom([:non_empty_map, :maybe_empty_map]) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| test "does not discard equal values when narrowing against negated types" do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # `other` carries a negation (`... and not {float()}`) from the clause | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # subtraction. Widening integers/floats inside that negation would wrongly | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # remove `{1}`, even though `{1} == {1.0}` at runtime. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| assert typecheck!( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [v, q], | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| other = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| case v do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| {a} when is_float(a) -> {:float, a} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| other -> other | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| w = if q, do: {1}, else: {1.5} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| case w do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| x when x == other -> {:matched, x} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| _ -> :nomatch | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |> to_quoted_string() == | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| "dynamic({:matched, {float() or integer()}}) or :nomatch" | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| test "does not discard equal values when narrowing against domain keys" do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # `==` coerces map values, so narrowing `x` from `x == y` must widen the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # `integer() => integer()` domain value to `integer() => number()`. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| assert typecheck!( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| y = %{1 => 1} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| w = %{1 => 1.0} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| case w do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| x when x == y and map_size(x) == 1 -> {:eq, x} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| _ -> :ne | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |> to_quoted_string() == | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ":ne or {:eq, %{integer() => float()} and not empty_map()}" | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+2097
to
+2139
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The unit tests on numberize are enough here!
Suggested change
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| test "consider external variables as not precise" do | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| assert typecheck!( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [x], | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Now I am thinking... isn't our bdd_map inherently wrong because it may rewrite the leafs which means they have a different ordering? I am thinking everything needs to be written as in this formula... which would also make numberize too expensive...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I recall one of AI reviews flagged the order not being preserved as an issue. I wasn’t able to produce code where it would surface as an evident bug. I dismissed the proposed fix with BDD rebuilds everywhere as a bad tradeoff