From b30903d1fcae504013d493c8d15f368a62e0e89e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 Nov 2024 16:15:14 +0100 Subject: [PATCH] refactor: make use of recursive structures in snapshot types (#6141) --- src/Lean/Elab/Frontend.lean | 8 +-- src/Lean/Elab/Tactic/Basic.lean | 7 +-- src/Lean/Elab/Tactic/BuiltinTactic.lean | 8 +-- src/Lean/Elab/Tactic/Induction.lean | 5 +- src/Lean/Elab/Term.lean | 11 +--- src/Lean/Language/Lean.lean | 50 ++++++++++--------- src/Lean/Language/Lean/Types.lean | 25 +++------- .../Server/FileWorker/RequestHandling.lean | 4 +- src/Lean/Server/FileWorker/Utils.lean | 6 +-- src/Lean/Server/Requests.lean | 10 ++-- 10 files changed, 59 insertions(+), 75 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 4ceb0e3b4498..d5d15fec1c69 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext) where go initialSnap t commands := let snap := t.get - let commands := commands.push snap.data + let commands := commands.push snap if let some next := snap.nextCmdSnap? then go initialSnap next.task commands else @@ -115,9 +115,9 @@ where -- snapshots as they subsume any info trees reported incrementally by their children. let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray' return { - commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees } - parserState := snap.data.parserState - cmdPos := snap.data.parserState.pos + commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees } + parserState := snap.parserState + cmdPos := snap.parserState.pos commands := commands.map (·.stx) inputCtx, initialSnap } diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 67cc91c88dcd..067513b70a00 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -218,7 +218,7 @@ where let old ← snap.old? -- If the kind is equal, we can assume the old version was a macro as well guard <| old.stx.isOfKind stx.getKind - let state ← old.val.get.data.finished.get.state? + let state ← old.val.get.finished.get.state? guard <| state.term.meta.core.nextMacroScope == nextMacroScope -- check absence of traces; see Note [Incremental Macros] guard <| state.term.meta.core.traceState.traces.size == 0 @@ -226,9 +226,10 @@ where return old.val.get Language.withAlwaysResolvedPromise fun promise => do -- Store new unfolding in the snapshot tree - snap.new.resolve <| .mk { + snap.new.resolve { stx := stx' diagnostics := .empty + inner? := none finished := .pure { diagnostics := .empty state? := (← Tactic.saveState) @@ -240,7 +241,7 @@ where new := promise old? := do let old ← old? - return ⟨old.data.stx, (← old.data.next.get? 0)⟩ + return ⟨old.stx, (← old.next.get? 0)⟩ } }) do evalTactic stx' return diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 920388bfa69c..aa02a0f84903 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -60,7 +60,7 @@ where if let some snap := (← readThe Term.Context).tacSnap? then if let some old := snap.old? then let oldParsed := old.val.get - oldInner? := oldParsed.data.inner? |>.map (⟨oldParsed.data.stx, ·⟩) + oldInner? := oldParsed.inner? |>.map (⟨oldParsed.stx, ·⟩) -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do let some snap := (← readThe Term.Context).tacSnap? @@ -70,10 +70,10 @@ where if let some old := snap.old? then -- `tac` must be unchanged given the narrow above; let's reuse `finished`'s state! let oldParsed := old.val.get - if let some state := oldParsed.data.finished.get.state? then + if let some state := oldParsed.finished.get.state? then reusableResult? := some ((), state) -- only allow `next` reuse in this case - oldNext? := oldParsed.data.next.get? 0 |>.map (⟨old.stx, ·⟩) + oldNext? := oldParsed.next.get? 0 |>.map (⟨old.stx, ·⟩) -- For `tac`'s snapshot task range, disregard synthetic info as otherwise -- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when @@ -89,7 +89,7 @@ where withAlwaysResolvedPromise fun next => do withAlwaysResolvedPromise fun finished => do withAlwaysResolvedPromise fun inner => do - snap.new.resolve <| .mk { + snap.new.resolve { desc := tac.getKind.toString diagnostics := .empty stx := tac diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 43cf7134ab1a..c086d40be32a 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -282,10 +282,11 @@ where -- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx` withAlwaysResolvedPromise fun finished => do withAlwaysResolvedPromises altStxs.size fun altPromises => do - tacSnap.new.resolve <| .mk { + tacSnap.new.resolve { -- save all relevant syntax here for comparison with next document version stx := mkNullNode altStxs diagnostics := .empty + inner? := none finished := { range? := none, task := finished.result } next := altStxs.zipWith altPromises fun stx prom => { range? := stx.getRange?, task := prom.result } @@ -298,7 +299,7 @@ where let old := old.val.get -- use old version of `mkNullNode altsSyntax` as guard, will be compared with new -- version and picked apart in `applyAltStx` - return ⟨old.data.stx, (← old.data.next[i]?)⟩ + return ⟨old.stx, (← old.next[i]?)⟩ new := prom } finished.resolve { diagnostics := .empty, state? := (← saveState) } diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 97f2873d512f..d375462ba75f 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -230,7 +230,7 @@ instance : ToSnapshotTree TacticFinishedSnapshot where toSnapshotTree s := ⟨s.toSnapshot, #[]⟩ /-- Snapshot just before execution of a tactic. -/ -structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Language.Snapshot where +structure TacticParsedSnapshot extends Language.Snapshot where /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/ stx : Syntax /-- Task for nested incrementality, if enabled for tactic. -/ @@ -240,16 +240,9 @@ structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Languag /-- Tasks for subsequent, potentially parallel, tactic steps. -/ next : Array (SnapshotTask TacticParsedSnapshot) := #[] deriving Inhabited - -/-- State after execution of a single synchronous tactic step. -/ -inductive TacticParsedSnapshot where - | mk (data : TacticParsedSnapshotData TacticParsedSnapshot) -deriving Inhabited -abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData TacticParsedSnapshot - | .mk data => data partial instance : ToSnapshotTree TacticParsedSnapshot where toSnapshotTree := go where - go := fun ⟨s⟩ => ⟨s.toSnapshot, + go := fun s => ⟨s.toSnapshot, s.inner?.toArray.map (·.map (sync := true) go) ++ #[s.finished.map (sync := true) toSnapshotTree] ++ s.next.map (·.map (sync := true) go)⟩ diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 90b2f9a3a983..a411ffafe501 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -348,7 +348,7 @@ where if let some (some processed) ← old.processedResult.get? then -- ...and the edit location is after the next command (see note [Incremental Parsing])... if let some nextCom ← processed.firstCmdSnap.get? then - if (← isBeforeEditPos nextCom.data.parserState.pos) then + if (← isBeforeEditPos nextCom.parserState.pos) then -- ...go immediately to next snapshot return (← unchanged old old.stx oldSuccess.parserState) @@ -470,20 +470,20 @@ where -- from `old` if let some oldNext := old.nextCmdSnap? then do let newProm ← IO.Promise.new - let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished => + let _ ← old.finishedSnap.bindIO (sync := true) fun oldFinished => -- also wait on old command parse snapshot as parsing is cheap and may allow for -- elaboration reuse oldNext.bindIO (sync := true) fun oldNext => do parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx return .pure () - prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result }) + prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result } } else prom.resolve old -- terminal command, we're done! -- fast path, do not even start new task for this snapshot if let some old := old? then if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then - if (← isBeforeEditPos nextCom.data.parserState.pos) then - return (← unchanged old old.data.parserState) + if (← isBeforeEditPos nextCom.parserState.pos) then + return (← unchanged old old.parserState) let beginPos := parserState.pos let scope := cmdState.scopes.head! @@ -500,7 +500,7 @@ where -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if -- only that whitespace changes, which is wasteful but still necessary because it may -- influence the range of error messages such as from a trailing `exact` - if stx.eqWithInfo old.data.stx then + if stx.eqWithInfo old.stx then -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged` return (← unchanged old parserState) -- on first change, make sure to cancel old invocation @@ -515,11 +515,12 @@ where -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation -- (as no-one should look at this result in that case) but anything containing `Environment` -- is not `Inhabited` - prom.resolve <| .mk (nextCmdSnap? := none) { + prom.resolve <| { diagnostics := .empty, stx := .missing, parserState elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf } finishedSnap := .pure { diagnostics := .empty, cmdState } tacticCache := (← IO.mkRef {}) + nextCmdSnap? := none } return @@ -537,29 +538,30 @@ where -- irrelevant in this case. let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩ let finishedSnap := { range? := endRange?, task := finishedPromise.result } - let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {}) + let tacticCache ← old?.map (·.tacticCache) |>.getDM (IO.mkRef {}) let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts let next? ← if Parser.isTerminalCommand stx then pure none -- for now, wait on "command finished" snapshot before parsing next command else some <$> IO.Promise.new + let nextCmdSnap? := next?.map + ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result }) let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog - let data := if minimalSnapshots && !Parser.isTerminalCommand stx then { - diagnostics - stx := .missing - parserState := {} - elabSnap := { range? := stx.getRange?, task := elabPromise.result } - finishedSnap - tacticCache - } else { - diagnostics, stx, parserState, tacticCache - elabSnap := { range? := stx.getRange?, task := elabPromise.result } - finishedSnap - } - prom.resolve <| .mk (nextCmdSnap? := next?.map - ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data + if minimalSnapshots && !Parser.isTerminalCommand stx then + prom.resolve { + diagnostics, finishedSnap, tacticCache, nextCmdSnap? + stx := .missing + parserState := {} + elabSnap := { range? := stx.getRange?, task := elabPromise.result } + } + else + prom.resolve { + diagnostics, stx, parserState, tacticCache, nextCmdSnap? + elabSnap := { range? := stx.getRange?, task := elabPromise.result } + finishedSnap + } let cmdState ← doElab stx cmdState beginPos - { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise } + { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise } finishedPromise tacticCache ctx if let some next := next? then -- We're definitely off the fast-forwarding path now @@ -645,6 +647,6 @@ where goCmd snap := if let some next := snap.nextCmdSnap? then goCmd next.get else - snap.data.finishedSnap.get.cmdState + snap.finishedSnap.get.cmdState end Lean diff --git a/src/Lean/Language/Lean/Types.lean b/src/Lean/Language/Lean/Types.lean index 7c1ec9d984dd..1f40dafc12c0 100644 --- a/src/Lean/Language/Lean/Types.lean +++ b/src/Lean/Language/Lean/Types.lean @@ -34,7 +34,7 @@ instance : ToSnapshotTree CommandFinishedSnapshot where toSnapshotTree s := ⟨s.toSnapshot, #[]⟩ /-- State after a command has been parsed. -/ -structure CommandParsedSnapshotData extends Snapshot where +structure CommandParsedSnapshot extends Snapshot where /-- Syntax tree of the command. -/ stx : Syntax /-- Resulting parser state. -/ @@ -48,27 +48,14 @@ structure CommandParsedSnapshotData extends Snapshot where finishedSnap : SnapshotTask CommandFinishedSnapshot /-- Cache for `save`; to be replaced with incrementality. -/ tacticCache : IO.Ref Tactic.Cache + /-- Next command, unless this is a terminal command. -/ + nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot) 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] |> + go s := ⟨s.toSnapshot, + #[s.elabSnap.map (sync := true) toSnapshotTree, + s.finishedSnap.map (sync := true) toSnapshotTree] |> pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩ /-- State after successful importing. -/ diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 424b475ad287..ab0afc5e18c8 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -33,9 +33,9 @@ def findCompletionCmdDataAtPos (pos : String.Pos) : Task (Option (Syntax × Elab.InfoTree)) := findCmdDataAtPos doc (pos := pos) fun s => Id.run do - let some tailPos := s.data.stx.getTailPos? + let some tailPos := s.stx.getTailPos? | return false - return pos.byteIdx <= tailPos.byteIdx + s.data.stx.getTrailingSize + return pos.byteIdx <= tailPos.byteIdx + s.stx.getTrailingSize def handleCompletion (p : CompletionParams) : RequestM (RequestTask CompletionList) := do diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index 8a85c1e7ee8c..c080813cf6d1 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -28,10 +28,10 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) : } <| .delayed <| headerSuccess.firstCmdSnap.task.bind go where go cmdParsed := - cmdParsed.data.finishedSnap.task.map fun finished => + cmdParsed.finishedSnap.task.map fun finished => .ok <| .cons { - stx := cmdParsed.data.stx - mpState := cmdParsed.data.parserState + stx := cmdParsed.stx + mpState := cmdParsed.parserState cmdState := finished.cmdState } (match cmdParsed.nextCmdSnap? with | some next => .delayed <| next.task.bind go diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 44dfbc88d333..e57fd94ce477 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -204,7 +204,7 @@ partial def findInfoTreeAtPos findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun | some infoTree => .pure <| some infoTree - | none => cmdParsed.data.finishedSnap.task.map (sync := true) fun s => + | none => cmdParsed.finishedSnap.task.map (sync := true) fun s => -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command assert! s.cmdState.infoState.trees.size == 1 some s.cmdState.infoState.trees[0]! @@ -225,11 +225,11 @@ def findCmdDataAtPos : Task (Option (Syntax × Elab.InfoTree)) := findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun - | some infoTree => .pure <| some (cmdParsed.data.stx, infoTree) - | none => cmdParsed.data.finishedSnap.task.map (sync := true) fun s => + | some infoTree => .pure <| some (cmdParsed.stx, infoTree) + | none => cmdParsed.finishedSnap.task.map (sync := true) fun s => -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command assert! s.cmdState.infoState.trees.size == 1 - some (cmdParsed.data.stx, s.cmdState.infoState.trees[0]!) + some (cmdParsed.stx, s.cmdState.infoState.trees[0]!) | none => .pure none /-- @@ -244,7 +244,7 @@ def findInfoTreeAtPosWithTrailingWhitespace : Task (Option Elab.InfoTree) := -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on -- the first character of the subsequent command if any) - findInfoTreeAtPos doc (·.data.parserState.pos ≥ pos) pos + findInfoTreeAtPos doc (·.parserState.pos ≥ pos) pos open Elab.Command in def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do