From d8ec900ae9fb4bfac71da1cbaf2d9ada347d45a4 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 6 Jan 2022 16:33:58 +0100
Subject: [PATCH] refactor: use array instead of list in AsyncElabState

---
 src/Lean/Server/FileWorker.lean | 16 ++++++++--------
 src/Lean/Server/References.lean |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 0f85fe8463..584fac7052 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -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
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 544f57740c..5ea4fecc9d 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -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