From fdbbdf68fc9f32577de83208749d209f9adf3f37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Jul 2019 17:07:39 -0700 Subject: [PATCH] refactor(library/init/lean/elaborator/basic): make sure `ElabState` does not depend on parser state cc @kha --- library/init/control/estate.lean | 9 +++ library/init/lean/elaborator/basic.lean | 89 +++++++++++++++---------- library/init/lean/message.lean | 4 +- library/init/lean/parser/module.lean | 69 +++++++++---------- library/init/lean/parser/parser.lean | 11 ++- 5 files changed, 105 insertions(+), 77 deletions(-) diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean index ae85db241e..553acac73f 100644 --- a/library/init/control/estate.lean +++ b/library/init/control/estate.lean @@ -134,6 +134,15 @@ instance : MonadState σ (EState ε σ) := instance : MonadExcept ε (EState ε σ) := { throw := @EState.throw _ _, catch := @EState.catch _ _ } +@[inline] def adaptState {σ₁ σ₂} (x : EState ε σ₁ α) (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) : EState ε σ α := +fun r => match r with + | ⟨Result.error _ _, h⟩ => unreachableError h + | ⟨Result.ok _ s, _⟩ => + let (s₁, s₂) := split s; + match x (resultOk.mk ⟨⟩ s₁) with + | Result.ok a s₁ => Result.ok a (merge s₁ s₂) + | Result.error e s₁ => Result.error e (merge s₁ s₂) + @[inline] def run (x : EState ε σ α) (s : σ) : Result ε σ α := x (resultOk.mk ⟨⟩ s) diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index 04fcf7e8dc..1c9c4ac8ca 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/library/init/lean/elaborator/basic.lean @@ -4,18 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude +import init.control.reader import init.lean.namegenerator import init.lean.scopes import init.lean.parser.module namespace Lean +structure ElabContext := +(fileName : String) +(fileMap : FileMap) + structure ElabScope := (options : Options := {}) structure ElabState := (env : Environment) -(parser : Parser.ModuleParser) +(messages : MessageLog := {}) (cmdPos : String.Pos := 0) (ngen : NameGenerator := {}) (scopes : List ElabScope := []) @@ -31,7 +36,7 @@ instance : Inhabited ElabException := ⟨other "error"⟩ end ElabException -abbrev Elab := EState ElabException ElabState +abbrev Elab := ReaderT ElabContext (EState ElabException ElabState) abbrev TermElab := Syntax → Elab Expr abbrev CommandElab := Syntax → Elab Unit @@ -180,11 +185,10 @@ mkElabAttribute `commandTerm "command" builtinCommandElabTable constant commandElabAttribute : CommandElabAttribute := default _ def logErrorAt (pos : String.Pos) (errorMsg : String) : Elab Unit := -do s ← get; - let ctx := s.parser.context; +do ctx ← read; let pos := ctx.fileMap.toPosition pos; - let msg := { Message . filename := ctx.filename, pos := pos, text := errorMsg }; - modify (fun s => { parser := { messages := s.parser.messages.add msg, .. s.parser }, .. s }) + let msg := { Message . filename := ctx.fileName, pos := pos, text := errorMsg }; + modify (fun s => { messages := s.messages.add msg, .. s }) def logErrorUsingCmdPos (errorMsg : String) : Elab Unit := do s ← get; @@ -223,61 +227,72 @@ match stx with | none => logError stx ("command elaborator failed, no support for syntax '" ++ toString k ++ "'") | _ => logErrorUsingCmdPos ("command elaborator failed, unexpected syntax") -def mkElabState (env : Environment) (parser : Parser.ModuleParser) : ElabState := -{ env := env, parser := parser } +structure FrontendState := +(elabState : ElabState) +(parserState : Parser.ModuleParserState) -def updateParser (p : Parser.ModuleParser) : Elab Unit := -modify (fun s => { parser := p, .. s }) +abbrev Frontend := ReaderT Parser.ParserContextCore (EState ElabException FrontendState) -def updateCmdPos : Elab Unit := -modify (fun s => { cmdPos := s.parser.pos, .. s }) +def getElabContext : Frontend ElabContext := +do c ← read; + pure { fileName := c.filename, fileMap := c.fileMap } -def processCommand : Elab Bool := +def elabCommandAtFrontend (stx : Syntax) : Frontend Unit := +do c ← getElabContext; + monadLift $ EState.adaptState (elabCommand stx c) + (fun (s : FrontendState) => (s.elabState, s.parserState)) + (fun es ps => { elabState := es, parserState := ps }) + +def updateCmdPos : Frontend Unit := +modify $ fun s => { elabState := { cmdPos := s.parserState.pos, .. s.elabState }, .. s } + +def processCommand : Frontend Bool := do updateCmdPos; s ← get; - let p := s.parser; - match Parser.parseCommand s.env p with - | (stx, p) => do - updateParser p; - if Parser.isEOI stx || Parser.isExitCommand stx then do + let es := s.elabState; + let ps := s.parserState; + c ← read; + match Parser.parseCommand es.env c ps es.messages with + | (cmd, ps, messages) => do + set { elabState := { messages := messages, .. es }, parserState := ps }; + if Parser.isEOI cmd || Parser.isExitCommand cmd then do pure true -- Done else do - elabCommand stx; + elabCommandAtFrontend cmd; pure false -partial def processCommandsAux : Unit → Elab Unit +partial def processCommandsAux : Unit → Frontend Unit | () := do done ← processCommand; if done then pure () else processCommandsAux () -def processCommands : Elab Unit := +def processCommands : Frontend Unit := processCommandsAux () -def processHeader (header : Syntax) (messages : MessageLog) : IO (Option Environment × MessageLog) := +def processHeader (header : Syntax) (messages : MessageLog) : IO (Environment × MessageLog) := do IO.println header; -- TODO env ← mkEmptyEnvironment; - pure (some env, messages) + pure (env, messages) -def testFrontend (input : String) (filename := "") : IO (Option Environment × MessageLog) := +def testFrontend (input : String) (fileName := "") : IO (Environment × MessageLog) := do env ← mkEmptyEnvironment; - let (stx, p) := Parser.mkModuleParser env input filename; - match stx with - | none => pure (none, p.messages) - | some stx => do - (optEnv, messages) ← processHeader stx p.messages; - match optEnv with - | none => pure (none, messages) - | some env => - let p := { messages := messages, .. p }; - let s := mkElabState env p; - match processCommands.run s with - | EState.Result.ok _ s => pure (some s.env, s.parser.messages) - | EState.Result.error _ s => pure (none, s.parser.messages) + let ctx := Parser.mkParserContextCore env input fileName; + match Parser.parseHeader env ctx with + | (header, parserState, messages) => do + (env, messages) ← processHeader header messages; + let elabState := { ElabState . env := env, messages := messages }; + match (processCommands ctx).run { elabState := elabState, parserState := parserState } with + | EState.Result.ok _ s => pure (s.elabState.env, s.elabState.messages) + | EState.Result.error _ s => pure (s.elabState.env, s.elabState.messages) + namespace Elab +instance {α} : Inhabited (Elab α) := +⟨fun _ => default _⟩ + /- Remark: in an ideal world where performance doesn't matter, we would define `Elab` as ``` ExceptT ElabException (StateT ElabException IO) diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index 099866b8e4..2d24fd9ac2 100644 --- a/library/init/lean/message.lean +++ b/library/init/lean/message.lean @@ -45,7 +45,9 @@ structure MessageLog := (revList : List Message := []) namespace MessageLog -def empty : MessageLog := ⟨[]⟩ +def empty : MessageLog := ⟨{}⟩ + +instance : Inhabited MessageLog := ⟨{}⟩ def add (msg : Message) (log : MessageLog) : MessageLog := ⟨msg :: log.revList⟩ diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index 9d23d6eb9c..8d4f374cc0 100644 --- a/library/init/lean/parser/module.lean +++ b/library/init/lean/parser/module.lean @@ -24,32 +24,30 @@ def updateTokens (c : ParserContext) : ParserContext := end Module -structure ModuleParser := -(context : ParserContextCore) +structure ModuleParserState := (pos : String.Pos := 0) -(messages : MessageLog := {}) -(recovering : Bool := false) +(recovering : Bool := false) -instance ModuleParser.inhabited : Inhabited ModuleParser := -⟨{context := default _}⟩ +instance ModuleParserState.inhabited : Inhabited ModuleParserState := +⟨{}⟩ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message := let pos := c.fileMap.toPosition pos; { filename := c.filename, pos := pos, text := errorMsg } -def mkModuleParser (env : Environment) (input : String) (filename := "") : Option Syntax × ModuleParser := -let c := mkParserContext env input filename; +def parseHeader (env : Environment) (c : ParserContextCore) : Syntax × ModuleParserState × MessageLog := +let c := c.toParserContext env; let c := Module.updateTokens c; -let s := mkParserState input; +let s := mkParserState c.input; let s := whitespace c s; let s := Module.header.fn (0:Nat) c s; +let stx := s.stxStack.back; match s.errorMsg with | some errorMsg => let msg := mkErrorMessage c s.pos (toString errorMsg); - (none, { context := c.toParserContextCore, pos := s.pos, messages := { MessageLog . }.add msg, recovering := true }) + (stx, { pos := s.pos, recovering := true }, { MessageLog . }.add msg) | none => - let stx := s.stxStack.back; - (stx, { context := c.toParserContextCore, pos := s.pos }) + (stx, { pos := s.pos }, {}) private def mkEOI (pos : String.Pos) : Syntax := let atom := mkAtom { pos := pos, trailing := "".toSubstring, leading := "".toSubstring } ""; @@ -68,45 +66,44 @@ match s.errorMsg with | some _ => pos + 1 | none => s.pos -partial def parseCommand (env : Environment) : ModuleParser → Syntax × ModuleParser -| p := - if p.context.input.atEnd p.pos then - (mkEOI p.pos, p) +partial def parseCommand (env : Environment) (c : ParserContextCore) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog +| s@{ pos := pos, recovering := recovering } messages := + if c.input.atEnd pos then + (mkEOI pos, s, messages) else - let c : ParserContext := { env := env, .. p.context }; - let s : ParserState := { cache := initCacheForInput c.input, pos := p.pos }; - let s := (commandParser : Parser).fn (0:Nat) c s; + let c := c.toParserContext env; + let s := { ParserState . cache := initCacheForInput c.input, pos := pos }; + let s := (commandParser : Parser).fn (0:Nat) c s; match s.errorMsg with | none => let stx := s.stxStack.back; - let p := { pos := s.pos, recovering := false, .. p }; - (stx, p) + (stx, { pos := s.pos }, messages) | some errorMsg => - if p.recovering then - let p := { pos := consumeInput c s.pos, .. p }; - parseCommand p + if recovering then + parseCommand { pos := consumeInput c s.pos, recovering := true } messages else - let msg := mkErrorMessage c s.pos (toString errorMsg); - let p := { pos := s.pos, recovering := true, messages := p.messages.add msg, .. p }; - parseCommand p + let msg := mkErrorMessage c s.pos (toString errorMsg); + let messages := messages.add msg; + parseCommand { pos := consumeInput c s.pos, recovering := true } messages -private partial def testModuleParserAux (env : Environment) (displayStx : Bool) : ModuleParser → IO Bool -| p := - match parseCommand env p with - | (stx, p) => +private partial def testModuleParserAux (env : Environment) (c : ParserContextCore) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool +| s messages := + match parseCommand env c s messages with + | (stx, s, messages) => if isEOI stx || isExitCommand stx then do - p.messages.toList.mfor $ fun msg => IO.println msg; - pure (!p.messages.hasErrors) + messages.toList.mfor $ fun msg => IO.println msg; + pure (!messages.hasErrors) else do when displayStx (IO.println stx); - testModuleParserAux p + testModuleParserAux s messages @[export lean.test_module_parser_core] def testModuleParser (env : Environment) (input : String) (filename := "") (displayStx := false) : IO Bool := timeit (filename ++ " parser") $ do - let (stx, p) := mkModuleParser env input filename; + let ctx := mkParserContextCore env input filename; + let (stx, s, messages) := parseHeader env ctx; when displayStx (IO.println stx); - testModuleParserAux env displayStx p + testModuleParserAux env ctx displayStx s messages end Parser end Lean diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 8bfded03e2..76f4766424 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -1381,13 +1381,18 @@ def getSyntaxNodeKinds : IO (List SyntaxNodeKind) := do s ← syntaxNodeKindSetRef.get; pure $ s.fold (fun ks k _ => k::ks) [] -def mkParserContext (env : Environment) (input : String) (filename : String) : ParserContext := -{ env := env, - input := input, +def mkParserContextCore (env : Environment) (input : String) (filename : String) : ParserContextCore := +{ input := input, filename := filename, fileMap := input.toFileMap, tokens := tokenTableAttribute.ext.getState env } +@[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 mkParserState (input : String) : ParserState := { cache := initCacheForInput input }