feat: LSP rename support

Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs

@@ -310,8 +310,9 @@ private async Task TestCodeAction(string source) {
               codeAction = await RequestResolveCodeAction(codeAction);
               var textDocumentEdit = codeAction.Edit?.DocumentChanges?.Single().TextDocumentEdit;
               Assert.NotNull(textDocumentEdit);
-              var modifiedOutput = string.Join("\n", ApplyEdits(textDocumentEdit, output)).Replace("\r\n", "\n");
-              var expectedOutput = string.Join("\n", ApplySingleEdit(ToLines(output), expectedRange, expectedNewText)).Replace("\r\n", "\n");
+              var modifiedOutput = DocumentEdits.ApplyEdits(textDocumentEdit, output);
+              var expectedOutput =
+                DocumentEdits.ApplyEdit(DocumentEdits.ToLines(output), expectedRange, expectedNewText);
               Assert.Equal(expectedOutput, modifiedOutput);
             }
           }
@@ -324,33 +325,5 @@ private async Task TestCodeAction(string source) {
 
     public CodeActionTest(ITestOutputHelper output) : base(output) {
     }
-
-    private static List<string> ApplyEdits(TextDocumentEdit textDocumentEdit, string output) {
-      var inversedEdits = textDocumentEdit.Edits.ToList()
-        .OrderByDescending(x => x.Range.Start.Line)
-        .ThenByDescending(x => x.Range.Start.Character);
-      var modifiedOutput = ToLines(output);
-      foreach (var textEdit in inversedEdits) {
-        modifiedOutput = ApplySingleEdit(modifiedOutput, textEdit.Range, textEdit.NewText);
-      }
-
-      return modifiedOutput;
-    }
-
-    private static List<string> ToLines(string output) {
-      return output.ReplaceLineEndings("\n").Split("\n").ToList();
-    }
-
-    private static List<string> ApplySingleEdit(List<string> modifiedOutput, Range range, string newText) {
-      var lineStart = modifiedOutput[range.Start.Line];
-      var lineEnd = modifiedOutput[range.End.Line];
-      modifiedOutput[range.Start.Line] =
-        lineStart.Substring(0, range.Start.Character) + newText +
-        lineEnd.Substring(range.End.Character);
-      modifiedOutput = modifiedOutput.Take(range.Start.Line).Concat(
-        modifiedOutput.Skip(range.End.Line)
-      ).ToList();
-      return modifiedOutput;
-    }
   }
 }

Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs

@@ -1,9 +1,6 @@
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using OmniSharp.Extensions.LanguageServer.Protocol;
-using OmniSharp.Extensions.LanguageServer.Protocol.Document;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
-using OmniSharp.Extensions.LanguageServer.Protocol.Progress;
-using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
@@ -78,6 +75,11 @@ requires Err?
       await AssertPositionsLineUpWithRanges(source);
     }
 
+    /// <summary>
+    /// Given <paramref name="source"/> with N positions, for each K from 0 to N exclusive,
+    /// assert that a RequestDefinition at position K
+    /// returns either the Kth range, or the range with key K (as a string).
+    /// </summary>
     private async Task AssertPositionsLineUpWithRanges(string source) {
       MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource,
         out var positions, out var ranges);
