diff --git a/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs b/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs index a92c7d99c33..f5393c1246c 100644 --- a/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs @@ -177,7 +177,8 @@ public void BindModuleNames(ProgramResolver resolver, ModuleBindings parentBindi var bindings = ModuleDef.BindModuleNames(resolver, parentBindings); if (!parentBindings.BindName(Name, this, bindings)) { - resolver.Reporter.Error(MessageSource.Resolver, tok, "Duplicate module name: {0}", Name); + parentBindings.TryLookup(Name, out var otherModule); + resolver.Reporter.Error(MessageSource.Resolver, new NestedToken(tok, otherModule.tok), "Duplicate module name: {0}", Name); } } diff --git a/Source/DafnyCore/AST/Modules/ModuleBindings.cs b/Source/DafnyCore/AST/Modules/ModuleBindings.cs index 68c65c349c4..2ce4e22f9de 100644 --- a/Source/DafnyCore/AST/Modules/ModuleBindings.cs +++ b/Source/DafnyCore/AST/Modules/ModuleBindings.cs @@ -25,14 +25,14 @@ public bool BindName(string name, ModuleDecl subModule, ModuleBindings b) { } } - public bool TryLookup(IToken name, out ModuleDecl m) { + public bool TryLookup(string name, out ModuleDecl m) { Contract.Requires(name != null); return TryLookupFilter(name, out m, l => true); } - public bool TryLookupFilter(IToken name, out ModuleDecl m, Func filter) { + public bool TryLookupFilter(string name, out ModuleDecl m, Func filter) { Contract.Requires(name != null); - if (modules.TryGetValue(name.val, out m) && filter(m)) { + if (modules.TryGetValue(name, out m) && filter(m)) { return true; } else if (parent != null) { return parent.TryLookupFilter(name, out m, filter); @@ -56,7 +56,7 @@ public bool ResolveQualifiedModuleIdRootAbstract(AbstractModuleDecl context, Mod Contract.Assert(qid != null); IToken root = qid.Path[0].StartToken; result = null; - bool res = TryLookupFilter(root, out result, + bool res = TryLookupFilter(root.val, out result, m => context != m && ((context.EnclosingModuleDefinition == m.EnclosingModuleDefinition && context.Exports.Count == 0) || m is LiteralModuleDecl)); return res; } @@ -72,7 +72,7 @@ public bool ResolveQualifiedModuleIdRootImport(AliasModuleDecl context, ModuleQu Contract.Assert(qid != null); IToken root = qid.Path[0].StartToken; result = null; - bool res = TryLookupFilter(root, out result, + bool res = TryLookupFilter(root.val, out result, m => context != m && ((context.EnclosingModuleDefinition == m.EnclosingModuleDefinition && context.Exports.Count == 0) || m is LiteralModuleDecl)); return res; } @@ -82,7 +82,7 @@ public bool ResolveQualifiedModuleIdRootRefines(ModuleDefinition context, Module Contract.Assert(qid != null); IToken root = qid.Path[0].StartToken; result = null; - bool res = TryLookupFilter(root, out result, m => m.EnclosingModuleDefinition != context); + bool res = TryLookupFilter(root.val, out result, m => m.EnclosingModuleDefinition != context); return res; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 9ea473870c2..2baf5a8f228 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -646,7 +646,7 @@ public ModuleBindings BindModuleNames(ProgramResolver resolver, ModuleBindings p // the add was successful } else { // there's already something with this name - var yes = bindings.TryLookup(subDecl.tok, out var prevDecl); + var yes = bindings.TryLookup(subDecl.tok.val, out var prevDecl); Contract.Assert(yes); if (prevDecl is AbstractModuleDecl || prevDecl is AliasModuleDecl) { resolver.Reporter.Error(MessageSource.Resolver, subDecl.tok, "Duplicate name of import: {0}", subDecl.Name); diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index 9f98cf7d11c..682ad068aa8 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -221,7 +221,7 @@ public async Task GetLastDocumentAsync() { return await CompilationManager.LastDocument; } - public async Task GetSnapshotAfterParsingAsync() { + public async Task GetStateAfterParsingAsync() { try { var parsedCompilation = await CompilationManager.ParsedCompilation; logger.LogDebug($"GetSnapshotAfterParsingAsync returns compilation version {parsedCompilation.Version}"); @@ -237,13 +237,13 @@ public async Task GetStateAfterResolutionAsync() { try { var resolvedCompilation = await CompilationManager.ResolvedCompilation; logger.LogDebug($"GetStateAfterResolutionAsync returns compilation version {resolvedCompilation.Version}"); + logger.LogDebug($"GetStateAfterResolutionAsync returns state version {latestIdeState.Value.Version}"); + return latestIdeState.Value; } catch (OperationCanceledException) { logger.LogDebug($"GetSnapshotAfterResolutionAsync caught OperationCanceledException for resolved compilation {Project.Uri}"); - return await GetSnapshotAfterParsingAsync(); + return await GetStateAfterParsingAsync(); } - logger.LogDebug($"GetStateAfterResolutionAsync returns state version {latestIdeState.Value.Version}"); - return latestIdeState.Value; } public async Task GetIdeStateAfterVerificationAsync() { diff --git a/Test/dafny0/ModuleInsertionErrors.dfy.expect b/Test/dafny0/ModuleInsertionErrors.dfy.expect index f4359d670a9..6a290d76296 100644 --- a/Test/dafny0/ModuleInsertionErrors.dfy.expect +++ b/Test/dafny0/ModuleInsertionErrors.dfy.expect @@ -1,4 +1,4 @@ -ModuleInsertionErrors.dfy(23,11): Error: Duplicate module name: B -ModuleInsertionErrors.dfy(24,11): Error: Duplicate module name: N -ModuleInsertionErrors.dfy(30,17): Error: Duplicate module name: O +ModuleInsertionErrors.dfy(23,11): Error: Duplicate module name: B [Related location] ModuleInsertionErrors.dfy(21,11) +ModuleInsertionErrors.dfy(24,11): Error: Duplicate module name: N [Related location] ModuleInsertionErrors.dfy(26,11) +ModuleInsertionErrors.dfy(30,17): Error: Duplicate module name: O [Related location] ModuleInsertionErrors.dfy(29,17) 3 resolution/type errors detected in ModuleInsertionErrors.dfy diff --git a/Test/git-issues/git-issue-478-errors.dfy.expect b/Test/git-issues/git-issue-478-errors.dfy.expect index c529c695867..94969c68de1 100644 --- a/Test/git-issues/git-issue-478-errors.dfy.expect +++ b/Test/git-issues/git-issue-478-errors.dfy.expect @@ -1,6 +1,6 @@ git-issue-478-errors.dfy(22,9): Error: Import declaration uses same name as a module in the same scope: LibW git-issue-478-errors.dfy(26,9): Error: Import declaration uses same name as a module in the same scope: LibX -git-issue-478-errors.dfy(36,7): Error: Duplicate module name: M +git-issue-478-errors.dfy(36,7): Error: Duplicate module name: M [Related location] git-issue-478-errors.dfy(35,7) git-issue-478-errors.dfy(7,7): Error: Import declaration uses same name as a module in the same scope: LibA git-issue-478-errors.dfy(11,7): Error: Import declaration uses same name as a module in the same scope: LibB git-issue-478-errors.dfy(37,7): Error: Import declaration uses same name as a module in the same scope: M