From 4246d98547755d11118f823685b3751ae6f1366a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 30 Aug 2022 18:07:46 +0200 Subject: [PATCH] fix: remove unnecessary `BaseIO` in `AsyncList` --- src/Lean/Server/AsyncList.lean | 38 +++++++++---------- src/Lean/Server/FileWorker.lean | 2 +- .../Server/FileWorker/RequestHandling.lean | 8 ++-- .../Server/FileWorker/WidgetRequests.lean | 2 +- src/Lean/Server/Requests.lean | 6 ++- 5 files changed, 29 insertions(+), 27 deletions(-) diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean index c24cb5a945..72e0fc629d 100644 --- a/src/Lean/Server/AsyncList.lean +++ b/src/Lean/Server/AsyncList.lean @@ -66,31 +66,30 @@ partial def getAll : AsyncList ε α → List α × Option ε | Except.error e => ⟨[], some e⟩ /-- Spawns a `Task` waiting on the prefix of elements for which `p` is true. -/ -partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → BaseIO (Task (List α × Option ε)) - | cons hd tl => do +partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → Task (List α × Option ε) + | cons hd tl => if p hd then - let t ← tl.waitAll p - return t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩ + (tl.waitAll p).map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩ else - return Task.pure ⟨[hd], none⟩ - | nil => return Task.pure ⟨[], none⟩ - | delayed tl => do - BaseIO.bindTask tl fun - | Except.ok tl => tl.waitAll p - | Except.error e => return Task.pure ⟨[], some e⟩ + .pure ⟨[hd], none⟩ + | nil => .pure ⟨[], none⟩ + | delayed tl => + tl.bind fun + | .ok tl => tl.waitAll p + | .error e => .pure ⟨[], some e⟩ /-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution when necessary to traverse the list. If the tail terminates before a matching element is found, the task throws the terminating value. -/ -partial def waitFind? (p : α → Bool) : AsyncList ε α → BaseIO (Task $ Except ε $ Option α) - | nil => return Task.pure <| Except.ok none - | cons hd tl => do - if p hd then return Task.pure <| Except.ok <| some hd +partial def waitFind? (p : α → Bool) : AsyncList ε α → Task (Except ε (Option α)) + | nil => .pure <| .ok none + | cons hd tl => + if p hd then .pure <| Except.ok <| some hd else tl.waitFind? p - | delayed tl => do - BaseIO.bindTask tl fun - | Except.ok tl => tl.waitFind? p - | Except.error e => return Task.pure <| Except.error e + | delayed tl => + tl.bind fun + | .ok tl => tl.waitFind? p + | .error e => .pure <| .error e /-- Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well. -/ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε) @@ -105,7 +104,8 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε | Except.error e => pure ⟨[], some e⟩ else pure ⟨[], none⟩ -def waitHead? (as : AsyncList ε α) : BaseIO (Task (Except ε (Option α))) := as.waitFind? (fun _ => true) +def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) := + as.waitFind? fun _ => true end AsyncList diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index ff33fbcd5a..cf11dfbb0e 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -280,7 +280,7 @@ section Updates let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext let cancelTk ← CancelToken.new -- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths` - let headSnapTask ← oldDoc.cmdSnaps.waitHead? + let headSnapTask := oldDoc.cmdSnaps.waitHead? let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do let headSnap? ← MonadExcept.ofExcept headSnap?? -- There is always at least one snapshot absent exceptions diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 60a6e2b246..046dd113ef 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -254,7 +254,7 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams) : RequestM (RequestTask DocumentSymbolResult) := do let doc ← readDoc -- bad: we have to wait on elaboration of the entire file before we can report document symbols - let t ← doc.cmdSnaps.waitAll + let t := doc.cmdSnaps.waitAll mapTask t fun (snaps, _) => do let mut stxs := snaps.map (·.stx) let (syms, _) := toDocumentSymbols doc.meta.text stxs @@ -331,7 +331,7 @@ partial def handleSemanticTokens (beginPos endPos : String.Pos) : RequestM (RequestTask SemanticTokens) := do let doc ← readDoc let text := doc.meta.text - let t ← doc.cmdSnaps.waitAll (·.beginPos < endPos) + let t := doc.cmdSnaps.waitAll (·.beginPos < endPos) mapTask t fun (snaps, _) => StateT.run' (s := { data := #[], lastLspPos := ⟨0, 0⟩ : SemanticTokensState }) do for s in snaps do @@ -416,7 +416,7 @@ def handleSemanticTokensRange (p : SemanticTokensRangeParams) partial def handleFoldingRange (_ : FoldingRangeParams) : RequestM (RequestTask (Array FoldingRange)) := do let doc ← readDoc - let t ← doc.cmdSnaps.waitAll + let t := doc.cmdSnaps.waitAll mapTask t fun (snaps, _) => do let stxs := snaps.map (·.stx) let (_, ranges) ← StateT.run (addRanges doc.meta.text [] stxs) #[] @@ -491,7 +491,7 @@ partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams) let t ← RequestM.asTask waitLoop RequestM.bindTask t fun doc? => do let doc ← liftExcept doc? - let t₁ ← doc.cmdSnaps.waitAll + let t₁ := doc.cmdSnaps.waitAll return t₁.map fun _ => pure WaitForDiagnostics.mk builtin_initialize diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index 067ea372e1..1978923009 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -98,7 +98,7 @@ def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : Reque let doc ← readDoc let rangeEnd := params.lineRange?.map fun range => doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩ - let t ← doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·) + let t := doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·) pure <| t.map fun (snaps, _) => let diags? := snaps.getLast?.map fun snap => snap.interactiveDiags.toArray.filter fun diag => diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index cf50ff0ab2..0fa4afb48c 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -67,6 +67,8 @@ abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m /-- Workers execute request handlers in this monad. -/ abbrev RequestM := ReaderT RequestContext <| EIO RequestError +abbrev RequestTask.pure (a : α) : RequestTask α := .pure (.ok a) + instance : MonadLift IO RequestM where monadLift x := do match ← x.toBaseIO with @@ -120,7 +122,7 @@ def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool) (notFoundX : RequestM β) (x : Snapshot → RequestM β) : RequestM (RequestTask β) := do - let findTask ← doc.cmdSnaps.waitFind? p + let findTask := doc.cmdSnaps.waitFind? p mapTask findTask <| waitFindSnapAux notFoundX x /-- See `withWaitFindSnap`. -/ @@ -128,7 +130,7 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool) (notFoundX : RequestM (RequestTask β)) (x : Snapshot → RequestM (RequestTask β)) : RequestM (RequestTask β) := do - let findTask ← doc.cmdSnaps.waitFind? p + let findTask := doc.cmdSnaps.waitFind? p bindTask findTask <| waitFindSnapAux notFoundX x /-- Create a task which waits for the snapshot containing `lspPos` and executes `f` with it.