Hover text for default decreases clauses of loops.

Collected various routines used to create resolved Dafny expressions into the Expression class.

3 files changed, 356 insertions, 249 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9b016a38..988b6717 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -235,6 +235,7 @@ namespace Microsoft.Dafny {
       }

     }

 

+    [Pure]

     public abstract bool Equals(Type that);

 

     public bool IsSubrangeType {

@@ -1083,6 +1084,27 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Yields all functions and methods that are members of some non-iterator class in the given

+    /// list of declarations, as well as any IteratorDecl's in that list.

+    /// </summary>

+    public static IEnumerable<ICallable> AllItersAndCallables(List<TopLevelDecl> declarations) {

+      foreach (var d in declarations) {

+        if (d is IteratorDecl) {

+          var iter = (IteratorDecl)d;

+          yield return iter;

+        } else if (d is ClassDecl) {

+          var cl = (ClassDecl)d;

+          foreach (var member in cl.Members) {

+            var clbl = member as ICallable;

+            if (clbl != null) {

+              yield return clbl;

+            }

+          }

+        }

+      }

+    }

+

     public static IEnumerable<IteratorDecl> AllIteratorDecls(List<TopLevelDecl> declarations) {

       foreach (var d in declarations) {

         var iter = d as IteratorDecl;

@@ -1395,6 +1417,7 @@ namespace Microsoft.Dafny {
     public Constructor Member_Init;  // created during registration phase of resolution; its specification is filled in during resolution

     public Predicate Member_Valid;  // created during registration phase of resolution; its specification is filled in during resolution

     public Method Member_MoveNext;  // created during registration phase of resolution; its specification is filled in during resolution

+    public readonly VarDecl YieldCountVariable;

     public IteratorDecl(IToken iteratorKeywordTok, IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

                         List<Formal> ins, List<Formal> outs,

                         Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,

@@ -1435,6 +1458,26 @@ namespace Microsoft.Dafny {
       OutsFields = new List<Field>();

       OutsHistoryFields = new List<Field>();

       DecreasesFields = new List<Field>();

+

+      YieldCountVariable = new VarDecl(tok, tok, "_yieldCount", new EverIncreasingType(), true);

+      YieldCountVariable.type = YieldCountVariable.OptionalType;  // resolve YieldCountVariable here

+    }

+

+    /// <summary>

+    /// This Dafny type exists only for the purpose of giving the yield-count variable a type, so

+    /// that the type can be recognized during translation of Dafny into Boogie.  It represents

+    /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),

+    /// not the usual (\lambda x,y :: x LESS y AND 0 ATMOST y).

+    /// </summary>

+    public class EverIncreasingType : BasicType

+    {

+      [Pure]

+      public override string TypeName(ModuleDefinition context) {

+        return "_increasingInt";

+      }

+      public override bool Equals(Type that) {

+        return that.Normalize() is EverIncreasingType;

+      }

     }

 

     bool ICodeContext.IsGhost { get { return false; } }

@@ -3097,6 +3140,7 @@ namespace Microsoft.Dafny {
   {

     public readonly List<MaybeFreeExpression> Invariants;

     public readonly Specification<Expression> Decreases;

+    public bool InferredDecreases;  // filled in by resolution

     public readonly Specification<FrameExpression> Mod;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -3802,6 +3846,180 @@ namespace Microsoft.Dafny {
     public virtual IEnumerable<Expression> SubExpressions {

       get { yield break; }

     }

+

+    public static IEnumerable<Expression> Conjuncts(Expression expr) {

+      Contract.Requires(expr != null);

+      Contract.Requires(expr.Type is BoolType);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));

+

+      // strip off parens

+      while (true) {

+        var pr = expr as ParensExpression;

+        if (pr == null) {

+          break;

+        } else {

+          expr = pr.E;

+        }

+      }

+

+      var bin = expr as BinaryExpr;

+      if (bin != null && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

+        foreach (Expression e in Conjuncts(bin.E0)) {

+          yield return e;

+        }

+        foreach (Expression e in Conjuncts(bin.E1)) {

+          yield return e;

+        }

+        yield break;

+      }

+      yield return expr;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 - e1"

+    /// </summary>

+    public static Expression CreateSubtract(Expression e0, Expression e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(e0.Type is IntType && e1.Type is IntType);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);

+      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here

+      s.Type = Type.Int;  // resolve here

+      return s;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e + n"

+    /// </summary>

+    public static Expression CreateIncrement(Expression e, int n) {

+      Contract.Requires(e != null);

+      Contract.Requires(e.Type is IntType);

+      Contract.Requires(0 <= n);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      if (n == 0) {

+        return e;

+      }

+      var nn = new LiteralExpr(e.tok, n);

+      nn.Type = Type.Int;

+      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Add, e, nn);

+      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;

+      p.Type = Type.Int;

+      return p;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e - n"

+    /// </summary>

+    public static Expression CreateDecrement(Expression e, int n) {

+      Contract.Requires(e != null);

+      Contract.Requires(e.Type is IntType);

+      Contract.Requires(0 <= n);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      if (n == 0) {

+        return e;

+      }

+      var nn = Expression.CreateIntLiteral(e.tok, n);

+      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);

+      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

+      p.Type = Type.Int;

+      return p;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "n"

+    /// </summary>

+    public static Expression CreateIntLiteral(IToken tok, int n) {

+      Contract.Requires(tok != null);

+      Contract.Requires(n != int.MinValue);

+      if (0 <= n) {

+        var nn = new LiteralExpr(tok, n);

+        nn.Type = Type.Int;

+        return nn;

+      } else {

+        return CreateDecrement(CreateIntLiteral(tok, 0), -n);

+      }

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 LESS e1"

+    /// </summary>

+    public static Expression CreateLess(Expression e0, Expression e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(e0.Type is IntType && e1.Type is IntType);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1);

+      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt;  // resolve here

+      s.Type = Type.Bool;  // resolve here

+      return s;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 ATMOST e1"

+    /// </summary>

+    public static Expression CreateAtMost(Expression e0, Expression e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(e0.Type is IntType && e1.Type is IntType);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1);

+      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

+      s.Type = Type.Bool;  // resolve here

+      return s;

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 && e1"

+    /// </summary>

+    public static Expression CreateAnd(Expression a, Expression b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Requires(a.Type is BoolType && b.Type is BoolType);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      if (LiteralExpr.IsTrue(a)) {

+        return b;

+      } else if (LiteralExpr.IsTrue(b)) {

+        return a;

+      } else {

+        var and = new BinaryExpr(a.tok, BinaryExpr.Opcode.And, a, b);

+        and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here

+        and.Type = Type.Bool;  // resolve here

+        return and;

+      }

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 ==> e1"

+    /// </summary>

+    public static Expression CreateImplies(Expression a, Expression b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Requires(a.Type is BoolType && b.Type is BoolType);

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) {

+        return b;

+      } else {

+        var imp = new BinaryExpr(a.tok, BinaryExpr.Opcode.Imp, a, b);

+        imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  // resolve here

+        imp.Type = Type.Bool;  // resolve here

+        return imp;

+      }

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "if test then e0 else e1"

+    /// </summary>

+    public static Expression CreateITE(Expression test, Expression e0, Expression e1) {

+      Contract.Requires(test != null);

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(test.Type is BoolType && e0.Type.Equals(e1.Type));

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      var ite = new ITEExpr(test.tok, test, e0, e1);

+      ite.Type = e0.type;  // resolve here

+      return ite;

+    }

   }

 

   /// <summary>

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 45e4eb14..be48e23a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -159,6 +159,7 @@ namespace Microsoft.Dafny
 

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

+      var origErrorCount = ErrorCount;

       var bindings = new ModuleBindings(null);

       var b = BindModuleNames(prog.DefaultModuleDef, bindings);

       bindings.BindName("_module", prog.DefaultModule, b);

@@ -269,6 +270,10 @@ namespace Microsoft.Dafny
         } else { Contract.Assert(false); }

         Contract.Assert(decl.Signature != null);

       }

+      if (ErrorCount != origErrorCount) {

+        // do nothing else

+        return;

+      }

       // compute IsRecursive bit for mutually recursive functions and methods

       foreach (var module in prog.Modules) {

         foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) {

@@ -300,8 +305,23 @@ namespace Microsoft.Dafny
           }

         }

       }

+      // fill in default decreases clauses:  for functions and methods, and for loops

       FillInDefaultDecreasesClauses(prog);

       foreach (var module in prog.Modules) {

+        foreach (var clbl in ModuleDefinition.AllItersAndCallables(module.TopLevelDecls)) {

+          Statement body = null;

+          if (clbl is Method) {

+            body = ((Method)clbl).Body;

+          } else if (clbl is IteratorDecl) {

+            body = ((IteratorDecl)clbl).Body;

+          }

+          if (body != null) {

+            var c = new FillInDefaultLoopDecreases_Visitor(this, clbl);

+            c.Visit(body);

+          }

+        }

+      }

+      foreach (var module in prog.Modules) {

         foreach (var iter in ModuleDefinition.AllIteratorDecls(module.TopLevelDecls)) {

           var tok = iter.IteratorKeywordTok;

           ReportAdditionalInformation(tok, Printer.IteratorClassToString(iter), tok.val.Length);

@@ -1639,7 +1659,7 @@ namespace Microsoft.Dafny
     #region Visitors

     class ResolverBottomUpVisitor : BottomUpVisitor

     {

-      Resolver resolver;

+      protected Resolver resolver;

       public ResolverBottomUpVisitor(Resolver resolver) {

         Contract.Requires(resolver != null);

         this.resolver = resolver;

@@ -2375,6 +2395,31 @@ namespace Microsoft.Dafny
     #endregion CheckEqualityTypes

 

     // ------------------------------------------------------------------------------------------------------

+    // ----- FillInDefaultLoopDecreases ---------------------------------------------------------------------

+    // ------------------------------------------------------------------------------------------------------

+    #region FillInDefaultLoopDecreases

+    class FillInDefaultLoopDecreases_Visitor : ResolverBottomUpVisitor

+    {

+      readonly ICallable EnclosingMethod;

+      public FillInDefaultLoopDecreases_Visitor(Resolver resolver, ICallable enclosingMethod)

+        : base(resolver) {

+        Contract.Requires(resolver != null);

+        Contract.Requires(enclosingMethod != null);

+        EnclosingMethod = enclosingMethod;

+      }

+      protected override void VisitOneStmt(Statement stmt) {

+        if (stmt is WhileStmt) {

+          var s = (WhileStmt)stmt;

+          resolver.FillInDefaultLoopDecreases(s, s.Guard, s.Decreases.Expressions, EnclosingMethod);

+        } else if (stmt is AlternativeLoopStmt) {

+          var s = (AlternativeLoopStmt)stmt;

+          resolver.FillInDefaultLoopDecreases(s, null, s.Decreases.Expressions, EnclosingMethod);

+        }

+      }

+    }

+    #endregion FillInDefaultLoopDecreases

+

+    // ------------------------------------------------------------------------------------------------------

     // ------------------------------------------------------------------------------------------------------

     // ------------------------------------------------------------------------------------------------------

 

@@ -4233,7 +4278,7 @@ namespace Microsoft.Dafny
           // do not build Result from the lines if there were errors, as it might be ill-typed and produce unnecessary resolution errors

           s.Result = s.ResultOp.StepExpr(s.Lines.First(), s.Lines.Last());

         } else {

-          s.Result = CalcStmt.DefaultOp.StepExpr(CreateResolvedLiteral(s.Tok, 0), CreateResolvedLiteral(s.Tok, 0));

+          s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0));

         }

         ResolveExpression(s.Result, true, codeContext);

         Contract.Assert(s.Result != null);        

@@ -4341,6 +4386,79 @@ namespace Microsoft.Dafny
         Contract.Assert(false); throw new cce.UnreachableException();

       }

     }

+

+    void FillInDefaultLoopDecreases(LoopStmt loopStmt, Expression guard, List<Expression> theDecreases, ICallable enclosingMethod) {

+      Contract.Requires(loopStmt != null);

+      Contract.Requires(theDecreases != null);

+

+      if (theDecreases.Count == 0 && guard != null) {

+        loopStmt.InferredDecreases = true;

+        Expression prefix = null;

+        foreach (Expression guardConjunct in Expression.Conjuncts(guard)) {

+          Expression guess = null;

+          BinaryExpr bin = guardConjunct as BinaryExpr;

+          if (bin != null) {

+            switch (bin.ResolvedOp) {

+              case BinaryExpr.ResolvedOpcode.Lt:

+              case BinaryExpr.ResolvedOpcode.Le:

+                // for A < B and A <= B, use the decreases B - A

+                guess = Expression.CreateSubtract(bin.E1, bin.E0);

+                break;

+              case BinaryExpr.ResolvedOpcode.Ge:

+              case BinaryExpr.ResolvedOpcode.Gt:

+                // for A >= B and A > B, use the decreases A - B

+                guess = Expression.CreateSubtract(bin.E0, bin.E1);

+                break;

+              case BinaryExpr.ResolvedOpcode.NeqCommon:

+                if (bin.E0.Type is IntType) {

+                  // for A != B where A and B are integers, use the absolute difference between A and B (that is: if A <= B then B-A else A-B)

+                  var AminusB = Expression.CreateSubtract(bin.E0, bin.E1);

+                  var BminusA = Expression.CreateSubtract(bin.E1, bin.E0);

+                  var test = Expression.CreateAtMost(bin.E0, bin.E1);

+                  guess = Expression.CreateITE(test, BminusA, AminusB);

+                }

+                break;

+              default:

+                break;

+            }

+          }

+          if (guess != null) {

+            if (prefix != null) {

+              // Make the following guess:  if prefix then guess else -1

+              guess = Expression.CreateITE(prefix, guess, Expression.CreateIntLiteral(prefix.tok, -1));

+            }

+            theDecreases.Add(guess);

+            break;  // ignore any further conjuncts

+          }

+          if (prefix == null) {

+            prefix = guardConjunct;

+          } else {

+            prefix = Expression.CreateAnd(prefix, guardConjunct);

+          }

+        }

+      }

+      if (enclosingMethod is IteratorDecl) {

+        var iter = (IteratorDecl)enclosingMethod;

+        var ie = new IdentifierExpr(loopStmt.Tok, iter.YieldCountVariable.Name);

+        ie.Var = iter.YieldCountVariable;  // resolve here

+        ie.Type = iter.YieldCountVariable.Type;  // resolve here

+        theDecreases.Insert(0, ie);

+        loopStmt.InferredDecreases = true;

+      }

+      if (loopStmt.InferredDecreases) {

+        string s = "decreases ";

+        if (theDecreases.Count == 0) {

+          s += ";";  // found nothing; indicate this more explicitly by just showing a semi-colon

+        } else {

+          string sep = "";

+          foreach (var d in theDecreases) {

+            s += sep + Printer.ExprToString(d);

+            sep = ", ";

+          }

+        }

+        ReportAdditionalInformation(loopStmt.Tok, s, loopStmt.Tok.val.Length);

+      }

+    }

     private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(codeContext != null);

 

@@ -6715,7 +6833,7 @@ namespace Microsoft.Dafny
             foundBoundsForBv = true;

           }

           // Go through the conjuncts of the range expression to look for bounds.

-          Expression lowerBound = bv.Type is NatType ? Resolver.CreateResolvedLiteral(bv.Tok, 0) : null;

+          Expression lowerBound = bv.Type is NatType ? Expression.CreateIntLiteral(bv.Tok, 0) : null;

           Expression upperBound = null;

           if (returnAllBounds && lowerBound != null) {

             bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

@@ -6771,7 +6889,7 @@ namespace Microsoft.Dafny
               case BinaryExpr.ResolvedOpcode.EqCommon:

                 if (bv.Type is IntType) {

                   var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

+                  bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Expression.CreateIncrement(otherOperand, 1)));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 } else if (returnAllBounds && bv.Type is SetType) {

@@ -6787,12 +6905,12 @@ namespace Microsoft.Dafny
                 if (whereIsBv == 0 && upperBound == null) {

                   upperBound = e1;  // bv < E

                 } else if (whereIsBv == 1 && lowerBound == null) {

-                  lowerBound = Plus(e0, 1);  // E < bv

+                  lowerBound = Expression.CreateIncrement(e0, 1);  // E < bv

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.Le:

                 if (whereIsBv == 0 && upperBound == null) {

-                  upperBound = Plus(e1, 1);  // bv <= E

+                  upperBound = Expression.CreateIncrement(e1, 1);  // bv <= E

                 } else if (whereIsBv == 1 && lowerBound == null) {

                   lowerBound = e0;  // E <= bv

                 }

@@ -7064,38 +7182,6 @@ namespace Microsoft.Dafny
       }

     }

 

-    public static Expression Plus(Expression e, int n) {

-      Contract.Requires(0 <= n);

-

-      var nn = new LiteralExpr(e.tok, n);

-      nn.Type = Type.Int;

-      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Add, e, nn);

-      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;

-      p.Type = Type.Int;

-      return p;

-    }

-

-    public static Expression Minus(Expression e, int n) {

-      Contract.Requires(0 <= n);

-

-      var nn = CreateResolvedLiteral(e.tok, n);

-      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);

-      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

-      p.Type = Type.Int;

-      return p;

-    }

-

-    public static Expression CreateResolvedLiteral(IToken tok, int n) {

-      Contract.Requires(tok != null);

-      if (0 <= n) {

-        var nn = new LiteralExpr(tok, n);

-        nn.Type = Type.Int;

-        return nn;

-      } else {

-        return Minus(CreateResolvedLiteral(tok, 0), -n);

-      }

-    }

-

     /// <summary>

     /// Returns the set of free variables in "expr".

     /// Requires "expr" to be successfully resolved.

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 974aeef0..a9546227 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1413,7 +1413,8 @@ namespace Microsoft.Dafny {
         builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

       // add the _yieldCount variable, and assume its initial value to be 0

-      yieldCountVariable = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "_yieldCount", Bpl.Type.Int));

+      yieldCountVariable = new Bpl.LocalVariable(iter.tok,

+        new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(currentDeclaration), TrType(iter.YieldCountVariable.Type)));

       yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran);  // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption

       localVariables.Add(yieldCountVariable);

       builder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0))));

@@ -1967,16 +1968,14 @@ namespace Microsoft.Dafny {
       var k = new IdentifierExpr(pp.tok, pp.K.Name);

       k.Var = pp.K;  // resolve here

       k.Type = pp.K.Type;  // resolve here

-      var kMinusOne = CreateIntSub(pp.tok, k, Resolver.CreateResolvedLiteral(pp.tok, 1));

+      var kMinusOne = Expression.CreateSubtract(k, Expression.CreateIntLiteral(pp.tok, 1));

 

       var s = new PrefixCallSubstituter(null, paramMap, pp.Co, kMinusOne, this);

       body = s.Substitute(body);

 

       // add antecedent "0 < _k ==>"

-      var kIsPositive = new BinaryExpr(pp.tok, BinaryExpr.Opcode.Lt, Resolver.CreateResolvedLiteral(pp.tok, 0), k);

-      kIsPositive.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt;  // resolve here

-      kIsPositive.Type = Type.Int;  // resolve here

-      return DafnyImp(kIsPositive, body);

+      var kIsPositive = Expression.CreateLess(Expression.CreateIntLiteral(pp.tok, 0), k);

+      return Expression.CreateImplies(kIsPositive, body);

     }

 

     void AddSynonymAxiom(Function f) {

@@ -2372,11 +2371,11 @@ namespace Microsoft.Dafny {
               var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);

               neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon;  // resolve here

               neqNull.Type = Type.Bool;  // resolve here

-              parRange = DafnyAnd(parRange, neqNull);

+              parRange = Expression.CreateAnd(parRange, neqNull);

             }

             foreach (var pre in m.Req) {

               if (!pre.IsFree) {

-                parRange = DafnyAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));

+                parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));

               }

             }

             // construct an expression (generator) for:  VF' << VF

@@ -3332,38 +3331,6 @@ namespace Microsoft.Dafny {
       return total;

     }

 

-    Expression DafnyAnd(Expression a, Expression b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-

-      if (LiteralExpr.IsTrue(a)) {

-        return b;

-      } else if (LiteralExpr.IsTrue(b)) {

-        return a;

-      } else {

-        BinaryExpr and = new BinaryExpr(a.tok, BinaryExpr.Opcode.And, a, b);

-        and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here

-        and.Type = Type.Bool;  // resolve here

-        return and;

-      }

-    }

-

-    Expression DafnyImp(Expression a, Expression b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-

-      if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) {

-        return b;

-      } else {

-        BinaryExpr imp = new BinaryExpr(a.tok, BinaryExpr.Opcode.Imp, a, b);

-        imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  // resolve here

-        imp.Type = Type.Bool;  // resolve here

-        return imp;

-      }

-    }

-

     Bpl.Expr BplAnd(IEnumerable<Bpl.Expr> conjuncts) {

       Contract.Requires(conjuncts != null);

       Bpl.Expr eq = Bpl.Expr.True;

@@ -3937,88 +3904,6 @@ namespace Microsoft.Dafny {
       }

     }

 

