From b97b0ad2aaea49a2db3ac0543443ec72bd97dfdc Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 21 Nov 2023 04:10:52 -0800 Subject: [PATCH] feat: rename request handler (#2462) This implements a request handler for the `textDocument/rename` LSP request, enabling renames via F2. It handles both local renames (e.g. `let x := 1; x` to `let y := 1; y`) as well as global renames (definitions). Unfortunately it does not work for "orphan" files outside a project, as it uses ilean data for the current file and this does not seem to be saved for orphan files. As a result, the test file does not work, although one can manually test the implementation against a project such as mathlib. (This issue already exists for the "references" request, e.g. ctrl click on the first `x` in `let x := 1; x` takes you to the second one only if you are not in an orphan file.) * Fixes leanprover-community/mathlib4#7124 --- src/Lean/Data/Lsp/Basic.lean | 23 +++++++---- src/Lean/Data/Lsp/Capabilities.lean | 1 + src/Lean/Data/Lsp/LanguageFeatures.lean | 11 ++++++ src/Lean/Elab/Structure.lean | 11 +++--- src/Lean/Server/References.lean | 34 +++++++++++----- src/Lean/Server/Watchdog.lean | 36 ++++++++++++++++- .../interactive/codeaction.lean.expected.out | 4 +- tests/lean/interactive/rename.lean | 39 +++++++++++++++++++ .../lean/interactive/rename.lean.expected.out | 19 +++++++++ 9 files changed, 152 insertions(+), 26 deletions(-) create mode 100644 tests/lean/interactive/rename.lean create mode 100644 tests/lean/interactive/rename.lean.expected.out diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index dfebbef026..f0baf7b6de 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -206,7 +206,7 @@ instance : FromJson DocumentChange where [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspaceEdit) -/ structure WorkspaceEdit where /-- Changes to existing resources. -/ - changes : RBMap DocumentUri TextEditBatch compare := ∅ + changes? : Option (RBMap DocumentUri TextEditBatch compare) := none /-- Depending on the client capability `workspace.workspaceEdit.resourceOperations` document changes are either an array of `TextDocumentEdit`s to express changes to n different text @@ -220,14 +220,14 @@ structure WorkspaceEdit where If a client neither supports `documentChanges` nor `workspace.workspaceEdit.resourceOperations` then only plain `TextEdit`s using the `changes` property are supported. -/ - documentChanges : Array DocumentChange := ∅ + documentChanges? : Option (Array DocumentChange) := none /-- A map of change annotations that can be referenced in `AnnotatedTextEdit`s or create, rename and delete file / folder operations. Whether clients honor this property depends on the client capability `workspace.changeAnnotationSupport`. -/ - changeAnnotations : RBMap String ChangeAnnotation compare := ∅ + changeAnnotations? : Option (RBMap String ChangeAnnotation compare) := none deriving ToJson, FromJson namespace WorkspaceEdit @@ -236,13 +236,22 @@ instance : EmptyCollection WorkspaceEdit := ⟨{}⟩ instance : Append WorkspaceEdit where append x y := { - changes := x.changes.mergeBy (fun _ v₁ v₂ => v₁ ++ v₂) y.changes - documentChanges := x.documentChanges ++ y.documentChanges - changeAnnotations := x.changeAnnotations.mergeBy (fun _ _v₁ v₂ => v₂) y.changeAnnotations + changes? := + match x.changes?, y.changes? with + | v, none | none, v => v + | some x, some y => x.mergeBy (fun _ v₁ v₂ => v₁ ++ v₂) y + documentChanges? := + match x.documentChanges?, y.documentChanges? with + | v, none | none, v => v + | some x, some y => x ++ y + changeAnnotations? := + match x.changeAnnotations?, y.changeAnnotations? with + | v, none | none, v => v + | some x, some y => x.mergeBy (fun _ _v₁ v₂ => v₂) y } def ofTextDocumentEdit (e : TextDocumentEdit) : WorkspaceEdit := - { documentChanges := #[DocumentChange.edit e]} + { documentChanges? := #[DocumentChange.edit e]} def ofTextEdit (doc : VersionedTextDocumentIdentifier) (te : TextEdit) : WorkspaceEdit := ofTextDocumentEdit { textDocument := doc, edits := #[te]} diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index e6c178544f..4cb723969d 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 + renameProvider? : Option RenameOptions := none workspaceSymbolProvider : Bool := false foldingRangeProvider : Bool := false semanticTokensProvider? : Option SemanticTokensOptions := none diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 32bd9c4b1a..99fdcd5c5f 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -351,5 +351,16 @@ structure FoldingRange where kind? : Option FoldingRangeKind := none deriving ToJson +structure RenameOptions where + prepareProvider : Bool := false + deriving FromJson, ToJson + +structure RenameParams extends TextDocumentPositionParams where + newName : String + deriving FromJson, ToJson + +structure PrepareRenameParams extends TextDocumentPositionParams + deriving FromJson, ToJson + end Lsp end Lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 1525124cd9..2406b49bad 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -101,8 +101,9 @@ leading_parser try (declModifiers >> ident >> " :: ") private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM StructCtorView := do let useDefault := do let declName := structDeclName ++ defaultCtorName - addAuxDeclarationRanges declName structStx[2] structStx[2] - pure { ref := structStx, modifiers := {}, name := defaultCtorName, declName } + let ref := structStx[1].mkSynthetic + addAuxDeclarationRanges declName ref ref + pure { ref, modifiers := {}, name := defaultCtorName, declName } if structStx[5].isNone then useDefault else @@ -123,7 +124,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let declName ← applyVisibility ctorModifiers.visibility declName addDocString' declName ctorModifiers.docString? addAuxDeclarationRanges declName ctor[1] ctor[1] - pure { ref := ctor, name, modifiers := ctorModifiers, declName } + pure { ref := ctor[1], name, modifiers := ctorModifiers, declName } def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do if modifiers.isNoncomputable then @@ -840,8 +841,8 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do pure (info.isSubobject && decl.binderInfo.isInstImplicit) withSaveInfoContext do -- save new env Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName) - if let some _ := view.ctor.ref[1].getPos? (canonicalOnly := true) then - Term.addTermInfo' view.ctor.ref[1] (← mkConstWithLevelParams view.ctor.declName) (isBinder := true) + if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then + Term.addTermInfo' view.ctor.ref (← mkConstWithLevelParams view.ctor.declName) (isBinder := true) for field in view.fields do -- may not exist if overriding inherited field if (← getEnv).contains field.declName then diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 44fb928f3c..d7bfa3af00 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -72,30 +72,42 @@ def merge (a : RefInfo) (b : RefInfo) : RefInfo := usages := a.usages.append b.usages } -def contains (self : RefInfo) (pos : Lsp.Position) : Bool := Id.run do +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 true + return range for range in self.usages do if contains range pos then - return true - false + return range + none where contains (range : Lsp.Range) (pos : Lsp.Position) : Bool := - range.start <= pos && pos < range.end + -- 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) + +def contains (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Bool := Id.run do + (self.findRange? pos includeStop).isSome end Lean.Lsp.RefInfo namespace Lean.Lsp.ModuleRefs open Server -def findAt (self : ModuleRefs) (pos : Lsp.Position) : Array RefIdent := Id.run do +def findAt (self : ModuleRefs) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do let mut result := #[] for (ident, info) in self.toList do - if info.contains pos then + if info.contains pos includeStop then result := result.push ident result +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 + none + end Lean.Lsp.ModuleRefs namespace Lean.Server @@ -270,11 +282,15 @@ 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 -def findAt (self : References) (module : Name) (pos : Lsp.Position) : Array RefIdent := Id.run do +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 + return refs.findAt pos includeStop #[] +def findRange? (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Option Range := do + let refs ← self.allRefs.find? module + refs.findRange? pos includeStop + def referringTo (self : References) (identModule : Name) (ident : RefIdent) (srcSearchPath : SearchPath) (includeDefinition : Bool := true) : IO (Array Location) := do let refsToCheck := match ident with diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index d517c46deb..a47b1ab255 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -352,7 +352,7 @@ def findDefinitions (p : TextDocumentPositionParams) : ServerM <| Array Location 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 do + for ident in references.findAt module p.position (includeStop := true) do if let some definition ← references.definitionOf? ident srcSearchPath then definitions := definitions.push definition return definitions @@ -363,7 +363,7 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do 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 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 return result @@ -386,6 +386,33 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf |>.map fun ((name, _), location) => { name, kind := SymbolKind.constant, location } +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 + +def handleRename (p : RenameParams) : ServerM Lsp.WorkspaceEdit := do + if (String.toName p.newName).isAnonymous then + throwServerError s!"Can't rename: `{p.newName}` is not an identifier" + let mut refs : HashMap DocumentUri (RBMap Lsp.Position Lsp.Position compare) := ∅ + for { uri, range } in (← handleReference { p with context.includeDeclaration := true }) do + refs := refs.insert uri <| (refs.findD uri ∅).insert range.start range.end + -- We have to filter the list of changes to put the ranges in order and + -- remove any duplicates or overlapping ranges, or else the rename will not apply + let changes := refs.fold (init := ∅) fun changes uri map => Id.run do + let mut last := ⟨0, 0⟩ + let mut arr := #[] + for (start, stop) in map do + if last ≤ start then + arr := arr.push { range := ⟨start, stop⟩, newText := p.newName } + last := stop + return changes.insert uri arr + return { changes? := some changes } + end RequestHandling section NotificationHandling @@ -507,6 +534,8 @@ section MessageHandling 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 def handleNotification (method : String) (params : Json) : ServerM Unit := do @@ -608,6 +637,9 @@ def mkLeanServerCapabilities : ServerCapabilities := { definitionProvider := true typeDefinitionProvider := true referencesProvider := true + renameProvider? := some { + prepareProvider := true + } workspaceSymbolProvider := true documentHighlightProvider := true documentSymbolProvider := true diff --git a/tests/lean/interactive/codeaction.lean.expected.out b/tests/lean/interactive/codeaction.lean.expected.out index feccb8bfbe..2f09c34825 100644 --- a/tests/lean/interactive/codeaction.lean.expected.out +++ b/tests/lean/interactive/codeaction.lean.expected.out @@ -7,9 +7,7 @@ [{"range": {"start": {"line": 30, "character": 4}, "end": {"line": 30, "character": 4}}, - "newText": "hello!!!"}]}], - "changes": {}, - "changeAnnotations": {}}} + "newText": "hello!!!"}]}]}} {"title": "a long-running action", "kind": "refactor", "data": diff --git a/tests/lean/interactive/rename.lean b/tests/lean/interactive/rename.lean new file mode 100644 index 0000000000..9554927272 --- /dev/null +++ b/tests/lean/interactive/rename.lean @@ -0,0 +1,39 @@ +-- Note: these tests do not work in the current test suite, you have +-- to run them inside a project + +variable (a : Nat) +def foo := + let a := 1; a + --^ textDocument/prepareRename + --^ textDocument/rename: {"newName": "blue"} + +structure Foo where + --^ textDocument/rename: {"newName": "Bar"} + a : Nat + deriving Repr + +#eval Foo.mk 1 + +namespace B + +structure Foo where + a : Nat + b : Nat + +def bar (x y : Nat) : Foo := + ⟨x, y⟩ + --^ textDocument/rename: {"newName": "z"} + +end B + +namespace Bar + + structure Foo where + --^ textDocument/rename: {"newName": "X"} + a : Nat + + def foobar (f : Foo) : Foo := f + +end Bar + +def foobar (f : Bar.Foo) : Bar.Foo := f diff --git a/tests/lean/interactive/rename.lean.expected.out b/tests/lean/interactive/rename.lean.expected.out new file mode 100644 index 0000000000..bf4b7aec4b --- /dev/null +++ b/tests/lean/interactive/rename.lean.expected.out @@ -0,0 +1,19 @@ +{"textDocument": {"uri": "file://rename.lean"}, + "position": {"line": 5, "character": 14}} +null +{"textDocument": {"uri": "file://rename.lean"}, + "position": {"line": 5, "character": 14}, + "newName": "blue"} +{"changes": {}} +{"textDocument": {"uri": "file://rename.lean"}, + "position": {"line": 9, "character": 10}, + "newName": "Bar"} +{"changes": {}} +{"textDocument": {"uri": "file://rename.lean"}, + "position": {"line": 23, "character": 6}, + "newName": "z"} +{"changes": {}} +{"textDocument": {"uri": "file://rename.lean"}, + "position": {"line": 30, "character": 12}, + "newName": "X"} +{"changes": {}}