From e137fa780f0393259c9ebdcdcc4db183e4f3bcd1 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 15 Jul 2020 11:28:49 +0200 Subject: [PATCH] feat: WIP snapshots Allow interactive editing by only recompiling parts of the file below the edit. --- src/Lean/Data/Lsp/Diagnostics.lean | 132 ++++++++++++++++++++++++++++- src/Lean/Data/Lsp/Structure.lean | 129 ++++------------------------ src/Lean/Server/Server.lean | 132 +++++++++++++++-------------- src/Lean/Server/Snapshots.lean | 70 +++++++++++++++ 4 files changed, 288 insertions(+), 175 deletions(-) create mode 100644 src/Lean/Server/Snapshots.lean diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index bb361dd798..627a81665d 100644 --- a/src/Lean/Data/Lsp/Diagnostics.lean +++ b/src/Lean/Data/Lsp/Diagnostics.lean @@ -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 diff --git a/src/Lean/Data/Lsp/Structure.lean b/src/Lean/Data/Lsp/Structure.lean index 0c51482eb7..05ab738626 100644 --- a/src/Lean/Data/Lsp/Structure.lean +++ b/src/Lean/Data/Lsp/Structure.lean @@ -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 diff --git a/src/Lean/Server/Server.lean b/src/Lean/Server/Server.lean index 8bbc3c987c..2f2ddc4555 100644 --- a/src/Lean/Server/Server.lean +++ b/src/Lean/Server/Server.lean @@ -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 ""; +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 ""; -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 ""; -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? diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean new file mode 100644 index 0000000000..8cecd81557 --- /dev/null +++ b/src/Lean/Server/Snapshots.lean @@ -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 ""; +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