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

feat: WIP snapshots

Browse source 
Allow interactive editing by only recompiling parts of the file below the edit.
This commit is contained in:
Wojciech Nawrocki 2020-07-15 11:28:49 +02:00 • committed by Leonardo de Moura
parent 0405fde21f
commit e137fa780f
4 changed files with 288 additions and 175 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

132
src/Lean/Data/Lsp/Diagnostics.lean
View file

@ -1,11 +1,121 @@
import Lean.Message
import Lean.Data.Json
import Lean.Data.Lsp.Structure
import Lean.Data.Lsp.Utf16
namespace Lean.Lsp
open Lean
open Lean.Json
inductive DiagnosticSeverity
| error | warning | information | hint
instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticSeverity.error
| some 2 => DiagnosticSeverity.warning
| some 3 => DiagnosticSeverity.information
| some 4 => DiagnosticSeverity.hint
| _ => none⟩
instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity :=
⟨fun o => match o with
| DiagnosticSeverity.error => (1 : Nat)
| DiagnosticSeverity.warning => (2 : Nat)
| DiagnosticSeverity.information => (3 : Nat)
| DiagnosticSeverity.hint => (4 : Nat)⟩
inductive DiagnosticCode
| int (i : Int)
| string (s : String)
instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
⟨fun j => match j with
| num (i : Int) => DiagnosticCode.int i
| str s => DiagnosticCode.string s
| _ => none⟩
instance diagnosticCodeHasToJson : HasToJson DiagnosticCode :=
⟨fun o => match o with
| DiagnosticCode.int i => i
| DiagnosticCode.string s => s⟩
inductive DiagnosticTag
/- Unused or unnecessary code.
Clients are allowed to render diagnostics with this tag faded out instead of having
an error squiggle. -/
| unnecessary
/- Deprecated or obsolete code.
Clients are allowed to rendered diagnostics with this tag strike through. -/
| deprecated
instance diagnosticTagHasFromJson : HasFromJson DiagnosticTag :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticTag.unnecessary
| some 2 => DiagnosticTag.deprecated
| _ => none⟩
instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
⟨fun o => match o with
| DiagnosticTag.unnecessary => (1 : Nat)
| DiagnosticTag.deprecated => (2 : Nat)⟩
/- Represents a related message and source code location for a diagnostic. This should be
used to point to code locations that cause or are related to a diagnostics, e.g when duplicating
a symbol in a scope. -/
structure DiagnosticRelatedInformation :=
(location : Location)
(message : String)
instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation :=
⟨fun j => do
location ← j.getObjValAs? Location "location";
message ← j.getObjValAs? String "message";
pure ⟨location, message⟩⟩
instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation :=
⟨fun o => mkObj $
⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩
structure Diagnostic :=
/- The range at which the message applies. -/
(range : Range)
/- The diagnostic's severity. Can be omitted. If omitted it is up to the
client to interpret diagnostics as error, warning, info or hint. -/
(severity? : Option DiagnosticSeverity := none)
/- The diagnostic's code, which might appear in the user interface. -/
(code? : Option DiagnosticCode := none)
/- A human-readable string describing the source of this
diagnostic, e.g. 'typescript' or 'super lint'. -/
(source? : Option String := none)
/- The diagnostic's message. -/
(message : String)
/- Additional metadata about the diagnostic.
@since 3.15.0 -/
(tags? : Option (Array DiagnosticTag) := none)
/- An array of related diagnostic information, e.g. when symbol-names within
a scope collide all definitions can be marked via this property. -/
(relatedInformation? : Option (Array DiagnosticRelatedInformation) := none)
instance diagnosticHasFromJson : HasFromJson Diagnostic :=
⟨fun j => do
range ← j.getObjValAs? Range "range";
let severity? := j.getObjValAs? DiagnosticSeverity "severity";
let code? := j.getObjValAs? DiagnosticCode "code";
let source? := j.getObjValAs? String "source";
message ← j.getObjValAs? String "message";
let tags? := j.getObjValAs? (Array DiagnosticTag) "tags";
let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation";
pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
instance diagnosticHasToJson : HasToJson Diagnostic :=
⟨fun o => mkObj $
⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++
opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩
structure PublishDiagnosticsParams :=
(uri : DocumentUri)
-- version number of document for which
@ -24,6 +134,26 @@ instance publishDiagnosticsParamsHasToJson : HasToJson PublishDiagnosticsParams
⟨fun o => mkObj $
⟨"uri", toJson o.uri⟩ :: opt "version" o.version? ++ ⟨"diagnostics", toJson o.diagnostics⟩ :: []⟩
/-- Transform a Lean Message into an LSP Diagnostic. -/
def msgToDiagnostic (text : DocumentText) (m : Lean.Message) : Diagnostic :=
-- Lean Message line numbers are 1-based while LSP Positions are 0-based.
let lowLn := m.pos.line - 1;
let low : Lsp.Position := ⟨lowLn, (text.get! lowLn).codepointPosToUtf16Pos m.pos.column⟩;
let high : Lsp.Position := match m.endPos with
| some endPos =>
let highLn := endPos.line - 1;
⟨highLn, (text.get! highLn).codepointPosToUtf16Pos endPos.column⟩
| none => low;
let range : Range := ⟨low, high⟩;
let severity := match m.severity with
| MessageSeverity.information => DiagnosticSeverity.information
| MessageSeverity.warning => DiagnosticSeverity.warning
| MessageSeverity.error => DiagnosticSeverity.error;
let source := "Lean 4 server";
let message := toString (format m.data);
{ range := range
, severity? := severity
, source? := source
, message := message}
end Lean.Lsp

129
src/Lean/Data/Lsp/Structure.lean
View file

@ -5,11 +5,14 @@ namespace Lean.Lsp
open Lean
open Lean.Json
-- all Ints in this file are Floats in LSP
-- all Ints/Nats in this file are Floats in LSP
-- as in http://tools.ietf.org/html/rfc3986
abbrev DocumentUri := String
-- LSP indexes text with rows and colums
abbrev DocumentText := Array String
-- character is accepted liberally: actual character := min(line length, character)
structure Position := (line : Nat) (character : Nat)
@ -19,6 +22,15 @@ instance positionHasFromJson : HasFromJson Position :=
character ← j.getObjValAs? Nat "character";
pure ⟨line, character⟩⟩
namespace Position
/-- Computes a linear position from an LSP-style 0-indexed (ln, col) position
and the text. -/
def lnColToLinearPos (pos : Position) (text : DocumentText) : String.Pos :=
text.foldrRange 0 pos.line (fun ln acc => acc + ln.length + 1) pos.character
end Position
-- [start, end)
structure Range := (start : Position) («end» : Position)
@ -35,70 +47,6 @@ structure LocationLink :=
-- must be a subrange of targetRange
(targetSelectionRange : Range)
inductive DiagnosticSeverity
| error | warning | information | hint
instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticSeverity.error
| some 2 => DiagnosticSeverity.warning
| some 3 => DiagnosticSeverity.information
| some 4 => DiagnosticSeverity.hint
| _ => none⟩
instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity :=
⟨fun o => match o with
| DiagnosticSeverity.error => (1 : Nat)
| DiagnosticSeverity.warning => (2 : Nat)
| DiagnosticSeverity.information => (3 : Nat)
| DiagnosticSeverity.hint => (4 : Nat)⟩
inductive DiagnosticCode
| int (i : Int)
| string (s : String)
instance diagnosticCodeHasToJson : HasToJson DiagnosticCode :=
⟨fun o => match o with
| DiagnosticCode.int i => i
| DiagnosticCode.string s => s⟩
inductive DiagnosticTag
/- Unused or unnecessary code.
Clients are allowed to render diagnostics with this tag faded out instead of having
an error squiggle. -/
| unnecessary
/- Deprecated or obsolete code.
Clients are allowed to rendered diagnostics with this tag strike through. -/
| deprecated
/- Represents a related message and source code location for a diagnostic. This should be
used to point to code locations that cause or are related to a diagnostics, e.g when duplicating
a symbol in a scope. -/
structure DiagnosticRelatedInformation :=
(location : Location)
(message : String)
structure Diagnostic :=
/- The range at which the message applies. -/
(range : Range)
/- The diagnostic's severity. Can be omitted. If omitted it is up to the
client to interpret diagnostics as error, warning, info or hint. -/
(severity? : Option DiagnosticSeverity := none)
/- The diagnostic's code, which might appear in the user interface. -/
(code? : Option DiagnosticCode := none)
/- A human-readable string describing the source of this
diagnostic, e.g. 'typescript' or 'super lint'. -/
(source? : Option String := none)
/- The diagnostic's message. -/
(message : String)
/- Additional metadata about the diagnostic.
@since 3.15.0 -/
(tags? : Option (Array DiagnosticTag) := none)
/- An array of related diagnostic information, e.g. when symbol-names within
a scope collide all definitions can be marked via this property. -/
(relatedInformation? : Option (Array DiagnosticRelatedInformation) := none)
structure Command :=
(title : String)
@ -133,7 +81,7 @@ structure VersionedTextDocumentIdentifier :=
-- increases after each change, undo and redo
-- none used when a document is not open and the
-- disk content is the master
(version? : Option Int := none)
(version? : Option Nat := none)
structure TextDocumentEdit :=
(textDocument : VersionedTextDocumentIdentifier)
@ -150,7 +98,7 @@ structure TextDocumentItem :=
-- when handling more than language
(languageId : String)
-- increases after each change, undo and redo
(version : Int)
(version : Nat)
(text : String)
-- parameter literal for requests
@ -205,46 +153,17 @@ instance locationHasFromJson : HasFromJson Location :=
range ← j.getObjValAs? Range "range";
pure ⟨uri, range⟩⟩
instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
⟨fun j => match j with
| num (i : Int) => DiagnosticCode.int i
| str s => DiagnosticCode.string s
| _ => none⟩
instance diagnosticTagFromJson : HasFromJson DiagnosticTag :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticTag.unnecessary
| some 2 => DiagnosticTag.deprecated
| _ => none⟩
instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation :=
⟨fun j => do
location ← j.getObjValAs? Location "location";
message ← j.getObjValAs? String "message";
pure ⟨location, message⟩⟩
instance diagnosticHasFromJson : HasFromJson Diagnostic :=
⟨fun j => do
range ← j.getObjValAs? Range "range";
let severity? := j.getObjValAs? DiagnosticSeverity "severity";
let code? := j.getObjValAs? DiagnosticCode "code";
let source? := j.getObjValAs? String "source";
message ← j.getObjValAs? String "message";
let tags? := j.getObjValAs? (Array DiagnosticTag) "tags";
let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation";
pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
instance versionedTextDocumentIdentifierHasFromJson : HasFromJson VersionedTextDocumentIdentifier :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
let version? := j.getObjValAs? Int "version";
let version? := j.getObjValAs? Nat "version";
pure ⟨uri, version?⟩⟩
instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
languageId ← j.getObjValAs? String "languageId";
version ← j.getObjValAs? Int "version";
version ← j.getObjValAs? Nat "version";
text ← j.getObjValAs? String "text";
pure ⟨uri, languageId, version, text⟩⟩
@ -276,18 +195,4 @@ instance locationHasToJson : HasToJson Location :=
⟨fun o => mkObj $
⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩
instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
⟨fun o => match o with
| DiagnosticTag.unnecessary => (1 : Nat)
| DiagnosticTag.deprecated => (2 : Nat)⟩
instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation :=
⟨fun o => mkObj $
⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩
instance diagnosticHasToJson : HasToJson Diagnostic :=
⟨fun o => mkObj $
⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++
opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩
end Lean.Lsp

