Fix a bug related to abstract imports and match expressions #5811
Conversation
| Alternatively, we could call all the rewriter.PostResolve methods | ||
| */ | ||
|
|
||
| new MatchFlattener(reporter).PostResolve(module); |
There was a problem hiding this comment.
This added line is the only semantic change in this PR
keyboardDrummer
changed the title
…dafny into unreachabelExprToBoogie
| void AfterNodeChildren() => afterChildren(currentNode); | ||
| toVisit.AddFirst((Action)AfterNodeChildren); |
There was a problem hiding this comment.
Nice fix, funny how simple and clean the original looks while also being completely wrong. :)
| Cloning with resolved fields is not an option, | ||
| because then internal references of the cloned code can point to the old code. | ||
| I(keyboardDrummer) think it would be better altogether if no cloning was done for abstract modules, |
There was a problem hiding this comment.
Out of curiosity what alternative do you imagine? Given the semantics of abstract modules are so close to the idea of making copies of the code, could the better path be doubling-down on clone testing? I don't feel like cloning is going away any time soon.
There was a problem hiding this comment.
Whatever operation you want to do on both the abstract module and the original module, where the two should behave mostly the same but somewhat differently, pass in a context object that allows you to differentiate between the two scenarios.
Given that I don't understand the code related to abstract modules, I would probably find related tests, reimplement without copying and see what breaks.
2 participants
Fixes #5808
Description
new MatchFlattener(reporter).PostResolve(module);after cloning elements for abstract imports, so.Flattenedis set.afterChildrenparameter inNode.Visit, so that closure is actually only called after the children are visited.How has this been tested?
Added a CLI test
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.