numberize - rewrite only positive leaves, add map value numberization - #15801
numberize - rewrite only positive leaves, add map value numberization#15801lukaszsamson wants to merge 2 commits into
numberize - rewrite only positive leaves, add map value numberization#15801Conversation
| 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)) |
There was a problem hiding this comment.
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.
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
|
@lukaszsamson I am thinking a better solution here would be have a field in the context called numberize. So when we assemble the type here: We set this value in the stack and we interpret all integers/floats in the literal as numbers. This makes it correct by construction and we can remove numberize. We still have to address 3 from 15799 though... perhaps we have a version of disjoint that ignores numbers... but that may be complicated. |
I tried that, see lukaszsamson/elixir@ls-numberize-map-domains...ls-numberize-flag-spike. It did not make |
We can apply the same technique in of_pattern_tree, no? If so, I'd say that PR is the way to go. The fact that we can track map keys and binaries correctly is a positive. |
@lukaszsamson can you tackle the pending item above and send a pull request as well? Thanks! |
Instead of calling |
I tried that in https://github.com/lukaszsamson/elixir/tree/ls-numberize-flag-spike-v2 compare but it makes the two bugs this PR fixes come back. It does not cover the variable to variable path, that branch is only reached when neither operand is quoted literal |
Yes. That would work. The only consequence is |
| 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 | ||
|
|
There was a problem hiding this comment.
The unit tests on numberize are enough here!
| 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 |
| 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 |
There was a problem hiding this comment.
| 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 | |
| bdd_intersection(new_leaf, left) | |
| |> bdd_union(union) | |
| |> bdd_union(bdd_difference(right, leaf)) |
There was a problem hiding this comment.
This above is more likely to be the correct formula. We rewrite only the leaf in positive position.
Addresses 1 and 2 from #15799
Extracted from #15800
AssistedBy: Claude Fable 5, GPT 5.6 Sol