opaque Lean.Elab.Do.experimental.intrinsic : Lean.Option Bool

def Lean.Elab.Do.warnIntrinsicExperimental {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (kw : Syntax) (what : MessageData) : m Unit

Report that an intrinsic verification form is experimental, at the keyword kw that introduces it. what names the form, as in m!"`assert` element".

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

def Lean.Elab.Do.DoOpsRef : Type

instance Lean.Elab.Do.instNonemptyDoOpsRef : Nonempty DoOpsRef

inductive Lean.Elab.Do.CodeLiveness : Type

Whether a code block is alive or dead.

• deadSyntactically : CodeLiveness

  We inferred the code is syntactically 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.)

@[instance_reducible]

instance Lean.Elab.Do.instToStringCodeLiveness : ToString CodeLiveness

@[instance_reducible]

instance Lean.Elab.Do.instToMessageDataCodeLiveness : ToMessageData CodeLiveness

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

The least upper bound of two code livenesses.

structure Lean.Elab.Do.MutVar : Type

A mutable variable declared by let mut in a do block.

• ident : Ident

  The identifier of the let mut declaration.

• baseId : FVarId

  The FVarId of the initial binding produced by let mut.

@[instance_reducible]

instance Lean.Elab.Do.instInhabitedMutVar : Inhabited MutVar

def Lean.Elab.Do.MutVar.getId (mutVar : MutVar) : Name

The raw Name of a mut variable, as found in the local context.

def Lean.Elab.Do.MutVar.mkAliasInfo (mutVar : MutVar) (id : FVarId) : FVarAliasInfo

Build an FVarAliasInfo recording that the reassignment binding id aliases the original let mut binding represented by mutVar.

@[instance_reducible]

instance Lean.Elab.Do.instToMessageDataMutVar : ToMessageData MutVar

structure Lean.Elab.Do.Context : Type

• monadInfo : MonadInfo

  Inferred and cached information about the monad.

• mutVars : Array MutVar

  The mutable variables in declaration order. Kept in sync with mutVarDefs; insertions go through declareMutVar / declareMutVars only.

• mutVarDefs : Std.HashMap Name MutVar

  Maps mutable variable names to their MutVar record. Kept in sync with mutVars.

• doBlockResultType : Expr

  The expected type of the current do block. This can be different from ReturnCont.resultType 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.

• ops : DoOpsRef

  Pluggable builders for pure and bind applications.

@[reducible, inline]

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

structure Lean.Elab.Do.DoOps : Type

Pluggable builders for the pure / bind applications emitted by the do elaborator.

• mkPureApp (α e : Expr) : DoElabM Expr

  Build pure (α:=α) e : m α.

• mkBindApp (α β e k : Expr) : DoElabM Expr

  Build bind (α:=α) (β:=β) e k : m β.

• isPureApp? : Expr → Option Expr

  If e is syntactically a pure … application, return the pure value; otherwise none. Used by DoElemCont.mkBindUnlessPure to contract e >>= pure to e and pure e >>= k to let x := e; k x.

• splitMonadApp? : Expr → TermElabM (Option (MonadInfo × Expr))

  Match a monad application m α, returning MonadInfo for m and α.

• mkMonadApp : Expr → DoElabM Expr

  Construct m α from α.

@[instance_reducible]

instance Lean.Elab.Do.instInhabitedDoOps : Inhabited DoOps

unsafe def Lean.Elab.Do.DoOps.toDoOpsRefImpl (o : DoOps) : DoOpsRef

@[implemented_by Lean.Elab.Do.DoOps.toDoOpsRefImpl]

opaque Lean.Elab.Do.DoOps.toDoOpsRef (o : DoOps) : DoOpsRef

unsafe def Lean.Elab.Do.DoOpsRef.toDoOpsImpl (r : DoOpsRef) : DoOps

@[implemented_by Lean.Elab.Do.DoOpsRef.toDoOpsImpl]

opaque Lean.Elab.Do.DoOpsRef.toDoOps (r : DoOpsRef) : DoOps

inductive Lean.Elab.Do.DoElemContKind : Type

Whether the continuation of a do element is duplicable. Saying nonDuplicable is always safe; duplicable allows for more optimizations.

• nonDuplicable : DoElemContKind
• duplicable : DoElemContKind

@[instance_reducible]

instance Lean.Elab.Do.instInhabitedDoElemContKind : Inhabited DoElemContKind

structure Lean.Elab.Do.DoElemCont : Type

Elaboration of a do block do $e; $rest, results in a call elabTerm `(do $e; $rest) = elabDoElem e dec, where elabDoElem 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.

@[instance_reducible]

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) = elabDoElem e dec, where elabDoElem 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.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 has refined resultType. So k must not hardcode the type resultType into its definition; rather it should infer the type of the return value argument.

@[instance_reducible]

instance Lean.Elab.Do.instInhabitedReturnCont : Inhabited ReturnCont

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)

@[instance_reducible]

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

Create a ReturnCont 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.DoOps.default : DoOps

DoOps emitting Pure.pure / Bind.bind.

def Lean.Elab.Do.declareMutVar {α : Type} (x : Ident) (k : DoElabM α) : DoElabM α

Register the given name as that of a mut variable.

def Lean.Elab.Do.declareMutVars {α : Type} (xs : Array Ident) (k : DoElabM α) : DoElabM α

Register the given names as that of mut variables.

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.

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.

def Lean.Elab.Do.findMutVar? (n : Name) : DoElabM (Option MutVar)

Look up a declared mut variable by its raw Name.

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

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

def Lean.Elab.Do.throwUnlessMutVarsDeclared (xs : Array Ident) : DoElabM Unit

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

def Lean.Elab.Do.checkMutVarsForShadowingOne (x : Ident) : DoElabM Unit

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

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.

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

Create a fresh α that would fit in m α.

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

@[inline]

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

@[inline]

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

def Lean.Elab.Do.withDeadCode {α : Type} (deadCode : CodeLiveness) (k : 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.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 be elaborated in a local context that contains the reassignment of x, but not the shadowing mut var definition of y.

def Lean.Elab.Do.mkMonadicResultTypeMismatchError (contType elementType : Expr) : MessageData

def Lean.Elab.Do.DoElemCont.ensureHasTypeAt (dec : DoElemCont) (ref : Syntax) (elementType : Expr) : DoElabM DoElemCont

Given a continuation dec, a reference ref, and an element result type elementType, returns a continuation derived from dec with result type elementType. If dec already has result type elementType, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result. The error is reported at ref.

def Lean.Elab.Do.DoElemCont.ensureUnitAt (dec : DoElemCont) (ref : Syntax) : DoElabM DoElemCont

Given a continuation dec and a reference ref, returns a continuation derived from dec with result type PUnit. If dec already has result type PUnit, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result. The error is reported at ref.

def Lean.Elab.Do.DoElemCont.ensureUnit (dec : DoElemCont) : DoElabM DoElemCont

Given a continuation dec, returns a continuation derived from dec with result type PUnit. If dec already has result type PUnit, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result.

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.

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

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

def Lean.Elab.Do.DoElemCont.withDeadCodeFromInfo (dec : DoElemCont) (info : ControlInfo) : DoElemCont

Wrap dec.k so it elaborates as dead iff info.noFallthrough.

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

If x is a mut variable, record that its current binding aliases the original let mut binding, so that go-to-definition and find-references treat both as the same variable.

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.

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

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

@[instance_reducible]

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

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

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

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

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.

def Lean.Elab.Do.getReturnCont : DoElabM ReturnCont

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

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

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

def Lean.Elab.Do.withRefinedResultType {α : Type} (doBlockResultType : Expr) (k : DoElabM α) : DoElabM α

Refine the result type of the do block and its return continuation for the scope of k, as needed for a dependent match branch where a bare return targets the refined branch type.

Relies on the return continuation result type coinciding with the do block result type, which holds for the tail-position dependent match this serves.

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.

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) (ops : DoOps := DoOps.default) : TermElabM Context

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

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

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

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

partial def Lean.Elab.Do.elabDoSeq (doSeq : DoSeq) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

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

def Lean.Elab.Do.elabDoWith (ops : DoOps) (doSeq : DoSeq) (expectedType? : Option Expr) : TermElabM Expr

Elaborate doSeq using ops for pure/bind construction.

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