132
src/Lean/Server/Server.lean
View file

@ -2,7 +2,7 @@ import Init.System.IO
import Std.Data.RBMap
import Lean.Environment
import Lean.Elab.Frontend
import Lean.Server.Snapshots
import Lean.Data.Lsp
import Lean.Data.Json.FromToJson
@ -15,16 +15,54 @@ open Lean.JsonRpc
open Lean.Lsp
open Lean.Elab
-- LSP indexes text with rows and colums
abbrev DocumentText := Array String
structure Document :=
(version : Int)
/-- A document editable in the sense that we track the environment
and parser state after each command so that edits can be applied
without recompiling code appearing earlier in the file. -/
structure EditableDocument :=
(version : Nat)
(text : DocumentText)
(headerEnv : Environment)
(headerParserState : Parser.ModuleParserState)
/- The first snapshot is that after the header. -/
(header : Snapshots.Snapshot)
/- Subsequent snapshots occur after each command. -/
-- TODO(WN): These should probably be asynchronous Tasks
(snapshots : List Snapshots.Snapshot)
abbrev DocumentMap := RBMap DocumentUri Document (fun a b => Decidable.decide (a < b))
/-- Compiles the contents of a Lean file. -/
def compileDocument (version : Nat) (contents : String)
: IO (MessageLog × EditableDocument) := do
let inputCtx := Parser.mkInputContext contents "<input>";
emptyEnv ← mkEmptyEnvironment;
let (headerStx, headerParserState, msgLog) := Parser.parseHeader emptyEnv inputCtx;
(headerEnv, msgLog) ← Elab.processHeader headerStx msgLog inputCtx;
let headerSnap : Snapshots.Snapshot := ⟨headerEnv, headerParserState⟩;
(msgLog, cmdSnaps) ← Snapshots.compileCmdsAfter contents msgLog headerSnap;
let docOut : EditableDocument := ⟨version, contents.splitOnEOLs.toArray, headerSnap, cmdSnaps⟩;
pure (msgLog, docOut)
def updateDocument (doc : EditableDocument) (changePos : String.Pos) (newVersion : Nat) (newContents : String)
: IO (MessageLog × EditableDocument) :=
if changePos < doc.header.pos then do -- The header changed, recompile everything.
e ← IO.stderr;
e.putStrLn $ "\nchangePos = " ++ toString changePos;
e.putStrLn "Recompiling header";
compileDocument newVersion newContents
else do
e ← IO.stderr;
e.putStrLn $ "\nchangePos = " ++ toString changePos;
let validSnaps := doc.snapshots.filter (fun snap => snap.pos ≤ changePos);
-- The lowest-in-the-file snapshot which is still valid;
let lastSnap := validSnaps.getLastD doc.header;
e.putStrLn $ "Last snap @ " ++ toString lastSnap.pos;
(msgLog, snaps) ← Snapshots.compileCmdsAfter newContents {} lastSnap;
let newDoc := { version := newVersion
, header := doc.header
, text := newContents.splitOnEOLs.toArray
, snapshots := doc.snapshots ++ snaps : EditableDocument };
pure (msgLog, newDoc)
abbrev DocumentMap :=
RBMap DocumentUri EditableDocument (fun a b => Decidable.decide (a < b))
structure ServerState :=
(i o : FS.Handle)
@ -35,78 +73,44 @@ match @fromJson? paramType _ params with
| some parsed => pure parsed
| none => throw (userError "got param with wrong structure")
def runFrontend (text : String) : IO (Environment × Environment × Parser.ModuleParserState × MessageLog) := do
let inputCtx := Parser.mkInputContext text "<input>";
emptyEnv ← mkEmptyEnvironment;
match Parser.parseHeader emptyEnv inputCtx with
| (headerStx, headerParserState, messages) => do
(headerEnv, messages) ← processHeader headerStx messages inputCtx;
parserStateRef ← IO.mkRef headerParserState;
cmdStateRef ← IO.mkRef $ Command.mkState headerEnv messages {};
IO.processCommands inputCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (headerEnv, cmdState.env, headerParserState, cmdState.messages)
def updateFrontend (doc : Document) (input : String) : IO (Environment × MessageLog) := do
let inputCtx := Parser.mkInputContext input "<input>";
parserStateRef ← IO.mkRef doc.headerParserState;
cmdStateRef ← IO.mkRef $ Command.mkState doc.headerEnv;
IO.processCommands inputCtx parserStateRef cmdStateRef;
cmdState ← cmdStateRef.get;
pure (cmdState.env, cmdState.messages)
def msgToDiagnostic (text : DocumentText) (m : Lean.Message) : Diagnostic :=
-- Lean Message line numbers are 1-based while LSP Positions are 0-based.
let lowLn := m.pos.line - 1;
let low : Lsp.Position := ⟨lowLn, (text.get! lowLn).codepointPosToUtf16Pos m.pos.column⟩;
let high : Lsp.Position := match m.endPos with
| some endPos =>
let highLn := endPos.line - 1;
⟨highLn, (text.get! highLn).codepointPosToUtf16Pos endPos.column⟩
| none => low;
let range : Range := ⟨low, high⟩;
let severity := match m.severity with
| MessageSeverity.information => DiagnosticSeverity.information
| MessageSeverity.warning => DiagnosticSeverity.warning
| MessageSeverity.error => DiagnosticSeverity.error;
let source := "Lean 4 server";
let message := toString (format m.data);
{ range := range
, severity? := severity
, source? := source
, message := message}
-- def ServerM α := StateT ServerState (IO α)
-- Computes a task with result type α in the ServerM monad.
-- def ServerTaskM α := ServerM (Task α)
-- Handles a request with params of type α and response params β.
-- def RequestHandler α β := Request α → ServerTaskM (Response β)
namespace ServerState
def findOpenDocument (s : ServerState) (key : DocumentUri) : IO Document := do
def findOpenDocument (s : ServerState) (key : DocumentUri) : IO EditableDocument := do
openDocuments ← s.openDocumentsRef.get;
match openDocuments.find? key with
| some doc => pure doc
| none => throw (userError "got unknown document uri")
def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : Document) : IO Unit :=
def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : EditableDocument) : IO Unit :=
s.openDocumentsRef.modify (fun documents => (documents.erase key).insert key val)
-- Clears diagnostics for the document version 'd'.
-- Clears diagnostics for the document version 'version'.
-- TODO how to clear all diagnostics? Sending version 'none' doesn't seem to work
def clearDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) : IO Unit :=
-- TODO arg should be versioneddocumentidentifier
def clearDiagnostics (s : ServerState) (uri : DocumentUri) (version : Nat) : IO Unit :=
writeLspNotification s.o "textDocument/publishDiagnostics"
{ uri := uri
, version? := d.version
, version? := version
, diagnostics := #[] : PublishDiagnosticsParams }
def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit :=
let diagnostics := log.msgs.map (msgToDiagnostic d.text);
def sendDiagnostics (s : ServerState) (uri : DocumentUri) (doc : EditableDocument)
(log : MessageLog) : IO Unit :=
let diagnostics := log.msgs.map (msgToDiagnostic doc.text);
writeLspNotification s.o "textDocument/publishDiagnostics"
{ uri := uri
, version? := d.version
, version? := doc.version
, diagnostics := diagnostics.toArray : PublishDiagnosticsParams }
def handleDidOpen (s : ServerState) (p : DidOpenTextDocumentParams) : IO Unit := do
let doc := p.textDocument;
let text := doc.text.splitOnEOLs;
(headerEnv, env, headerParserState, msgLog) ← runFrontend ("\n".intercalate text);
let newDoc : Document := ⟨doc.version, text.toArray, headerEnv, headerParserState⟩;
(msgLog, newDoc) ← compileDocument doc.version doc.text;
s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert doc.uri newDoc);
s.sendDiagnostics doc.uri newDoc msgLog
@ -121,16 +125,20 @@ else changes.forM $ fun change =>
match change with
| TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) => do
let newDocText := replaceRange oldDoc.text range newText;
(newEnv, msgLog) ← updateFrontend oldDoc ("\n".intercalate newDocText.toList);
let newDoc : Document := ⟨newVersion, newDocText, oldDoc.headerEnv, oldDoc.headerParserState⟩;
(msgLog, newDoc) ← updateDocument oldDoc
(range.start.lnColToLinearPos oldDoc.text)
newVersion
("\n".intercalate newDocText.toList);
s.updateOpenDocuments docId.uri newDoc;
-- Clients don't have to clear diagnostics, so we clear them
-- for the *previous* version here.
s.clearDiagnostics docId.uri oldDoc;
s.clearDiagnostics docId.uri oldDoc.version;
-- TODO(WN): at this point we need to re-add the diagnostics for above the
-- part that was recompiled. This should be stored in `Snapshot` probably
s.sendDiagnostics docId.uri newDoc msgLog
| TextDocumentContentChangeEvent.fullChange (text : String) =>
throw (userError "got content change that replaces the full document (not supported)")
throw (userError "TODO impl computing the diff of two sources.")
def handleDidClose (s : ServerState) (p : DidCloseTextDocumentParams) : IO Unit := do
-- TODO is any extra cleanup needed?

