From 317ca0117665b053742db46fa0912b25f9b05fd6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Aug 2023 16:19:08 +0200 Subject: [PATCH] Better legacy migration (#4436) ### Changes 1. Rename `LegacySymbolTable`, which is part of the non-LSP Dafny server, to `SuperLegacySymbolTable` 1. Rename `SignatureAndCompletionTable` to `LegacySignatureAndCompletionTable` 1. Let `SignatureAndCompletionTable` differentiate between positions in different files, so it doesn't get confused between symbols in different files when they have similar positions or ranges. 1. Only migrate state in `SignatureAndCompletionTable` that relates to the changed file ### Testing - There could be a test added for 3 but I didn't add it. - Merging this PR into this other PR (https://github.com/dafny-lang/dafny/pull/4419), reduces the time of the test `ManyFastEditsUsingLargeFilesAndIncludes` from 47 seconds to 8 seconds By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../DeclarationLocationMigrationTest.cs | 19 +++--- .../Synchronization/LookupMigrationTest.cs | 5 +- .../Synchronization/SymbolMigrationTest.cs | 4 +- .../Unit/GhostStateDiagnosticCollectorTest.cs | 5 +- .../Language/GhostStateDiagnosticCollector.cs | 2 +- .../IGhostStateDiagnosticCollector.cs | 2 +- .../Language/Symbols/ISymbolTableFactory.cs | 2 +- ...s => LegacySignatureAndCompletionTable.cs} | 60 ++++++++----------- .../Language/Symbols/SymbolTableFactory.cs | 31 +++++++--- .../Workspace/Documents/Compilation.cs | 2 +- .../Documents/CompilationAfterResolution.cs | 4 +- .../DafnyLanguageServer/Workspace/IdeState.cs | 2 +- .../Workspace/LanguageServerExtensions.cs | 2 +- .../DafnyLanguageServer/Workspace/Migrator.cs | 47 ++++++++++----- .../Workspace/SymbolGuesser.cs | 7 ++- .../Workspace/TextDocumentLoader.cs | 2 +- Source/DafnyServer/DafnyHelper.cs | 2 +- ...tionTable.cs => SuperLegacySymbolTable.cs} | 4 +- 18 files changed, 116 insertions(+), 86 deletions(-) rename Source/DafnyLanguageServer/Language/Symbols/{SignatureAndCompletionTable.cs => LegacySignatureAndCompletionTable.cs} (70%) rename Source/DafnyServer/{SignatureAndCompletionTable.cs => SuperLegacySymbolTable.cs} (99%) diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs index 394a1b2f6c1..582b90b8203 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs @@ -1,4 +1,5 @@ -using System.IO; +using System; +using System.IO; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; @@ -10,6 +11,7 @@ using Xunit; using Xunit.Abstractions; using Xunit.Sdk; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { @@ -22,8 +24,8 @@ public class DeclarationLocationMigrationTest : SynchronizationTestBase { // TODO The "BodyEndToken" used by the CreateDeclarationDictionary.CreateDeclarationDictionary() // does not incorporate the closing braces. - protected bool TryFindSymbolDeclarationByName(IdeState state, string symbolName, out SymbolLocation location) { - location = state.SignatureAndCompletionTable.Locations + protected bool TryFindSymbolDeclarationByName(IdeState state, string symbolName, out SymbolLocation location, Uri uri = null) { + location = state.SignatureAndCompletionTable.LocationsPerUri[uri ?? state.SignatureAndCompletionTable.LocationsPerUri.First().Key] .WithCancellation(CancellationToken) .Where(entry => entry.Key.Name == symbolName) .Select(entry => entry.Value) @@ -318,25 +320,28 @@ public async Task PassingANullChangeRangeClearsSymbolsTable() { [Fact] public async Task PassingANullChangeRangePreservesForeignSymbols() { + var directory = Path.Combine(Directory.GetCurrentDirectory(), "Lookup/TestFiles"); var source = "include \"foreign.dfy\"\nclass X {}"; - var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Lookup/TestFiles/test.dfy")); + var documentItem = CreateTestDocument(source, Path.Combine(directory, "test.dfy")); + var includePath = Path.Combine(directory, "foreign.dfy"); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _)); + var uri = documentItem.Uri.ToUri(); + Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _, new Uri(includePath))); // Try a change that breaks resolution. Symbols for `foreign.dfy` are kept. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "; include \"foreign.dfy\"\nclass Y {}"); document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(document); - Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _)); + Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _, new Uri(includePath))); // Finally we drop the reference to `foreign.dfy` and confirm that `A` is not accessible any more. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "class Y {}"); document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(document); - Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _)); + Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _, uri)); } public DeclarationLocationMigrationTest(ITestOutputHelper output) : this(output, LogLevel.Information) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs index 10e7810ee1a..8711b2fe1e6 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs @@ -1,4 +1,5 @@ using System.IO; +using System.Linq; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; @@ -266,7 +267,7 @@ reads this await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var originalDocument = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(originalDocument); - var lookupCountBefore = originalDocument.SignatureAndCompletionTable.LookupTree.Count; + var lookupCountBefore = originalDocument.SignatureAndCompletionTable.LookupTreePerUri.First().Value.Count; await ApplyChangeAndWaitCompletionAsync( ref documentItem, @@ -276,7 +277,7 @@ await ApplyChangeAndWaitCompletionAsync( var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.False(document.SignatureAndCompletionTable.TryGetSymbolAt((6, 9), out var _)); - Assert.Equal(lookupCountBefore - 1, document.SignatureAndCompletionTable.LookupTree.Count); + Assert.Equal(lookupCountBefore - 1, document.SignatureAndCompletionTable.LookupTreePerUri.First().Value.Count); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs index 3c14701f579..a83a3053539 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs @@ -30,7 +30,7 @@ await ApplyChangeAndWaitCompletionAsync( var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.Resolved); - Assert.Equal(2, document.SignatureAndCompletionTable.Locations.Keys.OfType().Count()); + Assert.Equal(2, document.SignatureAndCompletionTable.LocationsPerUri.First().Value.Keys.OfType().Count()); } [Fact] @@ -98,7 +98,7 @@ await ApplyChangeAndWaitCompletionAsync( var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.Resolved); - Assert.Single(document.SignatureAndCompletionTable.Locations.Keys.OfType()); + Assert.Single(document.SignatureAndCompletionTable.LocationsPerUri.First().Value.Keys.OfType()); } public SymbolMigrationTest(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index a828d150300..92ca320393f 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.Collections.Immutable; using System.IO; using System.Linq; using System.Threading; @@ -69,8 +70,8 @@ public void EnsureResilienceAgainstErrors() { var source = new CancellationTokenSource(); source.CancelAfter(TimeSpan.FromSeconds(50)); var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics( - new SignatureAndCompletionTable(null!, new CompilationUnit(rootUri, program), - null!, null!, new IntervalTree(), true) + new LegacySignatureAndCompletionTable(null!, new CompilationUnit(rootUri, program), + null!, null!, ImmutableDictionary>.Empty, true) , source.Token); Assert.Empty(ghostDiagnostics); } diff --git a/Source/DafnyLanguageServer/Language/GhostStateDiagnosticCollector.cs b/Source/DafnyLanguageServer/Language/GhostStateDiagnosticCollector.cs index 520016bfea7..e0ffa4ae9bc 100644 --- a/Source/DafnyLanguageServer/Language/GhostStateDiagnosticCollector.cs +++ b/Source/DafnyLanguageServer/Language/GhostStateDiagnosticCollector.cs @@ -30,7 +30,7 @@ public GhostStateDiagnosticCollector(DafnyOptions options, ILogger> GetGhostStateDiagnostics( - SignatureAndCompletionTable signatureAndCompletionTable, CancellationToken cancellationToken) { + LegacySignatureAndCompletionTable signatureAndCompletionTable, CancellationToken cancellationToken) { if (!options.Get(ServerCommand.GhostIndicators)) { return ImmutableDictionary>.Empty; } diff --git a/Source/DafnyLanguageServer/Language/IGhostStateDiagnosticCollector.cs b/Source/DafnyLanguageServer/Language/IGhostStateDiagnosticCollector.cs index e9e37b1e809..0068a301521 100644 --- a/Source/DafnyLanguageServer/Language/IGhostStateDiagnosticCollector.cs +++ b/Source/DafnyLanguageServer/Language/IGhostStateDiagnosticCollector.cs @@ -20,6 +20,6 @@ public interface IGhostStateDiagnosticCollector { /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. IReadOnlyDictionary> GetGhostStateDiagnostics( - SignatureAndCompletionTable signatureAndCompletionTable, CancellationToken cancellationToken); + LegacySignatureAndCompletionTable signatureAndCompletionTable, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Language/Symbols/ISymbolTableFactory.cs b/Source/DafnyLanguageServer/Language/Symbols/ISymbolTableFactory.cs index 03999d06ef4..e6d3964b258 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/ISymbolTableFactory.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/ISymbolTableFactory.cs @@ -16,7 +16,7 @@ public interface ISymbolTableFactory { /// A symbol table representing the provided compilation unit. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. - SignatureAndCompletionTable CreateFrom(CompilationUnit compilationUnit, CancellationToken cancellationToken); + LegacySignatureAndCompletionTable CreateFrom(CompilationUnit compilationUnit, CancellationToken cancellationToken); SymbolTable CreateFrom(Dafny.Program program, Compilation compilation, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs b/Source/DafnyLanguageServer/Language/Symbols/LegacySignatureAndCompletionTable.cs similarity index 70% rename from Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs rename to Source/DafnyLanguageServer/Language/Symbols/LegacySignatureAndCompletionTable.cs index 1eac147e6b9..7edb187493d 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/LegacySignatureAndCompletionTable.cs @@ -2,9 +2,10 @@ using IntervalTree; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Collections.Generic; +using System.Collections.Immutable; using System.Diagnostics.CodeAnalysis; +using System.Linq; using System.Threading; -using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; using Microsoft.Extensions.Logging.Abstractions; using AstElement = System.Object; @@ -14,8 +15,8 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { /// /// Represents the symbol table /// - public class SignatureAndCompletionTable { - private readonly ILogger logger; + public class LegacySignatureAndCompletionTable { + private readonly ILogger logger; // TODO Guard the properties from changes public CompilationUnit CompilationUnit { get; } @@ -28,12 +29,12 @@ public class SignatureAndCompletionTable { /// /// Gets the dictionary allowing to resolve the location of a specified symbol. Do not modify this instance. /// - public IDictionary Locations { get; } + public ImmutableDictionary> LocationsPerUri { get; } /// /// Gets the interval tree backing this symbol table. Do not modify this instance. /// - public IIntervalTree LookupTree { get; } + public ImmutableDictionary> LookupTreePerUri { get; } /// /// true if the symbol table results from a successful resolution by the dafny resolver. @@ -42,14 +43,14 @@ public class SignatureAndCompletionTable { private readonly DafnyLangTypeResolver typeResolver; - public static SignatureAndCompletionTable Empty(DafnyOptions options, DafnyProject project) { + public static LegacySignatureAndCompletionTable Empty(DafnyOptions options, DafnyProject project) { var emptyProgram = GetEmptyProgram(options, project.Uri); - return new SignatureAndCompletionTable( - NullLogger.Instance, + return new LegacySignatureAndCompletionTable( + NullLogger.Instance, new CompilationUnit(project.Uri, emptyProgram), new Dictionary(), - new Dictionary(), - new IntervalTree(), + ImmutableDictionary>.Empty, + ImmutableDictionary>.Empty, symbolsResolved: false); } @@ -68,35 +69,31 @@ public static Program GetEmptyProgram(DafnyOptions options, Uri uri) { return emptyProgram; } - public SignatureAndCompletionTable( - ILogger iLogger, + public LegacySignatureAndCompletionTable( + ILogger iLogger, CompilationUnit compilationUnit, IDictionary declarations, - IDictionary locations, - IIntervalTree lookupTree, + ImmutableDictionary> locationsPerUri, + ImmutableDictionary> lookupTreePerUri, bool symbolsResolved ) { CompilationUnit = compilationUnit; Declarations = declarations; - Locations = locations; - LookupTree = lookupTree; + LocationsPerUri = locationsPerUri; + LookupTreePerUri = lookupTreePerUri; Resolved = symbolsResolved; typeResolver = new DafnyLangTypeResolver(declarations); logger = iLogger; - - // TODO IntervalTree goes out of sync after any change and "fixes" its state upon the first query. Replace it with another implementation that can be queried without potential side-effects. - LookupTree.Query(new Position(0, 0)); } /// /// Tries to get a symbol at the specified location. + /// Only used for testing. /// - /// The requested position. - /// The symbol that could be identified at the given position, or null if no symbol could be identified. - /// true if a symbol was found, otherwise false. - /// Thrown if there was one more symbol at the specified position. This should never happen, unless there was an error. public bool TryGetSymbolAt(Position position, [NotNullWhen(true)] out ILocalizableSymbol? symbol) { - var symbolsAtPosition = LookupTree.Query(position); + var intervalTree = LookupTreePerUri.First().Value; + + var symbolsAtPosition = intervalTree.Query(position); symbol = null; // Use case: function f(a: int) {}, and hover over a. foreach (var potentialSymbol in symbolsAtPosition) { @@ -110,29 +107,20 @@ public bool TryGetSymbolAt(Position position, [NotNullWhen(true)] out ILocalizab return symbol != null; } - /// - /// Tries to get the location of the given symbol. - /// - /// The symbol to get the location of. - /// The current location of the specified symbol, or null if no location of the given symbol is known. - /// true if a location was found, otherwise false. - public bool TryGetLocationOf(ILegacySymbol symbol, [NotNullWhen(true)] out SymbolLocation? location) { - return Locations.TryGetValue(symbol, out location); - } - /// /// Resolves the innermost symbol that encloses the given position. /// + /// /// The position to get the innermost symbol of. /// A token to cancel the update operation before its completion. /// The innermost symbol at the specified position. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. - public ILegacySymbol GetEnclosingSymbol(Position position, CancellationToken cancellationToken) { + public ILegacySymbol GetEnclosingSymbol(Uri uri, Position position, CancellationToken cancellationToken) { // TODO use a suitable data-structure to resolve the locations efficiently. ILegacySymbol innerMostSymbol = CompilationUnit; var innerMostRange = new Range(new Position(0, 0), new Position(int.MaxValue, int.MaxValue)); - foreach (var (symbol, location) in Locations) { + foreach (var (symbol, location) in LocationsPerUri.GetValueOrDefault(uri) ?? ImmutableDictionary.Empty) { cancellationToken.ThrowIfCancellationRequested(); var range = location.Declaration; if (IsEnclosedBy(innerMostRange, range) && IsInside(range, position)) { diff --git a/Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs b/Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs index 30bce213845..45442f6584a 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs @@ -6,6 +6,7 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Collections.Generic; +using System.Collections.Immutable; using System.Linq; using System.Threading; using Microsoft.Dafny.LanguageServer.Workspace; @@ -15,15 +16,15 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class SymbolTableFactory : ISymbolTableFactory { private readonly ILogger logger; - private readonly ILogger loggerSymbolTable; + private readonly ILogger loggerSymbolTable; - public SymbolTableFactory(ILogger logger, ILogger loggerSymbolTable) { + public SymbolTableFactory(ILogger logger, ILogger loggerSymbolTable) { this.logger = logger; this.loggerSymbolTable = loggerSymbolTable; } - public SignatureAndCompletionTable CreateFrom(CompilationUnit compilationUnit, CancellationToken cancellationToken) { + public LegacySignatureAndCompletionTable CreateFrom(CompilationUnit compilationUnit, CancellationToken cancellationToken) { var program = compilationUnit.Program; var declarations = CreateDeclarationDictionary(compilationUnit, cancellationToken); var designatorVisitor = new DesignatorVisitor(logger, compilationUnit, declarations, compilationUnit, cancellationToken); @@ -40,7 +41,7 @@ public SignatureAndCompletionTable CreateFrom(CompilationUnit compilationUnit, C // prohibiting it to be null). logger.LogDebug("cannot create symbol table from a program with errors"); } - return new SignatureAndCompletionTable( + return new LegacySignatureAndCompletionTable( loggerSymbolTable, compilationUnit, declarations, @@ -83,7 +84,8 @@ private class DesignatorVisitor : SyntaxTreeVisitor { private ILegacySymbol currentScope; - public IIntervalTree SymbolLookup { get; } = new IntervalTree(); + public ImmutableDictionary> SymbolLookup { get; private set; } + = ImmutableDictionary>.Empty; public DesignatorVisitor( ILogger logger, CompilationUnit compilationUnit, IDictionary declarations, ILegacySymbol rootScope, CancellationToken cancellationToken) { @@ -235,12 +237,21 @@ private void RegisterTypeDesignator(ILegacySymbol scope, Type type) { private void RegisterDesignator(ILegacySymbol scope, AstElement node, Boogie.IToken token, string identifier) { var symbol = GetSymbolDeclarationByName(scope, identifier); if (symbol != null) { + if (token == Token.NoToken) { + return; + } // Many resolutions for automatically generated nodes (e.g. Decreases, Update when initializating a variable // at declaration) cause duplicated visits. These cannot be prevented at this time as it seems there's no way // to distinguish nodes from automatically created one (i.e. nodes of the original syntax tree vs. nodes of the // abstract syntax tree). We just ignore such duplicates until more information is availabe in the AST. var range = token.GetLspRange(); - SymbolLookup.Add(range.Start, range.End, symbol); + + var dafnyToken = (IToken)token; + var symbolLookupForUri = + SymbolLookup.GetValueOrDefault(dafnyToken.Uri) ?? new IntervalTree(); + SymbolLookup = SymbolLookup.SetItem(dafnyToken.Uri, symbolLookupForUri); + + symbolLookupForUri.Add(range.Start, range.End, symbol); if (designators.TryGetValue(node, out var registeredSymbol)) { if (registeredSymbol != symbol) { logger.LogDebug("Conflicting symbol resolution of designator named {Identifier} in {Filename}@({Line},{Column})", @@ -283,7 +294,8 @@ private void ProcessNestedScope(AstElement node, Boogie.IToken token, System.Act private class SymbolDeclarationLocationVisitor : ISymbolVisitor { private readonly CancellationToken cancellationToken; - public IDictionary Locations { get; } = new Dictionary(); + public ImmutableDictionary> Locations { get; private set; } + = ImmutableDictionary>.Empty; public SymbolDeclarationLocationVisitor(CancellationToken cancellationToken) { this.cancellationToken = cancellationToken; @@ -420,7 +432,10 @@ private void VisitChildren(ILegacySymbol symbol) { private void RegisterLocation(ILegacySymbol symbol, IToken token, Range name, Range declaration) { if (token.Filepath != null) { // The filename is null if we have a default or System based symbol. This is also reflected by the ranges being usually -1. - Locations.Add(symbol, new SymbolLocation(token.GetDocumentUri(), name, declaration)); + var locationsForUri = + Locations.GetValueOrDefault(token.Uri) ?? new Dictionary(); + Locations = Locations.SetItem(token.Uri, locationsForUri); + locationsForUri.Add(symbol, new SymbolLocation(token.GetDocumentUri(), name, declaration)); } } } diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs index 268842557ca..97ecc0eb365 100644 --- a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs @@ -40,7 +40,7 @@ public IdeState InitialIdeState(Compilation initialCompilation, DafnyOptions opt var program = new EmptyNode(); return ToIdeState(new IdeState(initialCompilation.Version, initialCompilation, program, ImmutableDictionary>.Empty, - SymbolTable.Empty(), SignatureAndCompletionTable.Empty(options, initialCompilation.Project), new(), + SymbolTable.Empty(), LegacySignatureAndCompletionTable.Empty(options, initialCompilation.Project), new(), Array.Empty(), ImmutableDictionary>.Empty, initialCompilation.RootUris.ToDictionary(uri => uri, uri => (VerificationTree)new DocumentVerificationTree(program, uri)) diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs index 6be9ff8f53f..e9a09946593 100644 --- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs @@ -17,7 +17,7 @@ public class CompilationAfterResolution : CompilationAfterParsing { public CompilationAfterResolution(CompilationAfterParsing compilationAfterParsing, IReadOnlyDictionary> diagnostics, SymbolTable? symbolTable, - SignatureAndCompletionTable signatureAndCompletionTable, + LegacySignatureAndCompletionTable signatureAndCompletionTable, IReadOnlyDictionary> ghostDiagnostics, IReadOnlyList verifiables, ConcurrentDictionary>>> translatedModules, @@ -33,7 +33,7 @@ List counterexamples } public List Counterexamples { get; set; } public SymbolTable? SymbolTable { get; } - public SignatureAndCompletionTable SignatureAndCompletionTable { get; } + public LegacySignatureAndCompletionTable SignatureAndCompletionTable { get; } public IReadOnlyDictionary> GhostDiagnostics { get; } public IReadOnlyList Verifiables { get; } public ConcurrentDictionary> ImplementationsPerVerifiable { get; } = new(); diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index b503d10f75a..16f044d03a6 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -28,7 +28,7 @@ public record IdeState( Node Program, IReadOnlyDictionary> ResolutionDiagnostics, SymbolTable SymbolTable, - SignatureAndCompletionTable SignatureAndCompletionTable, + LegacySignatureAndCompletionTable SignatureAndCompletionTable, Dictionary VerificationResults, IReadOnlyList Counterexamples, IReadOnlyDictionary> GhostRanges, diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index 2447ca9a83c..a3d054c5681 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -50,7 +50,7 @@ private static IServiceCollection WithDafnyWorkspace(this IServiceCollection ser .AddSingleton() .AddSingleton(provider => (changes, cancellationToken) => new Migrator( provider.GetRequiredService>(), - provider.GetRequiredService>(), + provider.GetRequiredService>(), changes, cancellationToken)) .AddSingleton() .AddSingleton() diff --git a/Source/DafnyLanguageServer/Workspace/Migrator.cs b/Source/DafnyLanguageServer/Workspace/Migrator.cs index cbc499f9c6b..0d5c3101f04 100644 --- a/Source/DafnyLanguageServer/Workspace/Migrator.cs +++ b/Source/DafnyLanguageServer/Workspace/Migrator.cs @@ -18,13 +18,13 @@ public class Migrator { private readonly ILogger logger; private readonly DidChangeTextDocumentParams changeParams; private readonly CancellationToken cancellationToken; - private readonly ILogger loggerSymbolTable; + private readonly ILogger loggerSymbolTable; private readonly Dictionary getPositionAtEndOfAppliedChangeCache = new(); public Migrator( ILogger logger, - ILogger loggerSymbolTable, + ILogger loggerSymbolTable, DidChangeTextDocumentParams changeParams, CancellationToken cancellationToken ) { @@ -112,26 +112,45 @@ private IEnumerable MigrateRelatedInformation(Text }; } - public SignatureAndCompletionTable MigrateSymbolTable(SignatureAndCompletionTable originalSymbolTable) { - var migratedLookupTree = originalSymbolTable.LookupTree; - var migratedDeclarations = originalSymbolTable.Locations; + public LegacySignatureAndCompletionTable MigrateSymbolTable(LegacySignatureAndCompletionTable originalSymbolTable) { + var uri = changeParams.TextDocument.Uri.ToUri(); + var migratedLookupTreeForUri = originalSymbolTable.LookupTreePerUri.GetValueOrDefault(uri); + var migratedLocationsForUri = originalSymbolTable.LocationsPerUri.GetValueOrDefault(uri); foreach (var change in changeParams.ContentChanges) { cancellationToken.ThrowIfCancellationRequested(); if (change.Range == null) { - migratedLookupTree = new IntervalTree(); + migratedLookupTreeForUri = new IntervalTree(); } else { - migratedLookupTree = ApplyLookupTreeChange(migratedLookupTree, change); + if (migratedLookupTreeForUri != null) { + migratedLookupTreeForUri = ApplyLookupTreeChange(migratedLookupTreeForUri, change); + } } - migratedDeclarations = ApplyDeclarationsChange(originalSymbolTable, migratedDeclarations, change, GetPositionAtEndOfAppliedChange(change)); + + if (migratedLocationsForUri != null) { + migratedLocationsForUri = ApplyDeclarationsChange(originalSymbolTable, migratedLocationsForUri, change, GetPositionAtEndOfAppliedChange(change)); + } + } + if (migratedLookupTreeForUri != null) { + logger.LogTrace("migrated the lookup tree, lookup before={SymbolsBefore}, after={SymbolsAfter}", + originalSymbolTable.LookupTreePerUri.Count, migratedLookupTreeForUri.Count); + // TODO IntervalTree goes out of sync after any change and "fixes" its state upon the first query. Replace it with another implementation that can be queried without potential side-effects. + migratedLookupTreeForUri.Query(new Position(0, 0)); + } + + var migratedLocations = originalSymbolTable.LocationsPerUri; + if (migratedLocationsForUri != null) { + migratedLocations = migratedLocations.SetItem(uri, migratedLocationsForUri); + } + var migratedLookupTrees = originalSymbolTable.LookupTreePerUri; + if (migratedLookupTreeForUri != null) { + migratedLookupTrees = migratedLookupTrees.SetItem(uri, migratedLookupTreeForUri); } - logger.LogTrace("migrated the lookup tree, lookup before={SymbolsBefore}, after={SymbolsAfter}", - originalSymbolTable.LookupTree.Count, migratedLookupTree.Count); - return new SignatureAndCompletionTable( + return new LegacySignatureAndCompletionTable( loggerSymbolTable, originalSymbolTable.CompilationUnit, originalSymbolTable.Declarations, - migratedDeclarations, - migratedLookupTree, + migratedLocations, + migratedLookupTrees, false ); } @@ -259,7 +278,7 @@ private static bool IsPositionAfterChange(Range changeRange, Position symbolFrom } private IDictionary ApplyDeclarationsChange( - SignatureAndCompletionTable originalSymbolTable, + LegacySignatureAndCompletionTable originalSymbolTable, IDictionary previousDeclarations, TextDocumentContentChangeEvent changeRange, Position? afterChangeEndOffset diff --git a/Source/DafnyLanguageServer/Workspace/SymbolGuesser.cs b/Source/DafnyLanguageServer/Workspace/SymbolGuesser.cs index c28dc76369d..65dbcc6b5ac 100644 --- a/Source/DafnyLanguageServer/Workspace/SymbolGuesser.cs +++ b/Source/DafnyLanguageServer/Workspace/SymbolGuesser.cs @@ -56,7 +56,7 @@ public Guesser(ILogger logger, IdeState state, CancellationToken cancellationTok } return (null, null); } - return GetSymbolAndTypeOfLastMember(position, memberAccesses); + return GetSymbolAndTypeOfLastMember(uri, position, memberAccesses); } private static Position? GetLinePositionBefore(Position requestPosition) { @@ -67,8 +67,9 @@ public Guesser(ILogger logger, IdeState state, CancellationToken cancellationTok return new Position(position.Line, position.Character - 1); } - private (ILegacySymbol? Designator, ILegacySymbol? Type) GetSymbolAndTypeOfLastMember(Position position, IReadOnlyList memberAccessChain) { - var enclosingSymbol = state.SignatureAndCompletionTable.GetEnclosingSymbol(position, cancellationToken); + private (ILegacySymbol? Designator, ILegacySymbol? Type) GetSymbolAndTypeOfLastMember(Uri uri, Position position, + IReadOnlyList memberAccessChain) { + var enclosingSymbol = state.SignatureAndCompletionTable.GetEnclosingSymbol(uri, position, cancellationToken); ILegacySymbol? currentDesignator = null; ILegacySymbol? currentDesignatorType = null; for (int currentMemberAccess = 0; currentMemberAccess < memberAccessChain.Count; currentMemberAccess++) { diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index f33c3f062b5..bd3f3982ae1 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -155,7 +155,7 @@ private IdeState CreateDocumentWithEmptySymbolTable(Compilation compilation, program, resolutionDiagnostics, SymbolTable.Empty(), - SignatureAndCompletionTable.Empty(dafnyOptions, compilation.Project), + LegacySignatureAndCompletionTable.Empty(dafnyOptions, compilation.Project), new(), Array.Empty(), ImmutableDictionary>.Empty, diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 0131a49c992..41ef045c000 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -98,7 +98,7 @@ private bool Boogie() { public void Symbols() { ServerUtils.ApplyArgs(args, options); if (Parse() && Resolve()) { - var symbolTable = new LegacySymbolTable(dafnyProgram); + var symbolTable = new SuperLegacySymbolTable(dafnyProgram); var symbols = symbolTable.CalculateSymbols(); Console.WriteLine("SYMBOLS_START " + ConvertToJson(symbols) + " SYMBOLS_END"); } else { diff --git a/Source/DafnyServer/SignatureAndCompletionTable.cs b/Source/DafnyServer/SuperLegacySymbolTable.cs similarity index 99% rename from Source/DafnyServer/SignatureAndCompletionTable.cs rename to Source/DafnyServer/SuperLegacySymbolTable.cs index 47fe9137250..7f5ce9ab86b 100644 --- a/Source/DafnyServer/SignatureAndCompletionTable.cs +++ b/Source/DafnyServer/SuperLegacySymbolTable.cs @@ -11,11 +11,11 @@ using Program = Microsoft.Dafny.Program; namespace DafnyServer { - public class LegacySymbolTable { + public class SuperLegacySymbolTable { private readonly Program _dafnyProgram; private readonly List _information = new(); - public LegacySymbolTable(Program dafnyProgram) { + public SuperLegacySymbolTable(Program dafnyProgram) { _dafnyProgram = dafnyProgram; }