Lean.Elab.Command

source

structure Lean.Elab.Command.Scope :

Type

header : String
opts : Lean.Options
currNamespace : Lean.Name
openDecls : List Lean.OpenDecl
levelNames : List Lean.Name
varDecls : Array Lean.Syntax
varUIds : Array Lean.Name
isNoncomputable : Bool

source

instance Lean.Elab.Command.instInhabitedScope :

Inhabited Lean.Elab.Command.Scope

Equations

Lean.Elab.Command.instInhabitedScope = { default := { header := default, opts := default, currNamespace := default, openDecls := default, levelNames := default, varDecls := default, varUIds := default, isNoncomputable := default } }

source

structure Lean.Elab.Command.State :

Type

env : Lean.Environment
messages : Lean.MessageLog
scopes : List Lean.Elab.Command.Scope
nextMacroScope : Nat
maxRecDepth : Nat
nextInstIdx : Nat
ngen : Lean.NameGenerator
infoState : Lean.Elab.InfoState
traceState : Lean.TraceState

source

instance Lean.Elab.Command.instInhabitedState :

Inhabited Lean.Elab.Command.State

Equations

Lean.Elab.Command.instInhabitedState = { default := { env := default, messages := default, scopes := default, nextMacroScope := default, maxRecDepth := default, nextInstIdx := default, ngen := default, infoState := default, traceState := default } }

source

structure Lean.Elab.Command.Context :

Type

fileName : String
fileMap : Lean.FileMap
currRecDepth : Nat
cmdPos : String.Pos
macroStack : Lean.Elab.MacroStack
currMacroScope : Lean.MacroScope
ref : Lean.Syntax

source

@[inline]

abbrev Lean.Elab.Command.CommandElabCoreM (ε : Type) (α : Type) :

Type

Equations

Lean.Elab.Command.CommandElabCoreM ε = ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO ε))

source

@[inline]

abbrev Lean.Elab.Command.CommandElabM (α : Type) :

Type

Equations

Lean.Elab.Command.CommandElabM = Lean.Elab.Command.CommandElabCoreM Lean.Exception

source

@[inline]

abbrev Lean.Elab.Command.CommandElab :

Type

Equations

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

source

@[inline]

abbrev Lean.Elab.Command.Linter :

Type

Equations

Lean.Linter = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

source

instance Lean.Elab.Command.instMonadCommandElabM :

Monad Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadCommandElabM = let i := inferInstanceAs (Monad Lean.Elab.Command.CommandElabM); Monad.mk

source

def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : optParam Lean.MessageLog { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }) (opts : optParam Lean.Options { entries := [] }) :

Lean.Elab.Command.State

Equations

Lean.Elab.Command.mkState env messages opts = { env := env, messages := messages, scopes := [{ header := "", opts := opts, currNamespace := Lean.Name.anonymous, openDecls := [], levelNames := [], varDecls := #[], varUIds := #[], isNoncomputable := false }], nextMacroScope := Lean.firstFrontendMacroScope + 1, maxRecDepth := Lean.Option.get opts Lean.maxRecDepth, nextInstIdx := 1, ngen := { namePrefix := `_uniq, idx := 1 }, infoState := { enabled := false, assignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, trees := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, traceState := { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } }

source

constant Lean.Elab.Command.lintersRef :

IO.Ref (Array Lean.Linter)

source

def Lean.Elab.Command.addLinter (l : Lean.Linter) :

IO Unit

Equations

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

source

instance Lean.Elab.Command.instMonadInfoTreeCommandElabM :

Lean.Elab.MonadInfoTree Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadInfoTreeCommandElabM = { getInfoState := do let a ← get pure a.infoState, modifyInfoState := fun f => modify fun s => { env := s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := f s.infoState, traceState := s.traceState } }

source

instance Lean.Elab.Command.instMonadEnvCommandElabM :

Lean.MonadEnv Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadEnvCommandElabM = { getEnv := do let a ← get pure a.env, modifyEnv := fun f => modify fun s => { env := f s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } }

source

instance Lean.Elab.Command.instMonadOptionsCommandElabM :

Lean.MonadOptions Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadOptionsCommandElabM = { getOptions := do let a ← get pure (List.head! a.scopes).opts }

source

def Lean.Elab.Command.getRef :

Lean.Elab.Command.CommandElabM Lean.Syntax

Equations

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

source

instance Lean.Elab.Command.instAddMessageContextCommandElabM :

Lean.AddMessageContext Lean.Elab.Command.CommandElabM

Equations

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

source

instance Lean.Elab.Command.instMonadRefCommandElabM :

Lean.MonadRef Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadRefCommandElabM = { getRef := Lean.Elab.Command.getRef, withRef := fun {α} ref x => withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, currRecDepth := ctx.currRecDepth, cmdPos := ctx.cmdPos, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, ref := ref }) x }

source

instance Lean.Elab.Command.instMonadTraceCommandElabM :

Lean.MonadTrace Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadTraceCommandElabM = { modifyTraceState := fun f => modify fun s => { env := s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := f s.traceState }, getTraceState := do let a ← get pure a.traceState }

source

instance Lean.Elab.Command.instAddErrorMessageContextCommandElabM :

Lean.AddErrorMessageContext Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instAddErrorMessageContextCommandElabM = { add := fun ref msg => do let ctx ← read let ref : Lean.Syntax := Lean.Elab.getBetterRef ref ctx.macroStack let msg ← Lean.addMessageContext msg let msg ← Lean.Elab.addMacroStack msg ctx.macroStack pure (ref, msg) }

source

def Lean.Elab.Command.mkMessageAux (ctx : Lean.Elab.Command.Context) (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : Lean.MessageSeverity) :

Lean.Message

Equations

Lean.Elab.Command.mkMessageAux ctx ref msgData severity = Lean.Elab.mkMessageCore ctx.fileName ctx.fileMap msgData severity (Option.getD (Lean.Syntax.getPos? ref) ctx.cmdPos)

source

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

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.liftCoreM x = do let s ← get let ctx ← read let heartbeats ← liftM IO.getNumHeartbeats let Eα : Type := Except Lean.Exception α let x : Lean.CoreM Eα := tryCatch (do let a ← x pure (Except.ok a)) fun ex => pure (Except.error ex) let x : EIO Lean.Exception (Eα × Lean.Core.State) := StateRefT'.run (ReaderT.run x (Lean.Elab.Command.mkCoreContext ctx s heartbeats)) { env := s.env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := s.ngen, traceState := s.traceState } let discr ← liftM x let x : Eα × Lean.Core.State := discr match x with | (ea, coreS) => do modify fun s => { env := coreS.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := coreS.ngen, infoState := s.infoState, traceState := coreS.traceState } match ea with | Except.ok a => pure a | Except.error e => throw e

source

@[inline]

def Lean.Elab.Command.liftEIO {α : Type} (x : EIO Lean.Exception α) :

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.liftEIO x = liftM x

source

@[inline]

def Lean.Elab.Command.liftIO {α : Type} (x : IO α) :

Lean.Elab.Command.CommandElabM α

Equations

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

source

instance Lean.Elab.Command.instMonadLiftTIOCommandElabM :

MonadLiftT IO Lean.Elab.Command.CommandElabM

Equations

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

source

def Lean.Elab.Command.getScope :

Lean.Elab.Command.CommandElabM Lean.Elab.Command.Scope

Equations

Lean.Elab.Command.getScope = do let a ← get pure (List.head! a.scopes)

source

instance Lean.Elab.Command.instMonadResolveNameCommandElabM :

Lean.MonadResolveName Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadResolveNameCommandElabM = { getCurrNamespace := do let a ← Lean.Elab.Command.getScope pure a.currNamespace, getOpenDecls := do let a ← Lean.Elab.Command.getScope pure a.openDecls }

source

instance Lean.Elab.Command.instMonadLogCommandElabM :

Lean.Elab.MonadLog Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadLogCommandElabM = Lean.Elab.MonadLog.mk Lean.getRef (do let a ← read pure a.fileName) fun msg => do let currNamespace ← Lean.getCurrNamespace let openDecls ← Lean.getOpenDecls let msg : Lean.Message := { fileName := msg.fileName, pos := msg.pos, endPos := msg.endPos, severity := msg.severity, caption := msg.caption, data := Lean.MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data } modify fun s => { env := s.env, messages := Lean.MessageLog.add msg s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState }

source

def Lean.Elab.Command.runLinters (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.runLinters stx = do let linters ← ST.Ref.get Lean.Elab.Command.lintersRef if Array.isEmpty linters = true then pure PUnit.unit else do let r ← forIn linters PUnit.unit fun linter r => do let savedState ← get tryFinally (tryCatch (linter stx) fun ex => Lean.Elab.logException ex) (modify fun s => { env := savedState.env, messages := s.messages, scopes := savedState.scopes, nextMacroScope := savedState.nextMacroScope, maxRecDepth := savedState.maxRecDepth, nextInstIdx := savedState.nextInstIdx, ngen := savedState.ngen, infoState := savedState.infoState, traceState := savedState.traceState }) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

def Lean.Elab.Command.getCurrMacroScope :

Lean.Elab.Command.CommandElabM Nat

Equations

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

source

def Lean.Elab.Command.getMainModule :

Lean.Elab.Command.CommandElabM Lean.Name

Equations

Lean.Elab.Command.getMainModule = do let a ← Lean.getEnv pure (Lean.Environment.mainModule a)

source

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

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.withFreshMacroScope x = do let fresh ← modifyGet fun st => (st.nextMacroScope, { env := st.env, messages := st.messages, scopes := st.scopes, nextMacroScope := st.nextMacroScope + 1, maxRecDepth := st.maxRecDepth, nextInstIdx := st.nextInstIdx, ngen := st.ngen, infoState := st.infoState, traceState := st.traceState }) withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, currRecDepth := ctx.currRecDepth, cmdPos := ctx.cmdPos, macroStack := ctx.macroStack, currMacroScope := fresh, ref := ctx.ref }) x

source

instance Lean.Elab.Command.instMonadQuotationCommandElabM :

Lean.MonadQuotation Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadQuotationCommandElabM = Lean.MonadQuotation.mk Lean.Elab.Command.getCurrMacroScope Lean.Elab.Command.getMainModule fun {α} => Lean.Elab.Command.withFreshMacroScope

source

unsafe def Lean.Elab.Command.mkCommandElabAttributeUnsafe :

IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

Equations

Lean.Elab.Command.mkCommandElabAttributeUnsafe = Lean.Elab.mkElabAttribute Lean.Elab.Command.CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"

source

@[implementedBy Lean.Elab.Command.mkCommandElabAttributeUnsafe]

constant Lean.Elab.Command.mkCommandElabAttribute :

IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

source

constant Lean.Elab.Command.commandElabAttribute :

Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab

source

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

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.withMacroExpansion beforeStx afterStx x = withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, currRecDepth := ctx.currRecDepth, cmdPos := ctx.cmdPos, macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, currMacroScope := ctx.currMacroScope, ref := ctx.ref }) x

source

instance Lean.Elab.Command.instMonadMacroAdapterCommandElabM :

Lean.Elab.MonadMacroAdapter Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadMacroAdapterCommandElabM = { getCurrMacroScope := Lean.getCurrMacroScope, getNextMacroScope := do let a ← get pure a.nextMacroScope, setNextMacroScope := fun next => modify fun s => { env := s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := next, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } }

source

instance Lean.Elab.Command.instMonadRecDepthCommandElabM :

Lean.MonadRecDepth Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadRecDepthCommandElabM = { withRecDepth := fun {α} d x => withReader (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, currRecDepth := d, cmdPos := ctx.cmdPos, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, ref := ctx.ref }) x, getRecDepth := do let a ← read pure a.currRecDepth, getMaxRecDepth := do let a ← get pure a.maxRecDepth }

source

constant Lean.Elab.Command.showPartialSyntaxErrors :

Lean.Option Bool

source

def Lean.Elab.Command.withLogging (x : Lean.Elab.Command.CommandElabM Unit) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.withLogging x = tryCatch x fun ex => match ex with | Lean.Exception.error x x_1 => Lean.Elab.logException ex | Lean.Exception.internal id x => if Lean.Elab.isAbortExceptionId id = true then pure () else do let idName ← Lean.Elab.Command.liftIO (Lean.InternalExceptionId.getName id) Lean.Elab.logError (Lean.toMessageData "internal exception " ++ Lean.toMessageData idName ++ Lean.toMessageData "")

source

partial def Lean.Elab.Command.elabCommand (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

source

def Lean.Elab.Command.elabCommandTopLevel (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.elabCommandTopLevel stx = Lean.withRef stx do let initMsgs ← modifyGet fun st => (st.messages, { env := st.env, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, scopes := st.scopes, nextMacroScope := st.nextMacroScope, maxRecDepth := st.maxRecDepth, nextInstIdx := st.nextInstIdx, ngen := st.ngen, infoState := st.infoState, traceState := st.traceState }) let initInfoTrees ← Lean.Elab.getResetInfoTrees Lean.Elab.Command.withLogging (Lean.Elab.Command.runLinters stx) Lean.Elab.Command.elabCommand stx let a ← get let msgs ← pure a.messages let a ← Lean.getOptions let _do_jp : Lean.MessageLog → PUnit → Lean.Elab.Command.CommandElabM Unit := fun msgs y => do let a ← Lean.Elab.getInfoTrees let r ← let col := a; forIn col PUnit.unit fun tree r => let cls := `Elab.info; do let a ← Lean.isTracingEnabledFor cls if a = true then do let a ← Lean.Internal.liftCoeM (Lean.Elab.InfoTree.format tree none) Lean.addTrace cls a pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r modify fun st => { env := st.env, messages := initMsgs ++ msgs, scopes := st.scopes, nextMacroScope := st.nextMacroScope, maxRecDepth := st.maxRecDepth, nextInstIdx := st.nextInstIdx, ngen := st.ngen, infoState := let src := st.infoState; { enabled := src.enabled, assignment := src.assignment, trees := initInfoTrees ++ st.infoState.trees }, traceState := st.traceState } Lean.Elab.Command.addTraceAsMessages if (!Lean.Option.get a Lean.Elab.Command.showPartialSyntaxErrors && Lean.MessageLog.hasErrors initMsgs && Lean.Syntax.hasMissing stx) = true then let msgs := { msgs := Std.PersistentArray.filter msgs.msgs fun msg => Lean.MessageData.hasTag (fun tag => tag == `Elab.synthPlaceholder || tag == `Tactic.unsolvedGoals || Lean.Name.isSuffixOf `_traceMsg tag) msg.data }; do let y ← pure PUnit.unit _do_jp msgs y else do let y ← pure PUnit.unit _do_jp msgs y

source

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

Lean.Elab.Command.CommandElab

Equations

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

source

instance Lean.Elab.Command.instInhabitedCommandElabM {α : Type} :

Inhabited (Lean.Elab.Command.CommandElabM α)

Equations

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

source

def Lean.Elab.Command.getBracketedBinderIds :

Lean.Syntax → Array Lean.Name

Equations

Lean.Elab.Command.getBracketedBinderIds x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.explicitBinder = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let yes := fun x ty? => let discr_4 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let annot? := Lean.Syntax.getOptional? discr_4; let ids := Lean.Syntax.getArgs discr_2; Array.map Lean.Syntax.getId ids; if Lean.Syntax.isNone discr_3 = true then yes () none else let discr_4 := discr_3; if Lean.Syntax.matchesNull discr_4 2 = true then let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let ty? := discr; yes () (some ty?) else let discr_5 := discr_3; let discr_6 := Lean.Syntax.getArg discr 2; let discr_7 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; #[] else let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.implicitBinder = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let yes := fun x ty? => let discr := Lean.Syntax.getArg discr 3; let ids := Lean.Syntax.getArgs discr_2; Array.map Lean.Syntax.getId ids; if Lean.Syntax.isNone discr_3 = true then yes () none else let discr_4 := discr_3; if Lean.Syntax.matchesNull discr_4 2 = true then let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let ty? := discr; yes () (some ty?) else let discr_5 := discr_3; let discr_6 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; #[] else let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.instBinder = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr_3 := Lean.Syntax.getArg discr_2 0; let discr_4 := Lean.Syntax.getArg discr_2 1; let discr_5 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let ty := discr_5; let id := discr_3; #[Lean.Syntax.getId id] else let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_3 0 = true then let discr_4 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let ty := discr_4; #[Lean.Name.anonymous] else let discr_4 := Lean.Syntax.getArg discr 1; let discr_5 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; #[] else let discr := x; #[]

source

def Lean.Elab.Command.liftTermElabM {α : Type} (declName? : Option Lean.Name) (x : Lean.Elab.TermElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.liftTermElabM declName? x = do let ctx ← read let s ← get let heartbeats ← liftM IO.getNumHeartbeats let scope : Lean.Elab.Command.Scope := List.head! s.scopes let x : Lean.Elab.TermElabM α := Lean.Elab.withSaveInfoContext x let x : Lean.MetaM (Except Lean.Exception α × Lean.Elab.Term.State) := Lean.Elab.Term.TermElabM.run (observing x) (Lean.Elab.Command.mkTermContext ctx s declName?) (Lean.Elab.Command.mkTermState scope s) let x : Lean.CoreM ((Except Lean.Exception α × Lean.Elab.Term.State) × Lean.Meta.State) := Lean.Meta.MetaM.run x Lean.Elab.Command.mkMetaContext { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } let x : EIO Lean.Exception (((Except Lean.Exception α × Lean.Elab.Term.State) × Lean.Meta.State) × Lean.Core.State) := Lean.Core.CoreM.run x (Lean.Elab.Command.mkCoreContext ctx s heartbeats) { env := s.env, nextMacroScope := s.nextMacroScope, ngen := s.ngen, traceState := { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } } let discr ← Lean.Elab.Command.liftEIO x let x : ((Except Lean.Exception α × Lean.Elab.Term.State) × Lean.Meta.State) × Lean.Core.State := discr match x with | (((ea, termS), metaS), coreS) => do modify fun s => { env := coreS.env, messages := Lean.Elab.Command.addTraceAsMessagesCore ctx (s.messages ++ termS.messages) coreS.traceState, scopes := s.scopes, nextMacroScope := coreS.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := coreS.ngen, infoState := let src := s.infoState; { enabled := src.enabled, assignment := src.assignment, trees := Std.PersistentArray.append s.infoState.trees termS.infoState.trees }, traceState := s.traceState } match ea with | Except.ok a => pure a | Except.error ex => throw ex

source

@[inline]

def Lean.Elab.Command.runTermElabM {α : Type} (declName? : Option Lean.Name) (elabFn : Array Lean.Expr → Lean.Elab.TermElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.runTermElabM declName? elabFn = do let scope ← Lean.Elab.Command.getScope Lean.Elab.Command.liftTermElabM declName? (Lean.Elab.Term.withAutoBoundImplicit (Lean.Elab.Term.elabBinders scope.varDecls fun xs => do Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let sectionFVars : Lean.NameMap Lean.Expr := ∅ let s : Subarray Lean.Expr := toStream xs let r ← let col := scope.varUIds; forIn col { fst := s, snd := sectionFVars } fun uid r => let s := r.fst; let sectionFVars := r.snd; match Stream.next? s with | none => pure (ForInStep.done { fst := s, snd := sectionFVars }) | some (x, s') => let s := s'; let sectionFVars := Lean.NameMap.insert sectionFVars uid x; do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := sectionFVars }) let x : MProd (Subarray Lean.Expr) (Lean.NameMap Lean.Expr) := r match x with | { fst := s, snd := sectionFVars } => withReader (fun a => { fileName := a.fileName, fileMap := a.fileMap, declName? := a.declName?, macroStack := a.macroStack, currMacroScope := a.currMacroScope, mayPostpone := a.mayPostpone, errToSorry := a.errToSorry, autoBoundImplicit := a.autoBoundImplicit, autoBoundImplicits := a.autoBoundImplicits, sectionVars := a.sectionVars, sectionFVars := sectionFVars, implicitLambda := a.implicitLambda, isNoncomputableSection := a.isNoncomputableSection, ignoreTCFailures := a.ignoreTCFailures }) do Lean.Elab.Term.resetMessageLog let xs ← Lean.Elab.Term.addAutoBoundImplicits xs Lean.Elab.Term.withoutAutoBoundImplicit (elabFn xs)))

source

@[inline]

def Lean.Elab.Command.catchExceptions (x : Lean.Elab.Command.CommandElabM Unit) :

Lean.Elab.Command.CommandElabCoreM Empty Unit

Equations

Lean.Elab.Command.catchExceptions x ctx ref = EIO.catchExceptions (Lean.Elab.Command.withLogging x ctx ref) fun x => pure ()

source

def Lean.Elab.Command.getScopes :

Lean.Elab.Command.CommandElabM (List Lean.Elab.Command.Scope)

Equations

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

source

def Lean.Elab.Command.modifyScope (f : Lean.Elab.Command.Scope → Lean.Elab.Command.Scope) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.modifyScope f = modify fun s => { env := s.env, messages := s.messages, scopes := match s.scopes with | h :: t => f h :: t | [] => panicWithPosWithDecl "Lean.Elab.Command" "Lean.Elab.Command.modifyScope" 411 16 "unreachable code has been reached", nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState }

source

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

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.withScope f x = do let a ← get match a.scopes with | [] => x | h :: t => tryFinally (do modify fun s => { env := s.env, messages := s.messages, scopes := f h :: t, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } x) (modify fun s => { env := s.env, messages := s.messages, scopes := h :: t, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState })

source

def Lean.Elab.Command.getLevelNames :

Lean.Elab.Command.CommandElabM (List Lean.Name)

Equations

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

source

def Lean.Elab.Command.addUnivLevel (idStx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.addUnivLevel idStx = Lean.withRef idStx (let id := Lean.Syntax.getId idStx; do let levelNames ← Lean.Elab.Command.getLevelNames if List.elem id levelNames = true then Lean.Elab.throwAlreadyDeclaredUniverseLevel id else Lean.Elab.Command.modifyScope fun scope => { header := scope.header, opts := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls, levelNames := id :: scope.levelNames, varDecls := scope.varDecls, varUIds := scope.varUIds, isNoncomputable := scope.isNoncomputable })

source

def Lean.Elab.Command.expandDeclId (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) :

Lean.Elab.Command.CommandElabM Lean.Elab.ExpandDeclIdResult

Equations

Lean.Elab.Command.expandDeclId declId modifiers = do let currNamespace ← Lean.getCurrNamespace let currLevelNames ← Lean.Elab.Command.getLevelNames let r ← Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers let a ← Lean.Elab.Command.getScope let r_1 ← let col := Array.concatMap Lean.Elab.Command.getBracketedBinderIds a.varDecls; forIn col PUnit.unit fun id r_1 => if (id == r.shortName) = true then do Lean.throwError (Lean.toMessageData "invalid declaration name '" ++ Lean.toMessageData r.shortName ++ Lean.toMessageData "', there is a section variable with the same name") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r_1 pure r