70
src/Lean/Server/Snapshots.lean Normal file
View file

@ -0,0 +1,70 @@
import Init.System.IO
import Lean.Elab.Import
import Lean.Elab.Command
/-! One can think of this module as being a partial reimplementation
of Lean.Elab.Frontend which also stores a snapshot of the world after
each command. Importantly, we allow starting compilation from any
snapshot/position in the file for interactive editing purposes. -/
namespace Lean
namespace Elab
namespace Snapshots
/-- What Lean knows about the world after each command. -/
structure Snapshot :=
/- The (ln,col) after the command. *Not* the
same as mpState.pos as that's a linear Nat. -/
--(pos : Position)
(env : Environment)
(mpState : Parser.ModuleParserState)
--(opts : Options) TODO these are set_option options right? might need to store them
def Snapshot.pos (s : Snapshot) : String.Pos := s.mpState.pos
/-- Compiles the next command occuring after the given snapshot.
If there is no next command, returns `none`. -/
-- NOTE(WN): this code is really very similar to Elab.Frontend.
-- Is there a point in generalizing it over "store snapshots"/"don't store snapshots" via
-- changing the FrontendM monad? I say no because it would likely result in
-- confusing isServer? conditionals.
-- TODO(WN): should probably take inputCtx and live in some SnapshotsM := ReaderT Context (EIO Empty)
def compileNextCmd (contents : String) (msgLog : MessageLog) (snap : Snapshot)
: IO (Option (MessageLog × Snapshot)) := do
let inputCtx := Parser.mkInputContext contents "<input>";
let (cmdStx, cmdParserState, msgLog) :=
Parser.parseCommand snap.env inputCtx snap.mpState msgLog;
e ← IO.stderr;
e.putStrLn $ "Cmd @ " ++ toString snap.pos ++ " = " ++ (toString $ cmdStx.formatStx none true);
if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
pure none
else do
cmdStateRef ← IO.mkRef $ Elab.Command.mkState snap.env msgLog { : Options };
let cmdCtx : Elab.Command.Context :=
{ cmdPos := snap.pos
, stateRef := cmdStateRef
, fileName := inputCtx.fileName
, fileMap := inputCtx.fileMap };
EIO.adaptExcept
(fun e => unreachable!) -- TODO(WN): ignoring exceptions ok here?
(Elab.Command.withLogging
(Elab.Command.elabCommand cmdStx)
cmdCtx);
postCmdState ← cmdStateRef.get;
let postCmdSnap : Snapshot := ⟨postCmdState.env, cmdParserState⟩;
pure $ some (postCmdState.messages, postCmdSnap)
partial def compileCmdsAfter (contents : String) : MessageLog → Snapshot
→ IO (MessageLog × List Snapshot)
| msgLog, snap => do
cmdOut ← compileNextCmd contents msgLog snap;
match cmdOut with
| some (msgLog, snap) => do
(msgLog, snaps) ← compileCmdsAfter msgLog snap;
pure (msgLog, snap :: snaps)
| none => pure (msgLog, [])
end Snapshots
end Elab
end Lean