- commandState : Lean.Elab.Command.State
- parserState : Lean.Parser.ModuleParserState
- cmdPos : String.Pos
- commands : Array Lean.Syntax
@[inline]
Equations
- Lean.Elab.Frontend.setCommandState commandState = modify fun s => { commandState := commandState, parserState := s.parserState, cmdPos := s.cmdPos, commands := s.commands }
@[inline]
Equations
- Lean.Elab.Frontend.runCommandElabM x = do let ctx ← read let s ← get let cmdCtx : Lean.Elab.Command.Context := { fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap, currRecDepth := 0, cmdPos := s.cmdPos, macroStack := [], currMacroScope := Lean.firstFrontendMacroScope, ref := Lean.Syntax.missing } let a ← liftM (EIO.toIO' (StateRefT'.run (x cmdCtx) s.commandState)) match a with | Except.error e => do let a ← liftM (Lean.MessageData.toString (Lean.Exception.toMessageData e)) throw (IO.Error.userError (toString "unexpected internal error: " ++ toString a ++ toString "")) | Except.ok (a, sNew) => do Lean.Elab.Frontend.setCommandState sNew pure a
Equations
- Lean.Elab.Frontend.elabCommandAtFrontend stx = Lean.Elab.Frontend.runCommandElabM do let a ← Lean.Elab.getInfoState let infoTreeEnabled : Bool := a.enabled let a ← Lean.getOptions let _do_jp : Unit → Lean.Elab.Command.CommandElabM Unit := fun y => do Lean.Elab.Command.elabCommandTopLevel stx Lean.Elab.enableInfoTree infoTreeEnabled if Lean.checkTraceOption a `Elab.info = true then do let y ← Lean.Elab.enableInfoTree _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Frontend.updateCmdPos = modify fun s => { commandState := s.commandState, parserState := s.parserState, cmdPos := s.parserState.pos, commands := s.commands }
Equations
- Lean.Elab.Frontend.getParserState = do let a ← get pure a.parserState
Equations
- Lean.Elab.Frontend.getCommandState = do let a ← get pure a.commandState
Equations
- Lean.Elab.Frontend.setParserState ps = modify fun s => { commandState := s.commandState, parserState := ps, cmdPos := s.cmdPos, commands := s.commands }
Equations
- Lean.Elab.Frontend.setMessages msgs = modify fun s => { commandState := let src := s.commandState; { env := src.env, messages := msgs, scopes := src.scopes, nextMacroScope := src.nextMacroScope, maxRecDepth := src.maxRecDepth, nextInstIdx := src.nextInstIdx, ngen := src.ngen, infoState := src.infoState, traceState := src.traceState }, parserState := s.parserState, cmdPos := s.cmdPos, commands := s.commands }
Equations
- Lean.Elab.Frontend.getInputContext = do let a ← read pure a.inputCtx
Equations
- Lean.Elab.Frontend.processCommand = do Lean.Elab.Frontend.updateCmdPos let cmdState ← Lean.Elab.Frontend.getCommandState let ictx ← Lean.Elab.Frontend.getInputContext let pstate ← Lean.Elab.Frontend.getParserState let scope : Lean.Elab.Command.Scope := List.head! cmdState.scopes let pmctx : Lean.Parser.ParserModuleContext := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } let pos : Lean.Position := Lean.FileMap.toPosition ictx.fileMap pstate.pos match Lean.profileit "parsing" scope.opts fun x => Lean.Parser.parseCommand ictx pmctx pstate cmdState.messages with | (cmd, ps, messages) => do modify fun s => { commandState := s.commandState, parserState := s.parserState, cmdPos := s.cmdPos, commands := Array.push s.commands cmd } Lean.Elab.Frontend.setParserState ps Lean.Elab.Frontend.setMessages messages if (Lean.Parser.isEOI cmd || Lean.Parser.isExitCommand cmd) = true then pure true else do Lean.profileitM IO.Error "elaboration" scope.opts (Lean.Elab.Frontend.elabCommandAtFrontend cmd) pure false
def
Lean.Elab.IO.processCommands
(inputCtx : Lean.Parser.InputContext)
(parserState : Lean.Parser.ModuleParserState)
(commandState : Lean.Elab.Command.State)
:
Equations
- Lean.Elab.IO.processCommands inputCtx parserState commandState = do let discr ← StateRefT'.run (ReaderT.run Lean.Elab.Frontend.processCommands { inputCtx := inputCtx }) { commandState := commandState, parserState := parserState, cmdPos := parserState.pos, commands := #[] } let x : Unit × Lean.Elab.Frontend.State := discr match x with | (x, s) => pure s
def
Lean.Elab.process
(input : String)
(env : Lean.Environment)
(opts : Lean.Options)
(fileName : optParam (Option String) none)
:
Equations
- Lean.Elab.process input env opts fileName = let fileName := Option.getD fileName ""; let inputCtx := Lean.Parser.mkInputContext input fileName; do let s ← Lean.Elab.IO.processCommands inputCtx { pos := 0, recovering := false } (Lean.Elab.Command.mkState env { 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) pure (s.commandState.env, s.commandState.messages)
Equations
- Lean.Elab.getPrintMessageEndPos opts = Lean.KVMap.getBool opts `printMessageEndPos
def
Lean.Elab.runFrontend
(input : String)
(opts : Lean.Options)
(fileName : String)
(mainModuleName : Lean.Name)
(trustLevel : optParam UInt32 0)
(ileanFileName? : optParam (Option String) none)
:
Equations
- Lean.Elab.runFrontend input opts fileName mainModuleName trustLevel ileanFileName? = let inputCtx := Lean.Parser.mkInputContext input fileName; do let discr ← Lean.Parser.parseHeader inputCtx let x : Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog := discr match x with | (header, parserState, messages) => do let discr ← Lean.Elab.processHeader header opts messages inputCtx trustLevel let x : Lean.Environment × Lean.MessageLog := discr match x with | (env, messages) => let env := Lean.Environment.setMainModule env mainModuleName; let commandState := Lean.Elab.Command.mkState env messages opts; let _do_jp := fun commandState y => do let s ← Lean.Elab.IO.processCommands inputCtx parserState commandState let r ← let col := Lean.MessageLog.toList s.commandState.messages; forIn col PUnit.unit fun msg r => do let a ← Lean.Message.toString msg (Lean.Elab.getPrintMessageEndPos opts) IO.print a pure (ForInStep.yield PUnit.unit) let x : PUnit := r let _do_jp : Unit → IO (Lean.Environment × Bool) := fun y => pure (s.commandState.env, !Lean.MessageLog.hasErrors s.commandState.messages) match ileanFileName? with | some ileanFileName => let trees := Std.PersistentArray.toArray s.commandState.infoState.trees; let references := Lean.Server.findModuleRefs inputCtx.fileMap trees false; let ilean := { version := 1, module := mainModuleName, references := references }; do let y ← IO.FS.writeFile { toString := ileanFileName } (Lean.Json.compress (Lean.toJson ilean)) _do_jp y | x => do let y ← pure PUnit.unit _do_jp y; if Option.isSome ileanFileName? = true then let commandState := { env := commandState.env, messages := commandState.messages, scopes := commandState.scopes, nextMacroScope := commandState.nextMacroScope, maxRecDepth := commandState.maxRecDepth, nextInstIdx := commandState.nextInstIdx, ngen := commandState.ngen, infoState := let src := commandState.infoState; { enabled := true, assignment := src.assignment, trees := src.trees }, traceState := commandState.traceState }; do let y ← pure PUnit.unit _do_jp commandState y else do let y ← pure PUnit.unit _do_jp commandState y