Refactor the error reporting code

The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.

1 files changed, 164 insertions, 0 deletions

diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
new file mode 100644
index 00000000..c3797574
--- /dev/null
+++ b/Source/Dafny/Reporting.cs
@@ -0,0 +1,164 @@
+using Microsoft.Boogie;

+using System;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Dafny {

+  public enum ErrorLevel {

+    Info, Warning, Error

+  }

+

+  public enum MessageSource {

+    Parser, Resolver, Translator, Rewriter, Other,

+    RefinementTransformer,

+    Cloner

+  }

+

+  public struct ErrorMessage {

+    public IToken token;

+    public string message;

+    public MessageSource source;

+  }

+

+  public abstract class ErrorReporter {

+    public bool ErrorsOnly { get; set; }

+    public Dictionary<ErrorLevel, List<ErrorMessage>> AllMessages { get; private set; }

+

+    protected ErrorReporter() {

+      ErrorsOnly = false;

+      AllMessages = new Dictionary<ErrorLevel, List<ErrorMessage>>();

+      AllMessages[ErrorLevel.Error] = new List<ErrorMessage>();

+      AllMessages[ErrorLevel.Warning] = new List<ErrorMessage>();

+      AllMessages[ErrorLevel.Info] = new List<ErrorMessage>();

+    }

+

+    protected bool ShouldDiscard(MessageSource source, ErrorLevel level) {

+      return ((ErrorsOnly && level != ErrorLevel.Error) ||

+              (!DafnyOptions.O.PrintTooltips && level == ErrorLevel.Info));

+    }

+

+    // This is the only thing that needs to be overriden

+    public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

+      var discard = ShouldDiscard(source, level);

+

+      if (!discard) {

+        AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });

+        return true;

+      }

+

+      return false;

+    }

+

+    public int Count(ErrorLevel level) {

+      return AllMessages[level].Count;

+    }

+

+    public void Error(MessageSource source, IToken tok, string msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Message(source, ErrorLevel.Error, tok, msg);

+    }

+

+    // This method required by the Parser

+    internal void Error(MessageSource source, string filename, int line, int col, string msg) {

+      var tok = new Token(line, col);

+      tok.filename = filename;

+      Error(source, tok, msg);

+    }

+

+    public void Error(MessageSource source, IToken tok, string msg, params object[] args) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Error(source, tok, String.Format(msg, args));

+    }

+

+    public void Error(MessageSource source, Declaration d, string msg, params object[] args) {

+      Contract.Requires(d != null);

+      Contract.Requires(msg != null);

+      Error(source, d.tok, msg, args);

+    }

+

+    public void Error(MessageSource source, Statement s, string msg, params object[] args) {

+      Contract.Requires(s != null);

+      Contract.Requires(msg != null);

+      Error(source, s.Tok, msg, args);

+    }

+

+    public void Error(MessageSource source, NonglobalVariable v, string msg, params object[] args) {

+      Contract.Requires(v != null);

+      Contract.Requires(msg != null);

+      Error(source, v.tok, msg, args);

+    }

+

+    public void Error(MessageSource source, Expression e, string msg, params object[] args) {

+      Contract.Requires(e != null);

+      Contract.Requires(msg != null);

+      Error(source, e.tok, msg, args);

+    }

+

+    public void Warning(MessageSource source, IToken tok, string msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Message(source, ErrorLevel.Warning, tok, msg);

+    }

+

+    public void Warning(MessageSource source, IToken tok, string msg, params object[] args) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Warning(source, tok, String.Format(msg, args));

+    }

+

+    public void Info(MessageSource source, IToken tok, string msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Message(source, ErrorLevel.Info, tok, msg);

+    }

+

+    public void Info(MessageSource source, IToken tok, string msg, params object[] args) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      Info(source, tok, String.Format(msg, args));

+    }

+

+    public string ErrorToString(ErrorLevel header, IToken tok, string msg) {

+      return ErrorToString_Internal(": " + header.ToString(), tok.filename, tok.line, tok.col, ": " + msg);

+    }

+

+    public string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

+      return ErrorToString_Internal(": " + header.ToString(), filename, oneBasedLine, oneBasedColumn, ": " + msg);

+    }

+

+    public string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

+      return String.Format("{0}({1},{2}){3}{4}", filename, oneBasedLine, oneBasedColumn - 1, header, msg ?? "");

+    }

+  }

+

+  public class ConsoleErrorReporter : ErrorReporter {

+    private ConsoleColor ColorForLevel(ErrorLevel level) {

+      switch (level) {

+        case ErrorLevel.Error:

+          return ConsoleColor.Red;

+        case ErrorLevel.Warning:

+          return ConsoleColor.Yellow;

+        case ErrorLevel.Info:

+          return ConsoleColor.Green;

+        default:

+          throw new cce.UnreachableException();

+      }

+    }

+

+    public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

+      if (base.Message(source, level, tok, msg)) {

+        ConsoleColor previousColor = Console.ForegroundColor;

+        Console.ForegroundColor = ColorForLevel(level);

+        Console.WriteLine(ErrorToString(level, tok, msg));

+        Console.ForegroundColor = previousColor;

+        return true;

+      } else {

+        return false;

+      }

+    }

+  }

+}