Improve reporting of related locations

Source/DafnyCore/AST/Types/MapType.cs

@@ -0,0 +1,76 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny;
+
+public class MapType : CollectionType {
+  public bool Finite {
+    get { return finite; }
+    set { finite = value; }
+  }
+  private bool finite;
+  public Type Range {
+    get { return range; }
+  }
+  private Type range;
+  public override void SetTypeArgs(Type domain, Type range) {
+    base.SetTypeArgs(domain, range);
+    Contract.Assume(this.range == null);  // Can only set once.  This is really a precondition.
+    this.range = range;
+  }
+  public MapType(bool finite, Type domain, Type range) : base(domain, range) {
+    Contract.Requires((domain == null && range == null) || (domain != null && range != null));
+    this.finite = finite;
+    this.range = range;
+  }
+  public Type Domain {
+    get { return Arg; }
+  }
+  public override string CollectionTypeName { get { return finite ? "map" : "imap"; } }
+  [System.Diagnostics.Contracts.Pure]
+  public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
+    Contract.Ensures(Contract.Result<string>() != null);
+    var targs = HasTypeArg() ? this.TypeArgsToString(options, context, parseAble) : "";
+    return CollectionTypeName + targs;
+  }
+  public override bool Equals(Type that, bool keepConstraints = false) {
+    var t = that.NormalizeExpand(keepConstraints) as MapType;
+    return t != null && Finite == t.Finite && Arg.Equals(t.Arg, keepConstraints) && Range.Equals(t.Range, keepConstraints);
+  }
+
+  public override Type Subst(IDictionary<TypeParameter, Type> subst) {
+    var dom = Domain.Subst(subst);
+    if (dom is InferredTypeProxy) {
+      ((InferredTypeProxy)dom).KeepConstraints = true;
+    }
+    var ran = Range.Subst(subst);
+    if (ran is InferredTypeProxy) {
+      ((InferredTypeProxy)ran).KeepConstraints = true;
+    }
+    if (dom == Domain && ran == Range) {
+      return this;
+    } else {
+      return new MapType(Finite, dom, ran);
+    }
+  }
+
+  public override Type ReplaceTypeArguments(List<Type> arguments) {
+    return new MapType(Finite, arguments[0], arguments[1]);
+  }
+
+  public override bool SupportsEquality {
+    get {
+      // A map type supports equality if both its Keys type and Values type does.  It is checked
+      // that the Keys type always supports equality, so we only need to check the Values type here.
+      return range.SupportsEquality;
+    }
+  }
+  public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatatypes) {
+    return Domain.ComputeMayInvolveReferences(visitedDatatypes) || Range.ComputeMayInvolveReferences(visitedDatatypes);
+  }
+
+  public override BinaryExpr.ResolvedOpcode ResolvedOpcodeForIn => BinaryExpr.ResolvedOpcode.InMap;
+  public override ComprehensionExpr.CollectionBoundedPool GetBoundedPool(Expression source) {
+    return new ComprehensionExpr.MapBoundedPool(source, Domain, Domain, Finite);
+  }
+}

Source/DafnyCore/AST/Types/Types.cs

@@ -2124,77 +2124,6 @@ public override ComprehensionExpr.CollectionBoundedPool GetBoundedPool(Expressio
     return new ComprehensionExpr.SeqBoundedPool(source, Arg, Arg);
   }
 }
