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

refactor: ParserContextCore and ParserContext

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-08 14:20:53 -08:00
parent 8484aa08f3
commit c4ad3a2390
5 changed files with 58 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/Init/Lean/Elab/Frontend.lean
View file

@ -15,7 +15,7 @@ structure Context :=
(commandStateRef : IO.Ref Command.State)
(parserStateRef : IO.Ref Parser.ModuleParserState)
(cmdPosRef : IO.Ref String.Pos)
(parserCtx : Parser.ParserContextCore)
(inputCtx : Parser.InputContext)
abbrev FrontendM := ReaderT Context (EIO Empty)
@ -25,7 +25,7 @@ EIO.catchExceptions x (fun _ => unreachable!)
@[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit :=
fun ctx => do
cmdPos ← liftIOCore! $ ctx.cmdPosRef.get;
let cmdCtx : Command.Context := { cmdPos := cmdPos, stateRef := ctx.commandStateRef, fileName := ctx.parserCtx.fileName, fileMap := ctx.parserCtx.fileMap };
let cmdCtx : Command.Context := { cmdPos := cmdPos, stateRef := ctx.commandStateRef, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap };
EIO.catchExceptions (x cmdCtx) (fun _ => pure ())
def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit :=
@ -48,17 +48,15 @@ fun ctx => liftIOCore! $ ctx.parserStateRef.set ps
def setMessages (msgs : MessageLog) : FrontendM Unit :=
fun ctx => liftIOCore! $ ctx.commandStateRef.modify $ fun s => { messages := msgs, .. s }
def getParserContext : FrontendM Parser.ParserContextCore := do
cs ← getCommandState;
ctx ← read;
pure { tokens := Parser.getTokenTable cs.env, .. ctx.parserCtx }
def getInputContext : FrontendM Parser.InputContext := do
ctx ← read; pure ctx.inputCtx
def processCommand : FrontendM Bool := do
updateCmdPos;
cs ← getCommandState;
ps ← getParserState;
px ← getParserContext;
match Parser.parseCommand cs.env px ps cs.messages with
cmdState ← getCommandState;
parserState ← getParserState;
inputCtx ← getInputContext;
match Parser.parseCommand cmdState.env inputCtx parserState cmdState.messages with
| (cmd, ps, messages) => do
setParserState ps;
setMessages messages;
@ -81,18 +79,18 @@ end Frontend
open Frontend
def IO.processCommands (parserCtx : Parser.ParserContextCore) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do
def IO.processCommands (inputCtx : Parser.InputContext) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do
ps ← parserStateRef.get;
cmdPosRef ← IO.mkRef ps.pos;
EIO.adaptExcept (fun (ex : Empty) => Empty.rec _ ex) $
processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx }
processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, inputCtx := inputCtx }
def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
let fileName := fileName.getD "<input>";
let parserCtx := Parser.mkParserContextCore env input fileName;
let inputCtx := Parser.mkInputContext input fileName;
parserStateRef ← IO.mkRef { Parser.ModuleParserState . };
cmdStateRef ← IO.mkRef $ Command.mkState env {} opts;
IO.processCommands parserCtx parserStateRef cmdStateRef;
IO.processCommands inputCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (cmdState.env, cmdState.messages)
@ -103,13 +101,13 @@ pure (env, messages.toList)
def runFrontend (env : Environment) (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
let fileName := fileName.getD "<input>";
let parserCtx := Parser.mkParserContextCore env input fileName;
match Parser.parseHeader env parserCtx with
let inputCtx := Parser.mkInputContext input fileName;
match Parser.parseHeader env inputCtx with
| (header, parserState, messages) => do
(env, messages) ← processHeader header messages parserCtx;
(env, messages) ← processHeader header messages inputCtx;
parserStateRef ← IO.mkRef parserState;
cmdStateRef ← IO.mkRef $ Command.mkState env messages opts;
IO.processCommands parserCtx parserStateRef cmdStateRef;
IO.processCommands inputCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (cmdState.env, cmdState.messages)

12
src/Init/Lean/Elab/Import.lean
View file

@ -18,23 +18,23 @@ imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
let id := stx.getIdAt 2;
{ module := normalizeModuleName id, runtimeOnly := runtime })
def processHeader (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
catch
(do env ← importModules (headerToImports header) trustLevel;
pure (env, messages))
(fun e => do
env ← mkEmptyEnvironment;
let spos := header.getPos.getD 0;
let pos := ctx.fileMap.toPosition spos;
pure (env, messages.add { fileName := ctx.fileName, data := toString e, pos := pos }))
let pos := inputCtx.fileMap.toPosition spos;
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }))
def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
env ← mkEmptyEnvironment;
let fileName := fileName.getD "<input>";
let ctx := Parser.mkParserContextCore env input fileName;
match Parser.parseHeader env ctx with
let inputCtx := Parser.mkInputContext input fileName;
match Parser.parseHeader env inputCtx with
| (header, parserState, messages) => do
pure (headerToImports header, ctx.fileMap.toPosition parserState.pos, messages)
pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
@[export lean_parse_imports]
def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do

