Include both locations in duplicate module name error messages (#4499)

Fixes #4289 <small>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).</small>
dafny-lang · Sep 15, 2023 · e1061f8 · e1061f8
1 parent c74ca32
commit e1061f8
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 16 deletions.
diff --git 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
@@ -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<ModuleDecl, bool> filter) {
+  public bool TryLookupFilter(string name, out ModuleDecl m, Func<ModuleDecl, bool> 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;
   }
 }
diff --git 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
@@ -221,7 +221,7 @@ public async Task<CompilationAfterParsing> GetLastDocumentAsync() {
     return await CompilationManager.LastDocument;
   }
 
-  public async Task<IdeState> GetSnapshotAfterParsingAsync() {
+  public async Task<IdeState> GetStateAfterParsingAsync() {
     try {
       var parsedCompilation = await CompilationManager.ParsedCompilation;
       logger.LogDebug($"GetSnapshotAfterParsingAsync returns compilation version {parsedCompilation.Version}");
@@ -237,13 +237,13 @@ public async Task<IdeState> 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<IdeState> GetIdeStateAfterVerificationAsync() {

diff --git 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
@@ -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