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, 14 insertions, 19 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index f959b537..323abc70 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -365,6 +365,7 @@ namespace Microsoft.Dafny
         return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

+

         var tk = Tok(e.tok);

         var bvs = e.BoundVars.ConvertAll(CloneBoundVar);

         var range = CloneExpr(e.Range);

@@ -703,22 +704,16 @@ namespace Microsoft.Dafny
   abstract class FixpointCloner : Cloner

   {

     protected readonly Expression k;

-    readonly Resolver resolver;

+    protected readonly ErrorReporter reporter;

     readonly string suffix;

-    protected FixpointCloner(Expression k, Resolver resolver)

+    protected FixpointCloner(Expression k, ErrorReporter reporter)

     {

       Contract.Requires(k != null);

-      Contract.Requires(resolver != null);

+      Contract.Requires(reporter != null);

       this.k = k;

-      this.resolver = resolver;

+      this.reporter = reporter;

       this.suffix = string.Format("#[{0}]", Printer.ExprToString(k));

     }

-    protected void ReportAdditionalInformation(IToken tok, string s)

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(s != null);

-      resolver.ReportAdditionalInformation(tok, s + suffix, s.Length);

-    }

   }

 

   /// <summary>

@@ -733,12 +728,12 @@ namespace Microsoft.Dafny
   {

     readonly bool isCoContext;

     readonly ISet<Expression> friendlyCalls;

-    public FixpointLemmaSpecificationSubstituter(ISet<Expression> friendlyCalls, Expression k, Resolver resolver, bool isCoContext)

-      : base(k, resolver)

+    public FixpointLemmaSpecificationSubstituter(ISet<Expression> friendlyCalls, Expression k, ErrorReporter reporter, bool isCoContext)

+      : base(k, reporter)

     {

       Contract.Requires(friendlyCalls != null);

       Contract.Requires(k != null);

-      Contract.Requires(resolver != null);

+      Contract.Requires(reporter != null);

       this.isCoContext = isCoContext;

       this.friendlyCalls = friendlyCalls;

     }

@@ -758,7 +753,7 @@ namespace Microsoft.Dafny
             args.Add(CloneExpr(arg));

           }

           var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args);

-          ReportAdditionalInformation(e.tok, e.Name);

+          reporter.Info(MessageSource.Cloner, e.tok, e.Name);

           return fexp;

         }

       } else if (expr is BinaryExpr && isCoContext) {

@@ -769,7 +764,7 @@ namespace Microsoft.Dafny
           var B = CloneExpr(e.E1);

           var teq = new TernaryExpr(Tok(e.tok), op, k, A, B);

           var opString = op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=";

-          ReportAdditionalInformation(e.tok, opString);

+          reporter.Info(MessageSource.Cloner, e.tok, opString);

           return teq;

         }

       }

@@ -804,12 +799,12 @@ namespace Microsoft.Dafny
   class FixpointLemmaBodyCloner : FixpointCloner

   {

     readonly FixpointLemma context;

-    public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, Resolver resolver)

-      : base(k, resolver)

+    public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ErrorReporter reporter)

+      : base(k, reporter)

     {

       Contract.Requires(context != null);

       Contract.Requires(k != null);

-      Contract.Requires(resolver != null);

+      Contract.Requires(reporter != null);

       this.context = context;

     }

     public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {

@@ -834,7 +829,7 @@ namespace Microsoft.Dafny
           apply.Args.ForEach(arg => args.Add(CloneExpr(arg)));

           var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args);

           var c = new ExprRhs(applyClone);

-          ReportAdditionalInformation(apply.tok, mse.Member.Name);

+          reporter.Info(MessageSource.Cloner, apply.tok, mse.Member.Name);

           return c;

         }

       }