Merge.

Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.

1 files changed, 58 insertions, 13 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e5d8250b..ffd6df63 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2961,19 +2961,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  /// <summary>

-  /// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to

-  /// the treatment of other in-parameters.

-  /// </summary>

-  public class ThisSurrogate : Formal

-  {

-    public ThisSurrogate(IToken tok, Type type)

-      : base(tok, "this", type, true, false) {

-      Contract.Requires(tok != null);

-      Contract.Requires(type != null);

-    }

-  }

-

   public class BoundVar : NonglobalVariable {

     public override bool IsMutable {

       get {

@@ -3947,6 +3934,9 @@ namespace Microsoft.Dafny {
       public override bool IsFinite {

         get { return false; }

       }

+      public override int Preference() {

+        return 0;

+      }

     }

 

     /// <summary>

@@ -5758,6 +5748,16 @@ namespace Microsoft.Dafny {
       Contract.Requires(name != null);

       Name = name;

     }

+    /// <summary>

+    /// Constructs a resolved IdentifierExpr.

+    /// </summary>

+    public IdentifierExpr(IVariable v)

+      : base(v.Tok) {

+      Contract.Requires(v != null);

+      Name = v.Name;

+      Var = v;

+      Type = v.Type;

+    }

   }

 

   /// <summary>

@@ -6692,9 +6692,33 @@ namespace Microsoft.Dafny {
       public virtual bool IsFinite {

         get { return true; }  // most bounds are finite

       }

+      public abstract int Preference(); // higher is better

+      

+      public static BoundedPool GetBest(List<BoundedPool> bounds) {

+        Contract.Requires(bounds != null && bounds.Count > 0);

+        var ret = bounds[0];

+        foreach (var bound in bounds) {

+          if (bound.Preference() > ret.Preference()) {

+            ret = bound;

+          } else {            

+            var retInt = ret as ComprehensionExpr.IntBoundedPool;

+            if (retInt != null && (retInt.LowerBound == null || retInt.UpperBound == null)) {

+              var boundInt = bound as ComprehensionExpr.IntBoundedPool;

+              if (boundInt != null) {

+                ret = new ComprehensionExpr.IntBoundedPool(retInt.LowerBound ?? boundInt.LowerBound, 

+                                                           retInt.UpperBound ?? boundInt.UpperBound);

+              }

+            }         

+          }

+        }

+        return ret;

+      }

     }

     public class BoolBoundedPool : BoundedPool

     {

+      public override int Preference() {

+        return 5;

+      }

     }

     public class IntBoundedPool : BoundedPool

     {

@@ -6709,36 +6733,57 @@ namespace Microsoft.Dafny {
           return LowerBound != null && UpperBound != null;

         }

       }

+      public override int Preference() {

+        return 1;

+      }

     }

     public class SetBoundedPool : BoundedPool

     {

       public readonly Expression Set;

       public SetBoundedPool(Expression set) { Set = set; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class SubSetBoundedPool : BoundedPool

     {

       public readonly Expression UpperBound;

       public SubSetBoundedPool(Expression set) { UpperBound = set; }

+      public override int Preference() {

+        return 1;

+      }

     }

     public class SuperSetBoundedPool : BoundedPool

     {

       public readonly Expression LowerBound;

       public SuperSetBoundedPool(Expression set) { LowerBound = set; }

+      public override int Preference() {

+        return 0;

+      }

     }

     public class MapBoundedPool : BoundedPool

     {

       public readonly Expression Map;

       public MapBoundedPool(Expression map) { Map = map; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class SeqBoundedPool : BoundedPool

     {

       public readonly Expression Seq;

       public SeqBoundedPool(Expression seq) { Seq = seq; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class DatatypeBoundedPool : BoundedPool

     {

       public readonly DatatypeDecl Decl;

       public DatatypeBoundedPool(DatatypeDecl d) { Decl = d; }

+      public override int Preference() {

+        return 5;

+      }

     }

 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver