structure Lean.Elab.Do.MonadInfo : Type

• m : Expr

  The inferred type of the monad of type Type u → Type v.

• u : Level

  The u in m : Type u → Type v.

• v : Level

  The v in m : Type u → Type v.

• cachedPUnit : Expr

  The cached PUnit expression.

• cachedPUnitUnit : Expr

  The cached PUnit.unit expression.

def Lean.Elab.Do.ContInfoRef : Type

instance Lean.Elab.Do.instNonemptyContInfoRef : Nonempty ContInfoRef

structure Lean.Elab.Do.Context : Type

• monadInfo : MonadInfo

  Inferred and cached information about the monad.

• mutVars : Array Name

  The mutable variables in declaration order.

• doBlockResultType : Expr

  The expected type of the current do block. This can be different from earlyReturnType in for loop do blocks, for example.

• contInfo : ContInfoRef

  Information about return, break and continue continuations.

structure Lean.Elab.Do.MonadInstanceCache : Type

• instPure : Option Expr

  The inferred Pure instance of (← read).monadInfo.m.

• instBind : Option Expr

  The inferred Bind instance of (← read).monadInfo.m.

• cachedPure : Option Expr

  The cached Pure.pure expression.

• cachedBind : Option Expr

  The cached Bind.bind expression.

instance Lean.Elab.Do.instNonemptyMonadInstanceCache : Nonempty MonadInstanceCache

structure Lean.Elab.Do.ContVarId : Type

A continuation metavariable.

When generating jumps to join points or filling in expressions for break or continue, it is still unclear what mutable variables need to be passed, because it depends on which mutable variables were reassigned in the control flow path to any of the jumps.

The mechanism of ContVarId allows to delay the assignment of the jump expressions until the local contexts of all the jumps are known.

• name : Name

def Lean.Elab.Do.instInhabitedContVarId.default : ContVarId

instance Lean.Elab.Do.instInhabitedContVarId : Inhabited ContVarId

instance Lean.Elab.Do.instBEqContVarId : BEq ContVarId

def Lean.Elab.Do.instBEqContVarId.beq : ContVarId → ContVarId → Bool

instance Lean.Elab.Do.instHashableContVarId : Hashable ContVarId

def Lean.Elab.Do.instHashableContVarId.hash : ContVarId → UInt64

structure Lean.Elab.Do.ContVarJump : Type

Information about a jump site associated to ContVarId. There will be one instance per jump site to a join point, or for each break or continue element.

• mvar : Expr

  The metavariable to be assigned with the jump to the join point. Conveniently, its captured local context is that of the jump, in which the new mutable variable definitions and result variable are in scope.

• ref : Syntax

  A reference for error reporting.

structure Lean.Elab.Do.ContVarInfo : Type

Information about a ContVarId.

• type : Expr

  The monadic type of the continuation.

• tunneledVars : Std.HashSet Name

  A superset of the local variable names that the jumps will refer to. Often the mut variables. Any let-bound FV will be turned into a have-bound FV by setting their nondep flag in the local context of the metavariable for the jump site. This is a technicality to ensure that isDefEq will not inline the lets.

• lctx : LocalContext

  Local context at the time the continuation variable was created.

• jumps : Array ContVarJump

  The tracked jumps to the continuation. Each contains a metavariable to be assigned later.

structure Lean.Elab.Do.State : Type

• monadInstanceCache : MonadInstanceCache
• contVars : Std.HashMap ContVarId ContVarInfo

instance Lean.Elab.Do.instNonemptyState : Nonempty State

@[reducible, inline]

abbrev Lean.Elab.Do.DoElabM (α : Type) : Type

structure Lean.Elab.Do.DoElemCont : Type

Elaboration of a do block do $e; $rest, results in a call elabTerm `(do $e; $rest) = elabElem e dec, where elabElem e · is the elaborator for do element e, and dec is the DoElemCont describing the elaboration of the rest of the block rest.

If the semantics of e resumes its continuation rest, its elaborator must bind its result to resultName, ensure that it has type resultType and then elaborate rest using dec.

Clearly, for term elements e : m α, the result has type α. More subtly, for binding elements let x := e or let x ← e, the result has type PUnit and is unrelated to the type of the bound variable x.

Examples:

• return drops the continuation; return x; pure () elaborates to pure x.
• let x ← e; rest x elaborates to e >>= fun x => rest x.
• let x := 3; let y ← (let x ← e); rest x elaborates to let x := 3; e >>= fun x_1 => let y := (); rest x, which is immediately zeta-reduced to let x := 3; e >>= fun x_1 => rest x.
• one; two elaborates to one >>= fun (_ : PUnit) => two; it is an error if one does not have type PUnit.

• resultName : Name

  The name of the monadic result variable.

• resultType : Expr

  The type of the monadic result.

• k : DoElabM Expr

  The continuation to elaborate the rest of the block.

def Lean.Elab.Do.instInhabitedDoElemCont.default : DoElemCont

instance Lean.Elab.Do.instInhabitedDoElemCont : Inhabited DoElemCont

@[reducible, inline]

abbrev Lean.Elab.Do.DoElab : Type

The type of elaborators for do block elements.

It is elabTerm `(do $e; $rest) = elabElem e dec, where elabElem e · is the elaborator for do element e, and dec is the DoElemCont describing the elaboration of the rest of the block rest.

structure Lean.Elab.Do.ContInfo : Type

Information about a success, return, break or continue continuation that will be filled in after the code using it has been elaborated.

• returnCont : DoElemCont
• breakCont : Option (DoElabM Expr)
• continueCont : Option (DoElabM Expr)

def Lean.Elab.Do.instInhabitedContInfo.default : ContInfo

instance Lean.Elab.Do.instInhabitedContInfo : Inhabited ContInfo

unsafe def Lean.Elab.Do.ContInfo.toContInfoRefImpl (m : ContInfo) : ContInfoRef

@[implemented_by Lean.Elab.Do.ContInfo.toContInfoRefImpl]

opaque Lean.Elab.Do.ContInfo.toContInfoRef (m : ContInfo) : ContInfoRef

unsafe def Lean.Elab.Do.ContInfoRef.toContInfoImpl (m : ContInfoRef) : ContInfo

@[implemented_by Lean.Elab.Do.ContInfoRef.toContInfoImpl]

opaque Lean.Elab.Do.ContInfoRef.toContInfo (m : ContInfoRef) : ContInfo

def Lean.Elab.Do.mkMonadicType (resultType : Expr) : DoElabM Expr

Constructs m α from α.

def Lean.Elab.Do.mkPUnit : DoElabM Expr

The cached PUnit expression.

def Lean.Elab.Do.mkPUnitUnit : DoElabM Expr

The cached PUnit.unit expression.

def Lean.Elab.Do.mkPureApp (α e : Expr) : DoElabM Expr

The expression pure (α:=α) e.

def Lean.Elab.Do.DoElemCont.mkPure (resultType : Expr) : TermElabM DoElemCont

Create a DoElemCont returning the result using pure.

def Lean.Elab.Do.mkBindApp (α β e k : Expr) : DoElabM Expr

The expression Bind.bind (α:=α) (β:=β) e k.

def Lean.Elab.Do.declareMutVar {α : Type} (x : Name) : DoElabM α → DoElabM α

Register the given name as that of a mut variable.

def Lean.Elab.Do.declareMutVar? {α : Type} (mutTk? : Option Syntax) (x : Name) (k : DoElabM α) : DoElabM α

Register the given name as that of a mut variable if the syntax token mut is present.

def Lean.Elab.Do.throwUnlessMutVarDeclared (x : Name) : DoElabM Unit

Throw an error if the given name is not a declared mut variable.

def Lean.Elab.Do.checkMutVarsForShadowing (x : Name) : DoElabM Unit

Throw an error if a declaration of the given name would shadow a mut variable.

def Lean.Elab.Do.mkFreshResultType (userName : Name := `α) : DoElabM Expr

Create a fresh α that would fit in m α.

def Lean.Elab.Do.synthUsingDefEq (msg : String) (expected actual : Expr) : DoElabM Unit

def Lean.Elab.Do.mkBindCancellingPure (x : Name) (eResultTy e : Expr) (k : Expr → DoElabM Expr) : DoElabM Expr

Has the effect of e >>= fun (x : eResultTy) => $(← k `(x)). Ensures that e has type m eResultTy.

def Lean.Elab.Do.elabType (ty? : Option (TSyntax `term)) (freshLevel : Bool := false) : DoElabM Expr

A variant of Term.elabType that takes the universe of the monad into account, unless freshLevel is set.

def Lean.Elab.Do.elabTerm (stx : Syntax) (expectedType? : Option Expr) : DoElabM Expr

def Lean.Elab.Do.elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) : DoElabM Expr

def Lean.Elab.Do.elabBinder {α : Type} (binder : Syntax) (x : Expr → DoElabM α) : DoElabM α

def Lean.Elab.Do.getReassignedMutVars (rootCtx : LocalContext) (mutVars : Std.HashSet Name) (childCtxs : Array LocalContext) : Std.HashSet Name

The subset of mutVars that were reassigned in any of the childCtxs relative to the given rootCtx.

def Lean.Elab.Do.addReachingDefsAsNonDep (rootCtx childCtx : LocalContext) (tunneledVars : Std.HashSet Name) : LocalContext

Adds the new reaching definitions of the given tunneledVars in childCtx relative to rootCtx as non-dependent decls.

def Lean.Elab.Do.mkFreshContVar (resultType : Expr) (tunneledVars : Array Name) : DoElabM ContVarId

Creates a new continuation variable of type m α given the result type α. The tunneledVars is a superset of the let-bound variable names that the jumps will refer to. Often it will be the mut variables. Leaving it empty inlines let-bound variables at jump sites.

def Lean.Elab.Do.ContVarId.find (contVarId : ContVarId) : DoElabM ContVarInfo

def Lean.Elab.Do.ContVarId.mkJump (contVarId : ContVarId) : DoElabM Expr

Creates a new jump site for the continuation variable, to be synthesized later.

def Lean.Elab.Do.ContVarId.jumpCount (contVarId : ContVarId) : DoElabM Nat

The number of jump sites allocated for the continuation variable.

def Lean.Elab.Do.ContVarId.synthesizeJumps (contVarId : ContVarId) (k : DoElabM Expr) : DoElabM Unit

Synthesize the jump sites for the continuation variable. k is run once for each jump site, in the LocalContext of the jump site. The result of k is used to fill in the jump site.

def Lean.Elab.Do.ContVarId.erase (contVarId : ContVarId) : DoElabM Unit

def Lean.Elab.Do.ContVarId.getReassignedMutVars (contVarId : ContVarId) (rootCtx : LocalContext) : DoElabM (Std.HashSet Name)

The subset of (← read).mutVars that were reassigned at any of the jump sites of the continuation variable. The result array has the same order as (← read).mutVars.

def Lean.Elab.Do.withLCtxKeepingMutVarDefs {α : Type} (oldCtx : LocalContext) (oldMutVars : Array Name) (resultName : Name) (k : DoElabM α) : DoElabM α

Restores the local context to oldCtx and adds the new reaching definitions of the mut vars and result. Then resume the continuation k with the mutVars restored to the given oldMutVars.

This function is useful to de-nest

let mut x := 0
let y := 3
let z ← do
  let mut y ← e
  x := y + 1
  pure y
let y := y + 3
pure (x + y + z)

into

let mut x := 0
let y := 3
let mut y† ← e
x := y† + 1
let z ← pure y†
let y := y + 3
pure (x + y + z)

Note that the continuation of the let z ← ... bind, roughly k := .cont `z _ `(let y := y + 3; pure (x + y + z)), needs to elaborated in a local context that contains the reassignment of x, but not the shadowing mut var definition of y.

def Lean.Elab.Do.DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr

Return $e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k), cancelling the bind if $(← dec.k) is pure $dec.resultName.

def Lean.Elab.Do.DoElemCont.continueWithUnit (dec : DoElemCont) : DoElabM Expr

Return let $k.resultName : PUnit := PUnit.unit; $(← k.k), ensuring that the result type of k.k is PUnit and then immediately zeta-reduce the let.

def Lean.Elab.Do.DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (caller : DoElemCont → DoElabM Expr) : DoElabM Expr

Call caller with a duplicable proxy of dec. When the proxy is elaborated more than once, a join point is introduced so that dec is only elaborated once to fill in the RHS of this join point.

This is useful for control-flow constructs like if and match, where multiple tail-called branches share the continuation.

def Lean.Elab.Do.bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr

Given a list of mut vars vars and an FVar tupleVar binding a tuple, bind the mut vars to the fields of the tuple and call k in the resulting local context.

def Lean.Elab.Do.getReturnCont : DoElabM DoElemCont

def Lean.Elab.Do.getBreakCont : DoElabM (Option (DoElabM Expr))

def Lean.Elab.Do.getContinueCont : DoElabM (Option (DoElabM Expr))

@[inline]

def Lean.Elab.Do.withProxyMutVarDefs {α : Type} [Inhabited α] (k : (Expr → MetaM Expr) → DoElabM α) : DoElabM α

Introduce proxy redefinitions for all mut vars and call the continuation k with a function elimProxyDefs : Expr → MetaM Expr similar to mkLetFVars that will replace the proxy defs with the actual reassigned or original definitions.

def Lean.Elab.Do.enterLoopBody {α : Type} (resultType : Expr) (returnCont : DoElemCont) (breakCont continueCont : DoElabM Expr) (body : DoElabM α) : DoElabM α

Prepare the context for elaborating the body of a loop. This includes setting the return continuation, break continuation, continue continuation, as well as the changed result type of the do block in the loop body.

def Lean.Elab.Do.withoutControl (k : DoElabM Expr) : DoElabM Expr

Prepare the context for elaborating the body of a do block that does not support mut vars, break, continue or return.

def Lean.Elab.Do.enterFinally (resultType : Expr) (k : DoElabM Expr) : DoElabM Expr

Prepare the context for elaborating the body of a finally block. There is no support for mut vars, break, continue or return in a finally block.

def Lean.Elab.Do.mkContext (expectedType? : Option Expr) : TermElabM Context

Create the Context for do elaboration from the given expected type of a do block.

structure Lean.Elab.Do.SavedState : Type

Backtrackable state for the TermElabM monad.

• term : Term.SavedState
• do : State

instance Lean.Elab.Do.instNonemptySavedState : Nonempty SavedState

def Lean.Elab.Do.SavedState.restore (s : SavedState) : DoElabM Unit

def Lean.Elab.Do.DoElabM.saveState : DoElabM SavedState

instance Lean.Elab.Do.instMonadBacktrackSavedStateDoElabM : MonadBacktrack SavedState DoElabM

unsafe def Lean.Elab.Do.mkDoElemElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute DoElab)

@[implemented_by Lean.Elab.Do.mkDoElemElabAttributeUnsafe]

opaque Lean.Elab.Do.mkDoElemElabAttribute (ref : Name) : IO (KeyedDeclsAttribute DoElab)

opaque Lean.Elab.Do.doElemElabAttribute : KeyedDeclsAttribute DoElab

Registers a do element elaborator for the given syntax node kind.

A do element elaborator should have type DoElab (which is Lean.Syntax → DoElemCont → DoElabM Expr), i.e. should take syntax of the given syntax node kind and a DoElemCont as parameters and produce an expression.

When elaborating a do block do e; rest, the elaborator for e is invoked with the syntax of e and the DoElemCont representing rest.

The elab_rules and elab commands should usually be preferred over using this attribute directly.

partial def Lean.Elab.Do.elabDoElem (stx : TSyntax `doElem) (cont : DoElemCont) : DoElabM Expr

def Lean.Elab.Do.elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : DoElemCont) : DoElabM Expr

def Lean.Elab.Do.elabDoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) (cont : DoElemCont) : DoElabM Expr

def Lean.Elab.Do.dooBlock : ParserDescr

def Lean.Elab.Do.elabDooBlock : Term.TermElab

def Lean.Elab.Do.elabDo : Term.TermElab