From 78a72741c68ddafe93fbb69428ee825f6ebda902 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 14 Mar 2024 17:21:19 +0100 Subject: [PATCH] fix: jump to correct definition when names overlap (#3656) Fixes #1170. This PR adds the module name to `RefIdent` in order to distinguish conflicting names from different files. This also fixes related issues in find-references or the call hierarchy feature. It also adds some docstrings and stylistically refactors a bunch of code. --- src/Lean/Data/Lsp/Internal.lean | 66 +++--- src/Lean/Linter/UnusedVariables.lean | 6 +- src/Lean/Server/References.lean | 295 +++++++++++++++++++-------- src/Lean/Server/Utils.lean | 42 +++- src/Lean/Server/Watchdog.lean | 127 +++++++----- tests/lean/run/944.lean | 6 +- 6 files changed, 360 insertions(+), 182 deletions(-) diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index f97eabd89d..1d25c0c8e4 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -24,44 +24,50 @@ Identifier of a reference. -/ inductive RefIdent where /-- Named identifier. These are used in all references that are globally available. -/ - | const : Name → RefIdent + | const (moduleName : Name) (identName : Name) : RefIdent /-- Unnamed identifier. These are used for all local references. -/ - | fvar : FVarId → RefIdent + | fvar (moduleName : Name) (id : 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}" +instance : ToJson FVarId where + toJson id := toJson 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 - -- See `FromJson Name` - let name ← match sName with - | "[anonymous]" => pure Name.anonymous - | _ => - let n := sName.toName - if n.isAnonymous then throw s!"expected a Name, got {sName}" - else pure n - match sPrefix with - | "c:" => return RefIdent.const name - | "f:" => return RefIdent.fvar <| FVarId.mk name - | _ => throw "string must start with 'c:' or 'f:'" +instance : FromJson FVarId where + fromJson? s := return ⟨← fromJson? s⟩ + +/-- Shortened representation of `RefIdent` for more compact serialization. -/ +inductive RefIdentJsonRepr + /-- Shortened representation of `RefIdent.const` for more compact serialization. -/ + | c (m n : Name) + /-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/ + | f (m : Name) (i : FVarId) + deriving FromJson, ToJson + +/-- Converts `id` to its compact serialization representation. -/ +def toJsonRepr : (id : RefIdent) → RefIdentJsonRepr + | const moduleName identName => .c moduleName identName + | fvar moduleName id => .f moduleName id + +/-- Converts `repr` to `RefIdent`. -/ +def fromJsonRepr : (repr : RefIdentJsonRepr) → RefIdent + | .c m n => const m n + | .f m i => fvar m i + +/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/ +def fromJson? (s : Json) : Except String RefIdent := + return fromJsonRepr (← Lean.FromJson.fromJson? s) + +/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/ +def toJson (id : RefIdent) : Json := + Lean.ToJson.toJson <| toJsonRepr id instance : FromJson RefIdent where - fromJson? - | (s : String) => fromString s - | j => Except.error s!"expected a String, got {j}" + fromJson? := fromJson? instance : ToJson RefIdent where - toJson ident := toString ident + toJson := toJson end RefIdent @@ -147,13 +153,13 @@ instance : FromJson RefInfo where def ModuleRefs := HashMap RefIdent RefInfo instance : ToJson ModuleRefs where - toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info) + toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info) instance : FromJson ModuleRefs where fromJson? j := do let node ← j.getObj? node.foldM (init := HashMap.empty) fun m k v => - return m.insert (← RefIdent.fromString k) (← fromJson? v) + return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v) /-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications. diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index e489d69f85..42d6aec6a9 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -188,9 +188,9 @@ def unusedVariables : Linter where for (ident, info) in refs.toList do match ident with - | .fvar id => + | .fvar _ id => vars := vars.insert id info - | .const _ => + | .const .. => if let some definition := info.definition then if let some range := definition.stx.getRange? then constDecls := constDecls.insert range @@ -241,7 +241,7 @@ def unusedVariables : Linter where continue -- check if variable is used - if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then + if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar _ id => tacticFVarUses.contains id | _ => false) then continue -- check linter options diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 721f55e03e..6d81745f34 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -10,34 +10,62 @@ import Lean.Server.Utils /-! # Representing collected and deduplicated definitions and usages -/ +set_option linter.missingDocs true + namespace Lean.Server open Lsp Lean.Elab Std +/-- +Global reference. Used by the language server to figure out which identifiers refer to which +other identifiers across the whole project. +-/ structure Reference where + /-- Identifier of this reference. -/ ident : RefIdent - /-- FVarIds that are logically identical to this reference -/ + /-- Identifiers that are logically identical to this reference. -/ aliases : Array RefIdent := #[] + /-- Range where this reference occurs. -/ range : Lsp.Range + /-- Syntax of this reference. -/ stx : Syntax + /-- `ContextInfo` at the point of elaboration of this reference. -/ ci : ContextInfo + /-- Additional `InfoTree` information for this reference. -/ info : Info + /-- Whether this reference declares `ident`. -/ isBinder : Bool +/-- Definition and usages of an identifier within a single module. -/ structure RefInfo where + /-- + Definition `Reference` of the identifier. + Is equal to `none` if e.g. the definition is outside of the module where this `RefInfo` is used. + -/ definition : Option Reference + /-- All usage `Reference`s of the identifier in a single module. -/ usages : Array Reference namespace RefInfo -def empty : RefInfo := ⟨ none, #[] ⟩ +/-- No definition, no usages. -/ +def empty : RefInfo := ⟨none, #[]⟩ -def addRef : RefInfo → Reference → RefInfo - | i@{ definition := none, .. }, ref@{ isBinder := true, .. } => +/-- +Adds `ref` to `i`. +If `i` has no `definition` and `ref` is a declaration, it becomes the `definition`. +If `i` already has a `definition` and `ref` is also a declaration, it is not added to `i`. +Otherwise, `ref` is added to `i.usages`. +-/ +def addRef (i : RefInfo) (ref : Reference) : RefInfo := + match i, ref with + | { definition := none, .. }, { isBinder := true, .. } => { i with definition := ref } - | i@{ usages, .. }, ref@{ isBinder := false, .. } => + | { definition := some .., .. }, { isBinder := true, .. } => + i + | { usages, .. }, { isBinder := false, .. } => { i with usages := usages.push ref } - | i, _ => i +/-- Converts `i` to a JSON-serializable `Lsp.RefInfo`. -/ def toLspRefInfo (i : RefInfo) : BaseIO Lsp.RefInfo := do let refToRefInfoLocation (ref : Reference) : BaseIO RefInfo.Location := do let parentDeclName? := ref.ci.parentDecl? @@ -64,14 +92,17 @@ def toLspRefInfo (i : RefInfo) : BaseIO Lsp.RefInfo := do end RefInfo +/-- All references from within a module for all identifiers used in a single module. -/ def ModuleRefs := HashMap RefIdent RefInfo namespace ModuleRefs +/-- Adds `ref` to the `RefInfo` corresponding to `ref.ident` in `self`. See `RefInfo.addRef`. -/ def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs := let refInfo := self.findD ref.ident RefInfo.empty self.insert ref.ident (refInfo.addRef ref) +/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs`. -/ def toLspModuleRefs (refs : ModuleRefs) : BaseIO Lsp.ModuleRefs := do let refs ← refs.toList.mapM fun (k, v) => do return (k, ← v.toLspRefInfo) @@ -84,48 +115,64 @@ end Lean.Server namespace Lean.Lsp.RefInfo open Server +/-- No definition, no usages -/ def empty : RefInfo := ⟨ none, #[] ⟩ -def merge (a : RefInfo) (b : RefInfo) : RefInfo := - { - definition? := b.definition?.orElse fun _ => a.definition? - usages := a.usages.append b.usages - } +/-- Combines the `usages` of `a` and `b` and prefers the `definition?` of `b` over that of `a`. -/ +def merge (a : RefInfo) (b : RefInfo) : RefInfo where + 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 contains range pos then - return range - for ⟨range, _⟩ in self.usages do - if contains range pos then - return range +/-- +Finds the first definition or usage in `self` where the `RefInfo.Location.range` +contains the given `pos`. The `includeStop` parameter can be used to toggle between closed-interval +and half-open-interval behavior for the range. Closed-interval behavior matches the expectation of +VSCode when selecting an identifier at a cursor position (see #767). +-/ +def findReferenceLocation? + (self : RefInfo) + (pos : Lsp.Position) + (includeStop : Bool := false) + : Option Location := do + if let some loc := self.definition? then + if contains loc.range pos then + return loc + for loc in self.usages do + if contains loc.range pos then + return loc none where contains (range : Lsp.Range) (pos : Lsp.Position) : Bool := - -- Note: includeStop is used here to toggle between closed-interval and half-open-interval - -- behavior for the range. Closed-interval behavior matches the expectation of VSCode - -- when selecting an identifier at a cursor position, see #767. range.start <= pos && (if includeStop then pos <= range.end else pos < range.end) +/-- Checks whether any of the ranges in `self.definition?` or `self.usages` contains `pos`. -/ def contains (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Bool := Id.run do - (self.findRange? pos includeStop).isSome + (self.findReferenceLocation? pos includeStop).isSome end Lean.Lsp.RefInfo namespace Lean.Lsp.ModuleRefs open Server -def findAt (self : ModuleRefs) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do +/-- +Find all identifiers in `self` with a reference in this module that contains `pos` in its range. +-/ +def findAt + (self : ModuleRefs) + (pos : Lsp.Position) + (includeStop := false) + : Array RefIdent := Id.run do let mut result := #[] - for (ident, info) in self.toList do + for (ident, info) in self.toArray do if info.contains pos includeStop then result := result.push ident result +/-- Finds the first range in `self` that contains `pos`. -/ def findRange? (self : ModuleRefs) (pos : Lsp.Position) (includeStop := false) : Option Range := do for (_, info) in self.toList do - if let some range := info.findRange? pos includeStop then - return range + if let some loc := info.findReferenceLocation? pos includeStop then + return loc.range none end Lean.Lsp.ModuleRefs @@ -137,13 +184,17 @@ open Elab /-- Content of individual `.ilean` files -/ structure Ilean where - version : Nat := 2 + /-- Version number of the ilean format. -/ + version : Nat := 3 + /-- Name of the module that this ilean data has been collected for. -/ module : Name + /-- All references of this module. -/ references : Lsp.ModuleRefs deriving FromJson, ToJson namespace Ilean +/-- Reads and parses the .ilean file at `path`. -/ def load (path : System.FilePath) : IO Ilean := do let content ← FS.readFile path match Json.parse content >>= fromJson? with @@ -153,23 +204,33 @@ def load (path : System.FilePath) : IO Ilean := do end Ilean /-! # Collecting and deduplicating definitions and usages -/ -def identOf : Info → Option (RefIdent × Bool) +/-- +Determines the `RefIdent` for the `Info` `i` of an identifier in `module` and +whether it is a declaration. +-/ +def identOf (module : Name) (i : Info) : Option (RefIdent × Bool) := + match i with | Info.ofTermInfo ti => match ti.expr with - | Expr.const n .. => some (RefIdent.const n, ti.isBinder) - | Expr.fvar id .. => some (RefIdent.fvar id, ti.isBinder) + | Expr.const n .. => some (RefIdent.const module n, ti.isBinder) + | Expr.fvar id => some (RefIdent.fvar module id, ti.isBinder) | _ => none - | Info.ofFieldInfo fi => some (RefIdent.const fi.projName, false) - | Info.ofOptionInfo oi => some (RefIdent.const oi.declName, false) + | Info.ofFieldInfo fi => some (RefIdent.const module fi.projName, false) + | Info.ofOptionInfo oi => some (RefIdent.const module oi.declName, false) | _ => none -def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference := Id.run <| StateT.run' (s := #[]) do - for tree in trees do - tree.visitM' (postNode := fun ci info _ => do - if let some (ident, isBinder) := identOf info then - if let some range := info.range? then - if info.stx.getHeadInfo matches .original .. then -- we are not interested in canonical syntax here - modify (·.push { ident, range := range.toLspRange text, stx := info.stx, ci, info, isBinder })) - get +/-- Finds all references in `trees`. -/ +def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference := + Id.run <| StateT.run' (s := #[]) do + for tree in trees do + tree.visitM' (postNode := fun ci info _ => do + let mod := ci.env.header.mainModule + let some (ident, isBinder) := identOf mod info + | return + let some range := info.range? + | return + if info.stx.getHeadInfo matches .original .. then -- we are not interested in canonical syntax here + modify (·.push { ident, range := range.toLspRange text, stx := info.stx, ci, info, isBinder })) + get /-- There are several different identifiers that should be considered equal for the purpose of finding @@ -228,10 +289,10 @@ where 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 + | .fvar ma a, .fvar .. => .fvar ma a + | .fvar .., .const mb b => .const mb b + | .const ma a, .fvar .. => .const ma a + | .const ma a, .const .. => .const ma a -- compress `idMap` so that all identifiers in a class point to the best representative for id in «class» do @@ -253,9 +314,11 @@ where insertIdMap id baseId -- apply `FVarAliasInfo` - trees.forM (·.visitM' (postNode := fun _ info _ => do + trees.forM (·.visitM' (postNode := fun ci info _ => do if let .ofFVarAliasInfo ai := info then - insertIdMap (.fvar ai.id) (.fvar ai.baseId))) + -- FVars can only be aliases of FVars of the same file / module + let mod := ci.env.header.mainModule + insertIdMap (.fvar mod ai.id) (.fvar mod ai.baseId))) get @@ -267,6 +330,11 @@ where if baseId != id then modify (·.insert id baseId) +/-- +Groups `refs` by identifier and range s.t. references with the same identifier and range +are added to the `aliases` of the representative of the group. +Yields to separate groups for declaration and usages if `allowSimultaneousBinderUse` is set. +-/ def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := false) : Array Reference := Id.run do let mut refsByIdAndRange : HashMap (RefIdent × Option Bool × Lsp.Range) Reference := HashMap.empty for ref in refs do @@ -279,6 +347,10 @@ def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := fals let dedupedRefs := refsByIdAndRange.fold (init := #[]) fun refs _ ref => refs.push ref return dedupedRefs.qsort (·.range < ·.range) +/-- +Finds all references in `trees` and deduplicates the result. +See `dedupReferences` and `combineIdents`. +-/ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool := true) (allowSimultaneousBinderUse := false) : ModuleRefs := Id.run do let mut refs := @@ -287,12 +359,13 @@ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool : findReferences text trees if !localVars then refs := refs.filter fun - | { ident := RefIdent.fvar _, .. } => false + | { ident := RefIdent.fvar .., .. } => false | _ => true refs.foldl (init := HashMap.empty) fun m ref => m.addRef ref /-! # Collecting and maintaining reference info from different sources -/ +/-- References from ilean files and current ilean information from file workers. -/ structure References where /-- References loaded from ilean files -/ ileans : HashMap Name (System.FilePath × Lsp.ModuleRefs) @@ -301,17 +374,25 @@ structure References where namespace References +/-- No ilean files, no information from workers. -/ def empty : References := { ileans := HashMap.empty, workers := HashMap.empty } +/-- Adds the contents of an ilean file `ilean` at `path` to `self`. -/ def addIlean (self : References) (path : System.FilePath) (ilean : Ilean) : References := { self with ileans := self.ileans.insert ilean.module (path, ilean.references) } +/-- Removes the ilean file data at `path` from `self`. -/ def removeIlean (self : References) (path : System.FilePath) : References := let namesToRemove := self.ileans.toList.filter (fun (_, p, _) => p == path) |>.map (fun (n, _, _) => n) namesToRemove.foldl (init := self) fun self name => { self with ileans := self.ileans.erase name } +/-- +Updates the worker references in `self` with the `refs` of the worker managing the module `name`. +Replaces the current references with `refs` if `version` is newer than the current version managed +in `refs` and otherwise merges the reference data if `version` is equal to the current version. +-/ def updateWorkerRefs (self : References) (name : Name) (version : Nat) (refs : Lsp.ModuleRefs) : References := Id.run do if let some (currVersion, _) := self.workers.find? name then if version > currVersion then @@ -323,78 +404,118 @@ def updateWorkerRefs (self : References) (name : Name) (version : Nat) (refs : L return { self with workers := self.workers.insert name (version, merged) } return self +/-- +Replaces the worker references in `self` with the `refs` of the worker managing the module `name` +if `version` is newer than the current version managed in `refs`. +-/ def finalizeWorkerRefs (self : References) (name : Name) (version : Nat) (refs : Lsp.ModuleRefs) : References := Id.run do if let some (currVersion, _) := self.workers.find? name then if version < currVersion then return self return { self with workers := self.workers.insert name (version, refs) } +/-- Erases all worker references in `self` for the worker managing `name`. -/ def removeWorkerRefs (self : References) (name : Name) : References := { self with workers := self.workers.erase name } +/-- Yields a map from all modules to all of their references. -/ def allRefs (self : References) : HashMap Name Lsp.ModuleRefs := - let ileanRefs := self.ileans.toList.foldl (init := HashMap.empty) fun m (name, _, refs) => m.insert name refs - self.workers.toList.foldl (init := ileanRefs) fun m (name, _, refs) => m.insert name refs + let ileanRefs := self.ileans.toArray.foldl (init := HashMap.empty) fun m (name, _, refs) => m.insert name refs + self.workers.toArray.foldl (init := ileanRefs) fun m (name, _, refs) => m.insert name refs +/-- +Yields all references in `self` for `ident`, as well as the `DocumentUri` that each +reference occurs in. +-/ +def allRefsFor + (self : References) + (srcSearchPath : SearchPath) + (ident : RefIdent) + : IO (Array (DocumentUri × Lsp.RefInfo)) := do + let refsToCheck := match ident with + | RefIdent.const .. => self.allRefs.toArray + | RefIdent.fvar identModule .. => + match self.allRefs.find? identModule with + | none => #[] + | some refs => #[(identModule, refs)] + let mut result := #[] + for (module, refs) in refsToCheck do + let some info := refs.find? ident + | continue + let some path ← srcSearchPath.findModuleWithExt "lean" module + | continue + -- 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 + result := result.push (uri, info) + return result + +/-- Yields all references in `module` at `pos`. -/ def findAt (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do if let some refs := self.allRefs.find? module then return refs.findAt pos includeStop #[] +/-- Yields the first reference in `module` at `pos`. -/ def findRange? (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Option Range := do let refs ← self.allRefs.find? module refs.findRange? pos includeStop +/-- Location and parent declaration of a reference. -/ structure DocumentRefInfo where + /-- Location of the reference. -/ location : Location + /-- Parent declaration of the reference. -/ parentInfo? : Option RefInfo.ParentDecl -def referringTo (self : References) (identModule : Name) (ident : RefIdent) (srcSearchPath : SearchPath) - (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 - | none => [] - | some refs => [(identModule, refs)] +/-- Yields locations and parent declaration for all references referring to `ident`. -/ +def referringTo + (self : References) + (srcSearchPath : SearchPath) + (ident : RefIdent) + (includeDefinition : Bool := true) + : IO (Array DocumentRefInfo) := do let mut result := #[] - for (module, refs) in refsToCheck do - if let some info := refs.find? ident 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 - if includeDefinition then - 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?⟩ + for (moduleUri, info) in ← self.allRefsFor srcSearchPath ident do + if includeDefinition then + if let some ⟨range, parentDeclInfo?⟩ := info.definition? then + result := result.push ⟨⟨moduleUri, range⟩, parentDeclInfo?⟩ + for ⟨range, parentDeclInfo?⟩ in info.usages do + result := result.push ⟨⟨moduleUri, range⟩, parentDeclInfo?⟩ return result -def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath) +/-- Yields the definition location of `ident`. -/ +def definitionOf? + (self : References) + (ident : RefIdent) + (srcSearchPath : SearchPath) : IO (Option DocumentRefInfo) := do - for (module, refs) in self.allRefs.toList do - if let some info := refs.find? ident 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, definitionRange⟩, definitionParentDeclInfo?⟩ + for (moduleUri, info) in ← self.allRefsFor srcSearchPath ident do + let some ⟨definitionRange, definitionParentDeclInfo?⟩ := info.definition? + | continue + return some ⟨⟨moduleUri, definitionRange⟩, definitionParentDeclInfo?⟩ return none -def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter : Name → Option α) - (maxAmount? : Option Nat := none) : IO $ Array (α × Location) := do +/-- Yields all definitions matching the given `filter`. -/ +def definitionsMatching + (self : References) + (srcSearchPath : SearchPath) + (filter : Name → Option α) + (maxAmount? : Option Nat := none) : IO $ Array (α × Location) := do let mut result := #[] for (module, refs) in self.allRefs.toList do - 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 ⟨definitionRange, _⟩) := (ident, info.definition?) then - if let some a := filter name then - result := result.push (a, ⟨uri, definitionRange⟩) - if let some maxAmount := maxAmount? then - if result.size >= maxAmount then - return result + let some path ← srcSearchPath.findModuleWithExt "lean" module + | continue + let uri := System.Uri.pathToUri <| ← IO.FS.realPath path + for (ident, info) in refs.toList do + let (RefIdent.const _ name, some ⟨definitionRange, _⟩) := (ident, info.definition?) + | continue + let some a := filter name + | continue + result := result.push (a, ⟨uri, definitionRange⟩) + if let some maxAmount := maxAmount? then + if result.size >= maxAmount then + return result return result end References diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 62ea33930b..b07428744e 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -14,17 +14,20 @@ import Lean.Server.InfoUtils namespace IO +/-- Throws an `IO.userError`. -/ def throwServerError (err : String) : IO α := throw (userError err) namespace FS.Stream -/-- Chains two streams by creating a new stream s.t. writing to it +/-- +Chains two streams by creating a new stream s.t. writing to it just writes to `a` but reading from it also duplicates the read output into `b`, c.f. `a | tee b` on Unix. NB: if `a` is written to but this stream is never read from, the output will *not* be duplicated. Use this if you only care -about the data that was actually read. -/ +about the data that was actually read. +-/ def chainRight (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream := { a with flush := a.flush *> b.flush @@ -66,18 +69,30 @@ end IO namespace Lean.Server +/-- Meta-Data of a document. -/ structure DocumentMeta where + /-- URI where the document is located. -/ uri : Lsp.DocumentUri + /-- Version number of the document. Incremented whenever the document is edited. -/ version : Nat + /-- Current text of the document. -/ text : FileMap + /-- + Controls when dependencies of the document are built on `textDocument/didOpen` notifications. + -/ dependencyBuildMode : Lsp.DependencyBuildMode deriving Inhabited +/-- Extracts an `InputContext` from `doc`. -/ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where input := doc.text.source fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString fileMap := doc.text +/-- +Replaces the range `r` (using LSP UTF-16 positions) in `text` (using UTF-8 positions) +with `newText`. +-/ def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap := let start := text.lspPosToUtf8Pos r.start let «end» := text.lspPosToUtf8Pos r.«end» @@ -87,8 +102,10 @@ def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMa open IO -/-- Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR -if that envvar is set. -/ +/-- +Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR +if that envvar is set. +-/ def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := do match (← IO.getEnv "LEAN_SERVER_LOG_DIR") with | none => pure h @@ -150,5 +167,22 @@ def mkApplyWorkspaceEditRequest (params : ApplyWorkspaceEditParams) : end Lean.Server +/-- +Converts an UTF-8-based `String.range` in `text` to an equivalent LSP UTF-16-based `Lsp.Range` +in `text`. +-/ def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range := ⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩ + +open Lean in +/-- +Attempts to find a module name in the roots denoted by `srcSearchPath` for `uri`. +Fails if `uri` is not a `file://` uri or if the given `uri` cannot be found in `srcSearchPath`. +-/ +def System.SearchPath.searchModuleNameOfUri + (srcSearchPath : SearchPath) + (uri : Lsp.DocumentUri) + : IO (Option Name) := do + let some path := Uri.fileUriToPath? uri + | return none + searchModuleNameOfFileName path srcSearchPath diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index d71bf587d0..239cf9ab7a 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -202,9 +202,9 @@ section ServerM def eraseFileWorker (uri : DocumentUri) : ServerM Unit := do let s ← read s.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri) - if let some path := fileUriToPath? uri then - if let some module ← searchModuleNameOfFileName path s.srcSearchPath then - s.references.modify fun refs => refs.removeWorkerRefs module + let some module ← s.srcSearchPath.searchModuleNameOfUri uri + | return + s.references.modify fun refs => refs.removeWorkerRefs module def log (msg : String) : ServerM Unit := do let st ← read @@ -213,17 +213,17 @@ section ServerM def handleIleanInfoUpdate (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.updateWorkerRefs module params.version params.references + let some module ← s.srcSearchPath.searchModuleNameOfUri fw.doc.uri + | return + 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 + let some module ← s.srcSearchPath.searchModuleNameOfUri fw.doc.uri + | return + 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. -/ @@ -408,31 +408,35 @@ section RequestHandling open FuzzyMatching def findDefinitions (p : TextDocumentPositionParams) : ServerM <| Array Location := do + let srcSearchPath := (← read).srcSearchPath + let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri + | return #[] + let references ← (← read).references.get let mut definitions := #[] - if let some path := fileUriToPath? p.textDocument.uri then - let srcSearchPath := (← read).srcSearchPath - 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 ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then - definitions := definitions.push definitionLocation + for ident in references.findAt module p.position (includeStop := true) do + if let some ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then + definitions := definitions.push definitionLocation return definitions def handleReference (p : ReferenceParams) : ServerM (Array Location) := do + let srcSearchPath := (← read).srcSearchPath + let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri + | return #[] + let references ← (← read).references.get let mut result := #[] - if let some path := fileUriToPath? p.textDocument.uri then - let srcSearchPath := (← read).srcSearchPath - 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.map (·.location) + for ident in references.findAt module p.position (includeStop := true) do + let identRefs ← references.referringTo srcSearchPath ident + p.context.includeDeclaration + result := result.append <| identRefs.map (·.location) return result -/-- Used in `CallHierarchyItem.data?` to retain the full call hierarchy item name. -/ +/-- +Used in `CallHierarchyItem.data?` to retain all the data needed to quickly re-identify the +call hierarchy item. +-/ structure CallHierarchyItemData where - name : Name + module : Name + name : Name deriving FromJson, ToJson /-- @@ -441,13 +445,16 @@ Extracts the CallHierarchyItemData from `item.data?` and returns `none` if this def CallHierarchyItemData.fromItem? (item : CallHierarchyItem) : Option CallHierarchyItemData := do fromJson? (← item.data?) |>.toOption -private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath) +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 => + | .const definitionModule 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 @@ -461,12 +468,19 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear uri := definitionLocation.uri range := definitionLocation.range, selectionRange := definitionLocation.range - data? := toJson { name := definitionName : CallHierarchyItemData } + data? := toJson { + module := definitionModule + name := definitionName + : CallHierarchyItemData + } } | _ => let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? | return none + let some definitionModule ← srcSearchPath.searchModuleNameOfUri definitionLocation.uri + | return none + -- Remove private header from name let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName @@ -476,22 +490,26 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear uri := definitionLocation.uri range := parentDeclRange, selectionRange := parentDeclSelectionRange - data? := toJson { name := parentDeclName : CallHierarchyItemData } + data? := toJson { + -- Assumption: The parent declaration of a reference lives in the same module + -- as the reference. + module := definitionModule + name := parentDeclName + : CallHierarchyItemData + } } 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 + let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri | 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 + let items ← idents.filterMapM fun ident => + callHierarchyItemOf? references ident srcSearchPath return items.qsort (·.name < ·.name) def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) @@ -499,21 +517,19 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) let some itemData := CallHierarchyItemData.fromItem? p.item | return #[] - 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 itemData.name) srcSearchPath false + let identRefs ← references.referringTo srcSearchPath (.const itemData.module itemData.name) false - let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do + let incomingCalls ← identRefs.filterMapM fun ⟨location, parentDecl?⟩ => do let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? | return none + let some refModule ← srcSearchPath.searchModuleNameOfUri location.uri + | return none + -- Remove private header from name let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName @@ -524,7 +540,11 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) uri := location.uri range := parentDeclRange selectionRange := parentDeclSelectionRange - data? := toJson { name := parentDeclName : CallHierarchyItemData } + data? := toJson { + module := refModule + name := parentDeclName + : CallHierarchyItemData + } } fromRanges := #[location.range] } @@ -547,11 +567,9 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) let some itemData := CallHierarchyItemData.fromItem? p.item | return #[] - let some path := fileUriToPath? p.item.uri - | return #[] - let srcSearchPath := (← read).srcSearchPath - let some module ← searchModuleNameOfFileName path srcSearchPath + + let some module ← srcSearchPath.searchModuleNameOfUri p.item.uri | return #[] let references ← (← read).references.get @@ -611,12 +629,11 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf def handlePrepareRename (p : PrepareRenameParams) : ServerM (Option Range) := do -- This just checks that the cursor is over a renameable identifier - if let some path := System.Uri.fileUriToPath? p.textDocument.uri then - let srcSearchPath := (← read).srcSearchPath - if let some module ← searchModuleNameOfFileName path srcSearchPath then - let references ← (← read).references.get - return references.findRange? module p.position (includeStop := true) - return none + let srcSearchPath := (← read).srcSearchPath + let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri + | return none + let references ← (← read).references.get + return references.findRange? module p.position (includeStop := true) def handleRename (p : RenameParams) : ServerM Lsp.WorkspaceEdit := do if (String.toName p.newName).isAnonymous then diff --git a/tests/lean/run/944.lean b/tests/lean/run/944.lean index 31ba45504d..17efd16afd 100644 --- a/tests/lean/run/944.lean +++ b/tests/lean/run/944.lean @@ -11,10 +11,10 @@ open Lsp def identOf : Info → Option (RefIdent × Bool) | .ofTermInfo ti => match ti.expr with - | .const n .. => some (.const n, ti.isBinder) - | .fvar id .. => some (.fvar id, ti.isBinder) + | .const n .. => some (.const `anonymous n, ti.isBinder) + | .fvar id .. => some (.fvar `anonymous id, ti.isBinder) | _ => none - | .ofFieldInfo fi => some (.const fi.projName, false) + | .ofFieldInfo fi => some (.const `anonymous fi.projName, false) | _ => none def isConst (e : Expr) : Bool :=