-    List<Expression> LoopDecreasesWithDefault(IToken tok, Expression Guard, List<Expression> Decreases, out bool inferredDecreases) {

-      Contract.Requires(tok != null);

-      Contract.Requires(Decreases != null);

-

-      List<Expression> theDecreases = Decreases;

-      inferredDecreases = false;

-      if (theDecreases.Count == 0 && Guard != null) {

-        theDecreases = new List<Expression>();

-        Expression prefix = null;

-        foreach (Expression guardConjunct in Conjuncts(Guard)) {

-          Expression guess = null;

-          BinaryExpr bin = guardConjunct as BinaryExpr;

-          if (bin != null) {

-            switch (bin.ResolvedOp) {

-              case BinaryExpr.ResolvedOpcode.Lt:

-              case BinaryExpr.ResolvedOpcode.Le:

-                // for A < B and A <= B, use the decreases B - A

-                guess = CreateIntSub(tok, bin.E1, bin.E0);

-                break;

-              case BinaryExpr.ResolvedOpcode.Ge:

-              case BinaryExpr.ResolvedOpcode.Gt:

-                // for A >= B and A > B, use the decreases A - B

-                guess = CreateIntSub(tok, bin.E0, bin.E1);

-                break;

-              case BinaryExpr.ResolvedOpcode.NeqCommon:

-                if (bin.E0.Type is IntType) {

-                  // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)

-                  Expression AminusB = CreateIntSub(tok, bin.E0, bin.E1);

-                  Expression BminusA = CreateIntSub(tok, bin.E1, bin.E0);

-                  Expression zero = Resolver.CreateResolvedLiteral(tok, 0);

-                  BinaryExpr test = new BinaryExpr(tok, BinaryExpr.Opcode.Le, zero, AminusB);

-                  test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

-                  test.Type = Type.Bool;  // resolve here

-                  guess = CreateIntITE(tok, test, AminusB, BminusA);

-                }

-                break;

-              default:

-                break;

-            }

-          }

-          if (guess != null) {

-            if (prefix != null) {

-              // Make the following guess:  if prefix then guess else -1

-              Expression negativeOne = Resolver.CreateResolvedLiteral(tok, -1);

-              guess = CreateIntITE(tok, prefix, guess, negativeOne);

-            }

-            theDecreases.Add(guess);

-            inferredDecreases = true;

-            break;  // ignore any further conjuncts

-          }

-          if (prefix == null) {

-            prefix = guardConjunct;

-          } else {

-            prefix = DafnyAnd(prefix, guardConjunct);

-          }

-        }

-      }

-      if (yieldCountVariable != null) {

-        var decr = new List<Expression>();

-        decr.Add(new BoogieWrapper(new Bpl.IdentifierExpr(tok, yieldCountVariable), new EverIncreasingType()));

-        decr.AddRange(theDecreases);

-        theDecreases = decr;

-      }

-      return theDecreases;

-    }

