refactor: split out Lean.Language.Lean.Types (#4881)
This commit is contained in:
Sebastian Ullrich
GitHub
parent
8acdafd5b3
commit
6a4159c4a7
5 changed files with 122 additions and 104 deletions
|
|
@ -10,8 +10,8 @@ Authors: Sebastian Ullrich
|
|||
|
||||
prelude
|
||||
import Lean.Language.Basic
|
||||
import Lean.Language.Lean.Types
|
||||
import Lean.Parser.Module
|
||||
import Lean.Elab.Command
|
||||
import Lean.Elab.Import
|
||||
|
||||
/-!
|
||||
|
|
@ -166,11 +166,6 @@ namespace Lean.Language.Lean
|
|||
open Lean.Elab Command
|
||||
open Lean.Parser
|
||||
|
||||
private def pushOpt (a? : Option α) (as : Array α) : Array α :=
|
||||
match a? with
|
||||
| some a => as.push a
|
||||
| none => as
|
||||
|
||||
/-- Option for capturing output to stderr during elaboration. -/
|
||||
register_builtin_option stderrAsMessages : Bool := {
|
||||
defValue := true
|
||||
|
|
@ -178,101 +173,6 @@ register_builtin_option stderrAsMessages : Bool := {
|
|||
descr := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
|
||||
}
|
||||
|
||||
/-! The hierarchy of Lean snapshot types -/
|
||||
|
||||
/-- Snapshot after elaboration of the entire command. -/
|
||||
structure CommandFinishedSnapshot extends Language.Snapshot where
|
||||
/-- Resulting elaboration state. -/
|
||||
cmdState : Command.State
|
||||
deriving Nonempty
|
||||
instance : ToSnapshotTree CommandFinishedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
|
||||
|
||||
/-- State after a command has been parsed. -/
|
||||
structure CommandParsedSnapshotData extends Snapshot where
|
||||
/-- Syntax tree of the command. -/
|
||||
stx : Syntax
|
||||
/-- Resulting parser state. -/
|
||||
parserState : Parser.ModuleParserState
|
||||
/--
|
||||
Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
|
||||
elaborator.
|
||||
-/
|
||||
elabSnap : SnapshotTask DynamicSnapshot
|
||||
/-- State after processing is finished. -/
|
||||
finishedSnap : SnapshotTask CommandFinishedSnapshot
|
||||
/-- Cache for `save`; to be replaced with incrementality. -/
|
||||
tacticCache : IO.Ref Tactic.Cache
|
||||
deriving Nonempty
|
||||
|
||||
/-- State after a command has been parsed. -/
|
||||
-- workaround for lack of recursive structures
|
||||
inductive CommandParsedSnapshot where
|
||||
/-- Creates a command parsed snapshot. -/
|
||||
| mk (data : CommandParsedSnapshotData)
|
||||
(nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
|
||||
deriving Nonempty
|
||||
/-- The snapshot data. -/
|
||||
abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
|
||||
| mk data _ => data
|
||||
/-- Next command, unless this is a terminal command. -/
|
||||
abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
|
||||
Option (SnapshotTask CommandParsedSnapshot)
|
||||
| mk _ next? => next?
|
||||
partial instance : ToSnapshotTree CommandParsedSnapshot where
|
||||
toSnapshotTree := go where
|
||||
go s := ⟨s.data.toSnapshot,
|
||||
#[s.data.elabSnap.map (sync := true) toSnapshotTree,
|
||||
s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
|
||||
pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
|
||||
|
||||
/-- State after successful importing. -/
|
||||
structure HeaderProcessedState where
|
||||
/-- The resulting initial elaboration state. -/
|
||||
cmdState : Command.State
|
||||
/-- First command task (there is always at least a terminal command). -/
|
||||
firstCmdSnap : SnapshotTask CommandParsedSnapshot
|
||||
|
||||
/-- State after the module header has been processed including imports. -/
|
||||
structure HeaderProcessedSnapshot extends Snapshot where
|
||||
/-- State after successful importing. -/
|
||||
result? : Option HeaderProcessedState
|
||||
isFatal := result?.isNone
|
||||
instance : ToSnapshotTree HeaderProcessedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot, #[] |>
|
||||
pushOpt (s.result?.map (·.firstCmdSnap.map (sync := true) toSnapshotTree))⟩
|
||||
|
||||
/-- State after successfully parsing the module header. -/
|
||||
structure HeaderParsedState where
|
||||
/-- Resulting parser state. -/
|
||||
parserState : Parser.ModuleParserState
|
||||
/-- Header processing task. -/
|
||||
processedSnap : SnapshotTask HeaderProcessedSnapshot
|
||||
|
||||
/-- State after the module header has been parsed. -/
|
||||
structure HeaderParsedSnapshot extends Snapshot where
|
||||
/-- Parser input context supplied by the driver, stored here for incremental parsing. -/
|
||||
ictx : Parser.InputContext
|
||||
/-- Resulting syntax tree. -/
|
||||
stx : Syntax
|
||||
/-- State after successful parsing. -/
|
||||
result? : Option HeaderParsedState
|
||||
isFatal := result?.isNone
|
||||
/-- Cancellation token for interrupting processing of this run. -/
|
||||
cancelTk? : Option IO.CancelToken
|
||||
|
||||
instance : ToSnapshotTree HeaderParsedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot,
|
||||
#[] |> pushOpt (s.result?.map (·.processedSnap.map (sync := true) toSnapshotTree))⟩
|
||||
|
||||
/-- Shortcut accessor to the final header state, if successful. -/
|
||||
def HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) :
|
||||
SnapshotTask (Option HeaderProcessedState) :=
|
||||
snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.pure none)
|
||||
|
||||
/-- Initial snapshot of the Lean language processor: a "header parsed" snapshot. -/
|
||||
abbrev InitialSnapshot := HeaderParsedSnapshot
|
||||
|
||||
/-- Lean-specific processing context. -/
|
||||
structure LeanProcessingContext extends ProcessingContext where
|
||||
/-- Position of the first file difference if there was a previous invocation. -/
|
||||
|
|
|
|||
119
src/Lean/Language/Lean/Types.lean
Normal file
119
src/Lean/Language/Lean/Types.lean
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
/-
|
||||
Copyright (c) 2023 Lean FRO. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Implementation of the Lean language: parsing and processing of header and commands, incremental
|
||||
recompilation
|
||||
|
||||
Authors: Sebastian Ullrich
|
||||
-/
|
||||
|
||||
prelude
|
||||
import Lean.Language.Basic
|
||||
import Lean.Elab.Command
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
namespace Lean.Language.Lean
|
||||
open Lean.Elab Command
|
||||
open Lean.Parser
|
||||
|
||||
private def pushOpt (a? : Option α) (as : Array α) : Array α :=
|
||||
match a? with
|
||||
| some a => as.push a
|
||||
| none => as
|
||||
|
||||
/-! The hierarchy of Lean snapshot types -/
|
||||
|
||||
/-- Snapshot after elaboration of the entire command. -/
|
||||
structure CommandFinishedSnapshot extends Language.Snapshot where
|
||||
/-- Resulting elaboration state. -/
|
||||
cmdState : Command.State
|
||||
deriving Nonempty
|
||||
instance : ToSnapshotTree CommandFinishedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
|
||||
|
||||
/-- State after a command has been parsed. -/
|
||||
structure CommandParsedSnapshotData extends Snapshot where
|
||||
/-- Syntax tree of the command. -/
|
||||
stx : Syntax
|
||||
/-- Resulting parser state. -/
|
||||
parserState : Parser.ModuleParserState
|
||||
/--
|
||||
Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
|
||||
elaborator.
|
||||
-/
|
||||
elabSnap : SnapshotTask DynamicSnapshot
|
||||
/-- State after processing is finished. -/
|
||||
finishedSnap : SnapshotTask CommandFinishedSnapshot
|
||||
/-- Cache for `save`; to be replaced with incrementality. -/
|
||||
tacticCache : IO.Ref Tactic.Cache
|
||||
deriving Nonempty
|
||||
|
||||
/-- State after a command has been parsed. -/
|
||||
-- workaround for lack of recursive structures
|
||||
inductive CommandParsedSnapshot where
|
||||
/-- Creates a command parsed snapshot. -/
|
||||
| mk (data : CommandParsedSnapshotData)
|
||||
(nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
|
||||
deriving Nonempty
|
||||
/-- The snapshot data. -/
|
||||
abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
|
||||
| mk data _ => data
|
||||
/-- Next command, unless this is a terminal command. -/
|
||||
abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
|
||||
Option (SnapshotTask CommandParsedSnapshot)
|
||||
| mk _ next? => next?
|
||||
partial instance : ToSnapshotTree CommandParsedSnapshot where
|
||||
toSnapshotTree := go where
|
||||
go s := ⟨s.data.toSnapshot,
|
||||
#[s.data.elabSnap.map (sync := true) toSnapshotTree,
|
||||
s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
|
||||
pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
|
||||
|
||||
/-- State after successful importing. -/
|
||||
structure HeaderProcessedState where
|
||||
/-- The resulting initial elaboration state. -/
|
||||
cmdState : Command.State
|
||||
/-- First command task (there is always at least a terminal command). -/
|
||||
firstCmdSnap : SnapshotTask CommandParsedSnapshot
|
||||
|
||||
/-- State after the module header has been processed including imports. -/
|
||||
structure HeaderProcessedSnapshot extends Snapshot where
|
||||
/-- State after successful importing. -/
|
||||
result? : Option HeaderProcessedState
|
||||
isFatal := result?.isNone
|
||||
instance : ToSnapshotTree HeaderProcessedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot, #[] |>
|
||||
pushOpt (s.result?.map (·.firstCmdSnap.map (sync := true) toSnapshotTree))⟩
|
||||
|
||||
/-- State after successfully parsing the module header. -/
|
||||
structure HeaderParsedState where
|
||||
/-- Resulting parser state. -/
|
||||
parserState : Parser.ModuleParserState
|
||||
/-- Header processing task. -/
|
||||
processedSnap : SnapshotTask HeaderProcessedSnapshot
|
||||
|
||||
/-- State after the module header has been parsed. -/
|
||||
structure HeaderParsedSnapshot extends Snapshot where
|
||||
/-- Parser input context supplied by the driver, stored here for incremental parsing. -/
|
||||
ictx : Parser.InputContext
|
||||
/-- Resulting syntax tree. -/
|
||||
stx : Syntax
|
||||
/-- State after successful parsing. -/
|
||||
result? : Option HeaderParsedState
|
||||
isFatal := result?.isNone
|
||||
/-- Cancellation token for interrupting processing of this run. -/
|
||||
cancelTk? : Option IO.CancelToken
|
||||
|
||||
instance : ToSnapshotTree HeaderParsedSnapshot where
|
||||
toSnapshotTree s := ⟨s.toSnapshot,
|
||||
#[] |> pushOpt (s.result?.map (·.processedSnap.map (sync := true) toSnapshotTree))⟩
|
||||
|
||||
/-- Shortcut accessor to the final header state, if successful. -/
|
||||
def HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) :
|
||||
SnapshotTask (Option HeaderProcessedState) :=
|
||||
snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.pure none)
|
||||
|
||||
/-- Initial snapshot of the Lean language processor: a "header parsed" snapshot. -/
|
||||
abbrev InitialSnapshot := HeaderParsedSnapshot
|
||||
|
|
@ -16,7 +16,7 @@ import Lean.Data.Json.FromToJson
|
|||
|
||||
import Lean.Util.FileSetupInfo
|
||||
import Lean.LoadDynlib
|
||||
import Lean.Language.Basic
|
||||
import Lean.Language.Lean
|
||||
|
||||
import Lean.Server.Utils
|
||||
import Lean.Server.AsyncList
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Wojciech Nawrocki, Marc Huisinga
|
||||
-/
|
||||
prelude
|
||||
import Lean.Language.Lean
|
||||
import Lean.Language.Lean.Types
|
||||
import Lean.Server.Utils
|
||||
import Lean.Server.Snapshots
|
||||
import Lean.Server.AsyncList
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ import Init.System.IO
|
|||
|
||||
import Lean.Elab.Import
|
||||
import Lean.Elab.Command
|
||||
import Lean.Language.Lean
|
||||
|
||||
import Lean.Widget.InteractiveDiagnostic
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue