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

refactor: CommandElabM and FrontendM in IO

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-03 18:10:01 -08:00
parent 3264210d88
commit bc7455e04e
5 changed files with 112 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
src/Init/Lean/Elab/Command.lean
View file

@ -14,10 +14,6 @@ namespace Lean
namespace Elab
namespace Command
structure Context :=
(fileName : String)
(fileMap : FileMap)
structure Scope :=
(kind : String)
(header : String)
@ -32,7 +28,6 @@ instance Scope.inhabited : Inhabited Scope := ⟨{ kind := "", header := "" }⟩
structure State :=
(env : Environment)
(messages : MessageLog := {})
(cmdPos : String.Pos := 0)
(scopes : List Scope := [{ kind := "root", header := "" }])
instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
@ -40,11 +35,44 @@ instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State :=
{ env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }] }
abbrev CommandElabM := ReaderT Context (EStateM Exception State)
structure Context :=
(fileName : String)
(fileMap : FileMap)
(stateRef : IO.Ref State)
(cmdPos : String.Pos := 0)
abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
abbrev CommandElabM := CommandElabCoreM Exception
abbrev CommandElab := SyntaxNode → CommandElabM Unit
def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
mkMessageAux ctx ref ("IO error, " ++ toString err) MessageSeverity.error
@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
EIO.adaptExcept (ioErrorToMessage ctx ref) x
@[inline] def liftIO {α} (ref : Syntax) (x : IO α) : CommandElabM α :=
fun ctx => liftIOCore ctx ref x
private def getState : CommandElabM State :=
fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.get
private def setState (s : State) : CommandElabM Unit :=
fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.set s
@[inline] private def modifyGetState {α} (f : State → α × State) : CommandElabM α := do
s ← getState; let (a, s) := f s; setState s; pure a
instance CommandElabCoreM.monadState : MonadState State CommandElabM :=
{ get := getState,
set := setState,
modifyGet := @modifyGetState }
instance CommandElabM.monadLog : MonadLog CommandElabM :=
{ getCmdPos := do s ← get; pure s.cmdPos,
{ getCmdPos := do ctx ← read; pure ctx.cmdPos,
getFileMap := do ctx ← read; pure ctx.fileMap,
getFileName := do ctx ← read; pure ctx.fileName,
logMessage := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
@ -107,7 +135,7 @@ let scope := s.scopes.head!;
{ config := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
fileName := ctx.fileName,
fileMap := ctx.fileMap,
cmdPos := s.cmdPos,
cmdPos := ctx.cmdPos,
currNamespace := scope.currNamespace,
univNames := scope.univNames,
openDecls := scope.openDecls }
@ -125,8 +153,22 @@ match result with
| EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α :=
fun ctx s => toCommandResult ctx s $ (Term.elabBinders (getVarDecls s) (fun _ => x)) (mkTermContext ctx s) (mkTermState s)
instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
⟨throw $ arbitrary _⟩
@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α := do
ctx ← read;
s ← get;
match ((Term.elabBinders (getVarDecls s) (fun _ => x)) (mkTermContext ctx s)).run (mkTermState s) with
| EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
| EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
catch x (fun ex => do logMessage ex; pure ())
@[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit :=
fun ctx => EIO.catchExceptions (withLogging x ctx) (fun _ => pure ())
def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
_root_.dbgTrace (toString a) $ fun _ => pure ()

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

@ -11,40 +11,52 @@ namespace Lean
namespace Elab
namespace Frontend
structure State :=
(commandState : Command.State)
(parserState : Parser.ModuleParserState)
structure Context :=
(commandStateRef : IO.Ref Command.State)
(parserStateRef : IO.Ref Parser.ModuleParserState)
(cmdPosRef : IO.Ref String.Pos)
(parserCtx : Parser.ParserContextCore)
abbrev FrontendM := ReaderT Parser.ParserContextCore (StateM State)
abbrev FrontendM := ReaderT Context (EIO Empty)
private def getCmdContext : FrontendM Command.Context := do
c ← read;
pure { fileName := c.fileName, fileMap := c.fileMap }
@[inline] def liftIOCore! {α} [Inhabited α] (x : IO α) : EIO Empty α :=
EIO.catchExceptions x (fun _ => unreachable!)
@[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit := do
fun ctx s =>
let parserState := s.parserState;
match x { fileName := ctx.fileName, fileMap := ctx.fileMap } s.commandState with
| EStateM.Result.ok _ newCmdState => ((), { commandState := newCmdState, parserState := parserState })
| EStateM.Result.error ex newCmdState =>
let newCmdState := { messages := newCmdState.messages.add ex, .. newCmdState };
((), { commandState := newCmdState, parserState := parserState })
@[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 };
EIO.catchExceptions (x cmdCtx) (fun _ => pure ())
def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit :=
runCommandElabM (Command.elabCommand stx)
runCommandElabM (Command.withLogging $ Command.elabCommand stx)
def updateCmdPos : FrontendM Unit :=
modify $ fun s => { commandState := { cmdPos := s.parserState.pos, .. s.commandState }, .. s }
fun ctx => do
parserState ← liftIOCore! $ ctx.parserStateRef.get;
liftIOCore! $ ctx.cmdPosRef.set parserState.pos
def getParserState : FrontendM Parser.ModuleParserState :=
fun ctx => liftIOCore! $ ctx.parserStateRef.get
def getCommandState : FrontendM Command.State :=
fun ctx => liftIOCore! $ ctx.commandStateRef.get
def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit :=
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 processCommand : FrontendM Bool := do
updateCmdPos;
s ← get;
let cs := s.commandState;
let ps := s.parserState;
cs ← getCommandState;
ps ← getParserState;
c ← read;
match Parser.parseCommand cs.env c ps cs.messages with
match Parser.parseCommand cs.env c.parserCtx ps cs.messages with
| (cmd, ps, messages) => do
set { commandState := { messages := messages, .. cs }, parserState := ps };
setParserState ps;
setMessages messages;
if Parser.isEOI cmd || Parser.isExitCommand cmd then do
pure true -- Done
else do
@ -64,23 +76,33 @@ end Frontend
open Frontend
def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : Environment × MessageLog :=
let fileName := fileName.getD "<input>";
let ctx := Parser.mkParserContextCore env input fileName;
let cmdState := Command.mkState env {} opts;
match (processCommands ctx).run { commandState := cmdState, parserState := {} } with
| (_, { commandState := { env := env, messages := messages, .. }, .. }) => (env, messages)
def IO.processCommands (parserCtx : Parser.ParserContextCore) (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) => unreachable!) $ -- TODO: compiler support for Empty.rec is missing
processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx }
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;
parserStateRef ← IO.mkRef { Parser.ModuleParserState . };
cmdStateRef ← IO.mkRef $ Command.mkState env {} opts;
IO.processCommands parserCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (cmdState.env, cmdState.messages)
def testFrontend (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
env ← mkEmptyEnvironment;
let fileName := fileName.getD "<input>";
let ctx := Parser.mkParserContextCore env input fileName;
match Parser.parseHeader env ctx with
let parserCtx := Parser.mkParserContextCore env input fileName;
match Parser.parseHeader env parserCtx with
| (header, parserState, messages) => do
(env, messages) ← processHeader header messages ctx;
let cmdState := Command.mkState env messages opts;
match (processCommands ctx).run { commandState := cmdState, parserState := parserState } with
| (_, { commandState := { env := env, messages := messages, .. }, .. }) => pure (env, messages)
(env, messages) ← processHeader header messages parserCtx;
parserStateRef ← IO.mkRef parserState;
cmdStateRef ← IO.mkRef $ Command.mkState env messages opts;
IO.processCommands parserCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (cmdState.env, cmdState.messages)
end Elab
end Lean

4
src/Init/System/IO.lean
View file

@ -26,9 +26,9 @@ def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
@[inline] def EIO.adaptExcept {α ε ε'} (f : ε → ε') (x : EIO ε α) : EIO ε' α :=
EStateM.adaptExcept f x
@[inline] def EIO.catchExceptions {ε} (x : EIO ε Unit) (h : ε → EIO Empty Unit) : EIO Empty Unit :=
@[inline] def EIO.catchExceptions {α ε} (x : EIO ε α) (h : ε → EIO Empty α) : EIO Empty α :=
fun s => match x s with
| EStateM.Result.ok _ s => EStateM.Result.ok () s
| EStateM.Result.ok a s => EStateM.Result.ok a s
| EStateM.Result.error ex s => h ex s
instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))

2
tests/lean/run/frontend1.lean
View file

@ -5,7 +5,7 @@ open Lean.Elab
def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
do env ← MetaIO.getEnv;
opts ← MetaIO.getOptions;
let (env, messages) := process input env opts;
(env, messages) ← liftM $ process input env opts;
messages.forM $ fun msg => IO.println msg;
when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");

2
tests/lean/run/termParserAttr.lean
View file

@ -5,7 +5,7 @@ open Lean.Elab
def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
do env ← MetaIO.getEnv;
opts ← MetaIO.getOptions;
let (env, messages) := process input env opts;
(env, messages) ← liftM $ process input env opts;
messages.toList.forM $ fun msg => IO.println msg;
when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");