Equations
- Lean.Elab.headerToImports header = let imports := if Lean.Syntax.isNone (Lean.Syntax.getOp header 0) = true then [{ module := `Init, runtimeOnly := false }] else []; imports ++ List.map (fun stx => let runtime := !Lean.Syntax.isNone (Lean.Syntax.getOp stx 1); let id := Lean.Syntax.getId (Lean.Syntax.getOp stx 2); { module := id, runtimeOnly := runtime }) (Array.toList (Lean.Syntax.getArgs (Lean.Syntax.getOp header 1)))
def
Lean.Elab.processHeader
(header : Lean.Syntax)
(opts : Lean.Options)
(messages : Lean.MessageLog)
(inputCtx : Lean.Parser.InputContext)
(trustLevel : optParam UInt32 0)
:
Equations
- Lean.Elab.processHeader header opts messages inputCtx trustLevel = tryCatch (do let env ← Lean.importModules (Lean.Elab.headerToImports header) opts trustLevel pure (env, messages)) fun e => do let env ← Lean.mkEmptyEnvironment 0 let spos : String.Pos := Option.getD (Lean.Syntax.getPos? header) 0 let pos : Lean.Position := Lean.FileMap.toPosition inputCtx.fileMap spos pure (env, Lean.MessageLog.add { fileName := inputCtx.fileName, pos := pos, endPos := none, severity := Lean.MessageSeverity.error, caption := "", data := Function.comp Lean.MessageData.ofFormat Lean.format (toString e) } messages)
Equations
- Lean.Elab.parseImports input fileName = let fileName := Option.getD fileName ""; 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) => pure (Lean.Elab.headerToImports header, Lean.FileMap.toPosition inputCtx.fileMap parserState.pos, messages)
Equations
- Lean.Elab.printImports input fileName = do let discr ← Lean.Elab.parseImports input fileName let x : List Lean.Import × Lean.Position × Lean.MessageLog := discr match x with | (deps, pos, log) => do let r ← forIn deps PUnit.unit fun dep r => do let fname ← Lean.findOLean dep.module IO.println fname pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit