From 8a8acfce83766b1f8b07f961e38dc9ecd03c5d32 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 7 Dec 2023 18:22:06 +0100 Subject: [PATCH] feat: add call hierarchy support --- src/Lean/Data/HashMap.lean | 10 + src/Lean/Data/Lsp/Capabilities.lean | 1 + src/Lean/Data/Lsp/Internal.lean | 74 +++++-- src/Lean/Data/Lsp/LanguageFeatures.lean | 131 ++++++++++--- src/Lean/Data/Lsp/Utf16.lean | 6 + 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 | 146 +++++++++++++- tests/lean/linterUnusedVariables.lean | 4 +- .../linterUnusedVariables.lean.expected.out | 2 - 13 files changed, 455 insertions(+), 133 deletions(-) diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index 99660540ba4b..e6c108a5bfec 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -227,3 +227,13 @@ 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 + +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..a15166b8d8cb 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -19,7 +19,7 @@ reduce the size of the resulting JSON. -/ inductive RefIdent where | const : Name → RefIdent - | fvar : FVarId → RefIdent + | fvar : FVarId → RefIdent deriving BEq, Hashable, Inhabited namespace RefIdent @@ -43,33 +43,79 @@ 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 +structure RefInfo.ParentDecl where + name : Name + range : Lsp.Range + selectionRange : Lsp.Range + deriving ToJson + +structure RefInfo.Location where + range : Lsp.Range + parentDecl? : Option RefInfo.ParentDecl + structure RefInfo where - definition : Option Lsp.Range - usages : Array Lsp.Range + definition? : Option RefInfo.Location + 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 +134,7 @@ 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 references : ModuleRefs deriving FromJson, ToJson diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 851b0aa88844..cf66da7d523f 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -153,35 +153,66 @@ 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 @@ -191,7 +222,7 @@ structure DocumentSymbolAux (Self : Type) where range : Range selectionRange : Range children? : Option (Array Self) := none - deriving ToJson + deriving FromJson, ToJson inductive DocumentSymbol where | mk (sym : DocumentSymbolAux DocumentSymbol) @@ -212,10 +243,16 @@ 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 @@ -223,7 +260,39 @@ structure SymbolInformation where 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 diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean index caf784ea9774..9c8a97e227b5 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,8 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position := end FileMap end Lean + +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..5d35051f2544 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` + +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 e8e7edb88c7f..57c62954c917 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -378,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 @@ -391,9 +391,140 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do 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 + 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 #[] @@ -566,6 +697,14 @@ section MessageHandling 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" => @@ -683,6 +822,7 @@ def mkLeanServerCapabilities : ServerCapabilities := { definitionProvider := true typeDefinitionProvider := true referencesProvider := true + callHierarchyProvider := true renameProvider? := some { prepareProvider := true } 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]