From f9e5f1f1fd7bcc0edb9f7af29b5a4529dfafb393 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 25 Jan 2024 15:43:23 +0100 Subject: [PATCH] feat: add call hierarchy support (#3082) This PR adds support for the "call hierarchy" feature of LSP that allows quickly navigating both inbound and outbound call sites of functions. In this PR, "call" is taken to mean "usage", so inbound and outbound references of all kinds of identifiers (e.g. functions or types) can be navigated. To implement the call hierarchy feature, this PR implements the LSP requests `textDocument/prepareCallHierarchy`, `callHierarchy/incomingCalls` and `callHierarchy/outgoingCalls`.
Showing the call hierarchy (click to show image) ![show_call_hierarchy](https://github.com/leanprover/lean4/assets/10852073/add13943-013c-4d0a-a2d4-a7c57ad2ae26)
Incoming calls (click to show image) ![incoming_calls](https://github.com/leanprover/lean4/assets/10852073/9a803cb4-6690-42b4-9c5c-f301f76367a7)
Outgoing calls (click to show image) ![outgoing_calls](https://github.com/leanprover/lean4/assets/10852073/a7c4f193-51ab-4365-9473-0309319b1cfe)
It is based on #3159, which should be merged before this PR. To route the parent declaration name through to the language server, the `.ilean` format is adjusted, breaking backwards compatibility with version 1 of the ILean format and yielding version 2. This PR also makes the following more minor adjustments: - `Lean.Server.findModuleRefs` now also combines the identifiers of constants and FVars and prefers constant over FVars for the combined identifier. This is necessary because e.g. declarations declared using `where` yield both a constant (for usage outside of the function) and an FVar (for usage inside of the function) with the same range, whereas we would typically like all references to refer to the former. This also fixes a bug introduced in #2462 where renaming a declaration declared using `where` would not rename usages outside of the function, as well as a bug in the unused variable linter where `where` declarations would be reported as unused even if they were being used outside of the function. - The function converting `Lean.Server.RefInfo` to `Lean.Lsp.RefInfo` now also computes the `Lean.DeclarationRanges` for parent declaration names via `MetaM` and must hence be in `IO` now. - Add a utility function `Array.groupByKey` to `HashMap.lean`. - Stylistic refactoring of `Watchdog.lean` and `LanguageFeatures.lean`. --- RELEASES.md | 4 +- src/Lean/Data/HashMap.lean | 14 + src/Lean/Data/Lsp/Capabilities.lean | 1 + src/Lean/Data/Lsp/Internal.lean | 100 +++++- src/Lean/Data/Lsp/LanguageFeatures.lean | 179 +++++++--- src/Lean/Data/Lsp/Utf16.lean | 11 + src/Lean/Elab/Frontend.lean | 2 +- src/Lean/Server/FileWorker.lean | 2 +- .../Server/FileWorker/RequestHandling.lean | 18 +- src/Lean/Server/GoTo.lean | 7 +- src/Lean/Server/References.lean | 185 ++++++---- src/Lean/Server/Watchdog.lean | 331 ++++++++++++++---- tests/lean/linterUnusedVariables.lean | 4 +- .../linterUnusedVariables.lean.expected.out | 2 - 14 files changed, 633 insertions(+), 227 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 5a022f1e17e7..6cf6384ed1b1 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -192,7 +192,9 @@ example : x + foo 2 = 12 + x := by ought to be applied to multiple functions, the `decreasing_by` clause has to be repeated at each of these functions. -* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See https://github.com/leanprover/lean4/pull/3159 for how to migrate your code. +* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See [PR #3159](https://github.com/leanprover/lean4/pull/3159) for how to migrate your code. + +* Add language server support for [call hierarchy requests](https://devblogs.microsoft.com/cppblog/c-extension-in-vs-code-1-16-release-call-hierarchy-more/) ([PR #3082](https://github.com/leanprover/lean4/pull/3082)). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again. v4.5.0 diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index 59c5bd8c6b77..4ff2087f5c70 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -227,3 +227,17 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β := match m.find? p.fst with | none => m.insert p.fst p.snd | some v => m.insert p.fst $ f v p.snd) +end Lean.HashMap + +/-- +Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array +`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`. +-/ +def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β) + : Lean.HashMap α (Array β) := Id.run do + let mut groups := ∅ + for x in xs do + let group := groups.findD (key x) #[] + groups := groups.erase (key x) -- make `group` referentially unique + groups := groups.insert (key x) (group.push x) + return groups diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index 4cb723969dc1..02e5e94f6e05 100644 --- a/src/Lean/Data/Lsp/Capabilities.lean +++ b/src/Lean/Data/Lsp/Capabilities.lean @@ -74,6 +74,7 @@ structure ServerCapabilities where declarationProvider : Bool := false typeDefinitionProvider : Bool := false referencesProvider : Bool := false + callHierarchyProvider : Bool := false renameProvider? : Option RenameOptions := none workspaceSymbolProvider : Bool := false foldingRangeProvider : Bool := false diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index 37c5fb9af37d..0112a6ead0a0 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -8,6 +8,8 @@ Authors: Joscha Mennicken import Lean.Expr import Lean.Data.Lsp.Basic +set_option linter.missingDocs true -- keep it documented + /-! This file contains types for communication between the watchdog and the workers. These messages are not visible externally to users of the LSP server. -/ @@ -17,17 +19,27 @@ namespace Lean.Lsp /-! Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON. -/ +/-- +Identifier of a reference. +-/ inductive RefIdent where + /-- Named identifier. These are used in all references that are globally available. -/ | const : Name → RefIdent - | fvar : FVarId → RefIdent + /-- Unnamed identifier. These are used for all local references. -/ + | fvar : FVarId → RefIdent deriving BEq, Hashable, Inhabited namespace RefIdent +/-- Converts the reference identifier to a string by prefixing it with a symbol. -/ def toString : RefIdent → String | RefIdent.const n => s!"c:{n}" | RefIdent.fvar id => s!"f:{id.name}" +/-- +Converts the string representation of a reference identifier back to a reference identifier. +The string representation must have been created by `RefIdent.toString`. +-/ def fromString (s : String) : Except String RefIdent := do let sPrefix := s.take 2 let sName := s.drop 2 @@ -43,33 +55,92 @@ def fromString (s : String) : Except String RefIdent := do | "f:" => return RefIdent.fvar <| FVarId.mk name | _ => throw "string must start with 'c:' or 'f:'" +instance : FromJson RefIdent where + fromJson? + | (s : String) => fromString s + | j => Except.error s!"expected a String, got {j}" + +instance : ToJson RefIdent where + toJson ident := toString ident + end RefIdent +/-- Information about the declaration surrounding a reference. -/ +structure RefInfo.ParentDecl where + /-- Name of the declaration surrounding a reference. -/ + name : Name + /-- Range of the declaration surrounding a reference. -/ + range : Lsp.Range + /-- Selection range of the declaration surrounding a reference. -/ + selectionRange : Lsp.Range + deriving ToJson + +/-- +Denotes the range of a reference, as well as the parent declaration of the reference. +If the reference is itself a declaration, then it contains no parent declaration. +-/ +structure RefInfo.Location where + /-- Range of the reference. -/ + range : Lsp.Range + /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/ + parentDecl? : Option RefInfo.ParentDecl + +/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/ structure RefInfo where - definition : Option Lsp.Range - usages : Array Lsp.Range + /-- Definition site of the reference. May be `none` when we cannot find a definition site. -/ + definition? : Option RefInfo.Location + /-- Usage sites of the reference. -/ + usages : Array RefInfo.Location instance : ToJson RefInfo where toJson i := let rangeToList (r : Lsp.Range) : List Nat := [r.start.line, r.start.character, r.end.line, r.end.character] + let parentDeclToList (d : RefInfo.ParentDecl) : List Json := + let name := d.name.toString |> toJson + let range := rangeToList d.range |>.map toJson + let selectionRange := rangeToList d.selectionRange |>.map toJson + [name] ++ range ++ selectionRange + let locationToList (l : RefInfo.Location) : List Json := + let range := rangeToList l.range |>.map toJson + let parentDecl := l.parentDecl?.map parentDeclToList |>.getD [] + range ++ parentDecl Json.mkObj [ - ("definition", toJson $ i.definition.map rangeToList), - ("usages", toJson $ i.usages.map rangeToList) + ("definition", toJson $ i.definition?.map locationToList), + ("usages", toJson $ i.usages.map locationToList) ] instance : FromJson RefInfo where fromJson? j := do - let listToRange (l : List Nat) : Except String Lsp.Range := match l with + let toRange : List Nat → Except String Lsp.Range | [sLine, sChar, eLine, eChar] => pure ⟨⟨sLine, sChar⟩, ⟨eLine, eChar⟩⟩ - | _ => throw s!"Expected list of length 4, not {l.length}" - let definition ← j.getObjValAs? (Option $ List Nat) "definition" - let definition ← match definition with + | l => throw s!"Expected list of length 4, not {l.length}" + let toParentDecl (a : Array Json) : Except String RefInfo.ParentDecl := do + let name := String.toName <| ← fromJson? a[0]! + let range ← a[1:5].toArray.toList |>.mapM fromJson? + let range ← toRange range + let selectionRange ← a[5:].toArray.toList |>.mapM fromJson? + let selectionRange ← toRange selectionRange + return ⟨name, range, selectionRange⟩ + let toLocation (l : List Json) : Except String RefInfo.Location := do + let l := l.toArray + if l.size != 4 && l.size != 13 then + .error "Expected list of length 4 or 13, not {l.size}" + let range ← l[:4].toArray.toList |>.mapM fromJson? + let range ← toRange range + if l.size == 13 then + let parentDecl ← toParentDecl l[4:].toArray + return ⟨range, parentDecl⟩ + else + return ⟨range, none⟩ + + let definition? ← j.getObjValAs? (Option $ List Json) "definition" + let definition? ← match definition? with | none => pure none - | some list => some <$> listToRange list - let usages ← j.getObjValAs? (Array $ List Nat) "usages" - let usages ← usages.mapM listToRange - pure { definition, usages } + | some list => some <$> toLocation list + let usages ← j.getObjValAs? (Array $ List Json) "usages" + let usages ← usages.mapM toLocation + pure { definition?, usages } /-- References from a single module/file -/ def ModuleRefs := HashMap RefIdent RefInfo @@ -88,7 +159,8 @@ instance : FromJson ModuleRefs where Contains the file's definitions and references. -/ structure LeanIleanInfoParams where /-- Version of the file these references are from. -/ - version : Nat + version : Nat + /-- All references for the file. -/ references : ModuleRefs deriving FromJson, ToJson diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 99fdcd5c5f99..cf66da7d523f 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -36,16 +36,16 @@ instance : FromJson CompletionItemKind where structure InsertReplaceEdit where newText : String - insert : Range + insert : Range replace : Range deriving FromJson, ToJson structure CompletionItem where - label : String - detail? : Option String := none + label : String + detail? : Option String := none documentation? : Option MarkupContent := none - kind? : Option CompletionItemKind := none - textEdit? : Option InsertReplaceEdit := none + kind? : Option CompletionItemKind := none + textEdit? : Option InsertReplaceEdit := none /- tags? : CompletionItemTag[] deprecated? : boolean @@ -63,7 +63,7 @@ structure CompletionItem where structure CompletionList where isIncomplete : Bool - items : Array CompletionItem + items : Array CompletionItem deriving FromJson, ToJson structure CompletionParams extends TextDocumentPositionParams where @@ -74,7 +74,7 @@ structure Hover where /- NOTE we should also accept MarkedString/MarkedString[] here but they are deprecated, so maybe can get away without. -/ contents : MarkupContent - range? : Option Range := none + range? : Option Range := none deriving ToJson, FromJson structure HoverParams extends TextDocumentPositionParams @@ -153,45 +153,76 @@ inductive SymbolKind where | event | operator | typeParameter + deriving BEq, Hashable, Inhabited + +instance : FromJson SymbolKind where + fromJson? + | 1 => .ok .file + | 2 => .ok .module + | 3 => .ok .namespace + | 4 => .ok .package + | 5 => .ok .class + | 6 => .ok .method + | 7 => .ok .property + | 8 => .ok .field + | 9 => .ok .constructor + | 10 => .ok .enum + | 11 => .ok .interface + | 12 => .ok .function + | 13 => .ok .variable + | 14 => .ok .constant + | 15 => .ok .string + | 16 => .ok .number + | 17 => .ok .boolean + | 18 => .ok .array + | 19 => .ok .object + | 20 => .ok .key + | 21 => .ok .null + | 22 => .ok .enumMember + | 23 => .ok .struct + | 24 => .ok .event + | 25 => .ok .operator + | 26 => .ok .typeParameter + | j => .error s!"invalid symbol kind {j}" instance : ToJson SymbolKind where - toJson - | SymbolKind.file => 1 - | SymbolKind.module => 2 - | SymbolKind.namespace => 3 - | SymbolKind.package => 4 - | SymbolKind.class => 5 - | SymbolKind.method => 6 - | SymbolKind.property => 7 - | SymbolKind.field => 8 - | SymbolKind.constructor => 9 - | SymbolKind.enum => 10 - | SymbolKind.interface => 11 - | SymbolKind.function => 12 - | SymbolKind.variable => 13 - | SymbolKind.constant => 14 - | SymbolKind.string => 15 - | SymbolKind.number => 16 - | SymbolKind.boolean => 17 - | SymbolKind.array => 18 - | SymbolKind.object => 19 - | SymbolKind.key => 20 - | SymbolKind.null => 21 - | SymbolKind.enumMember => 22 - | SymbolKind.struct => 23 - | SymbolKind.event => 24 - | SymbolKind.operator => 25 - | SymbolKind.typeParameter => 26 + toJson + | .file => 1 + | .module => 2 + | .namespace => 3 + | .package => 4 + | .class => 5 + | .method => 6 + | .property => 7 + | .field => 8 + | .constructor => 9 + | .enum => 10 + | .interface => 11 + | .function => 12 + | .variable => 13 + | .constant => 14 + | .string => 15 + | .number => 16 + | .boolean => 17 + | .array => 18 + | .object => 19 + | .key => 20 + | .null => 21 + | .enumMember => 22 + | .struct => 23 + | .event => 24 + | .operator => 25 + | .typeParameter => 26 structure DocumentSymbolAux (Self : Type) where - name : String - detail? : Option String := none - kind : SymbolKind + name : String + detail? : Option String := none + kind : SymbolKind -- tags? : Array SymbolTag - range : Range + range : Range selectionRange : Range - children? : Option (Array Self) := none - deriving ToJson + children? : Option (Array Self) := none + deriving FromJson, ToJson inductive DocumentSymbol where | mk (sym : DocumentSymbolAux DocumentSymbol) @@ -212,18 +243,56 @@ instance : ToJson DocumentSymbolResult where inductive SymbolTag where | deprecated + deriving BEq, Hashable, Inhabited + +instance : FromJson SymbolTag where + fromJson? + | 1 => .ok .deprecated + | j => .error s!"unknown symbol tag {j}" instance : ToJson SymbolTag where - toJson - | SymbolTag.deprecated => 1 + toJson + | .deprecated => 1 structure SymbolInformation where - name : String - kind : SymbolKind - tags : Array SymbolTag := #[] - location : Location + name : String + kind : SymbolKind + tags : Array SymbolTag := #[] + location : Location containerName? : Option String := none - deriving ToJson + deriving FromJson, ToJson + +structure CallHierarchyPrepareParams extends TextDocumentPositionParams + deriving FromJson, ToJson + +structure CallHierarchyItem where + name : String + kind : SymbolKind + tags? : Option (Array SymbolTag) := none + detail? : Option String := none + uri : DocumentUri + range : Range + selectionRange : Range + -- data? : Option unknown + deriving FromJson, ToJson, BEq, Hashable, Inhabited + +structure CallHierarchyIncomingCallsParams where + item : CallHierarchyItem + deriving FromJson, ToJson + +structure CallHierarchyIncomingCall where + «from» : CallHierarchyItem + fromRanges : Array Range + deriving FromJson, ToJson, Inhabited + +structure CallHierarchyOutgoingCallsParams where + item : CallHierarchyItem + deriving FromJson, ToJson + +structure CallHierarchyOutgoingCall where + to : CallHierarchyItem + fromRanges : Array Range + deriving FromJson, ToJson, Inhabited inductive SemanticTokenType where -- Used by Lean @@ -304,14 +373,14 @@ example {v : SemanticTokenModifier} : open SemanticTokenModifier in cases v <;> native_decide structure SemanticTokensLegend where - tokenTypes : Array String + tokenTypes : Array String tokenModifiers : Array String deriving FromJson, ToJson structure SemanticTokensOptions where legend : SemanticTokensLegend - range : Bool - full : Bool /- | { + range : Bool + full : Bool /- | { delta?: boolean; } -/ deriving FromJson, ToJson @@ -322,12 +391,12 @@ structure SemanticTokensParams where structure SemanticTokensRangeParams where textDocument : TextDocumentIdentifier - range : Range + range : Range deriving FromJson, ToJson structure SemanticTokens where resultId? : Option String := none - data : Array Nat + data : Array Nat deriving FromJson, ToJson structure FoldingRangeParams where @@ -343,12 +412,12 @@ instance : ToJson FoldingRangeKind where toJson | FoldingRangeKind.comment => "comment" | FoldingRangeKind.imports => "imports" - | FoldingRangeKind.region => "region" + | FoldingRangeKind.region => "region" structure FoldingRange where startLine : Nat - endLine : Nat - kind? : Option FoldingRangeKind := none + endLine : Nat + kind? : Option FoldingRangeKind := none deriving ToJson structure RenameOptions where diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean index caf784ea9774..49a4c87323d9 100644 --- a/src/Lean/Data/Lsp/Utf16.lean +++ b/src/Lean/Data/Lsp/Utf16.lean @@ -8,6 +8,7 @@ import Init.Data.String import Init.Data.Array import Lean.Data.Lsp.Basic import Lean.Data.Position +import Lean.DeclarationRange /-! LSP uses UTF-16 for indexing, so we need to provide some primitives to interact with Lean strings using UTF-16 indices. -/ @@ -86,3 +87,13 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position := end FileMap end Lean + +/-- +Convert the Lean `DeclarationRange` to an LSP `Range` by turning the 1-indexed line numbering into a +0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed +offset. +-/ +def Lean.DeclarationRange.toLspRange (r : Lean.DeclarationRange) : Lsp.Range := { + start := ⟨r.pos.line - 1, r.charUtf16⟩ + «end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ +} diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 1541952ce0aa..79bd136585f4 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -118,7 +118,7 @@ def runFrontend if let some ileanFileName := ileanFileName? then let trees := s.commandState.infoState.trees.toArray let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) - let ilean := { module := mainModuleName, references : Lean.Server.Ilean } + let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean } IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean pure (s.commandState.env, !s.commandState.messages.hasErrors) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 30c1e44e3133..9d7802f011a2 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -76,7 +76,7 @@ section Elab private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do let trees := snaps.map fun snap => snap.infoTree - let references := findModuleRefs m.text trees (localVars := true) + let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs let param := { version := m.version, references : LeanIleanInfoParams } hOut.writeLspNotification { method, param } diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index d04203f62ba5..ad74b293ff04 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -290,23 +290,23 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams) | `(do%$i $elems) => highlightReturn? (i.getRange?.get!.toLspRange text) elems | stx => stx.getArgs.findSome? (highlightReturn? doRange?) - let highlightRefs? (snaps : Array Snapshot) : Option (Array DocumentHighlight) := Id.run do + let highlightRefs? (snaps : Array Snapshot) : IO (Option (Array DocumentHighlight)) := do let trees := snaps.map (·.infoTree) - let refs : Lsp.ModuleRefs := findModuleRefs text trees + let refs : Lsp.ModuleRefs ← findModuleRefs text trees |>.toLspModuleRefs let mut ranges := #[] - for ident in ← refs.findAt p.position do - if let some info ← refs.find? ident then - if let some definition := info.definition then - ranges := ranges.push definition - ranges := ranges.append info.usages + for ident in refs.findAt p.position do + if let some info := refs.find? ident then + if let some ⟨definitionRange, _⟩ := info.definition? then + ranges := ranges.push definitionRange + ranges := ranges.append <| info.usages.map (·.range) if ranges.isEmpty then return none - some <| ranges.map ({ range := ·, kind? := DocumentHighlightKind.text }) + return some <| ranges.map ({ range := ·, kind? := DocumentHighlightKind.text }) withWaitFindSnap doc (fun s => s.endPos > pos) (notFoundX := pure #[]) fun snap => do let (snaps, _) ← doc.cmdSnaps.getFinishedPrefix - if let some his := highlightRefs? snaps.toArray then + if let some his ← highlightRefs? snaps.toArray then return his if let some hi := highlightReturn? none snap.stx then return #[hi] diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean index 313d0db91862..1c31eb024b48 100644 --- a/src/Lean/Server/GoTo.lean +++ b/src/Lean/Server/GoTo.lean @@ -34,14 +34,11 @@ def locationLinksFromDecl (srcSearchPath : SearchPath) (uri : DocumentUri) (n : let ranges? ← findDeclarationRanges? n if let (some ranges, some modUri) := (ranges?, modUri?) then - let declRangeToLspRange (r : DeclarationRange) : Lsp.Range := - { start := ⟨r.pos.line - 1, r.charUtf16⟩ - «end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ } let ll : LocationLink := { originSelectionRange? := originRange? targetUri := modUri - targetRange := declRangeToLspRange ranges.range - targetSelectionRange := declRangeToLspRange ranges.selectionRange + targetRange := ranges.range.toLspRange + targetSelectionRange := ranges.selectionRange.toLspRange } return #[ll] return #[] diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index d7bfa3af002c..dbf487a321b8 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -13,18 +13,18 @@ namespace Lean.Server open Lsp Lean.Elab Std structure Reference where - ident : RefIdent + ident : RefIdent /-- FVarIds that are logically identical to this reference -/ - aliases : Array RefIdent := #[] - range : Lsp.Range - stx : Syntax - ci : ContextInfo - info : Info + aliases : Array RefIdent := #[] + range : Lsp.Range + stx : Syntax + ci : ContextInfo + info : Info isBinder : Bool structure RefInfo where definition : Option Reference - usages : Array Reference + usages : Array Reference namespace RefInfo @@ -37,11 +37,26 @@ def addRef : RefInfo → Reference → RefInfo { i with usages := usages.push ref } | i, _ => i -instance : Coe RefInfo Lsp.RefInfo where - coe self := - { - definition := self.definition.map (·.range) - usages := self.usages.map (·.range) +def toLspRefInfo (i : RefInfo) : IO Lsp.RefInfo := do + let refToRefInfoLocation (ref : Reference) : IO RefInfo.Location := do + let parentDeclName? := ref.ci.parentDecl? + let parentDeclRanges? ← ref.ci.runMetaM ref.info.lctx do + let some parentDeclName := parentDeclName? + | return none + findDeclarationRanges? parentDeclName + return { + range := ref.range + parentDecl? := do + let parentDeclName ← parentDeclName? + let parentDeclRange := (← parentDeclRanges?).range.toLspRange + let parentDeclSelectionRange := (← parentDeclRanges?).selectionRange.toLspRange + return ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ + } + let definition? ← i.definition.mapM refToRefInfoLocation + let usages ← i.usages.mapM refToRefInfoLocation + return { + definition? := definition? + usages := usages } end RefInfo @@ -54,8 +69,10 @@ def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs := let refInfo := self.findD ref.ident RefInfo.empty self.insert ref.ident (refInfo.addRef ref) -instance : Coe ModuleRefs Lsp.ModuleRefs where - coe self := HashMap.ofList <| List.map (fun (k, v) => (k, v)) <| self.toList +def toLspModuleRefs (refs : ModuleRefs) : IO Lsp.ModuleRefs := do + let refs ← refs.toList.mapM fun (k, v) => do + return (k, ← v.toLspRefInfo) + return HashMap.ofList refs end ModuleRefs @@ -68,15 +85,15 @@ def empty : RefInfo := ⟨ none, #[] ⟩ def merge (a : RefInfo) (b : RefInfo) : RefInfo := { - definition := b.definition.orElse fun _ => a.definition + definition? := b.definition?.orElse fun _ => a.definition? usages := a.usages.append b.usages } def findRange? (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Option Range := do - if let some range := self.definition then + if let some ⟨range, _⟩ := self.definition? then if contains range pos then return range - for range in self.usages do + for ⟨range, _⟩ in self.usages do if contains range pos then return range none @@ -117,8 +134,8 @@ open Elab /-- Content of individual `.ilean` files -/ structure Ilean where - version : Nat := 1 - module : Name + version : Nat := 2 + module : Name references : Lsp.ModuleRefs deriving FromJson, ToJson @@ -152,64 +169,98 @@ def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference : get /-- -The `FVarId`s of a function parameter in the function's signature and body -differ. However, they have `TermInfo` nodes with `binder := true` in the exact -same position. Moreover, macros such as do-reassignment `x := e` may create -chains of variable definitions where a helper definition overlaps with a use -of a variable. - -This function changes every such group to use a single `FVarId` (the head of the -chain/DAG) and gets rid of duplicate definitions. +There are several different identifiers that should be considered equal for the purpose of finding +all references of an identifier: +- `FVarId`s of a function parameter in the function's signature and body +- Chains of helper definitions like those created for do-reassignment `x := e` +- Overlapping definitions like those defined by `where` declarations that define both an FVar + (for local usage) and a constant (for non-local usage) +- Identifiers connected by `FVarAliasInfo` such as variables before and after `match` generalization + +In the first three cases that are not explicitly denoted as aliases with an `FVarAliasInfo`, the +corresponding `Reference`s have the exact same range. +This function finds all definitions that have the exact same range as another definition or usage +and collapses them into a single identifier. It also collapses identifiers connected by +an `FVarAliasInfo`. +When collapsing identifiers, it prefers using a `RefIdent.const name` over a `RefIdent.fvar id` for +all identifiers that are being collapsed into one. -/ -partial def combineFvars (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do +partial def combineIdents (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do -- Deduplicate definitions based on their exact range - let mut posMap : HashMap Lsp.Range FVarId := HashMap.empty + let mut posMap : HashMap Lsp.Range RefIdent := HashMap.empty for ref in refs do - if let { ident := RefIdent.fvar id, range, isBinder := true, .. } := ref then - posMap := posMap.insert range id + if let { ident, range, isBinder := true, .. } := ref then + posMap := posMap.insert range ident - let idMap := buildIdMap posMap + let idMap := useConstRepresentatives <| buildIdMap posMap let mut refs' := #[] for ref in refs do - match ref with - | { ident := ident@(RefIdent.fvar id), .. } => - if idMap.contains id then - refs' := refs'.push { ref with ident := applyIdMap idMap ident, aliases := #[ident] } - else if !idMap.contains id then - refs' := refs'.push ref - | _ => + let id := ref.ident + if idMap.contains id then + refs' := refs'.push { ref with ident := findCanonicalRepresentative idMap id, aliases := #[id] } + else if !idMap.contains id then refs' := refs'.push ref refs' where - findCanonicalBinder (idMap : HashMap FVarId FVarId) (id : FVarId) : FVarId := - match idMap.find? id with - | some id' => findCanonicalBinder idMap id' -- recursion depth is expected to be very low - | none => id - - applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent - | m, RefIdent.fvar id => RefIdent.fvar <| findCanonicalBinder m id - | _, ident => ident + useConstRepresentatives (idMap : HashMap RefIdent RefIdent) + : HashMap RefIdent RefIdent := Id.run do + let insertIntoClass classesById id := + let representative := findCanonicalRepresentative idMap id + let «class» := classesById.findD representative ∅ + let classesById := classesById.erase representative -- make `«class»` referentially unique + let «class» := «class».insert id + classesById.insert representative «class» + + -- collect equivalence classes + let mut classesById : HashMap RefIdent (HashSet RefIdent) := ∅ + for ⟨id, baseId⟩ in idMap.toArray do + classesById := insertIntoClass classesById id + classesById := insertIntoClass classesById baseId + + let mut r := ∅ + for ⟨currentRepresentative, «class»⟩ in classesById.toArray do + -- find best representative (ideally a const if available) + let mut bestRepresentative := currentRepresentative + for id in «class» do + bestRepresentative := + match bestRepresentative, id with + | .fvar a, .fvar _ => .fvar a + | .fvar _, .const b => .const b + | .const a, .fvar _ => .const a + | .const a, .const _ => .const a + + -- compress `idMap` so that all identifiers in a class point to the best representative + for id in «class» do + if id != bestRepresentative then + r := r.insert id bestRepresentative + return r + + findCanonicalRepresentative (idMap : HashMap RefIdent RefIdent) (id : RefIdent) : RefIdent := Id.run do + let mut canonicalRepresentative := id + while idMap.contains canonicalRepresentative do + canonicalRepresentative := idMap.find! canonicalRepresentative + return canonicalRepresentative buildIdMap posMap := Id.run <| StateT.run' (s := HashMap.empty) do -- map fvar defs to overlapping fvar defs/uses for ref in refs do - if let { ident := RefIdent.fvar baseId, range, .. } := ref then - if let some id := posMap.find? range then - insertIdMap id baseId + let baseId := ref.ident + if let some id := posMap.find? ref.range then + insertIdMap id baseId -- apply `FVarAliasInfo` trees.forM (·.visitM' (postNode := fun _ info _ => do if let .ofFVarAliasInfo ai := info then - insertIdMap ai.id ai.baseId)) + insertIdMap (.fvar ai.id) (.fvar ai.baseId))) get - -- NOTE: poor man's union-find; see also `findCanonicalBinder` + -- poor man's union-find; see also `findCanonicalBinder` insertIdMap id baseId := do let idMap ← get - let id := findCanonicalBinder idMap id - let baseId := findCanonicalBinder idMap baseId + let id := findCanonicalRepresentative idMap id + let baseId := findCanonicalRepresentative idMap baseId if baseId != id then modify (·.insert id baseId) @@ -229,7 +280,7 @@ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool : (allowSimultaneousBinderUse := false) : ModuleRefs := Id.run do let mut refs := dedupReferences (allowSimultaneousBinderUse := allowSimultaneousBinderUse) <| - combineFvars trees <| + combineIdents trees <| findReferences text trees if !localVars then refs := refs.filter fun @@ -291,8 +342,12 @@ def findRange? (self : References) (module : Name) (pos : Lsp.Position) (include let refs ← self.allRefs.find? module refs.findRange? pos includeStop +structure DocumentRefInfo where + location : Location + parentInfo? : Option RefInfo.ParentDecl + def referringTo (self : References) (identModule : Name) (ident : RefIdent) (srcSearchPath : SearchPath) - (includeDefinition : Bool := true) : IO (Array Location) := do + (includeDefinition : Bool := true) : IO (Array DocumentRefInfo) := do let refsToCheck := match ident with | RefIdent.const _ => self.allRefs.toList | RefIdent.fvar _ => match self.allRefs.find? identModule with @@ -306,22 +361,22 @@ def referringTo (self : References) (identModule : Name) (ident : RefIdent) (src -- opened in the right folder let uri := System.Uri.pathToUri <| ← IO.FS.realPath path if includeDefinition then - if let some range := info.definition then - result := result.push ⟨uri, range⟩ - for range in info.usages do - result := result.push ⟨uri, range⟩ + if let some ⟨range, parentDeclInfo?⟩ := info.definition? then + result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩ + for ⟨range, parentDeclInfo?⟩ in info.usages do + result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩ return result def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath) - : IO (Option Location) := do + : IO (Option DocumentRefInfo) := do for (module, refs) in self.allRefs.toList do if let some info := refs.find? ident then - if let some definition := info.definition then + if let some ⟨definitionRange, definitionParentDeclInfo?⟩ := info.definition? then if let some path ← srcSearchPath.findModuleWithExt "lean" module then -- Resolve symlinks (such as `src` in the build dir) so that files are -- opened in the right folder let uri := System.Uri.pathToUri <| ← IO.FS.realPath path - return some ⟨uri, definition⟩ + return some ⟨⟨uri, definitionRange⟩, definitionParentDeclInfo?⟩ return none def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter : Name → Option α) @@ -331,9 +386,9 @@ def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter if let some path ← srcSearchPath.findModuleWithExt "lean" module then let uri := System.Uri.pathToUri <| ← IO.FS.realPath path for (ident, info) in refs.toList do - if let (RefIdent.const name, some definition) := (ident, info.definition) then + if let (RefIdent.const name, some ⟨definitionRange, _⟩) := (ident, info.definition?) then if let some a := filter name then - result := result.push (a, ⟨uri, definition⟩) + result := result.push (a, ⟨uri, definitionRange⟩) if let some maxAmount := maxAmount? then if result.size >= maxAmount then return result diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index e308041468b1..7a496fb73532 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -22,42 +22,49 @@ For general server architecture, see `README.md`. This module implements the wat ## Watchdog state -Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted -workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes -to the header and thus restart the corresponding worker, freeing its imports. +Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly +restarted workers, the watchdog needs to maintain the current state of each file. It can also use +this state to detect changes to the header and thus restart the corresponding worker, freeing its +imports. TODO(WN): -We may eventually want to keep track of approximately (since this isn't knowable exactly) where in the file a worker -crashed. Then on restart, we tell said worker to only parse up to that point and query the user about how to proceed -(continue OR allow the user to fix the bug and then continue OR ..). Without this, if the crash is deterministic, -users may be confused about why the server seemingly stopped working for a single file. +We may eventually want to keep track of approximately (since this isn't knowable exactly) where in +the file a worker crashed. Then on restart, we tell said worker to only parse up to that point and +query the user about how to proceed (continue OR allow the user to fix the bug and then continue OR +..). Without this, if the crash is deterministic, users may be confused about why the server +seemingly stopped working for a single file. ## Watchdog <-> worker communication -The watchdog process and its file worker processes communicate via LSP. If the necessity arises, -we might add non-standard commands similarly based on JSON-RPC. Most requests and notifications -are forwarded to the corresponding file worker process, with the exception of these notifications: +The watchdog process and its file worker processes communicate via LSP. If the necessity arises, we +might add non-standard commands similarly based on JSON-RPC. Most requests and notifications are +forwarded to the corresponding file worker process, with the exception of these notifications: -- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a task to - asynchronously receive LSP packets from the worker (e.g. request responses). +- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a + task to asynchronously receive LSP packets from the worker (e.g. request + responses). - textDocument/didChange: Update the local file state so that it can be resent to restarted workers. Then forward the `didChange` notification. -- textDocument/didClose: Signal a shutdown to the file worker and remove the associated watchdog state. +- textDocument/didClose: Signal a shutdown to the file worker and remove the associated watchdog + state. Moreover, we don't implement the full protocol at this level: -- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with its server - capabilities. Consequently, the watchdog will not send an `initialized` notification to the worker. -- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full current state of - the file. No additional `didOpen` notifications will be forwarded to the worker process. +- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with + its server capabilities. Consequently, the watchdog will not send an `initialized` notification to + the worker. +- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full + current state of the file. No additional `didOpen` notifications will be forwarded to the worker + process. - `$/cancelRequest` notifications are forwarded to all file workers. -- File workers are always terminated with an `exit` notification, without previously receiving a `shutdown` request. - Similarly, they never receive a `didClose` notification. +- File workers are always terminated with an `exit` notification, without previously receiving a + `shutdown` request. Similarly, they never receive a `didClose` notification. ## Watchdog <-> client communication -The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add -non-standard extensions in case they're needed, for example to communicate tactic state. +The watchdog itself should implement the LSP standard as closely as possible. However we reserve the +right to add non-standard extensions in case they're needed, for example to communicate tactic +state. -/ namespace Lean.Server.Watchdog @@ -83,13 +90,13 @@ section Utils | ioError (e : IO.Error) inductive WorkerState where - /-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker - and when reading a request reply. - In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. - Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. - Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded - to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file - worker arrives. -/ + /-- The watchdog can detect a crashed file worker in two places: When trying to send a message + to the file worker and when reading a request reply. + In the latter case, the forwarding task terminates and delegates a `crashed` event to the + main task. Then, in both cases, the file worker has its state set to `crashed` and requests + that are in-flight are errored. Upon receiving the next packet for that file worker, the file + worker is restarted and the packet is forwarded to it. If the crash was detected while writing + a packet, we queue that packet until the next packet for the file worker arrives. -/ | crashed (queuedMsgs : Array JsonRpc.Message) | running @@ -102,11 +109,12 @@ section FileWorker proc : Process.Child workerCfg commTask : Task WorkerEvent state : WorkerState - -- This should not be mutated outside of namespace FileWorker, as it is used as shared mutable state - /-- The pending requests map contains all requests - that have been received from the LSP client, but were not answered yet. - We need them for forwarding cancellation requests to the correct worker as well as cleanly aborting - requests on worker crashes. -/ + -- This should not be mutated outside of namespace FileWorker, + -- as it is used as shared mutable state + /-- The pending requests map contains all requests that have been received from the LSP client, + but were not answered yet. + We need them for forwarding cancellation requests to the correct worker as well as cleanly + aborting requests on worker crashes. -/ pendingRequestsRef : IO.Ref PendingRequestMap namespace FileWorker @@ -120,8 +128,10 @@ section FileWorker def erasePendingRequest (fw : FileWorker) (id : RequestID) : IO Unit := fw.pendingRequestsRef.modify fun pendingRequests => pendingRequests.erase id - def errorPendingRequests (fw : FileWorker) (hError : FS.Stream) (code : ErrorCode) (msg : String) : IO Unit := do - let pendingRequests ← fw.pendingRequestsRef.modifyGet (fun pendingRequests => (pendingRequests, RBMap.empty)) + def errorPendingRequests (fw : FileWorker) (hError : FS.Stream) (code : ErrorCode) (msg : String) + : IO Unit := do + let pendingRequests ← fw.pendingRequestsRef.modifyGet + fun pendingRequests => (pendingRequests, RBMap.empty) for ⟨id, _⟩ in pendingRequests do hError.writeLspResponseError { id := id, code := code, message := msg } @@ -173,13 +183,15 @@ section ServerM let s ← read if let some path := fileUriToPath? fw.doc.uri then if let some module ← searchModuleNameOfFileName path s.srcSearchPath then - s.references.modify fun refs => refs.updateWorkerRefs module params.version params.references + s.references.modify fun refs => + refs.updateWorkerRefs module params.version params.references def handleIleanInfoFinal (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do let s ← read if let some path := fileUriToPath? fw.doc.uri then if let some module ← searchModuleNameOfFileName path s.srcSearchPath then - s.references.modify fun refs => refs.finalizeWorkerRefs module params.version params.references + s.references.modify fun refs => + refs.finalizeWorkerRefs module params.version params.references /-- Creates a Task which forwards a worker's messages into the output stream until an event which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/ @@ -217,8 +229,9 @@ section ServerM | 0 => -- Worker was terminated fw.errorPendingRequests o ErrorCode.contentModified - (s!"The file worker for {fw.doc.uri} has been terminated. Either the header has changed," - ++ " or the file was closed, or the server is shutting down.") + (s!"The file worker for {fw.doc.uri} has been terminated. " + ++ "Either the header has changed, or the file was closed, " + ++ " or the server is shutting down.") -- one last message to clear the diagnostics for this file so that stale errors -- do not remain in the editor forever. publishDiagnostics fw.doc #[] o @@ -227,8 +240,13 @@ section ServerM return .importsChanged | _ => -- Worker crashed - fw.errorPendingRequests o (if exitCode = 1 then ErrorCode.workerExited else ErrorCode.workerCrashed) - s!"Server process for {fw.doc.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug"}." + let (errorCode, errorCausePointer) := + if exitCode = 1 then + (ErrorCode.workerExited, "see stderr for exception") + else + (ErrorCode.workerCrashed, "likely due to a stack overflow or a bug") + fw.errorPendingRequests o errorCode + s!"Server process for {fw.doc.uri} crashed, {errorCausePointer}." publishProgressAtPos fw.doc 0 o (kind := LeanFileProgressKind.fatalError) return WorkerEvent.crashed err loop @@ -300,15 +318,22 @@ section ServerM updateFileWorkers { ←findFileWorker! uri with state := WorkerState.crashed queuedMsgs } /-- Tries to write a message, sets the state of the FileWorker to `crashed` if it does not succeed - and restarts the file worker if the `crashed` flag was already set. Just logs an error if there - is no FileWorker at this `uri`. + and restarts the file worker if the `crashed` flag was already set. Just logs an error if + there is no FileWorker at this `uri`. Messages that couldn't be sent can be queued up via the queueFailedMessage flag and will be discharged after the FileWorker is restarted. -/ - def tryWriteMessage (uri : DocumentUri) (msg : JsonRpc.Message) (queueFailedMessage := true) (restartCrashedWorker := false) : - ServerM Unit := do + def tryWriteMessage + (uri : DocumentUri) + (msg : JsonRpc.Message) + (queueFailedMessage := true) + (restartCrashedWorker := false) + : ServerM Unit := do let some fw ← findFileWorker? uri | do - (←read).hLog.putStrLn s!"Cannot send message to unknown document '{uri}':\n{(toJson msg).compress}" + let errorMsg := + s!"Cannot send message to unknown document '{uri}':\n" + ++ s!"{(toJson msg).compress}" + (←read).hLog.putStrLn errorMsg return match fw.state with | WorkerState.crashed queuedMsgs => @@ -353,8 +378,8 @@ def findDefinitions (p : TextDocumentPositionParams) : ServerM <| Array Location if let some module ← searchModuleNameOfFileName path srcSearchPath then let references ← (← read).references.get for ident in references.findAt module p.position (includeStop := true) do - if let some definition ← references.definitionOf? ident srcSearchPath then - definitions := definitions.push definition + if let some ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then + definitions := definitions.push definitionLocation return definitions def handleReference (p : ReferenceParams) : ServerM (Array Location) := do @@ -364,10 +389,142 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do if let some module ← searchModuleNameOfFileName path srcSearchPath then let references ← (← read).references.get for ident in references.findAt module p.position (includeStop := true) do - let identRefs ← references.referringTo module ident srcSearchPath p.context.includeDeclaration - result := result.append identRefs + let identRefs ← references.referringTo module ident srcSearchPath + p.context.includeDeclaration + result := result.append <| identRefs.map (·.location) return result +private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath) + : IO (Option CallHierarchyItem) := do + let some ⟨definitionLocation, parentDecl?⟩ ← refs.definitionOf? ident srcSearchPath + | return none + + match ident with + | .const definitionName => + -- If we have a constant with a proper name, use it. + -- If `callHierarchyItemOf?` is used either on the name of a definition itself or e.g. an + -- `inductive` constructor, this is the right thing to do and using the parent decl is + -- the wrong thing to do. + return some { + name := definitionName.toString + kind := SymbolKind.constant + uri := definitionLocation.uri + range := definitionLocation.range, + selectionRange := definitionLocation.range + } + | _ => + let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? + | return none + + return some { + name := parentDeclName.toString + kind := SymbolKind.constant + uri := definitionLocation.uri + range := parentDeclRange, + selectionRange := parentDeclSelectionRange + } + +def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams) + : ServerM (Array CallHierarchyItem) := do + let some path := fileUriToPath? p.textDocument.uri + | return #[] + + let srcSearchPath := (← read).srcSearchPath + let some module ← searchModuleNameOfFileName path srcSearchPath + | return #[] + + let references ← (← read).references.get + let idents := references.findAt module p.position (includeStop := true) + + let items ← idents.filterMapM fun ident => callHierarchyItemOf? references ident srcSearchPath + return items + +def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) + : ServerM (Array CallHierarchyIncomingCall) := do + let some path := fileUriToPath? p.item.uri + | return #[] + + let srcSearchPath := (← read).srcSearchPath + let some module ← searchModuleNameOfFileName path srcSearchPath + | return #[] + + let references ← (← read).references.get + let identRefs ← references.referringTo module (.const p.item.name.toName) srcSearchPath false + + let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do + + let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? + | return none + return some { + «from» := { + name := parentDeclName.toString + kind := SymbolKind.constant + uri := location.uri + range := parentDeclRange + selectionRange := parentDeclSelectionRange + } + fromRanges := #[location.range] + } + + return collapseSameIncomingCalls incomingCalls + +where + + collapseSameIncomingCalls (incomingCalls : Array CallHierarchyIncomingCall) + : Array CallHierarchyIncomingCall := + let grouped := incomingCalls.groupByKey (·.«from») + let collapsed := grouped.toArray.map fun ⟨_, group⟩ => { + «from» := group[0]!.«from» + fromRanges := group.concatMap (·.fromRanges) + } + collapsed + +def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) + : ServerM (Array CallHierarchyOutgoingCall) := do + let some path := fileUriToPath? p.item.uri + | return #[] + + let srcSearchPath := (← read).srcSearchPath + let some module ← searchModuleNameOfFileName path srcSearchPath + | return #[] + + let references ← (← read).references.get + + let some refs := references.allRefs.find? module + | return #[] + + let items ← refs.toArray.filterMapM fun ⟨ident, info⟩ => do + let outgoingUsages := info.usages.filter fun usage => Id.run do + let some parentDecl := usage.parentDecl? + | return false + return p.item.name.toName == parentDecl.name + + let outgoingUsages := outgoingUsages.map (·.range) + if outgoingUsages.isEmpty then + return none + + let some item ← callHierarchyItemOf? references ident srcSearchPath + | return none + + -- filter local defs from outgoing calls + if item.name == p.item.name then + return none + + return some ⟨item, outgoingUsages⟩ + + return collapseSameOutgoingCalls items + +where + + collapseSameOutgoingCalls (outgoingCalls : Array CallHierarchyOutgoingCall) + : Array CallHierarchyOutgoingCall := + let grouped := outgoingCalls.groupByKey (·.to) + let collapsed := grouped.toArray.map fun ⟨_, group⟩ => { + to := group[0]!.to + fromRanges := group.concatMap (·.fromRanges) + } + collapsed + def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInformation) := do if p.query.isEmpty then return #[] @@ -436,7 +593,8 @@ section NotificationHandling let newDocText := foldDocumentChanges changes oldDoc.text let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText, oldDoc.dependencyBuildMode⟩ updateFileWorkers { fw with doc := newDoc } - tryWriteMessage doc.uri (Notification.mk "textDocument/didChange" p) (restartCrashedWorker := true) + let notification := Notification.mk "textDocument/didChange" p + tryWriteMessage doc.uri notification (restartCrashedWorker := true) def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit := terminateFileWorker p.textDocument.uri @@ -469,15 +627,18 @@ section NotificationHandling if (← fw.pendingRequestsRef.get).contains p.id then tryWriteMessage uri (Notification.mk "$/cancelRequest" p) (queueFailedMessage := false) - def forwardNotification {α : Type} [ToJson α] [FileSource α] (method : String) (params : α) : ServerM Unit := + def forwardNotification {α : Type} [ToJson α] [FileSource α] (method : String) (params : α) + : ServerM Unit := tryWriteMessage (fileSource params) (Notification.mk method params) (queueFailedMessage := true) end NotificationHandling section MessageHandling def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with - | Except.ok parsed => pure parsed - | Except.error inner => throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}" + | Except.ok parsed => + pure parsed + | Except.error inner => + throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}" def forwardRequestToWorker (id : RequestID) (method : String) (params : Json) : ServerM Unit := do let uri: DocumentUri ← @@ -532,25 +693,48 @@ section MessageHandling (← read).hOut.writeLspResponse ⟨id, definitions⟩ return match method with - | "textDocument/references" => handle ReferenceParams (Array Location) handleReference - | "workspace/symbol" => handle WorkspaceSymbolParams (Array SymbolInformation) handleWorkspaceSymbol - | "textDocument/prepareRename" => handle PrepareRenameParams (Option Range) handlePrepareRename - | "textDocument/rename" => handle RenameParams WorkspaceEdit handleRename - | _ => forwardRequestToWorker id method params + | "textDocument/references" => + handle ReferenceParams (Array Location) handleReference + | "workspace/symbol" => + handle WorkspaceSymbolParams (Array SymbolInformation) handleWorkspaceSymbol + | "textDocument/prepareCallHierarchy" => + handle CallHierarchyPrepareParams (Array CallHierarchyItem) handlePrepareCallHierarchy + | "callHierarchy/incomingCalls" => + handle CallHierarchyIncomingCallsParams (Array CallHierarchyIncomingCall) + handleCallHierarchyIncomingCalls + | "callHierarchy/outgoingCalls" => + handle Lsp.CallHierarchyOutgoingCallsParams (Array CallHierarchyOutgoingCall) + handleCallHierarchyOutgoingCalls + | "textDocument/prepareRename" => + handle PrepareRenameParams (Option Range) handlePrepareRename + | "textDocument/rename" => + handle RenameParams WorkspaceEdit handleRename + | _ => + forwardRequestToWorker id method params def handleNotification (method : String) (params : Json) : ServerM Unit := do - let handle := (fun α [FromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler) + let handle := fun α [FromJson α] (handler : α → ServerM Unit) => + parseParams α params >>= handler match method with - | "textDocument/didOpen" => handle _ handleDidOpen - | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange - | "textDocument/didClose" => handle DidCloseTextDocumentParams handleDidClose - | "workspace/didChangeWatchedFiles" => handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles - | "$/cancelRequest" => handle CancelParams handleCancelRequest - | "$/lean/rpc/connect" => handle RpcConnectParams (forwardNotification method) - | "$/lean/rpc/release" => handle RpcReleaseParams (forwardNotification method) - | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (forwardNotification method) - | _ => - if !"$/".isPrefixOf method then -- implementation-dependent notifications can be safely ignored + | "textDocument/didOpen" => + handle _ handleDidOpen + | "textDocument/didChange" => + handle DidChangeTextDocumentParams handleDidChange + | "textDocument/didClose" => + handle DidCloseTextDocumentParams handleDidClose + | "workspace/didChangeWatchedFiles" => + handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles + | "$/cancelRequest" => + handle CancelParams handleCancelRequest + | "$/lean/rpc/connect" => + handle RpcConnectParams (forwardNotification method) + | "$/lean/rpc/release" => + handle RpcReleaseParams (forwardNotification method) + | "$/lean/rpc/keepAlive" => + handle RpcKeepAliveParams (forwardNotification method) + | _ => + -- implementation-dependent notifications can be safely ignored + if !"$/".isPrefixOf method then (←read).hLog.putStrLn s!"Got unsupported notification: {method}" end MessageHandling @@ -614,7 +798,8 @@ section MainLoop handleCrash fw.doc.uri #[] mainLoop clientTask | WorkerEvent.terminated => - throwServerError "Internal server error: got termination event for worker that should have been removed" + throwServerError <| "Internal server error: got termination event for worker that " + ++ "should have been removed" | .importsChanged => startFileWorker fw.doc mainLoop clientTask @@ -637,6 +822,7 @@ def mkLeanServerCapabilities : ServerCapabilities := { definitionProvider := true typeDefinitionProvider := true referencesProvider := true + callHierarchyProvider := true renameProvider? := some { prepareProvider := true } @@ -677,7 +863,8 @@ def initAndRunWatchdogAux : ServerM Unit := do def findWorkerPath : IO System.FilePath := do let mut workerPath ← IO.appPath if let some path := (←IO.getEnv "LEAN_SYSROOT") then - workerPath := System.FilePath.mk path / "bin" / "lean" |>.addExtension System.FilePath.exeExtension + workerPath := System.FilePath.mk path / "bin" / "lean" + |>.addExtension System.FilePath.exeExtension if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then workerPath := System.FilePath.mk path return workerPath diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean index 926d319416ec..bed42cb20256 100644 --- a/tests/lean/linterUnusedVariables.lean +++ b/tests/lean/linterUnusedVariables.lean @@ -23,10 +23,10 @@ def usedAndUnusedVariables : Nat := 3 x -def unusedWhereVariable : Nat := +def whereVariable : Nat := 3 where - x := 5 + x := 5 -- x is globally available via `whereVariable.x` def unusedWhereArgument : Nat := f 2 diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index b36b23ebfa7d..6be84fef0fa4 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/tests/lean/linterUnusedVariables.lean.expected.out @@ -1,9 +1,7 @@ linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables] -linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables] -linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables] linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]