[LSP] Add handler for workspace/symbol requests

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.

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -46,6 +46,18 @@
     <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="Lookup\TestFiles\test-workspace-symbols.dfy">
+      <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+    </None>
+    <None Update="Lookup\TestFiles\multiple-matches.dfy">
+      <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+    </None>
     <None Update="Synchronization\TestFiles\semanticError.dfy">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </None>

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/TestFiles/multiple-matches.dfy

@@ -0,0 +1,7 @@
+method longerNameWithFooInIt() returns (x: int) {
+    x := 42;
+}
+
+method prefixFoo() returns (x: int) {
+    x := 23;
+}

Source/DafnyLanguageServer.Test/Lookup/TestFiles/test-workspace-symbols.dfy

@@ -0,0 +1,15 @@
+class TestClass {}
+
+module TestModule {}
+
+function TestFunction(): int { 42 }
+
+method TestMethod() returns (x: int) {
+  x := 42;
+}
+
+datatype TestDatatype = TestConstructor
+
+trait TestTrait {}
+
+predicate TestPredicate { false }

Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs

@@ -0,0 +1,112 @@
+using System;
+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();
+      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 == "method foo() returns (x: int)" &&
+                                       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 == "method bar() returns (x: int)" &&
+                                        si.Kind == SymbolKind.Method &&
+                                        si.Location.Uri.ToString().EndsWith("includes-foo.dfy"));
+    }
+
+    [Fact]
+    public async Task AllRelevantSymbolKindsDetected() {
+      var cwd = Directory.GetCurrentDirectory();
+      var pathA = Path.Combine(cwd, "Lookup/TestFiles/test-workspace-symbols.dfy");
+      var documentItemA = CreateTestDocument(await File.ReadAllTextAsync(pathA), pathA);
+
+      await client.OpenDocumentAndWaitAsync(documentItemA, CancellationToken);
+
+      var testSymbols = new List<string>();
+      testSymbols.Add("TestClass");
+      testSymbols.Add("TestModule");
+      testSymbols.Add("TestFunction");
+      testSymbols.Add("TestDatatype");
+      testSymbols.Add("TestConstructor");
+      testSymbols.Add("TestTrait");
+      testSymbols.Add("TestPredicate");
+
+      var response = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
+        Query = "test"
+      });
+      foreach (var testSymbol in testSymbols) {
+        Assert.True(response.Any(symb => symb.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, symb => symb.Name == "method foo() returns (x: int)" &&
+                                        symb.Location.Uri.ToString().EndsWith("defines-foo.dfy"));
+    }
+
+    [Fact]
+    public async Task TwoMatchesOrderedCorrectly() {
+      var cwd = Directory.GetCurrentDirectory();
+      var path = Path.Combine(cwd, "Lookup/TestFiles/multiple-matches.dfy");
+      var documentItem = CreateTestDocument(await File.ReadAllTextAsync(path), path);
+
+      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/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();
+      Dictionary<SymbolInformation, int> result = new Dictionary<SymbolInformation, int>();
+      // Using a LINQ traversal here would be more readable, but to be as responsive
+      // to cancellations as possible, we instead use a loop:
+      foreach (var projManager in projects.Managers) {
+        cancellationToken.ThrowIfCancellationRequested();
+        var state = await projManager.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;
+          }
+          // GetDescription is not quite the right thing to use here,
+          // as it includes things like keywords and the signature of the
+          // the definitions. However, extracting just the name from
+          // an ISymbol requires explicit case splitting for each definition
+          var description = def.GetDescription(dafnyOptions);
+          if (description.ToLower().Contains(queryText)) {
+            // The fewer extra characters there are in the string, the
+            // better the match.
+            var dist = description.Length - queryText.Length;
+            result.TryAdd(new SymbolInformation {
+              Name = description,
+              ContainerName = def.Kind.ToString(),
+              Kind = FromDafnySymbolKind(def.Kind),
+              Location = Workspace.Util.CreateLocation(def.NameToken)
+            }, dist);
+          }
+        }
+      }
+
+      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,25 @@ 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>();
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Function);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Class);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Enum);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Method);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.EnumMember);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Struct);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Interface);
+      relevantDafnySymbolKinds.Add(DafnySymbolKind.Namespace);
+      // TODO: Since these definitions are checked for whether they
+      //       contain substrings when answering workspace/resolve queries,
+      //       it would improve performance to find a data structure allowing
+      //       to compute this efficiently
+      var definitions = visited
+        .OfType<ISymbol>()
+        .Where(symb => relevantDafnySymbolKinds.Contains(symb.Kind))
+        .ToImmutableList();
+
+      return new SymbolTable(usages, definitions);
     }
 
     private static IDictionary<AstElement, ILocalizableSymbol> CreateDeclarationDictionary(CompilationUnit compilationUnit, CancellationToken cancellationToken) {

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(),

Source/DafnyLanguageServer/Workspace/SymbolTable.cs

@@ -20,9 +20,10 @@ public static SymbolTable Empty() {
   private SymbolTable() {
     DeclarationToUsages = ImmutableDictionary<IDeclarationOrUsage, ISet<IDeclarationOrUsage>>.Empty;
     UsageToDeclaration = ImmutableDictionary<IDeclarationOrUsage, IDeclarationOrUsage>.Empty;
+    Definitions = ImmutableList<ISymbol>.Empty;
   }
 
-  public SymbolTable(IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage declaration)> usages) {
+  public SymbolTable(IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage declaration)> usages, ImmutableList<ISymbol> definitions) {
     var safeUsages1 = usages.Where(k => k.usage.NameToken.Uri != null).ToImmutableList();
     var safeUsages = usages.Where(k => k.usage.NameToken.Uri != null && k.declaration.NameToken.Uri != null).ToImmutableList();
 
@@ -34,6 +35,8 @@ public SymbolTable(IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage
       g => g.Key,
       g => (ISet<IDeclarationOrUsage>)g.Select(k => k.usage).ToHashSet());
 
+    Definitions = definitions;
+
     var symbols = safeUsages.Select(u => u.declaration).
       Concat(safeUsages.Select(u => u.usage)).
       Where(s => !AutoGeneratedToken.Is(s.NameToken));
@@ -58,7 +61,13 @@ public SymbolTable(IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage
   /// <summary>
   /// Maps each symbol declaration to usages of the symbol, not including the declaration itself.
   /// </summary>
-  private ImmutableDictionary<IDeclarationOrUsage, ISet<IDeclarationOrUsage>> DeclarationToUsages { get; }
+  public ImmutableDictionary<IDeclarationOrUsage, ISet<IDeclarationOrUsage>> DeclarationToUsages { get; }
+
+  /// <summary>
+  ///  A list of all definitions, such as methods, classes, functions, etc., used for workspace-wide symbol
+  /// lookup.
+  /// </summary>
+  public ImmutableList<ISymbol> Definitions { get; }
 
   public ISet<Location> GetUsages(Uri uri, Position position) {
     if (nodePositions.TryGetValue(uri, out var forFile)) {

docs/dev/news/4619.feat

@@ -0,0 +1 @@
+Implemented support for workspace/symbol request to allow IDE navigation by symbol.