Merge

7 files changed, 110 insertions, 43 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 9495d64e..4d352f65 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1335,7 +1335,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

           wr.Write("@{0} => ", bv.Name);

         }

-        TrExpr(e.Body);

+        TrExpr(e.LogicalBody());

         for (int i = 0; i < n; i++) {

           wr.Write(")");

         }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 39c4c29d..0ce1835f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1361,6 +1361,7 @@ QuantifierGuts<out Expression/*!*/ q>
      List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

      Attributes attrs = null;

      Triggers trigs = null;

+     Expression range = null;

      Expression/*!*/ body;

   .)

   ( Forall                                     (. x = t;  univ = true; .)

@@ -1372,12 +1373,15 @@ QuantifierGuts<out Expression/*!*/ q>
     IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

   }

   { AttributeOrTrigger<ref attrs, ref trigs> }

+  [ "|"

+    Expression<out range>

+  ]

   QSep

   Expression<out body>

   (. if (univ) {

-       q = new ForallExpr(x, bvars, body, trigs, attrs);

+       q = new ForallExpr(x, bvars, range, body, trigs, attrs);

      } else {

-       q = new ExistsExpr(x, bvars, body, trigs, attrs);

+       q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

      }

      parseVarScope.PopMarker();

   .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f76f24de..ad7f5fb6 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2300,17 +2300,23 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class QuantifierExpr : Expression {

+  /// <summary>

+  /// A ComprehensionExpr has the form:

+  ///   BINDER x Attributes | Range(x) :: Term(x)

+  /// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true".

+  /// Currently, BINDER is one of the logical quantifiers "exists" or "forall".

+  /// </summary>

+  public abstract class ComprehensionExpr : Expression {

     public readonly List<BoundVar/*!*/>/*!*/ BoundVars;

-    public readonly Expression/*!*/ Body;

+    public readonly Expression Range;

+    public readonly Expression/*!*/ Term;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(BoundVars != null);

-      Contract.Invariant(Body != null);

+      Contract.Invariant(Term != null);

     }

 

-    public readonly Triggers Trigs;

     public readonly Attributes Attributes;

 

     public abstract class BoundedPool { }

@@ -2338,23 +2344,40 @@ namespace Microsoft.Dafny {
     }

 

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

-    // invariant bounds == null || bounds.Count == BoundVars.Count;

+    // invariant Bounds == null || Bounds.Count == BoundVars.Count;

 

-    public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)

+    public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Attributes attrs)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(bvars));

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

 

       this.BoundVars = bvars;

-      this.Body = body;

-      this.Trigs = trigs;

+      this.Range = range;

+      this.Term = term;

       this.Attributes = attrs;

     }

 

     public override IEnumerable<Expression> SubExpressions {

-      get { yield return Body; }

+      get {

+        if (Range != null) { yield return Range; }

+        yield return Term; 

+      }

+    }

+  }

+

+  public abstract class QuantifierExpr : ComprehensionExpr {

+    public readonly Triggers Trigs;

+

+    public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Triggers trigs, Attributes attrs)

+      : base(tok, bvars, range, term, attrs) {

+      Contract.Requires(tok != null);

+      Contract.Requires(cce.NonNullElements(bvars));

+      Contract.Requires(term != null);

+

+      this.Trigs = trigs;

     }

+    public abstract Expression/*!*/ LogicalBody();

   }

 

   public class Triggers {

@@ -2373,20 +2396,38 @@ namespace Microsoft.Dafny {
   }

 

   public class ForallExpr : QuantifierExpr {

-    public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)

-      : base(tok, bvars, body, trig, attrs) {

+    public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)

+      : base(tok, bvars, range, term, trig, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

       Contract.Requires(tok != null);

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

+    }

+    public override Expression/*!*/ LogicalBody() {

+      if (Range == null) {

+        return Term;

+      }

+      var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.Imp, Range, Term);

+      body.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;

+      body.Type = Term.Type;

+      return body;

     }

   }

 

   public class ExistsExpr : QuantifierExpr {

-    public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)

