[LSP] Add handler for workspace/symbol requests [dafny-lang#4619] (da…

…fny-lang#4620)

### Description

This implements a response for workspace/symbol queries as documented
here:

https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspace_symbol

This allows jumping to symbols by name across a workspace (e.g. in
VSCode, typing `#foo` in the navigation prompt allows jumping to an
identifier containing foo as a substring).

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

### How has this been tested
- Added unit tests in DafnyLanguageServer.Test.
- Manually tested on some projects.

Addresses [dafny-lang#4619](dafny-lang#4619)

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -46,6 +46,12 @@
     <None Update="Lookup\TestFiles\find-refs-b.dfy">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </None>
+    <None Update="Lookup\TestFiles\defines-foo.dfy">
+      <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+    </None>
+    <None Update="Lookup\TestFiles\includes-foo.dfy">
+      <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+    </None>
     <None Update="Synchronization\TestFiles\semanticError.dfy">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </None>

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -479,19 +479,6 @@ await AssertHoverMatches(documentItem, (2, 22),
       );
     }
 
-    private async Task<TextDocumentItem> GetDocumentItem(string source, string filename, bool includeProjectFile) {
-      var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
-      source = source.TrimStart();
-      if (includeProjectFile) {
-        var projectFile = CreateTestDocument("", Path.Combine(directory, DafnyProject.FileName));
-        await client.OpenDocumentAndWaitAsync(projectFile, CancellationToken);
-      }
-      var documentItem = CreateTestDocument(source, Path.Combine(directory, filename));
-      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      var document = await Projects.GetLastDocumentAsync(documentItem);
-      Assert.True(document is CompilationAfterResolution);
-      return documentItem;
-    }
 
     public HoverVerificationTest(ITestOutputHelper output) : base(output) {
     }

Source/DafnyLanguageServer.Test/Lookup/TestFiles/defines-foo.dfy

@@ -0,0 +1,3 @@
+method foo() returns (x: int) {
+    x := 42;
+}

Source/DafnyLanguageServer.Test/Lookup/TestFiles/includes-foo.dfy

@@ -0,0 +1,6 @@
+include "defines-foo.dfy"
+
+method bar() returns (x: int) {
+    var temp := foo();
+    x := temp + 2;
+}

Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs

@@ -0,0 +1,133 @@
+using System.Collections.Generic;
+using System.Collections.Immutable;
+using System.IO;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using OmniSharp.Extensions.LanguageServer.Protocol.Workspace;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
+
+  public class WorkspaceSymbolTest : ClientBasedLanguageServerTest {
+
+    [Fact]
+    public async Task WorkspaceSymbolsAcrossFiles() {
+      var cwd = Directory.GetCurrentDirectory();
+      // These tests are not inlined since a later test uses only "includes-foo.dfy", but not
+      // "defines-foo.dfy" but relies on the former existing. This would complicate
+      // the test setup when inlining the file contents.
+      var pathA = Path.Combine(cwd, "Lookup/TestFiles/defines-foo.dfy");
+      var pathB = Path.Combine(cwd, "Lookup/TestFiles/includes-foo.dfy");
+      var documentItemA = CreateTestDocument(await File.ReadAllTextAsync(pathA), pathA);
+      var documentItemB = CreateTestDocument(await File.ReadAllTextAsync(pathB), pathB);
+
+      await client.OpenDocumentAndWaitAsync(documentItemA, CancellationToken);
+      await client.OpenDocumentAndWaitAsync(documentItemB, CancellationToken);
+
+      var matchesFo = await client.RequestWorkspaceSymbols(
+        new WorkspaceSymbolParams {
+          Query = "fo"
+        }
+      );
+      Assert.Single(matchesFo);
+      Assert.Contains(matchesFo, si => si.Name == "foo" &&
+                                       si.Kind == SymbolKind.Method &&
+                                       si.Location.Uri.ToString().EndsWith("defines-foo.dfy"));
+
+      var matchesBar = await client.RequestWorkspaceSymbols(
+        new WorkspaceSymbolParams {
+          Query = "bar"
+        });
+      Assert.Single(matchesBar);
+      Assert.Contains(matchesBar, si => si.Name == "bar" &&
+                                        si.Kind == SymbolKind.Method &&
+                                        si.Location.Uri.ToString().EndsWith("includes-foo.dfy"));
+    }
+
+    [Fact]
+    public async Task AllRelevantSymbolKindsDetected() {
+      var documentItem = await GetDocumentItem(@"
+class TestClass {}
+
+module TestModule {}
+
+function TestFunction(): int { 42 }
+
+method TestMethod() returns (x: int) {
+  x := 42;
+}
+
+datatype TestDatatype = TestConstructor
+
+trait TestTrait {}
+
+predicate TestPredicate { false }", "test-workspace-symbols.dfy", false);
+
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+      var testSymbols = new List<string> {
+        "TestClass",
+        "TestModule",
+        "TestFunction",
+        "TestDatatype",
+        "TestConstructor",
+        "TestTrait",
+        "TestPredicate",
+      };
+
+      var response = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
+        Query = "test"
+      });
+      foreach (var testSymbol in testSymbols) {
+        Assert.True(response.Any(symbol => symbol.Name.Contains(testSymbol)),
+          $"Could not find {testSymbol}");
+      }
+    }
+
+    [Fact]
+    public async Task SymbolImportedFromUnopenedFileDetected() {
+      var cwd = Directory.GetCurrentDirectory();
+      var path = Path.Combine(cwd, "Lookup/TestFiles/includes-foo.dfy");
+      var documentItem = CreateTestDocument(await File.ReadAllTextAsync(path), path);
+
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+      var response = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
+        Query = "foo"
+      });
+      Assert.Single(response);
+      Assert.Contains(response, symbol => symbol.Name == "foo" &&
+                                        symbol.Location.Uri.ToString().EndsWith("defines-foo.dfy"));
+    }
+
+    [Fact]
+    public async Task TwoMatchesOrderedCorrectly() {
+      var documentItem = await GetDocumentItem(@"method longerNameWithFooInIt() returns (x: int) {
+    x := 42;
+}
+
+method prefixFoo() returns (x: int) {
+    x := 23;
+}", "multiple-matches.dfy", false);
+
+
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+      var response = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
+        Query = "foo"
+      });
+      var items = response.ToImmutableList();
+      Assert.Equal(2, response.Count());
+      Assert.Contains("prefixFoo", items[0].Name);
+      Assert.Contains("longerNameWithFooInIt", items[1].Name);
+    }
+
+    public WorkspaceSymbolTest(ITestOutputHelper output) : base(output) {
+    }
+
+  }
+}

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -419,4 +419,18 @@ protected Task ApplyChangesAndWaitCompletionAsync(VersionedTextDocumentIdentifie
     });
     return client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken);
   }
