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

Equations

• Lean.Elab.Do.ContInfoRef = Lean.Elab.Do.ContInfoRefPointed✝.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

Equations

• Lean.Elab.Do.instInhabitedContVarId.default = { name := default }

instance Lean.Elab.Do.instInhabitedContVarId : Inhabited ContVarId

Equations

• Lean.Elab.Do.instInhabitedContVarId = { default := Lean.Elab.Do.instInhabitedContVarId.default }

instance Lean.Elab.Do.instBEqContVarId : BEq ContVarId

Equations

• Lean.Elab.Do.instBEqContVarId = { beq := Lean.Elab.Do.instBEqContVarId.beq }

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

Equations

• Lean.Elab.Do.instBEqContVarId.beq { name := a } { name := b } = (a == b)
• Lean.Elab.Do.instBEqContVarId.beq x✝¹ x✝ = false

instance Lean.Elab.Do.instHashableContVarId : Hashable ContVarId

Equations

• Lean.Elab.Do.instHashableContVarId = { hash := Lean.Elab.Do.instHashableContVarId.hash }

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

Equations

• Lean.Elab.Do.instHashableContVarId.hash { name := a } = mixHash 0 (hash a)

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

Equations

• Lean.Elab.Do.DoElabM = ReaderT Lean.Elab.Do.Context (StateRefT' IO.RealWorld Lean.Elab.Do.State Lean.Elab.TermElabM)

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

Equations

• Lean.Elab.Do.instInhabitedDoElemCont.default = { resultName := default, resultType := default, k := default }

instance Lean.Elab.Do.instInhabitedDoElemCont : Inhabited DoElemCont

Equations

• Lean.Elab.Do.instInhabitedDoElemCont = { default := Lean.Elab.Do.instInhabitedDoElemCont.default }

@[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.

Equations

• Lean.Elab.Do.DoElab = (Lean.TSyntax `doElem → Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr)

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

Equations

• Lean.Elab.Do.instInhabitedContInfo.default = { returnCont := default, breakCont := default, continueCont := default }

instance Lean.Elab.Do.instInhabitedContInfo : Inhabited ContInfo

Equations

• Lean.Elab.Do.instInhabitedContInfo = { default := Lean.Elab.Do.instInhabitedContInfo.default }

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

Equations

• m.toContInfoRefImpl = unsafeCast m

@[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

Equations

• m.toContInfoImpl = unsafeCast m

@[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 α.

Equations

• Lean.Elab.Do.mkMonadicType resultType = do let __do_lift ← read pure (Lean.mkApp __do_lift.monadInfo.m resultType)

def Lean.Elab.Do.mkPUnit : DoElabM Expr

The cached PUnit expression.

Equations

• Lean.Elab.Do.mkPUnit = do let __do_lift ← read pure __do_lift.monadInfo.cachedPUnit

def Lean.Elab.Do.mkPUnitUnit : DoElabM Expr

The cached PUnit.unit expression.

Equations

• Lean.Elab.Do.mkPUnitUnit = do let __do_lift ← read pure __do_lift.monadInfo.cachedPUnitUnit

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

The expression pure (α:=α) e.

Equations

• Lean.Elab.Do.mkPureApp α e = do let e ← liftM (Lean.Elab.Term.ensureHasType (some α) e) let __do_lift ← Lean.Elab.Do.getCachedPure✝ pure (Lean.mkApp2 __do_lift α e)

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

Create a DoElemCont returning the result using pure.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Register the given name as that of a mut variable.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Elab.Do.declareMutVar? mutTk? x k = if mutTk?.isSome = true then Lean.Elab.Do.declareMutVar x k else k

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Create a fresh α that would fit in m α.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Do.elabTerm stx expectedType? = do let __discr ← liftM (Lean.Elab.Do.withPendingMVars✝ (Lean.Elab.Term.elabTerm stx expectedType?)) match __discr with | (e, _pendingMVars) => pure e

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

Equations

• Lean.Elab.Do.elabTermEnsuringType stx expectedType? = do let e ← liftM (Lean.Elab.Term.elabTermEnsuringType stx expectedType?) pure e

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The number of jump sites allocated for the continuation variable.

Equations

• contVarId.jumpCount = do let info ← contVarId.find pure info.jumps.size

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• contVarId.erase = modify fun (s : Lean.Elab.Do.State) => { monadInstanceCache := s.monadInstanceCache, contVars := s.contVars.erase contVarId }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• dec.mkBindUnlessPure e = Lean.Elab.Do.mkBindCancellingPure dec.resultName dec.resultType e fun (x : Lean.Expr) => dec.k

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Elab.Do.bindMutVarsFromTuple vars tupleVar k = do let __do_lift ← liftM tupleVar.getType Lean.Elab.Do.bindMutVarsFromTuple.go✝ k vars tupleVar __do_lift #[]

def Lean.Elab.Do.getReturnCont : DoElabM DoElemCont

Equations

• Lean.Elab.Do.getReturnCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.returnCont

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

Equations

• Lean.Elab.Do.getBreakCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.breakCont

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

Equations

• Lean.Elab.Do.getContinueCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.continueCont

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• s.restore = do liftM s.term.restore set s.do

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

Equations

• Lean.Elab.Do.DoElabM.saveState = do let __do_lift ← liftM Lean.Elab.Term.saveState let __do_lift_1 ← get pure { term := __do_lift, «do» := __do_lift_1 }

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

Equations

• Lean.Elab.Do.instMonadBacktrackSavedStateDoElabM = { saveState := Lean.Elab.Do.DoElabM.saveState, restoreState := fun (b : Lean.Elab.Do.SavedState) => b.restore }

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

Equations

• Lean.Elab.Do.mkDoElemElabAttributeUnsafe ref = Lean.Elab.mkElabAttribute Lean.Elab.Do.DoElab `builtin_doElem_elab `doElem_elab `Lean.Parser.Term.doElem `Lean.Elab.Do.DoElab "do element" ref

@[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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Do.elabDoSeq doSeq cont = Lean.Elab.Do.elabDoElems1 (Lean.Parser.Term.getDoElems doSeq) cont

def Lean.Elab.Do.dooBlock : ParserDescr

Equations

• Lean.Elab.Do.dooBlock = Lean.ParserDescr.node `Lean.Elab.Do.dooBlock 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "doo") (Lean.ParserDescr.const `doSeq))

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.