Skip to content

feat: New do Elaborator#918

Open
mpenciak wants to merge 20 commits intoAeneasVerif:mainfrom
mpenciak:mp/do_elab
Open

feat: New do Elaborator#918
mpenciak wants to merge 20 commits intoAeneasVerif:mainfrom
mpenciak:mp/do_elab

Conversation

@mpenciak
Copy link
Copy Markdown
Collaborator

@mpenciak mpenciak commented Apr 7, 2026

We implement a new do elaborator for extracted monadic code. The new elaborator is only triggered for do blocks of type Result, and there is a new option Aeneas.newDoElab which can be unset to use the old elaborator.

The new elaborator works on a subset of the do syntax which doesn't include early returns, so we can avoid any do jumps and the resulting expression will be a sequence of binds.

We also treat the pattern matching syntax in let bindings using Function.uncurry to avoid the built-in match syntax elaboration.

Included is a new delaborator that delabs the new expressions to the expected syntax.

@mpenciak mpenciak marked this pull request as ready for review April 23, 2026 20:03
@mpenciak mpenciak changed the title new do elab feat: New do Elaborator Apr 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant