max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/Lean/frontend): fixed last file

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-20 16:11:26 -07:00
parent 8fbe31a96d
commit 493bc63598
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
library/init/Lean/frontend.lean
View file

@ -19,14 +19,14 @@ do t ← Parser.mkTokenTrie $
Parser.tokens Term.builtinTrailingParsers,
pure $ {
filename := filename, input := input, tokens := t,
FileMap := FileMap.fromString input,
fileMap := FileMap.fromString input,
commandParsers := command.builtinCommandParsers,
leadingTermParsers := Term.builtinLeadingParsers,
trailingTermParsers := Term.builtinTrailingParsers,
}
def runFrontend (filename input : String) (printMsg : Message → Io unit) (collectOutputs : Bool) :
StateT environment Io (List Syntax) := λ env, do
def runFrontend (filename input : String) (printMsg : Message → IO unit) (collectOutputs : Bool) :
StateT environment IO (List Syntax) := λ env, do
parserCfg ← ioOfExcept $ mkConfig filename input,
-- TODO(Sebastian): `parseHeader` should be called directly by Lean.cpp
match parseHeader parserCfg with
@ -38,8 +38,8 @@ def runFrontend (filename input : String) (printMsg : Message → Io unit) (coll
let opts := Options.mk.setBool `Trace.asMessages tt,
let elabSt := Elaborator.mkState elabCfg env opts,
let addOutput (out : Syntax) outs := if collectOutputs then out::outs else [],
Io.Prim.iterate (pSnap, elabSt, parserCfg, expanderCfg, ([] : List Syntax)) $ λ ⟨pSnap, elabSt, parserCfg, expanderCfg, outs⟩, do {
let pos := parserCfg.FileMap.toPosition pSnap.it.offset,
IO.Prim.iterate (pSnap, elabSt, parserCfg, expanderCfg, ([] : List Syntax)) $ λ ⟨pSnap, elabSt, parserCfg, expanderCfg, outs⟩, do {
let pos := parserCfg.fileMap.toPosition pSnap.it.offset,
r ← monadLift $ profileitPure "parsing" pos $ λ _, parseCommand parserCfg pSnap,
match r with
| (cmd, Except.error msg) := do {
@ -53,7 +53,7 @@ def runFrontend (filename input : String) (printMsg : Message → Io unit) (coll
r ← monadLift $ profileitPure "expanding" pos $ λ _, (expand cmd).run expanderCfg,
match r with
| Except.ok cmd' := do {
--Io.println cmd',
--IO.println cmd',
elabSt ← monadLift $ profileitPure "elaborating" pos $ λ _, Elaborator.processCommand elabCfg elabSt cmd',
elabSt.messages.toList.mfor printMsg,
if cmd'.isOfKind Module.eoi then
@ -70,10 +70,10 @@ def runFrontend (filename input : String) (printMsg : Message → Io unit) (coll
}
@[export lean_process_file]
def processFile (f s : String) (json : Bool) : StateT environment Io unit := do
let printMsg : Message → Io unit := λ msg,
def processFile (f s : String) (json : Bool) : StateT environment IO unit := do
let printMsg : Message → IO unit := λ msg,
if json then
Io.println $ "{\"fileName\": \"<stdin>\", \"posLine\": " ++ toString msg.pos.line ++
IO.println $ "{\"fileName\": \"<stdin>\", \"posLine\": " ++ toString msg.pos.line ++
", \"posCol\": " ++ toString msg.pos.column ++
", \"severity\": " ++ repr (match msg.severity with
| MessageSeverity.information := "information"
@ -81,7 +81,7 @@ def processFile (f s : String) (json : Bool) : StateT environment Io unit := do
| MessageSeverity.error := "error") ++
", \"caption\": " ++ repr msg.caption ++
", \"text\": " ++ repr msg.text ++ "}"
else Io.println msg.toString,
else IO.println msg.toString,
-- print and erase uncaught exceptions
catch
(runFrontend f s printMsg ff *> pure ())