source
structure Lean.Elab.Command.State :
Type

- env : Environment
- messages : MessageLog
- scopes : List Scope
- usedQuotCtxts : NameSet
- nextMacroScope : Nat
- maxRecDepth : Nat
- ngen : NameGenerator
- auxDeclNGen : DeclNameGenerator
- infoState : InfoState
- traceState : TraceState
- snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree)

Instances For

source
instance Lean.Elab.Command.instNonemptyState :
Nonempty State
source
structure Lean.Elab.Command.Context :
Type

- fileName : String
- fileMap : FileMap
- currRecDepth : Nat
- cmdPos : String.Pos.Raw
- macroStack : MacroStack
- quotContext? : Option Name
- currMacroScope : MacroScope
- ref : Syntax
- snap? : Option (Language.SnapshotBundle Language.DynamicSnapshot)

  Snapshot for incremental reuse and reporting of command elaboration. Currently only used for (mutual) defs and contained tactics, in which case the `DynamicSnapshot` is a `HeadersParsedSnapshot`.

  Definitely resolved in `Lean.Elab.Command.elabCommandTopLevel`.

  Invariant: if the bundle's `old?` is set, the context and state at the beginning of current and old elaboration are identical.

- cancelTk? : Option IO.CancelToken

  Cancellation token forwarded to `Core.cancelTk?`.

- suppressElabErrors : Bool

  If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration errors; see also `logMessage` below.

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Command.CommandElabM (α : Type) :
Type
Equations

- Lean.Elab.Command.CommandElabM = ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO Lean.Exception))

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Command.CommandElab :
Type
Equations

- Lean.Elab.Command.CommandElab = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

Instances For

source
structure Lean.Elab.Command.Linter :
Type

- run : Syntax → CommandElabM Unit
- name : Name

Instances For

source
@[always_inline]
instance Lean.Elab.Command.instMonadCommandElabM :
Monad CommandElabM
Equations

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

source
@[inline]
def Lean.Elab.Command.tryCatch {α : Type} (x : CommandElabM α) (h : Exception → CommandElabM α) :
CommandElabM α

Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do want to catch and process them at the command level.

Equations

- Lean.Elab.Command.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => if ex.isInterrupt = true then throw ex else h ex

Instances For

source
instance Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM :
MonadExceptOf Exception CommandElabM
Equations

- Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Elab.Command.tryCatch }

source
def Lean.Elab.Command.mkState (env : Environment) (messages : MessageLog := { }) (opts : Options := { }) :
State
Equations

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

Instances For

source
opaque Lean.Elab.Command.lintersRef :
IO.Ref (Array Linter)
source
def Lean.Elab.Command.addLinter (l : Linter) :
IO Unit
Equations

- Lean.addLinter l = do let ls ← ST.Ref.get Lean.Elab.Command.lintersRef ST.Ref.set Lean.Elab.Command.lintersRef (ls.push l)

Instances For

source
instance Lean.Elab.Command.instMonadInfoTreeCommandElabM :
MonadInfoTree CommandElabM
Equations

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

source
instance Lean.Elab.Command.instMonadEnvCommandElabM :
MonadEnv CommandElabM
Equations

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

source
@[always_inline]
instance Lean.Elab.Command.instMonadOptionsCommandElabM :
MonadOptions CommandElabM
Equations

- Lean.Elab.Command.instMonadOptionsCommandElabM = { getOptions := do let __do_lift ← get pure __do_lift.scopes.head!.opts }

source
def Lean.Elab.Command.getRef :
CommandElabM Syntax
Equations

- Lean.Elab.Command.getRef = do let __do_lift ← read pure __do_lift.ref

Instances For

source
instance Lean.Elab.Command.instAddMessageContextCommandElabM :
AddMessageContext CommandElabM
Equations

- Lean.Elab.Command.instAddMessageContextCommandElabM = { addMessageContext := Lean.addMessageContextPartial }

source
instance Lean.Elab.Command.instMonadRefCommandElabM :
MonadRef CommandElabM
Equations

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

source
instance Lean.Elab.Command.instMonadTraceCommandElabM :
MonadTrace CommandElabM
Equations

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

source
instance Lean.Elab.Command.instAddErrorMessageContextCommandElabM :
AddErrorMessageContext CommandElabM
Equations

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

