From 904fcded9ae0a3219ccccf7c62f116b332deb9ac Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 15 May 2011 22:02:08 -0700
Subject: Dafny: added optional range expressions to logical quantifiers,
 preparing for addition other other comprehensions (like set comprehension)

---
 Source/Dafny/Dafny.atg | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'Source/Dafny/Dafny.atg')

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();
   .)
-- 
cgit v1.2.3