-public class MapType : CollectionType {
-  public bool Finite {
-    get { return finite; }
-    set { finite = value; }
-  }
-  private bool finite;
-  public Type Range {
-    get { return range; }
-  }
-  private Type range;
-  public override void SetTypeArgs(Type domain, Type range) {
-    base.SetTypeArgs(domain, range);
-    Contract.Assume(this.range == null);  // Can only set once.  This is really a precondition.
-    this.range = range;
-  }
-  public MapType(bool finite, Type domain, Type range) : base(domain, range) {
-    Contract.Requires((domain == null && range == null) || (domain != null && range != null));
-    this.finite = finite;
-    this.range = range;
-  }
-  public Type Domain {
-    get { return Arg; }
-  }
-  public override string CollectionTypeName { get { return finite ? "map" : "imap"; } }
-  [System.Diagnostics.Contracts.Pure]
-  public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
-    Contract.Ensures(Contract.Result<string>() != null);
-    var targs = HasTypeArg() ? this.TypeArgsToString(options, context, parseAble) : "";
-    return CollectionTypeName + targs;
-  }
-  public override bool Equals(Type that, bool keepConstraints = false) {
-    var t = that.NormalizeExpand(keepConstraints) as MapType;
-    return t != null && Finite == t.Finite && Arg.Equals(t.Arg, keepConstraints) && Range.Equals(t.Range, keepConstraints);
-  }
-
-  public override Type Subst(IDictionary<TypeParameter, Type> subst) {
-    var dom = Domain.Subst(subst);
-    if (dom is InferredTypeProxy) {
-      ((InferredTypeProxy)dom).KeepConstraints = true;
-    }
-    var ran = Range.Subst(subst);
-    if (ran is InferredTypeProxy) {
-      ((InferredTypeProxy)ran).KeepConstraints = true;
-    }
-    if (dom == Domain && ran == Range) {
-      return this;
-    } else {
-      return new MapType(Finite, dom, ran);
-    }
-  }
-
-  public override Type ReplaceTypeArguments(List<Type> arguments) {
-    return new MapType(Finite, arguments[0], arguments[1]);
-  }
-
-  public override bool SupportsEquality {
-    get {
-      // A map type supports equality if both its Keys type and Values type does.  It is checked
-      // that the Keys type always supports equality, so we only need to check the Values type here.
-      return range.SupportsEquality;
-    }
-  }
-  public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatatypes) {
-    return Domain.ComputeMayInvolveReferences(visitedDatatypes) || Range.ComputeMayInvolveReferences(visitedDatatypes);
-  }
-
-  public override BinaryExpr.ResolvedOpcode ResolvedOpcodeForIn => BinaryExpr.ResolvedOpcode.InMap;
-  public override ComprehensionExpr.CollectionBoundedPool GetBoundedPool(Expression source) {
-    return new ComprehensionExpr.MapBoundedPool(source, Domain, Domain, Finite);
-  }
-}
 
 public abstract class TypeProxy : Type {
   public override IEnumerable<INode> Children => Enumerable.Empty<Node>();

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -79,11 +79,15 @@ private string GetFileLine(Uri uri, int lineIndex) {
     if (0 <= lineIndex && lineIndex < lines.Count) {
       return lines[lineIndex];
     }
-    return "<nonexistent line>";
+    return null;
   }
 
   public void WriteSourceCodeSnippet(IToken tok, TextWriter tw) {
     string line = GetFileLine(tok.Uri, tok.line - 1);
+    if (line == null) {
+      return;
+    }
+
     string lineNumber = tok.line.ToString();
     string lineNumberSpaces = new string(' ', lineNumber.Length);
     string columnSpaces = new string(' ', tok.col - 1);
@@ -149,4 +153,4 @@ public override void ReportEndVerifyImplementation(Implementation implementation
     var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok);
     VerificationResults.Add(new ConsoleLogEntry(impl, DistillVerificationResult(result)));
   }
-}
+}

Source/DafnyCore/Generic/ConsoleErrorReporter.cs

