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

refactor: use array instead of list in AsyncElabState

Browse source
This commit is contained in:
Joscha 2022-01-06 16:33:58 +01:00 • committed by Sebastian Ullrich
parent ab52480b69
commit d8ec900ae9
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Server/FileWorker.lean
View file

@ -67,16 +67,16 @@ structure WorkerContext where
section Elab
structure AsyncElabState where
headerSnap : Snapshot
snaps : List Snapshot
snaps : Array Snapshot
private def AsyncElabState.lastSnap (s : AsyncElabState) : Snapshot :=
s.snaps.getLastD s.headerSnap
s.snaps.getD (s.snaps.size - 1) s.headerSnap
abbrev AsyncElabM := StateT AsyncElabState $ ExceptT ElabTaskError IO
-- Placed here instead of Lean.Server.Utils because of an import loop
private def publishReferences (m : DocumentMeta) (s : AsyncElabState) (hOut : FS.Stream) : IO Unit := do
let trees := (s.headerSnap :: s.snaps).map fun snap => snap.infoTree
let trees := (s.snaps.insertAt 0 s.headerSnap).map fun snap => snap.infoTree
let references := findModuleRefs m.text trees (localVars := true)
hOut.writeLspNotification {
method := "$/lean/ileanInfo"
@ -96,7 +96,7 @@ section Elab
return none
publishProgressAtPos m lastSnap.endPos ctx.hOut
let snap ← compileNextCmd m.text lastSnap
set { s with snaps := s.snaps.append [snap] }
set { s with snaps := s.snaps.push snap }
-- TODO(MH): check for interrupt with increased precision
cancelTk.check
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
@ -116,7 +116,7 @@ section Elab
/-- Elaborates all commands after the last snap (using `headerSnap` if `snaps`
is empty), emitting the diagnostics into `hOut`. -/
def unfoldCmdSnaps (m : DocumentMeta) (headerSnap : Snapshot) (snaps : List Snapshot) (cancelTk : CancelToken)
def unfoldCmdSnaps (m : DocumentMeta) (headerSnap : Snapshot) (snaps : Array Snapshot) (cancelTk : CancelToken)
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
if snaps.isEmpty && headerSnap.msgLog.hasErrors then
-- Treat header processing errors as fatal so users aren't swamped with
@ -242,7 +242,7 @@ section Initialization
srcSearchPath := srcSearchPath
initParams := initParams
}
let cmdSnaps ← unfoldCmdSnaps meta headerSnap [] cancelTk ctx
let cmdSnaps ← unfoldCmdSnaps meta headerSnap #[] cancelTk ctx
let doc : EditableDocument := ⟨meta, headerSnap, cmdSnaps, cancelTk⟩
return (ctx,
{ doc := doc
@ -280,7 +280,7 @@ section Updates
let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos)
if validSnaps.length = 0 then
let cancelTk ← CancelToken.new
let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap [] cancelTk ctx
let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap #[] cancelTk ctx
modify fun st => { st with doc := ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩ }
else
/- When at least one valid non-header snap exists, it may happen that a change does not fall
@ -296,7 +296,7 @@ section Updates
if newLastStx != lastSnap.stx then
validSnaps ← validSnaps.dropLast
let cancelTk ← CancelToken.new
let newSnaps ← unfoldCmdSnaps newMeta newHeaderSnap validSnaps cancelTk ctx
let newSnaps ← unfoldCmdSnaps newMeta newHeaderSnap validSnaps.toArray cancelTk ctx
let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps
modify fun st => { st with doc := ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩ }
end Updates

4
src/Lean/Server/References.lean
View file

@ -99,7 +99,7 @@ def identOf : Info → Option (RefIdent × Bool)
| Info.ofFieldInfo fi => some (RefIdent.const fi.projName, false)
| _ => none
def findReferences (text : FileMap) (trees : List InfoTree) : Array Reference := Id.run do
def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference := Id.run do
let mut refs := #[]
for tree in trees do
refs := refs.appendList <| tree.deepestNodes fun _ info _ => Id.run do
@ -146,7 +146,7 @@ where
| m, RefIdent.fvar id => RefIdent.fvar <| m.findD id id
| _, ident => ident
def findModuleRefs (text : FileMap) (trees : List InfoTree) (localVars : Bool := true)
def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool := true)
: ModuleRefs := Id.run do
let mut refs := combineFvars <| findReferences text trees
if !localVars then