structure Lean.Elab.Do.ControlStack : Type

• description : Unit → MessageData
• m : DoElabM Expr
• stM : Expr → DoElabM Expr
• runInBase : Expr → DoElabM Expr
• restoreCont : DoElemCont → DoElabM DoElemCont

def Lean.Elab.Do.ControlStack.unStM (m : ControlStack) (stMα : Expr) : DoElabM Expr

def Lean.Elab.Do.ControlStack.base (mi : MonadInfo) : ControlStack

def Lean.Elab.Do.ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ : Expr) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrapper : Name) (getCont : DoElabM (DoElabM Expr)) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.exceptT (baseMonadInfo : MonadInfo) (exceptTWrapper casesOnWrapper : Name) (getCont : DoElabM ReturnCont) (ε : Expr) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.earlyReturnT (baseMonadInfo : MonadInfo) (ρ : Expr) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.breakT (baseMonadInfo : MonadInfo) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.continueT (baseMonadInfo : MonadInfo) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.mkBreak (base : ControlStack) (hasContinue : Bool) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkContinue (base : ControlStack) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkReturn (base : ControlStack) (r : Expr) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkPure (base : ControlStack) (resultName : Name) : DoElabM Expr

structure Lean.Elab.Do.EffectForwarder : Type

Plan for embedding a non-tail-resumptive body inside origCont via a monad-transformer stack.

• origCont : DoElemCont

  Continuation of the surrounding do block; restored after the body.

• returnBase? : Option ControlStack

  Substack at which the early-return handler was installed, if any.

• breakBase? : Option ControlStack

  Substack at which the break handler was installed, if any.

• continueBase? : Option ControlStack

  Substack at which the continue handler was installed, if any.

• liftedStack : ControlStack

  The full transformer stack over the base monad.

• liftedDoBlockResultType : Expr

  The body's elaboration type, stM dec.resultType.

def Lean.Elab.Do.EffectForwarder.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM EffectForwarder

Build the lifter plan for a body whose effects are summarised by info.

def Lean.Elab.Do.EffectForwarder.lift (l : EffectForwarder) (elabElem : DoElemCont → DoElabM Expr) : DoElabM Expr

Elaborate elabElem in the lifted stack: install break/continue/return handlers funnelling into liftedStack and set the doBlock result type to liftedDoBlockResultType. Semantically MonadControl.liftWith fun runInBase => elabElem (runInBase pure). Conts passed to elabElem are implicitly wrapped in runInBase, realised later by ControlStack.mkBreak/mkContinue/mkReturn once the transformer stack t is fixed by aggregating effects across all lift sites for this lifter.

def Lean.Elab.Do.EffectForwarder.restoreCont (l : EffectForwarder) : DoElabM DoElemCont

Build a DoElemCont that unpacks the lifted body's result and resumes origCont.k.