The Pattern-Matching Bug: testsuite improvements#13121
Conversation
5e80857 to
96553a3
Compare
ncik-roberts
left a comment
There was a problem hiding this comment.
Thank you for these tests, which I expect to make upcoming review easier.
| (* This pattern-matching is in fact total: a Match_failure case is | ||
| not necessary for soundness. *) |
There was a problem hiding this comment.
| (* This pattern-matching is in fact total: a Match_failure case is | |
| not necessary for soundness. *) | |
| (* This pattern-matching is in fact total: the Match_failure case | |
| conservatively inserted by the pattern match compiler is not | |
| necessary for soundness. *) |
To distinguish this case more clearly from the "This pattern-matching is partial: a Match_failure case is necessary for soundness." comment below on a test where
the case is not inserted.
There was a problem hiding this comment.
I had more explanations before but I repeat those sentences for several examples and the duplication was bad. To take your suggestion into account I added an explanatory paragraph at the beginning of the test file.
| (f/297 = | ||
| (function x/298 : int |
There was a problem hiding this comment.
Mild suggestion: Did you consider adding -dno-unique-ids to the test's flags? That would make this part of the test somewhat less sensitive to the code that comes before, for future changes.
There was a problem hiding this comment.
I don't want to use -dno-unique-ids for pattern-matching tests due to the frequent name conflicts with *match*/nnn identifiers generated during pattern-matching: if we passed the option, some of the -dlambda outputs would become ambiguous. In this testfile for example, the tests immediately below the one you are commenting binds both *match*/307 and *match*/309.
It would be nice to avoid this by tweaking the pattern-matching compiler to generate distinct names in a deterministic way (my idea is to use the path from the root to the current position as a distinguishing suffix), but I never did the work of implement this (not immediate) quality-of-life improvement.
|
Note: this PR and also #13129 would need a maintainer approval so that I can merge them and send the next, more interesting PR in the stack. It would be nice to do this sooner rather than later to benefit from the potential availability of @ncik-roberts. |
96553a3 to
cf35906
Compare
|
(I have updated the PR after handling the review comments.) |
|
I will approve once @ncik-roberts approves the review changes. |
ncik-roberts
left a comment
There was a problem hiding this comment.
My review was very much nits and I'm happy with the responses so I'll approve.
Octachron
left a comment
There was a problem hiding this comment.
Approving on @ncik-roberts behalf (and also because having more tests to explain the behaviour of the pattern-matching compiler is nice).
I am still working on #7241; the next installment of bugfixing PRs is taking a bit more effort than I expected, and here is a PR that only improves the testsuite for this bug in order to make reviewer's life easier in the short future. (cc @Octachron, @trefis, @lthls, @ncik-roberts)
The first commit refines an existing test in a "simple" and a "complex" version. Currently there is only the "complex" version in the testsuite, but both versions behave differently in some cases, and while trying to reason about the compiler behavior I found the behavior surprising. (If someone remembers the full details, we considered two approaches to fix the "context" part of the #7241 bug, and eventually I decided on one; the testsuite was written when I was still working on the first/earlier approach, and so it lacks distinctions that did not matter with that different implementation.)
The second commit adds a more complex test for the "totality bug" part of the fix of #7241, fix which has not been merged yet. This is about testing what happens on argument positions that are immutable themselves (they result from projecting an immutable field) but they are "transitively mutable", they are transitively under a mutable position. This is related to a discussion that we had with @ncik-roberts in #12555 (comment) . Adding a new testcase for this behavior proved very useful because it let me realize that my current "fix for the totality issue" was incomplete in this situation. (I went back and forth on how to handle transitivity, and my working branches include a simplistic approach that I thought was complete and in fact is not.)
The third commit adds coverage for cases that are currently handled by the
check_partiallogic within runtime/matching.ml, which is a pre-existing, incomplete criterion to downgrade certain pattern-matching problems from Total to Partial. (This heuristic fires when one clause has both mutable fields and either a lazy pattern or a guard.) The final fix for the Pattern-Matching Bug subsumes this incomplete criterion (in a way that also lets us un-pessimize certain programs I think), so that logic will be removed in a further PR. The new testcases ensure that we would detect a regression coming from this, by testing the various settings where it applies.