This PR adds two new fields to `DoOps`, `splitMonadApp?` and
`mkMonadApp`, so that callers of `elabDoWith` can use indexed monads
like `Measure α` (where `Measure : (α : Type u) → [MeasureSpace α] →
Type u` carries instance arguments) that the default `m α` decomposition
cannot handle. The existing behavior moves into `DoOps.default`.
`splitMonadApp?` replaces the hard-coded `.app m α` step inside the
`extractMonadInfo` recursion, and `mkMonadApp` replaces the hard-coded
`mkApp m α` used to construct the monadic type.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
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.
