Skip to content
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.

Sign up for GitHub

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

Add replay history to match names between two downwards traversals #3302

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add replay history to match names between two downwards traversals #3302

wants to merge 3 commits into from

Commits on Nov 22, 2024

  1. Add replay history to match names beetween two downwards traversals 

    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. 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).
    @Gbury
    Gbury committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    b23499c View commit details
    Browse the repository at this point in the history

  2. fix error

    @Gbury
    Gbury committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    4501e36 View commit details
    Browse the repository at this point in the history

  3. fix compare

    @Gbury
    Gbury committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    376f390 View commit details
    Browse the repository at this point in the history