3
src/Init/Lean/Elab/Quotation.lean
View file

@ -412,8 +412,7 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
@[export lean_parse_expr]
def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Except String (Syntax × String.Pos) := do
let c := Parser.mkParserContextCore env input "<foo>";
let c := c.toParserContext env;
let c := Parser.mkParserContext env (Parser.mkInputContext input "<foo>");
let s := Parser.mkParserState c.input;
let s := s.setPos pos;
let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn Parser.appPrec c s;

40
src/Init/Lean/Parser/Module.lean
View file

@ -34,16 +34,16 @@ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : St
let pos := c.fileMap.toPosition pos;
{ fileName := c.fileName, pos := pos, data := errorMsg }
def parseHeader (env : Environment) (c : ParserContextCore) : Syntax × ModuleParserState × MessageLog :=
let c := c.toParserContext env;
let c := Module.updateTokens c;
let s := mkParserState c.input;
let s := whitespace c s;
let s := Module.header.fn (0:Nat) c s;
def parseHeader (env : Environment) (inputCtx : InputContext) : Syntax × ModuleParserState × MessageLog :=
let ctx := mkParserContext env inputCtx;
let ctx := Module.updateTokens ctx;
let s := mkParserState ctx.input;
let s := whitespace ctx s;
let s := Module.header.fn (0:Nat) ctx s;
let stx := s.stxStack.back;
match s.errorMsg with
| some errorMsg =>
let msg := mkErrorMessage c s.pos (toString errorMsg);
let msg := mkErrorMessage ctx s.pos (toString errorMsg);
(stx, { pos := s.pos, recovering := true }, { MessageLog . }.add msg)
| none =>
(stx, { pos := s.pos }, {})
@ -65,12 +65,12 @@ match s.errorMsg with
| some _ => pos + 1
| none => s.pos
partial def parseCommand (env : Environment) (c : ParserContextCore) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
| s@{ pos := pos, recovering := recovering }, messages =>
if c.input.atEnd pos then
if inputCtx.input.atEnd pos then
(mkEOI pos, s, messages)
else
let c := c.toParserContext env;
let c := mkParserContext env inputCtx;
let s := { ParserState . cache := initCacheForInput c.input, pos := pos };
let s := whitespace c s;
let s := (commandParser : Parser).fn (0:Nat) c s;
@ -86,9 +86,9 @@ partial def parseCommand (env : Environment) (c : ParserContextCore) : ModulePar
let messages := messages.add msg;
parseCommand { pos := consumeInput c s.pos, recovering := true } messages
private partial def testModuleParserAux (env : Environment) (c : ParserContextCore) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool
private partial def testModuleParserAux (env : Environment) (inputCtx : InputContext) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool
| s, messages =>
match parseCommand env c s messages with
match parseCommand env inputCtx s messages with
| (stx, s, messages) =>
if isEOI stx || isExitCommand stx then do
messages.forM $ fun msg => IO.println msg;
@ -100,14 +100,14 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo
@[export lean_test_module_parser]
def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
timeit (fileName ++ " parser") $ do
let ctx := mkParserContextCore env input fileName;
let (stx, s, messages) := parseHeader env ctx;
let inputCtx := mkInputContext input fileName;
let (stx, s, messages) := parseHeader env inputCtx;
when displayStx (IO.println stx);
testModuleParserAux env ctx displayStx s messages
testModuleParserAux env inputCtx displayStx s messages
partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleParserState → MessageLog → Array Syntax → IO Syntax
partial def parseFileAux (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Array Syntax → IO Syntax
| state, msgs, stxs =>
match parseCommand env ctx state msgs with
match parseCommand env inputCtx state msgs with
| (stx, state, msgs) =>
if isEOI stx then
if msgs.isEmpty then
@ -122,9 +122,9 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
def parseFile (env : Environment) (fname : String) : IO Syntax := do
fname ← IO.realPath fname;
contents ← IO.readTextFile fname;
let ctx := mkParserContextCore env contents fname;
let (stx, state, messages) := parseHeader env ctx;
parseFileAux env ctx state messages #[stx]
let inputCtx := mkInputContext contents fname;
let (stx, state, messages) := parseHeader env inputCtx;
parseFileAux env inputCtx state messages #[stx]
end Parser
end Lean

29
src/Init/Lean/Parser/Parser.lean
View file

@ -73,17 +73,20 @@ abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit
def SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet :=
s.insert k ()
structure ParserContextCore :=
/-
Input string and related data. Recall that the `FileMap` is a helper structure for mapping
`String.Pos` in the input string to line/column information. -/
structure InputContext :=
(input : String)
(fileName : String)
(fileMap : FileMap)
(tokens : TokenTable)
instance ParserContextCore.inhabited : Inhabited ParserContextCore :=
⟨{ input := "", fileName := "", fileMap := arbitrary _, tokens := {} }⟩
instance InputContext.inhabited : Inhabited InputContext :=
⟨{ input := "", fileName := "", fileMap := arbitrary _ }⟩
structure ParserContext extends ParserContextCore :=
structure ParserContext extends InputContext :=
(env : Environment)
(tokens : TokenTable)
structure Error :=
(unexpected : String := "")
@ -1423,23 +1426,21 @@ s.2.foldl (fun ks k _ => k::ks) []
def getTokenTable (env : Environment) : TokenTable :=
(tokenTableAttribute.ext.getState env).2
def mkParserContextCore (env : Environment) (input : String) (fileName : String) : ParserContextCore :=
def mkInputContext (input : String) (fileName : String) : InputContext :=
{ input := input,
fileName := fileName,
fileMap := input.toFileMap,
tokens := getTokenTable env }
fileMap := input.toFileMap }
@[inline] def ParserContextCore.toParserContext (env : Environment) (ctx : ParserContextCore) : ParserContext :=
{ env := env, toParserContextCore := ctx }
def mkParserContext (env : Environment) (input : String) (fileName : String) : ParserContext :=
(mkParserContextCore env input fileName).toParserContext env
def mkParserContext (env : Environment) (ctx : InputContext) : ParserContext :=
{ toInputContext := ctx,
env := env,
tokens := getTokenTable env }
def mkParserState (input : String) : ParserState :=
{ cache := initCacheForInput input }
def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "<input>") (kind := "<main>") : Except String Syntax :=
let c := mkParserContext env input fileName;
let c := mkParserContext env (mkInputContext input fileName);
let s := mkParserState input;
let s := whitespace c s;
let s := prattParser kind tables (0 : Nat) c s;