@@ -18,51 +18,63 @@ private ConsoleColor ColorForLevel(ErrorLevel level) {
   }
 
   protected override bool MessageCore(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) {
-    if (base.MessageCore(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) {
-      // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI
-      msg = msg.Replace("\n", "\n ");
+    var printMessage = base.MessageCore(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info);
+    if (!printMessage) {
+      return false;
+    }
+
+    // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI
+    msg = msg.Replace("\n", "\n ");
+
+    ConsoleColor previousColor = Console.ForegroundColor;
+    if (Options.OutputWriter == Console.Out) {
+      Console.ForegroundColor = ColorForLevel(level);
+    }
+    var errorLine = ErrorToString(level, tok, msg);
 
-      ConsoleColor previousColor = Console.ForegroundColor;
-      if (Options.OutputWriter == Console.Out) {
-        Console.ForegroundColor = ColorForLevel(level);
+    if (Options.Verbose && !String.IsNullOrEmpty(errorId) && errorId != "none") {
+      errorLine += " (ID: " + errorId + ")\n";
+      var info = ErrorRegistry.GetDetail(errorId);
+      if (info != null) {
+        errorLine += info; // already ends with eol character
       }
-      var errorLine = ErrorToString(level, tok, msg);
-      while (tok is NestedToken nestedToken) {
-        tok = nestedToken.Inner;
-        if (tok.Filepath == nestedToken.Filepath &&
-            tok.line == nestedToken.line &&
-            tok.col == nestedToken.col) {
-          continue;
-        }
-        msg = nestedToken.Message ?? "[Related location]";
-        errorLine += $" {msg} {tok.TokenToString(Options)}";
+    } else {
+      errorLine += "\n";
+    }
+
+    var innerToken = tok;
+    while (innerToken is NestedToken nestedToken) {
+      innerToken = nestedToken.Inner;
+      if (innerToken.Filepath == nestedToken.Filepath &&
+          innerToken.line == nestedToken.line &&
+          innerToken.col == nestedToken.col) {
+        continue;
       }
 
-      if (Options.Verbose && !String.IsNullOrEmpty(errorId) && errorId != "none") {
-        errorLine += " (ID: " + errorId + ")\n";
-        var info = ErrorRegistry.GetDetail(errorId);
-        if (info != null) {
-          errorLine += info; // already ends with eol character
-        }
+      var innerMessage = nestedToken.Message;
+      if (innerMessage == null) {
+        innerMessage = "Related location";
       } else {
-        errorLine += "\n";
+        innerMessage = "Related location: " + innerMessage;
       }
 
-      Options.OutputWriter.Write(errorLine);
+      errorLine += $"{innerToken.TokenToString(Options)}: {innerMessage}\n";
+    }
 
-      if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) {
-        TextWriter tw = new StringWriter();
-        new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
-        Options.OutputWriter.Write(tw.ToString());
-      }
+    Options.OutputWriter.Write(errorLine);
 
-      if (Options.OutputWriter == Console.Out) {
-        Console.ForegroundColor = previousColor;
-      }
-      return true;
+
+    if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) {
+      TextWriter tw = new StringWriter();
+      new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
+      Options.OutputWriter.Write(tw.ToString());
+    }
+
+    if (Options.OutputWriter == Console.Out) {
+      Console.ForegroundColor = previousColor;
     }
 
-    return false;
+    return true;
   }
 
   public ConsoleErrorReporter(DafnyOptions options) : base(options) {

Source/DafnyCore/Generic/ErrorReporter.cs

@@ -17,7 +17,7 @@ protected ErrorReporter(DafnyOptions options) {
   public bool HasErrorsUntilResolver => ErrorCountUntilResolver > 0;
   public int ErrorCountUntilResolver => CountExceptVerifierAndCompiler(ErrorLevel.Error);
 
-  public virtual bool Message(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) {
+  public bool Message(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) {
     if (Options.WarningsAsErrors && level == ErrorLevel.Warning) {
       level = ErrorLevel.Error;
     }

Source/DafnyCore/JsonDiagnostics.cs

@@ -61,9 +61,10 @@ private static JsonObject SerializeRelated(Boogie.IToken tok, string? category,
   }
 
   private static IEnumerable<JsonNode> SerializeInnerTokens(Boogie.IToken tok) {
-    while (tok is NestedToken ntok) {
-      tok = ntok.Inner;
-      yield return SerializeRelated(tok, null, "Related location");
+    while (tok is NestedToken nestedToken) {
+      tok = nestedToken.Inner;
+      var message = nestedToken.Message != null ? "Related location: " + nestedToken.Message : "Related location";
+      yield return SerializeRelated(tok, null, message);
     }
   }
 
@@ -112,7 +113,7 @@ public DafnyJsonConsolePrinter(DafnyOptions options) : base(options) {
 public class JsonConsoleErrorReporter : BatchErrorReporter {
   protected override bool MessageCore(MessageSource source, ErrorLevel level, string errorID, Dafny.IToken tok, string msg) {
     if (base.MessageCore(source, level, errorID, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) {
-      new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Options.OutputWriter);
+      new DiagnosticMessageData(source, level, tok, level == ErrorLevel.Error ? "Error" : null, msg, null).WriteJsonTo(Options.OutputWriter);
       return true;
     }
 
@@ -121,4 +122,4 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri
 
   public JsonConsoleErrorReporter(DafnyOptions options) : base(options) {
   }
-}
+}

Source/DafnyCore/Resolver/ProgramResolver.cs

@@ -219,7 +219,8 @@ protected void InstantiateReplaceableModules(Program dafnyProgram) {
       if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) {
         var target = compiledModule.Implements.Target.Def;
         if (target.Replacement != null) {
-          Reporter!.Error(MessageSource.Compiler, new NestedToken(compiledModule.Tok, target.Replacement.Tok, "Other replacing module:"),
+          Reporter!.Error(MessageSource.Compiler, new NestedToken(compiledModule.Tok, target.Replacement.Tok,
+              $"other replacing module"),
             "a replaceable module may only be replaced once");
         } else {
           target.Replacement = compiledModule.Replacement ?? compiledModule;

Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs

@@ -58,7 +58,7 @@ protected override WorkspaceSymbolRegistrationOptions CreateRegistrationOptions(
               Name = name,
               ContainerName = def.Kind.ToString(),
               Kind = FromDafnySymbolKind(def.Kind),
-              Location = Workspace.Util.CreateLocation(def.NameToken)
+              Location = Workspace.DiagnosticUtil.CreateLocation(def.NameToken)
             }, matchDistance);
           }
         }