-      : base(tok, bvars, body, trig, attrs) {

+    public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)

+      : base(tok, bvars, range, term, trig, attrs) {

       Contract.Requires(cce.NonNullElements(bvars));

       Contract.Requires(tok != null);

-      Contract.Requires(body != null);

+      Contract.Requires(term != null);

+    }

+    public override Expression/*!*/ LogicalBody() {

+      if (Range == null) {

+        return Term;

+      }

+      var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.And, Range, Term);

+      body.ResolvedOp = BinaryExpr.ResolvedOpcode.And;

+      body.Type = Term.Type;

+      return body;

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 70259973..983996d1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1920,6 +1920,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

 		Attributes attrs = null;

 		Triggers trigs = null;

+		Expression range = null;

 		Expression/*!*/ body;

 		

 		if (la.kind == 101 || la.kind == 102) {

@@ -1940,12 +1941,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		while (la.kind == 7) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

+		if (la.kind == 17) {

+			Get();

+			Expression(out range);

+		}

 		QSep();

 		Expression(out body);

 		if (univ) {

-		 q = new ForallExpr(x, bvars, body, trigs, attrs);

+		 q = new ForallExpr(x, bvars, range, body, trigs, attrs);

 		} else {

-		  q = new ExistsExpr(x, bvars, body, trigs, attrs);

+		  q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

 		}

 		parseVarScope.PopMarker();

 		

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 003a977c..6dcf0020 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -931,14 +931,19 @@ namespace Microsoft.Dafny {
         wr.Write(" ");

         PrintAttributes(e.Attributes);

         PrintTriggers(e.Trigs);

+        if (e.Range != null) {

+          wr.Write("| ");

+          PrintExpression(e.Range);

+          wr.Write(" ");

+        }

         wr.Write(":: ");

         if (0 <= indent) {

           int ind = indent + IndentAmount;

           wr.WriteLine();

           Indent(ind);

-          PrintExpression(e.Body, ind);

+          PrintExpression(e.Term, ind);

         } else {

-          PrintExpression(e.Body);

+          PrintExpression(e.Term);

         }

         if (parensNeeded) { wr.Write(")"); }

         

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c2f6c38..c7deb42f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2227,10 +2227,17 @@ namespace Microsoft.Dafny {
           }

           ResolveType(v.tok, v.Type);

         }

-        ResolveExpression(e.Body, twoState, specContext);

-        Contract.Assert(e.Body.Type != null);  // follows from postcondition of ResolveExpression

-        if (!UnifyTypes(e.Body.Type, Type.Bool)) {

-          Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type);

+        if (e.Range != null) {

+          ResolveExpression(e.Range, twoState, specContext);

+          Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

+          if (!UnifyTypes(e.Range.Type, Type.Bool)) {

+            Error(expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);

+          }

+        }

+        ResolveExpression(e.Term, twoState, specContext);

+        Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.Term.Type, Type.Bool)) {

+          Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);

         }

         // Since the body is more likely to infer the types of the bound variables, resolve it

         // first (above) and only then resolve the attributes and triggers (below).

@@ -2391,7 +2398,7 @@ namespace Microsoft.Dafny {
           // Go through the conjuncts of the range expression look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

-          foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {

+          foreach (var conjunct in NormalizedConjuncts(e.LogicalBody(), e is ExistsExpr)) {

             var c = conjunct as BinaryExpr;

             if (c == null) {

               goto CHECK_NEXT_CONJUNCT;

@@ -2715,7 +2722,7 @@ namespace Microsoft.Dafny {
 

       } else  if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

-        var s = FreeVariables(e.Body);

+        var s = FreeVariables(e.LogicalBody());

         foreach (var bv in e.BoundVars) {

           s.Remove(bv);

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 557fcaf0..253a1f9b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1511,7 +1511,7 @@ namespace Microsoft.Dafny {
         return z == null ? r : BplAnd(r, z);

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Bpl.Expr total = IsTotal(e.Body, etran);

+        Bpl.Expr total = IsTotal(e.LogicalBody(), etran);

         if (total != Bpl.Expr.True) {

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

@@ -1638,7 +1638,7 @@ namespace Microsoft.Dafny {
         return BplAnd(t0, t1);

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Bpl.Expr total = CanCallAssumption(e.Body, etran);

+        Bpl.Expr total = CanCallAssumption(e.LogicalBody(), etran);

         if (total != Bpl.Expr.True) {

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

@@ -1986,7 +1986,7 @@ namespace Microsoft.Dafny {
             builder.Add(new Bpl.AssumeCmd(bv.tok, wh));

           }

         }

-        Expression body = Substitute(e.Body, null, substMap);

+        Expression body = Substitute(e.LogicalBody(), null, substMap);

         CheckWellformed(body, options, locals, builder, etran);

 

       } else if (expr is ITEExpr) {

@@ -4415,13 +4415,17 @@ namespace Microsoft.Dafny {
             }

             tr = new Bpl.Trigger(expr.tok, true, tt, tr);

           }

-          Bpl.Expr body = TrExpr(e.Body);

+          var antecedent = typeAntecedent;

+          if (e.Range != null) {

+            antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));

+          }

+          Bpl.Expr body = TrExpr(e.Term);

           

           if (e is ForallExpr) {

-            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(typeAntecedent, body));

+            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));

           } else {

             Contract.Assert(e is ExistsExpr);

-            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(typeAntecedent, body));

+            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(antecedent, body));

           }

         

         } else if (expr is ITEExpr) {

@@ -5220,7 +5224,7 @@ namespace Microsoft.Dafny {
 

             substMap.Add(n, ieK);

           }

-          Expression bodyK = Substitute(e.Body, null, substMap);

+          Expression bodyK = Substitute(e.LogicalBody(), null, substMap);

 

           Bpl.Expr less = DecreasesCheck(toks, types, kk, nn, etran, null, null, false, true);

 

@@ -5252,7 +5256,7 @@ namespace Microsoft.Dafny {
           typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

           foreach (var kase in caseProduct) {

             var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);

-            var bdy = etran.LayerOffset(1).TrExpr(e.Body);

+            var bdy = etran.LayerOffset(1).TrExpr(e.LogicalBody());

             Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));

             splits.Add(new SplitExprInfo(false, q));

           }

@@ -5344,7 +5348,7 @@ namespace Microsoft.Dafny {
       // consider automatically applying induction

       var inductionVariables = new List<BoundVar>();

       foreach (var n in e.BoundVars) {

-        if (VarOccursInArgumentToRecursiveFunction(e.Body, n, null)) {

+        if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

           if (CommandLineOptions.Clo.Trace) {

             Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);

             new Printer(Console.Out).PrintExpression(e);

@@ -5447,7 +5451,7 @@ namespace Microsoft.Dafny {
           VarOccursInArgumentToRecursiveFunction(e.E1, n, p);

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Body, n, null);

+        return VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null);

       } else if (expr is ITEExpr) {

         var e = (ITEExpr)expr;

         return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) ||  // test is not "elevated"

@@ -5617,14 +5621,15 @@ namespace Microsoft.Dafny {
         

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

-        Expression newBody = Substitute(e.Body, receiverReplacement, substMap);

+        Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

+        Expression newTerm = Substitute(e.Term, receiverReplacement, substMap);

         Triggers newTrigs = SubstTriggers(e.Trigs, receiverReplacement, substMap);

         Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);

-        if (newBody != e.Body || newTrigs != e.Trigs || newAttrs != e.Attributes) {

+        if (newRange != e.Range || newTerm != e.Term || newTrigs != e.Trigs || newAttrs != e.Attributes) {

           if (expr is ForallExpr) {

-            newExpr = new ForallExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);

+            newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);

           } else {

-            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);

+            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);

           }

         }