-}
+
+  protected async Task<TextDocumentItem> GetDocumentItem(string source, string filename, bool includeProjectFile) {
+    var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    source = source.TrimStart();
+    if (includeProjectFile) {
+      var projectFile = CreateTestDocument("", Path.Combine(directory, DafnyProject.FileName));
+      await client.OpenDocumentAndWaitAsync(projectFile, CancellationToken);
+    }
+    var documentItem = CreateTestDocument(source, Path.Combine(directory, filename));
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var document = await Projects.GetLastDocumentAsync(documentItem);
+    Assert.NotNull(document);
+    return documentItem;
+  }
+}

Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs

@@ -0,0 +1,104 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.Immutable;
+using System.Linq;
+using System.Threading;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using OmniSharp.Extensions.LanguageServer.Protocol.Workspace;
+
+namespace Microsoft.Dafny.LanguageServer.Handlers {
+  public class DafnyWorkspaceSymbolHandler : WorkspaceSymbolsHandlerBase {
+    private readonly ILogger logger;
+    private readonly IProjectDatabase projects;
+    private readonly DafnyOptions dafnyOptions;
+
+    public DafnyWorkspaceSymbolHandler(ILogger<DafnyWorkspaceSymbolHandler> logger, IProjectDatabase projects, DafnyOptions dafnyOptions) {
+      this.logger = logger;
+      this.projects = projects;
+      this.dafnyOptions = dafnyOptions;
+    }
+
+    protected override WorkspaceSymbolRegistrationOptions CreateRegistrationOptions(WorkspaceSymbolCapability capability,
+      ClientCapabilities clientCapabilities) {
+      return new WorkspaceSymbolRegistrationOptions {
+        WorkDoneProgress = false
+      };
+    }
+
+    public override async Task<Container<SymbolInformation>?> Handle(WorkspaceSymbolParams request, CancellationToken cancellationToken) {
+      var queryText = request.Query.ToLower();
+      var result = new Dictionary<SymbolInformation, int>();
+      foreach (var projectManager in projects.Managers) {
+        cancellationToken.ThrowIfCancellationRequested();
+        var state = await projectManager.GetStateAfterParsingAsync();
+        foreach (var def in state.SymbolTable.Definitions) {
+          cancellationToken.ThrowIfCancellationRequested();
+          // CreateLocation called below uses the .Uri field of Tokens which
+          // seems to occasionally be null while testing this from VSCode
+          if (def.NameToken == null || def.NameToken.Uri == null) {
+            logger.LogWarning($"Definition without name token in symbol table: {def}");
+            continue;
+          }
+          if (def.NameToken.val == null) {
+            logger.LogWarning($"Definition without name in symbol table: {def}");
+            continue;
+          }
+
+          // This matching could be improved by using the qualified name of the symbol here.
+          var name = def.NameToken.val;
+          if (name.ToLower().Contains(queryText)) {
+            // The fewer extra characters there are in the string, the
+            // better the match.
+            var matchDistance = name.Length - queryText.Length;
+            result.TryAdd(new SymbolInformation {
+              Name = name,
+              ContainerName = def.Kind.ToString(),
+              Kind = FromDafnySymbolKind(def.Kind),
+              Location = Workspace.Util.CreateLocation(def.NameToken)
+            }, matchDistance);
+          }
+        }
+      }
+
+      return result.OrderBy(kvPair => kvPair.Value).Select(kvPair => kvPair.Key).ToImmutableList();
+    }
+
+    private SymbolKind FromDafnySymbolKind(DafnySymbolKind dafnySymbolKind) {
+      // DafnySymbolKind is a copy of SymbolKind as described in its documentation.
+      // This conversion function can be removed once it is no longer a copy.
+      switch (dafnySymbolKind) {
+        case DafnySymbolKind.File: return SymbolKind.File;
+        case DafnySymbolKind.Module: return SymbolKind.Module;
+        case DafnySymbolKind.Namespace: return SymbolKind.Namespace;
+        case DafnySymbolKind.Package: return SymbolKind.Package;
+        case DafnySymbolKind.Class: return SymbolKind.Class;
+        case DafnySymbolKind.Method: return SymbolKind.Method;
+        case DafnySymbolKind.Property: return SymbolKind.Property;
+        case DafnySymbolKind.Field: return SymbolKind.Field;
+        case DafnySymbolKind.Constructor: return SymbolKind.Constructor;
+        case DafnySymbolKind.Enum: return SymbolKind.Enum;
+        case DafnySymbolKind.Interface: return SymbolKind.Interface;
+        case DafnySymbolKind.Function: return SymbolKind.Function;
+        case DafnySymbolKind.Variable: return SymbolKind.Variable;
+        case DafnySymbolKind.Constant: return SymbolKind.Constant;
+        case DafnySymbolKind.String: return SymbolKind.String;
+        case DafnySymbolKind.Number: return SymbolKind.Number;
+        case DafnySymbolKind.Boolean: return SymbolKind.Boolean;
+        case DafnySymbolKind.Array: return SymbolKind.Array;
+        case DafnySymbolKind.Object: return SymbolKind.Object;
+        case DafnySymbolKind.Key: return SymbolKind.Key;
+        case DafnySymbolKind.Null: return SymbolKind.Null;
+        case DafnySymbolKind.EnumMember: return SymbolKind.EnumMember;
+        case DafnySymbolKind.Struct: return SymbolKind.Struct;
+        case DafnySymbolKind.Event: return SymbolKind.Event;
+        case DafnySymbolKind.Operator: return SymbolKind.Operator;
+        case DafnySymbolKind.TypeParameter: return SymbolKind.TypeParameter;
+        default: throw new ArgumentException($"Unknown Dafny symbol kind: {dafnySymbolKind}");
+      }
+    }
+  }
+}

Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs

@@ -25,7 +25,8 @@ public static LanguageServerOptions WithDafnyHandlers(this LanguageServerOptions
         .WithHandler<DafnyCounterExampleHandler>()
         .WithHandler<DafnyCodeActionHandler>()
         .WithHandler<DafnyFormattingHandler>()
-        .WithHandler<VerificationHandler>();
+        .WithHandler<VerificationHandler>()
+        .WithHandler<DafnyWorkspaceSymbolHandler>();
     }
   }
 }

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

@@ -58,7 +58,27 @@ public SymbolTable CreateFrom(Program program, Compilation compilation, Cancella
         .SelectMany(r => r.GetResolvedDeclarations().Select(declaration =>
           ((IDeclarationOrUsage)r, declaration))).ToList();
 
-      return new SymbolTable(usages);
+      var relevantDafnySymbolKinds = new HashSet<DafnySymbolKind> {
+        DafnySymbolKind.Function,
+        DafnySymbolKind.Class,
+        DafnySymbolKind.Enum,
+        DafnySymbolKind.Method,
+        DafnySymbolKind.EnumMember,
+        DafnySymbolKind.Struct,
+        DafnySymbolKind.Interface,
+        DafnySymbolKind.Namespace,
+      };
+      // Since these definitions are checked for whether they
+      // contain substrings when answering workspace/resolve queries,
+      // performance can be improved by storing their names in a
+      // data structure that makes this operation cheaper, such as
+      // a suffix tree.
+      var definitions = visited
+        .OfType<ISymbol>()
+        .Where(symbol => relevantDafnySymbolKinds.Contains(symbol.Kind))
+        .ToImmutableList();
+
+      return new SymbolTable(usages, definitions);
     }
 
     private static IDictionary<AstElement, ILocalizableSymbol> CreateDeclarationDictionary(CompilationUnit compilationUnit, CancellationToken cancellationToken) {
@@ -88,7 +108,7 @@ private class DesignatorVisitor : SyntaxTreeVisitor {
         = ImmutableDictionary<Uri, IIntervalTree<Position, ILocalizableSymbol>>.Empty;
 
       public DesignatorVisitor(
-          ILogger logger, CompilationUnit compilationUnit, IDictionary<AstElement, ILocalizableSymbol> declarations, ILegacySymbol rootScope, CancellationToken cancellationToken) {
+        ILogger logger, CompilationUnit compilationUnit, IDictionary<AstElement, ILocalizableSymbol> declarations, ILegacySymbol rootScope, CancellationToken cancellationToken) {
         this.logger = logger;
         this.compilationUnit = compilationUnit;
         this.declarations = declarations;
@@ -318,7 +338,7 @@ public Unit Visit(ModuleSymbol moduleSymbol) {
           moduleSymbol.Declaration.tok,
           moduleSymbol.Declaration.tok.GetLspRange(),
           moduleSymbol.Declaration.RangeToken.ToLspRange()
-          );
+        );
         VisitChildren(moduleSymbol);
         return Unit.Value;
       }
@@ -440,4 +460,4 @@ private void RegisterLocation(ILegacySymbol symbol, IToken token, Range name, Ra
       }
     }
   }
-}
+}

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -122,7 +122,7 @@ public static Diagnostic ToLspDiagnostic(this DafnyDiagnostic dafnyDiagnostic) {
     };
   }
 
-  private static Location CreateLocation(IToken token) {
+  public static Location CreateLocation(IToken token) {
     var uri = DocumentUri.Parse(token.Uri.AbsoluteUri);
     return new Location {
       Range = token.GetLspRange(),