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

inductive Lean.Elab.Do.CodeLiveness : Type

Whether a code block is alive or dead.

• deadSyntactically : CodeLiveness

  We inferred the code is semantically dead and don't need to elaborate it at all.

• deadSemantically : CodeLiveness

  We inferred the code is semantically dead, but we need to elaborate it to produce a program.

• alive : CodeLiveness

  The code is alive. (Or it is dead, but we failed to prove it so.)

@[implicit_reducible]

instance Lean.Elab.Do.instToStringCodeLiveness : ToString CodeLiveness

Equations

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

@[implicit_reducible]

instance Lean.Elab.Do.instToMessageDataCodeLiveness : ToMessageData CodeLiveness

Equations

• Lean.Elab.Do.instToMessageDataCodeLiveness = { toMessageData := fun (l : Lean.Elab.Do.CodeLiveness) => (Lean.MessageData.ofFormat ∘ Std.format) (toString l) }

def Lean.Elab.Do.CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness

The least upper bound of two code livenesses.

Equations

• Lean.Elab.Do.CodeLiveness.alive.lub b = Lean.Elab.Do.CodeLiveness.alive
• a.lub Lean.Elab.Do.CodeLiveness.alive = Lean.Elab.Do.CodeLiveness.alive
• Lean.Elab.Do.CodeLiveness.deadSyntactically.lub b = b
• a.lub Lean.Elab.Do.CodeLiveness.deadSyntactically = a
• a.lub b = a

structure Lean.Elab.Do.Context : Type

• monadInfo : MonadInfo

  Inferred and cached information about the monad.

• mutVars : Array Ident

  The mutable variables in declaration order.

• mutVarDefs : Std.HashMap Name FVarId

  Maps mutable variable names to their initial FVarIds.

• 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.

• deadCode : CodeLiveness

  Whether the current do element is dead code. elabDoElem will emit a warning if not .alive.

@[reducible, inline]

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

Equations

• Lean.Elab.Do.DoElabM = ReaderT Lean.Elab.Do.Context Lean.Elab.TermElabM

inductive Lean.Elab.Do.DoElemContKind : Type

Whether the continuation of a do element is duplicable and if so whether it is just pure r for the result variable r. Saying nonDuplicable is always safe; duplicable allows for more optimizations.

• nonDuplicable : DoElemContKind
• duplicable : DoElemContKind

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedDoElemContKind : Inhabited DoElemContKind

Equations

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

def Lean.Elab.Do.instInhabitedDoElemContKind.default : DoElemContKind

Equations

• Lean.Elab.Do.instInhabitedDoElemContKind.default = Lean.Elab.Do.DoElemContKind.nonDuplicable

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. It assumes that the result of the do block is bound to resultName with the correct type (that is, resultType, potentially refined by a dependent match).

• kind : DoElemContKind

  Whether we are OK with generating the code of the continuation multiple times, e.g. in different branches of a match or if.

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedDoElemCont : Inhabited DoElemCont

Equations

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

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

Equations

• Lean.Elab.Do.instInhabitedDoElemCont.default = { resultName := default, resultType := default, k := default, kind := 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.ReturnCont : Type

• resultType : Expr
• k : Expr → DoElabM Expr

  The elaborator constructing a jump site to the return continuation, given some return value. The type of this return value determines the type of the jump expression; this could very well be different than the resultType in case an intervening match as refined resultType. So k must not hardcode the type resultType into its definition; rather it should infer the type of the return value argument.

def Lean.Elab.Do.instInhabitedReturnCont.default : ReturnCont

Equations

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

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedReturnCont : Inhabited ReturnCont

Equations

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

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 : ReturnCont
• 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 }

@[implicit_reducible]

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

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

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.ReturnCont.mkPure (resultType : Expr) : TermElabM ReturnCont

Create a ReturnCont 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 : Ident) (k : 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.declareMutVars {α : Type} (xs : Array Ident) (k : DoElabM α) : DoElabM α

Register the given names as that of mut variables.

Equations

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

def Lean.Elab.Do.declareMutVar? {α : Type} (mutTk? : Option Syntax) (x : Ident) (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.declareMutVars? {α : Type} (mutTk? : Option Syntax) (xs : Array Ident) (k : DoElabM α) : DoElabM α

Register the given names as that of mut variables if the syntax token mut is present.

Equations

• Lean.Elab.Do.declareMutVars? mutTk? xs k = if mutTk?.isSome = true then Lean.Elab.Do.declareMutVars xs k else k

def Lean.Elab.Do.throwUnlessMutVarDeclared (x : Ident) : 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.throwUnlessMutVarsDeclared (xs : Array Ident) : DoElabM Unit

Throw an error if the given names are not declared mut variables.

Equations

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

def Lean.Elab.Do.checkMutVarsForShadowingOne (x : Ident) : 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.checkMutVarsForShadowing (xs : Array Ident) : 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 := `α) (kind : MetavarKind := MetavarKind.natural) : DoElabM Expr

Create a fresh α that would fit in m α.

Equations

• Lean.Elab.Do.mkFreshResultType userName kind = do let __do_lift ← read liftM (Lean.Meta.mkFreshExprMVar (some (Lean.mkSort (Lean.mkLevelSucc __do_lift.monadInfo.u))) kind userName)

@[inline]

def Lean.Elab.Do.controlAtTermElabM {α : Type} (k : ({β : Type} → DoElabM β → TermElabM β) → TermElabM α) : DoElabM α

Like controlAt TermElabM, but it maintains the state using the DoElabM's ref cell instead of returning it in the TermElabM result. This makes it possible to run multiple DoElabM computations in a row.

Equations

• Lean.Elab.Do.controlAtTermElabM k ctx = k fun {β : Type} (x : Lean.Elab.Do.DoElabM β) => x ctx

@[inline]

def Lean.Elab.Do.mapTermElabM (f : {α : Type} → TermElabM α → TermElabM α) {α : Type} (k : DoElabM α) : DoElabM α

Equations

• Lean.Elab.Do.mapTermElabM f k = Lean.Elab.Do.controlAtTermElabM fun (runInBase : {β : Type} → Lean.Elab.Do.DoElabM β → Lean.Elab.TermElabM β) => f (runInBase k)

@[inline]

def Lean.Elab.Do.map1TermElabM {β : Sort u_1} (f : {α : Type} → (β → TermElabM α) → TermElabM α) {α : Type} (k : β → DoElabM α) : DoElabM α

Equations

• Lean.Elab.Do.map1TermElabM f k = Lean.Elab.Do.controlAtTermElabM fun (runInBase : {β : Type} → Lean.Elab.Do.DoElabM β → Lean.Elab.TermElabM β) => f fun (b : β) => runInBase (k b)

def Lean.Elab.Do.withDeadCode {α : Type} (deadCode : CodeLiveness) (k : 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.withLCtxKeepingMutVarDefs {α : Type} (oldLCtx : LocalContext) (oldCtx : Context) (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 or e is some pure computation.

Equations

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

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.elabAsSyntacticallyDeadCode (dec : DoElemCont) : DoElabM Unit

Elaborate the DoElemCont with the deadCode flag set to deadSyntactically to emit warnings.

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 #[]

structure Lean.Elab.Do.SavedState : Type

Backtrackable state for the TermElabM monad.

• term : Term.SavedState

instance Lean.Elab.Do.instNonemptySavedState : Nonempty SavedState

def Lean.Elab.Do.SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : DoElabM Unit

Equations

• s.restore restoreInfo = liftM (s.term.restore restoreInfo)

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

Equations

• Lean.Elab.Do.DoElabM.saveState = do let __do_lift ← liftM Lean.Elab.Term.saveState pure { term := __do_lift }

@[implicit_reducible]

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 }

def Lean.Elab.Do.observingPostpone {α : Type} (x : DoElabM α) : DoElabM (Option α)

Equations

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

def Lean.Elab.Do.doElabToSyntaxWithExpectedType {α : Type} (hint : MessageData) (doElab : Option Expr → DoElabM Expr) (k : Term → DoElabM α) (ref : Syntax := Syntax.missing) : DoElabM α

Equations

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

def Lean.Elab.Do.doElabToSyntax {α : Type} (hint : MessageData) (doElab : DoElabM Expr) (k : Term → DoElabM α) (ref : Syntax := Syntax.missing) : DoElabM α

Equations

• Lean.Elab.Do.doElabToSyntax hint doElab k ref = Lean.Elab.Do.doElabToSyntaxWithExpectedType hint (fun (_ty? : Option Lean.Expr) => doElab) k ref

def Lean.Elab.Do.DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : ControlInfo) (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.getReturnCont : DoElabM ReturnCont

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.withDoBlockResultType {α : Type} (doBlockResultType : Expr) (k : DoElabM α) : DoElabM α

Set the new do block result type for the scope of the continuation k.

Equations

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

def Lean.Elab.Do.enterLoopBody {α : Type} (breakCont continueCont : DoElabM Expr) (returnCont : ReturnCont) (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

• Lean.Elab.Do.enterFinally resultType k = Lean.Elab.Do.withoutControl (Lean.Elab.Do.withDoBlockResultType resultType k)

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.

def Lean.Elab.Do.expandNestedActions {kind : SyntaxNodeKinds} (stx : TSyntax kind) : DoElabM (Array (TSyntax `doElem) × TSyntax kind)

Equations

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

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) (catchExPostpone : Bool := true) : DoElabM Expr

partial def Lean.Elab.Do.elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

partial def Lean.Elab.Do.elabDoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

def Lean.Elab.Do.elabNestedAction : 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.