-

-    /// <summary>

-    /// This Dafny type, which exists only during translation of Dafny into Boogie, represents

-    /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),

-    /// not the usual (\lambda x,y :: x LESS y AND 0 ATMOST y).

-    /// </summary>

-    public class EverIncreasingType : BasicType

-    {

-      [Pure]

-      public override string TypeName(ModuleDefinition context) {

-        return "_increasingInt";

-      }

-      public override bool Equals(Type that) {

-        return that.Normalize() is EverIncreasingType;

-      }

-    }

-

     void CloneVariableAsBoundVar(IToken tok, IVariable iv, string prefix, out BoundVar bv, out IdentifierExpr ie) {

       Contract.Requires(tok != null);

       Contract.Requires(iv != null);

@@ -4849,7 +4734,7 @@ namespace Microsoft.Dafny {
         return Bpl.Type.Bool;

       } else if (type is IntType) {

         return Bpl.Type.Int;

-      } else if (type is EverIncreasingType) {

+      } else if (type is IteratorDecl.EverIncreasingType) {

         return Bpl.Type.Int;

       } else if (type.IsTypeParameter) {

         return predef.BoxType;

@@ -5551,7 +5436,7 @@ namespace Microsoft.Dafny {
           var g = Substitute(tup.Item2, null, substMap);

           var subrange = SubrangeConstraint(x.tok, guess, x.Type);

           if (subrange != null) {

-            g = CreateAnd(x.tok, subrange, g);

+            g = Expression.CreateAnd(subrange, g);

           }

           result.Add(new Tuple<List<BoundVar>, Expression>(tup.Item1, g));

         }

@@ -5613,7 +5498,7 @@ namespace Microsoft.Dafny {
           if (bound is ComprehensionExpr.IntBoundedPool) {

             var bnd = (ComprehensionExpr.IntBoundedPool)bound;

             if (bnd.LowerBound != null) yield return bnd.LowerBound;

-            if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);

+            if (bnd.UpperBound != null) yield return Expression.CreateDecrement(bnd.UpperBound, 1);

           } else if (bound is ComprehensionExpr.SubSetBoundedPool) {

             var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;

             yield return bnd.UpperBound;

@@ -6090,9 +5975,7 @@ namespace Microsoft.Dafny {
       int loopId = loopHeapVarCount;

       loopHeapVarCount++;

 

-      // use simple heuristics to create a default decreases clause, if none is given

-      bool inferredDecreases;

-      List<Expression> theDecreases = LoopDecreasesWithDefault(s.Tok, Guard, s.Decreases.Expressions, out inferredDecreases);

+      var theDecreases = s.Decreases.Expressions;

 

       Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreLoopHeap" + loopId, predef.HeapType));

       locals.Add(preLoopHeapVar);

@@ -6218,7 +6101,7 @@ namespace Microsoft.Dafny {
         }

         Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);

         string msg;

-        if (inferredDecreases) {

+        if (s.InferredDecreases) {

           msg = "cannot prove termination; try supplying a decreases clause for the loop";

           if (s is RefinedWhileStmt) {

             msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)";

@@ -6508,86 +6391,6 @@ namespace Microsoft.Dafny {
       }

     }

 

-    static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type is IntType && e1.Type is IntType);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-      BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);

-      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here

-      s.Type = Type.Int;  // resolve here

-      return s;

-    }

-

-    static Expression CreateIntAtMost(IToken tok, Expression e0, Expression e1) {

-      Contract.Requires(tok != null);

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type is IntType && e1.Type is IntType);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-      BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Le, e0, e1);