source
instance Lean.Elab.Command.instMonadDeclNameGeneratorCommandElabM :
MonadDeclNameGenerator CommandElabM
Equations

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

source
def Lean.Elab.Command.getCurrMacroScope :
CommandElabM Nat
Equations

- Lean.Elab.Command.getCurrMacroScope = do let __do_lift ← read pure __do_lift.currMacroScope

Instances For

source
def Lean.Elab.Command.getMainModule :
CommandElabM Name
Equations

- Lean.Elab.Command.getMainModule = do let __do_lift ← Lean.getEnv pure __do_lift.mainModule

Instances For

source
def Lean.Elab.Command.withFreshMacroScope {α : Type} (x : CommandElabM α) :
CommandElabM α
Equations

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

Instances For

source
instance Lean.Elab.Command.instMonadQuotationCommandElabM :
MonadQuotation CommandElabM
Equations

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

source
def Lean.Elab.Command.liftCoreM {α : Type} (x : CoreM α) :
CommandElabM α
Equations

- Lean.Elab.Command.liftCoreM x = do let __do_lift ← Lean.Elab.Command.runCore✝ (observing x) ofExcept __do_lift

Instances For

source
@[inline]
def Lean.Elab.Command.liftIO {α : Type} (x : IO α) :
CommandElabM α
Equations

- Lean.Elab.Command.liftIO x = do let ctx ← read liftM (IO.toEIO (fun (ex : IO.Error) => Lean.Exception.error ctx.ref ((Lean.MessageData.ofFormat ∘ Std.format) ex.toString)) x)

Instances For

source
instance Lean.Elab.Command.instMonadLiftTIOCommandElabM :
MonadLiftT IO CommandElabM
Equations

- Lean.Elab.Command.instMonadLiftTIOCommandElabM = { monadLift := fun {α : Type} => Lean.Elab.Command.liftIO }

source
def Lean.Elab.Command.getScope :
CommandElabM Scope

Return the current scope.

Equations

- Lean.Elab.Command.getScope = do let __do_lift ← get pure __do_lift.scopes.head!

Instances For

source
instance Lean.Elab.Command.instMonadResolveNameCommandElabM :
MonadResolveName CommandElabM
Equations

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

source
instance Lean.Elab.Command.instMonadLogCommandElabM :
MonadLog CommandElabM
Equations

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

source
def Lean.Elab.Command.runLinters (stx : Syntax) :
CommandElabM Unit
Equations

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

Instances For

source
@[inline]
def Lean.Elab.Command.withLoggingExceptions (x : CommandElabM Unit) :
CommandElabM Unit

Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function catches interrupt exceptions as well and thus is intended for use at the top level of elaboration. Interrupt and abort exceptions are caught but not logged.

Equations

- Lean.Elab.Command.withLoggingExceptions x ctx ref = liftM ((Lean.Elab.withLogging x ctx ref).catchExceptions fun (x : Lean.Exception) => pure ())

Instances For

source
def Lean.Elab.Command.wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option IO.CancelToken) :
CommandElabM (α → EIO Exception β)

Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state.

Equations

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

Instances For

source
def Lean.Elab.Command.wrapAsyncAsSnapshot {α : Type} (act : α → CommandElabM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) :
CommandElabM (α → BaseIO Language.SnapshotTree)

Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for `logSnapshotTask` tasks, which are reported as part of the returned tree. The given cancellation token, if any, should be stored in a `SnapshotTask` for the server to trigger it when the result is no longer needed.

Equations

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

Instances For

source
def Lean.Elab.Command.logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) :
CommandElabM Unit

Includes a given task (such as from `wrapAsyncAsSnapshot`) in the overall snapshot tree for this command's elaboration, making its result available to reporting and the language server. The reporter will not know about this snapshot tree node until the main elaboration thread for this command has finished so this function is not useful for incremental reporting within a longer elaboration thread but only for tasks that outlive it such as background kernel checking or proof elaboration.

Equations

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

Instances For

source
def Lean.Elab.Command.runLintersAsync (stx : Syntax) :
CommandElabM Unit
Equations

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

Instances For

source
opaque Lean.Elab.Command.commandElabAttribute :
KeyedDeclsAttribute CommandElab

Registers a command elaborator for the given syntax node kind.

A command elaborator should have type `Lean.Elab.Command.CommandElab` (which is `Lean.Syntax → Lean.Elab.Term.CommandElabM Unit`), i.e. should take syntax of the given syntax node kind as a parameter and perform an action.

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

source
def Lean.Elab.Command.withoutCommandIncrementality {α : Type} (cond : Bool) (act : CommandElabM α) :
CommandElabM α

Disables incremental command reuse and reporting for `act` if `cond` is true by setting `Context.snap?` to `none`.

Equations

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

Instances For

source
def Lean.Elab.Command.withMacroExpansion {α : Type} (beforeStx afterStx : Syntax) (x : CommandElabM α) :
CommandElabM α

Elaborate `x` with `stx` on the macro stack

Equations

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

Instances For

source
instance Lean.Elab.Command.instMonadMacroAdapterCommandElabM :
MonadMacroAdapter CommandElabM
Equations

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

source
instance Lean.Elab.Command.instMonadRecDepthCommandElabM :
MonadRecDepth CommandElabM
Equations

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

source
structure Lean.Elab.Command.MacroExpandedSnapshot extends Lean.Language.Snapshot :
Type

Snapshot after macro expansion of a command.

- desc : String
- diagnostics : Diagnostics
- infoTree? : Option Elab.InfoTree
- traces : TraceState
- isFatal : Bool
- macroDecl : Name

  The declaration name of the macro.

- newStx : Syntax

  The expanded syntax tree.

- newNextMacroScope : Nat

  `State.nextMacroScope` after expansion.

- hasTraces : Bool

  Whether any traces were present after expansion.

- next : Array (Language.SnapshotTask Language.DynamicSnapshot)

  Follow-up elaboration snapshots, one per command if `newStx` is a sequence of commands.

Instances For

source
instance Lean.Elab.Command.instTypeNameMacroExpandedSnapshot :
TypeName MacroExpandedSnapshot
Equations

- Lean.Elab.Command.instTypeNameMacroExpandedSnapshot = Lean.Elab.Command.inst✝

source
instance Lean.Elab.Command.instToSnapshotTreeMacroExpandedSnapshot :
Language.ToSnapshotTree MacroExpandedSnapshot
Equations

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

source
partial def Lean.Elab.Command.elabCommand (stx : Syntax) :
CommandElabM Unit
source
opaque Lean.Elab.Command.showPartialSyntaxErrors :
Lean.Option Bool

Option for showing elaboration errors from partial syntax errors.

source
def Lean.Elab.Command.withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) :
CommandElabM Unit

If `hint?` is `some hint`, establishes a new context for macro scope naming and runs `act` in it, otherwise runs `act` directly without changes.

Context names as documented in Note `Macro Scope Representation` help with avoiding rebuilds and `prefer_native` lookup misses from macro scopes in declaration names and other exported information. This function establishes a new context with a globally unique name by combining the name of the current module with `hint` while also checking for previously used `hint`s in the same module. Thus `hint` does not need to be unique but ensuring it is usually unique helps with keeping the context name stable.

In the current implementation, we call `withInitQuotContext` once in `elabCommandTopLevel` using the source input of the command as the hint. This helps with keeping macro scopes stable on changes to other parts of the file but not on changes to the command itself. Thus in each declaration elaborator we call `withInitQuotContext` again with the declaration name(s) as a hint so that changes to any other part of the declaration do not change the context name.

Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Command.withInitQuotContext hint? act = act

Instances For

source
def Lean.Elab.Command.elabCommandTopLevel (stx : Syntax) :
CommandElabM Unit

`elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after macro expansion etc.

Equations

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

Instances For

source
def Lean.Elab.Command.adaptExpander (exp : Syntax → CommandElabM Syntax) :
CommandElab

Adapt a syntax transformation to a regular, command-producing elaborator.

Equations

- Lean.Elab.Command.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Command.withMacroExpansion stx stx' (Lean.Elab.Command.elabCommand stx')

Instances For

source
instance Lean.Elab.Command.instInhabitedCommandElabM {α : Type} :
Inhabited (CommandElabM α)
Equations

- Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

source
def Lean.Elab.Command.mkMetaContext :
Meta.Context

The environment linter framework needs to be able to run linters with the same context as `liftTermElabM`, so we expose that context as a public function here.

Equations

- Lean.Elab.Command.mkMetaContext = { keyedConfig := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }.toConfigWithKey }

Instances For

source
def Lean.Elab.Command.getBracketedBinderIds :
Syntax → CommandElabM (Array Name)

Return identifier names in the given bracketed binder.

Equations

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

Instances For

source
def Lean.Elab.Command.liftTermElabM {α : Type} (x : TermElabM α) :
CommandElabM α

Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

Note that `x` is executed with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.

If you need to access the free variables corresponding to the ones declared using the `variable` command, consider using `runTermElabM`.

Recall that `TermElabM` actions can automatically lift `MetaM` and `CoreM` actions. Example:

    public import Lean

    open Lean Elab Command Meta

    def printExpr (e : Expr) : MetaM Unit := do
      IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}"

    #eval
      liftTermElabM do
        printExpr (mkConst ``Nat)

Equations

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

Instances For

source
instance Lean.Elab.Command.instMonadEvalTermElabMCommandElabM :
MonadEval TermElabM CommandElabM
Equations

- Lean.Elab.Command.instMonadEvalTermElabMCommandElabM = { monadEval := fun {α : Type} => Lean.Elab.Command.liftTermElabM }

source
def Lean.Elab.Command.runTermElabM {α : Type} (elabFn : Array Expr → TermElabM α) :
CommandElabM α

Execute the monadic action `elabFn xs` as a `CommandElabM` monadic action, where `xs` are free variables corresponding to all active scoped variables declared using the `variable` command.

This method is similar to `liftTermElabM`, but it elaborates all scoped variables declared using the `variable` command.

Example:

    public import Lean

    public section

    open Lean Elab Command Meta

    variable {α : Type u} {f : α → α}
    variable (n : Nat)

    #eval
      runTermElabM fun xs => do
        for x in xs do
          IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"

Equations

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

Instances For

source
def Lean.Elab.Command.getScopes :
CommandElabM (List Scope)

Return the stack of all currently active scopes: the base scope always comes last; new scopes are prepended in the front. In particular, the current scope is always the first element.

Equations

- Lean.Elab.Command.getScopes = do let __do_lift ← get pure __do_lift.scopes

Instances For

source
def Lean.Elab.Command.modifyScope (f : Scope → Scope) :
CommandElabM Unit
Equations

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

Instances For

source
def Lean.Elab.Command.withScope {α : Type} (f : Scope → Scope) (x : CommandElabM α) :
CommandElabM α
Equations

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

Instances For

source
def Lean.Elab.Command.getLevelNames :
CommandElabM (List Name)
Equations

- Lean.Elab.Command.getLevelNames = do let __do_lift ← Lean.Elab.Command.getScope pure __do_lift.levelNames

Instances For

source
def Lean.Elab.Command.addUnivLevel (idStx : Syntax) :
CommandElabM Unit
Equations

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

Instances For

source
def Lean.liftCommandElabM {α : Type} (cmd : Elab.Command.CommandElabM α) (throwOnError : Bool := true) :
CoreM α

Lifts an action in `CommandElabM` into `CoreM`, updating the environment, messages, info trees, traces, the name generator, and macro scopes. The action is run in a context with an empty message log, empty trace state, and empty info trees.

If `throwOnError` is true, then if the command produces an error message, it is converted into an exception. In this case, info trees and messages are not carried over.

Commands that modify the processing of subsequent commands, such as `open` and `namespace` commands, only have an effect for the remainder of the `CommandElabM` computation passed here, and do not affect subsequent commands.

Warning: when using this from `MetaM` monads, the caches are not reset. If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache` to reset the instance cache. While the `modifyEnv` function for `MetaM` clears its caches entirely, `liftCommandElabM` has no way to reset these caches.

Equations

- Lean.liftCommandElabM cmd throwOnError = do let __do_lift ← Lean.liftCommandElabMCore✝ (observing cmd) throwOnError ofExcept __do_lift

Instances For

source
partial def Lean.withSetOptionIn (cmd : Elab.Command.CommandElab) :
Elab.Command.CommandElab

Given a command elaborator `cmd`, returns a new command elaborator that first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.