@@ -126,10 +128,10 @@ public async Task FunctionCallAndGotoOnDeclaration() {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
 
       var fibonacciSpecOnItself = (await RequestDefinition(documentItem, positions[0]));
-      Assert.False(fibonacciSpecOnItself.Any());
+      Assert.Single(fibonacciSpecOnItself);
 
       var nOnItself = (await RequestDefinition(documentItem, positions[1]));
-      Assert.False(nOnItself.Any());
+      Assert.Single(nOnItself);
 
       var fibonacciCall = (await RequestDefinition(documentItem, positions[2])).Single();
       Assert.Equal(ranges[0], fibonacciCall.Location!.Range);
@@ -209,7 +211,7 @@ method DoIt() {
       Assert.Equal(ranges[1], usizeReference.Location.Range);
 
       var lengthDefinition = (await RequestDefinition(documentItem, positions[1]));
-      Assert.False(lengthDefinition.Any());
+      Assert.Single(lengthDefinition);
 
       var providerImport = (await RequestDefinition(documentItem, positions[0])).Single();
       Assert.Equal(ranges[0], providerImport.Location!.Range);

Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs

@@ -0,0 +1,185 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.Immutable;
+using System.IO;
+using System.Linq;
+using System.Threading.Tasks;
+using JetBrains.Annotations;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Refactoring {
+  public class RenameTest : ClientBasedLanguageServerTest {
+    [Fact]
+    public async Task ImplicitProjectFails() {
+      var source = @"
+const i := 0
+".TrimStart();
+
+      var documentItem = await CreateAndOpenTestDocument(source);
+      await Assert.ThrowsAnyAsync<Exception>(() => RequestRename(documentItem, new Position(0, 6), "j"));
+    }
+
+    [Fact]
+    public async Task InvalidNewNameIsNoOp() {
+      var documentItem = await CreateAndOpenTestDocument("");
+      var workspaceEdit = await RequestRename(documentItem, new Position(0, 0), "");
+      Assert.Null(workspaceEdit);
+    }
+
+    [Fact]
+    public async Task RenameNonSymbolFails() {
+      var tempDir = await SetUpProjectFile();
+      var documentItem = await CreateAndOpenTestDocument("module Foo {}", Path.Combine(tempDir, "tmp.dfy"));
+      var workspaceEdit = await RequestRename(documentItem, new Position(0, 6), "space");
+      Assert.Null(workspaceEdit);
+    }
+
+    [Fact]
+    public async Task RenameDeclarationRenamesUsages() {
+      var source = @"
+const [>><i<] := 0
+method M() {
+  print [>i<] + [>i<];
+}
+".TrimStart();
+
+      var tempDir = await SetUpProjectFile();
+      await AssertRangesRenamed(source, tempDir, "foobar");
+    }
+
+    [Fact]
+    public async Task RenameUsageRenamesDeclaration() {
+      var source = @"
+method [>foobar<]()
+method U() { [>><foobar<](); }
+".TrimStart();
+
+      var tempDir = await SetUpProjectFile();
+      await AssertRangesRenamed(source, tempDir, "M");
+    }
+
+    [Fact]
+    public async Task RenameUsageRenamesOtherUsages() {
+      var source = @"
+module [>A<] {}
+module B { import [>A<] }
+module C { import [>><A<] }
+module D { import [>A<] }
+".TrimStart();
+
+      var tempDir = await SetUpProjectFile();
+      await AssertRangesRenamed(source, tempDir, "AAA");
+    }
+
+    [Fact]
+    public async Task RenameDeclarationAcrossFiles() {
+      var sourceA = @"
+module A {
+  class [>><C<] {}
+}
+".TrimStart();
+      var sourceB = @"
+module B {
+  import A
+  method M(c: A.[>C<]) {}
+}
+".TrimStart();
+
+      var tempDir = await SetUpProjectFile();
+      await AssertRangesRenamed(new[] { sourceA, sourceB }, tempDir, "CCC");
+    }
+
+    [Fact]
+    public async Task RenameUsageAcrossFiles() {
+      var sourceA = @"
+abstract module [>A<] {}
+".TrimStart();
+      var sourceB = @"
+abstract module B { import [>><A<] }
+".TrimStart();
+
+      var tempDir = await SetUpProjectFile();
+      await AssertRangesRenamed(new[] { sourceA, sourceB }, tempDir, "AAA");
+    }
+
+    /// <summary>
+    /// Create an empty project file in a new temporary directory, and return the temporary directory's path.
+    /// </summary>
+    protected async Task<string> SetUpProjectFile() {
+      var tempDir = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+      Directory.CreateDirectory(tempDir);
+      var projectFilePath = Path.Combine(tempDir, DafnyProject.FileName);
+      await File.WriteAllTextAsync(projectFilePath, "");
+      return tempDir;
+    }
+
+    protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+      return base.SetUp(o => {
+        o.Set(ServerCommand.ProjectMode, true);
+        modifyOptions?.Invoke(o);
+      });
+    }
+
+    /// <summary>
+    /// Assert that after requesting a rename to <paramref name="newName"/>
+    /// at the markup position in <paramref name="source"/>
+    /// (there must be exactly one markup position),
+    /// all markup ranges are renamed.
+    /// </summary>
+    private async Task AssertRangesRenamed(string source, string tempDir, string newName) {
+      await AssertRangesRenamed(new[] { source }, tempDir, newName);
+    }
+
+    private record DocPosRange(TextDocumentItem Document, [CanBeNull] Position Position, ImmutableArray<Range> Ranges);
+
+    /// <summary>
+    /// Assert that after requesting a rename to <paramref name="newName"/>
+    /// at the markup position in <paramref name="sources"/>
+    /// (there must be exactly one markup position among all sources),
+    /// all markup ranges are renamed.
+    /// </summary>
+    private async Task AssertRangesRenamed(IEnumerable<string> sources, string tempDir, string newName) {
+      var items = sources.Select(async (source, sourceIndex) => {
+        MarkupTestFile.GetPositionsAndRanges(source, out var cleanSource,
+          out var positions, out var ranges);
+        var documentItem = await CreateAndOpenTestDocument(cleanSource, Path.Combine(tempDir, $"tmp{sourceIndex}.dfy"));
+        Assert.InRange(positions.Count, 0, 1);
+        return new DocPosRange(documentItem, positions.FirstOrDefault((Position)null), ranges);
+      }).Select(task => task.Result).ToImmutableList();
+
+      var itemWithPos = items.Single(item => item.Position != null);
+      var workspaceEdit = await RequestRename(itemWithPos.Document, itemWithPos.Position, newName);
+      Assert.NotNull(workspaceEdit.Changes);
+
+      foreach (var (document, _, ranges) in items) {
+        Assert.Contains(document.Uri, workspaceEdit.Changes);
+        var editedText = DocumentEdits.ApplyEdits(workspaceEdit.Changes[document.Uri], document.Text);
+        var expectedChanges = ranges.Select(range => new TextEdit {
+          Range = range,
+          NewText = newName,
+        });
+        var expectedText = DocumentEdits.ApplyEdits(expectedChanges, document.Text);
+        Assert.Equal(expectedText, editedText);
+      }
+    }
+
+    private async Task<WorkspaceEdit> RequestRename(
+      TextDocumentItem documentItem, Position position, string newName) {
+      await AssertNoResolutionErrors(documentItem);
+      return await client.RequestRename(
+        new RenameParams {
+          TextDocument = documentItem.Uri,
+          Position = position,
+          NewName = newName,
+        }, CancellationToken);
+    }
+
+    public RenameTest(ITestOutputHelper output) : base(output) {
+    }
+  }
+}

Source/DafnyLanguageServer.Test/Util/DocumentEdits.cs

@@ -0,0 +1,44 @@
+using System.Collections.Generic;
+using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+
+public class DocumentEdits {
+  public static string ApplyEdits(TextDocumentEdit textDocumentEdit, string text) {
+    return ApplyEdits(textDocumentEdit.Edits, text);
+  }
+
+  public static string ApplyEdits(IEnumerable<TextEdit> edits, string text) {
+    var inversedEdits = edits.ToList()
+      .OrderByDescending(x => x.Range.Start.Line)
+      .ThenByDescending(x => x.Range.Start.Character);
+    var modifiedText = ToLines(text);
+    foreach (var textEdit in inversedEdits) {
+      modifiedText = ApplyEditLinewise(modifiedText, textEdit.Range, textEdit.NewText);
+    }
+
+    return string.Join("\n", modifiedText);
+  }
+
+
+  public static List<string> ToLines(string text) {
+    return text.ReplaceLineEndings("\n").Split("\n").ToList();
+  }
+
+  public static string FromLines(List<string> lines) {
+    return string.Join("\n", lines).ReplaceLineEndings("\n");
+  }
+
+  public static string ApplyEdit(List<string> lines, Range range, string newText) {
+    return FromLines(ApplyEditLinewise(lines, range, newText));
+  }
+
+  public static List<string> ApplyEditLinewise(List<string> lines, Range range, string newText) {
+    var lineStart = lines[range.Start.Line];
+    var lineEnd = lines[range.End.Line];
+    lines[range.Start.Line] = lineStart[..range.Start.Character] + newText + lineEnd[range.End.Character..];
+    lines = lines.Take(range.Start.Line).Concat(lines.Skip(range.End.Line)).ToList();
+    return lines;
+  }
+}

Source/DafnyLanguageServer/Handlers/DafnyReferencesHandler.cs

@@ -1,4 +1,3 @@
-using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace;
@@ -36,14 +35,9 @@ public override async Task<LocationContainer> Handle(ReferenceParams request, Ca
 
       var requestUri = request.TextDocument.Uri.ToUri();
       var declaration = state.SymbolTable.GetDeclaration(requestUri, request.Position);
-
-      // The declaration graph is not reflexive, so the position might be on a declaration; return references to it
-      if (declaration == null) {
-        return state.SymbolTable.GetUsages(requestUri, request.Position).ToArray();
-      }
-
-      // If the position is not on a declaration, return references to its declaration
-      return state.SymbolTable.GetUsages(declaration.Uri.ToUri(), declaration.Range.Start).ToArray();
+      return declaration == null
+        ? new LocationContainer()
+        : LocationContainer.From(state.SymbolTable.GetUsages(declaration.Uri.ToUri(), declaration.Range.Start));
     }
   }
 }