-      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

-      s.Type = Type.Bool;  // resolve here

-      return s;

-    }

-

-    static Expression CreateAnd(IToken tok, Expression e0, Expression e1) {

-      Contract.Requires(tok != null);

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type is BoolType && e1.Type is BoolType);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-      BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.And, e0, e1);

-      s.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here

-      s.Type = Type.Bool;  // resolve here

-      return s;

-    }

-

-    static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)

-    {

-      Contract.Requires(tok != null);

-      Contract.Requires(test != null);

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

-      Contract.Requires(test.Type is BoolType && e0.Type is IntType && e1.Type is IntType);

-      Contract.Ensures(Contract.Result<Expression>() != null);

-

-      ITEExpr ite = new ITEExpr(tok, test, e0, e1);

-      ite.Type = Type.Int;  // resolve here

-      return ite;

-    }

-

-    public IEnumerable<Expression> Conjuncts(Expression expr)

-    {

-      Contract.Requires(expr != null);

-      Contract.Requires(expr.Type is BoolType);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));

-

-      // strip off parens

-      while (true) {

-        var pr = expr as ParensExpression;

-        if (pr == null) {

-          break;

-        } else {

-          expr = pr.E;

-        }

-      }

-

-      var bin = expr as BinaryExpr;

-      if (bin != null && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

-        foreach (Expression e in Conjuncts(bin.E0)) {

-          yield return e;

-        }

-        foreach (Expression e in Conjuncts(bin.E1)) {

-          yield return e;

-        }

-        yield break;

-      }

-      yield return expr;

-    }

-

     Dictionary<IVariable, Expression> SetupBoundVarsAsLocals(List<BoundVar> boundVars, StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

       Contract.Requires(boundVars != null);

       Contract.Requires(builder != null);

@@ -6844,7 +6647,7 @@ namespace Microsoft.Dafny {
           atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);

         }

 

-      } else if (ty0 is EverIncreasingType) {

+      } else if (ty0 is IteratorDecl.EverIncreasingType) {

         eq = Bpl.Expr.Eq(e0, e1);

         less = Bpl.Expr.Gt(e0, e1);

         atmost = Bpl.Expr.Ge(e0, e1);

@@ -7550,7 +7353,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tp != null);

 

       if (tp is NatType) {

-        return CreateIntAtMost(tok, Resolver.CreateResolvedLiteral(tok, 0), e);

+        return Expression.CreateAtMost(Expression.CreateIntLiteral(tok, 0), e);

       }

       return null;

     }