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

@@ -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]}

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

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

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

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

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

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":

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

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": {}}