feat: pluggable pure/bind builders for do elaboration#13507
Merged
Conversation
This PR exposes the `Pure.pure` / `Bind.bind` applications emitted by the `do` elaborator as pluggable closures, so external surface syntaxes (e.g. an `ido` notation for indexed monads) can reuse the full `do` machinery while emitting alternate constants. `Context` carries a new `DoOps` record (wrapped via an opaque `DoOpsRef` to break the cycle with `DoElabM`) with `mkPureApp`, `mkBindApp`, and `isPureApp?` fields. `mkPureApp` and `mkBindApp` become thin dispatchers; the original bodies move to `DoOps.default`. `isPureApp?` returns the pure value as an `Expr` rather than a `Bool`, so overrides aren't locked into `Pure.pure`'s 4-argument layout. A new `elabDoWith` entry point takes a `DoOps` plus a `doSeq`; `elabDo` is now `elabDoWith .default` applied to a matched ``(do $doSeq)``. Control-flow features (`mut`, `return`, `break`, `continue`, `for`) and the transformer stack (`StateT`, `OptionT`, `ExceptT`, `EarlyReturnT`, `BreakT`, `ContinueT`) remain hard-coded to `Monad`; generalising them is deferred to a follow-up. A new `tests/elab/doNotationPluggableOps.lean` registers an Atkey-style indexed monad and an `ido` surface syntax that drives `elabDoWith`, covering the forms of `do` that are supported under the minimal scope.
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Contributor
Author
|
!bench |
|
Benchmark results for 72ef5c4 against cae4dec are in. No significant results found. @sgraf812
Small changes (1🟥)
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
This PR exposes the
Pure.pure/Bind.bindapplications emitted by thedoelaborator as pluggable closures, so external surface syntaxes (e.g. anidonotation for indexed monads) can reuse the fulldomachinery while emitting alternate constants.Contextcarries a newDoOpsrecord (wrapped via an opaqueDoOpsRefto break the cycle withDoElabM) withmkPureApp,mkBindApp, andisPureApp?fields.mkPureAppandmkBindAppbecome thin dispatchers; the original bodies move toDoOps.default.isPureApp?returns the pure value as anExprrather than aBool, so overrides aren't locked intoPure.pure's 4-argument layout. A newelabDoWithentry point takes aDoOpsplus adoSeq;elabDois nowelabDoWith .defaultapplied to a matched(do $doSeq).Control-flow features (
mut,return,break,continue,for) and the transformer stack (StateT,OptionT,ExceptT,EarlyReturnT,BreakT,ContinueT) remain hard-coded toMonad; generalising them is deferred to a follow-up. A newtests/elab/doNotationPluggableOps.leanregisters an Atkey-style indexed monad and anidosurface syntax that driveselabDoWith, covering the forms ofdothat are supported under the minimal scope.