Add replay history to match names between two downwards traversals #3302
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
[Note: This is a pre-requisite of match-in-match; the mechanism introduced is not yet used in this PR, but will be used by continuation specialization when the PR for match-in-match is opened]
In some cases (mostly the upcoming continuation specialization for match-in-match), we are interested in doing multiple downwards pass on a single term. In such cases, it might be necessary to relate the names of variables and continuations from the first pass to those from the subsequent passes. The predominant use of that for now should be to correctly handle continuations that have been lifted during the first pass, and whose calls should be rewritten in subsequent passes (including their lifted arguments).
This is done by storing the sequence of names generated when opening name abstractions during the first downwards pass. On subsequent passes, each new variable and continuation "consumes" an element of that sequence, allowing to establish the correspondance between names. As a safety measure, we check that correspondings names are in the same "renaming equivalence class", though note that this is not a guarantee (for isntance, by default all continuation have no names and therefore will all be in the same "renaming equivalence class").
Additionally, and this is more specific to continuation specialization but generalizable to other future uses, it is necessary to have some kind of replayability of inlining decisions. Indeed each inlining decision will change the sequence of bound names that are opened during the downwards pass, which would currently break the hypothesis of replay histories that exactly the same sequence of binders are opened during both downwards passes. In the case of match-in-match this is simple: the handler that we want to specialize ends with a switch, which means that any call inside the handler have been inlined, so the replay history has a boolean to denote that we want to inline everything while replaying the handler downwards pass. For other more complex uses, inlining decisions could be stored alongside the bound variables and continuations, so that they can be replayed, either as is, or within some notion of compatibility.
Finally, we also need to make it so that recursive continuations are bound in an order that is stable through renaming, so we change the map of continuation to an Lmap for recursive continuation bindings.
In the future, this replay mechanism would also be useful to do widening for recursive continuations (but that's a far away future).