From 4baa0fad00861977f7ab9b11161adb1cb0d691cf Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 18 May 2011 17:19:18 -0700
Subject: Dafny: added set comprehension expressions

---
 Binaries/DafnyRuntime.cs       |  34 ++++++++++----
 Source/Dafny/Compiler.cs       |  65 +++++++++++++++++++++++++-
 Source/Dafny/Dafny.atg         |  26 +++++++++++
 Source/Dafny/DafnyAst.cs       |  24 ++++++++--
 Source/Dafny/Parser.cs         |  90 ++++++++++++++++++++++++------------
 Source/Dafny/Printer.cs        |  23 +++++++++-
 Source/Dafny/Resolver.cs       |  60 +++++++++++++++++-------
 Source/Dafny/Scanner.cs        | 102 ++++++++++++++++++++---------------------
 Source/Dafny/Translator.cs     |  99 ++++++++++++++++++++++++++++++---------
 Test/dafny0/Answer             |  13 ++++++
 Test/dafny0/Comprehensions.dfy |  40 ++++++++++++++++
 Test/dafny0/runtest.bat        |   1 +
 12 files changed, 441 insertions(+), 136 deletions(-)
 create mode 100644 Test/dafny0/Comprehensions.dfy

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index b10aeac9..46a3f3df 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -18,9 +18,16 @@ namespace Dafny
     public static Set<T> FromElements(params T[] values) {
       Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
       foreach (T t in values)
-        d.Add(t, true);
+        d[t] = true;
       return new Set<T>(d);
     }
+    public static Set<T> FromCollection(ICollection<T> values) {
+      Dictionary<T, bool> d = new Dictionary<T, bool>();
+      foreach (T t in values)
+        d[t] = true;
+      return new Set<T>(d);
+    }
+    
     public IEnumerable<T> Elements {
       get {
         return dict.Keys;
@@ -98,7 +105,7 @@ namespace Dafny
       } else {
         a = other.dict; b = dict;
       }
-      Dictionary<T, bool> r = new Dictionary<T, bool>();
+      var r = new Dictionary<T, bool>();
       foreach (T t in a.Keys) {
         if (b.ContainsKey(t))
           r.Add(t, true);
@@ -110,7 +117,7 @@ namespace Dafny
         return this;
       else if (other.dict.Count == 0)
         return this;
-      Dictionary<T, bool> r = new Dictionary<T, bool>();
+      var r = new Dictionary<T, bool>();
       foreach (T t in dict.Keys) {
         if (!other.dict.ContainsKey(t))
           r.Add(t, true);
@@ -226,6 +233,7 @@ namespace Dafny
     }
   }
   public partial class Helpers {
+    // Computing forall/exists quantifiers
     public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
       if (frall) {
         return pred(false) && pred(true);
@@ -239,17 +247,25 @@ namespace Dafny
       }
       return frall;
     }
-    public static bool QuantSet<T>(Dafny.Set<T> set, bool frall, System.Predicate<T> pred) {
-      foreach (var t in set.Elements) {
-        if (pred(t) != frall) { return !frall; }
+    public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+      foreach (var u in set.Elements) {
+        if (pred(u) != frall) { return !frall; }
       }
       return frall;
     }
-    public static bool QuantSeq<T>(Dafny.Sequence<T> seq, bool frall, System.Predicate<T> pred) {
-      foreach (var t in seq.Elements) {
-        if (pred(t) != frall) { return !frall; }
+    public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+      foreach (var u in seq.Elements) {
+        if (pred(u) != frall) { return !frall; }
       }
       return frall;
     }
+    // Enumerating other collections
+    public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+    public static IEnumerable<bool> AllBooleans {
+      get {
+        yield return false;
+        yield return true;
+      }
+    }
   }
 }
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4d352f65..f1a649ee 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1306,7 +1306,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds
         var n = e.BoundVars.Count;
         Contract.Assert(e.Bounds.Count == n);
-        for (int i = n; 0 <= --i; ) {
+        for (int i = 0; i < n; i++) {
           var bound = e.Bounds[i];
           var bv = e.BoundVars[i];
           // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
@@ -1339,7 +1339,68 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < n; i++) {
           wr.Write(")");
         }
-      
+
+      } else if (expr is SetComprehension) {
+        var e = (SetComprehension)expr;
+        // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like:
+        // ((ComprehensionDelegate<G>)delegate() {
+        //   var _coll = new List<G>();
+        //   foreach (L l in sq.Elements) {
+        //     foreach (K k in st.Elements) {
+        //       for (BigInteger j = Lo; j < Hi; j++) {
+        //         for (bool i in Helper.AllBooleans) {
+        //           if (R(i,j,k,l)) {
+        //             _coll.Add(Term(i,j,k,l));
+        //           }
+        //         }
+        //       }
+        //     }
+        //   }
+        //   return Dafny.Set<G>.FromCollection(_coll);
+        // })()
+        Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds
+        var typeName = TypeName(((SetType)e.Type).Arg);
+        wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);
+        wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);
+        var n = e.BoundVars.Count;
+        Contract.Assert(e.Bounds.Count == n);
+        for (int i = 0; i < n; i++) {
+          var bound = e.Bounds[i];
+          var bv = e.BoundVars[i];
+          if (bound is QuantifierExpr.BoolBoundedPool) {
+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name);
+          } else if (bound is QuantifierExpr.IntBoundedPool) {
+            var b = (QuantifierExpr.IntBoundedPool)bound;
+            wr.Write("for (var @{0} = ", bv.Name);
+            TrExpr(b.LowerBound);
+            wr.Write("; @{0} < ", bv.Name);
+            TrExpr(b.UpperBound);
+            wr.Write("; @{0}++) {{ ", bv.Name);
+          } else if (bound is QuantifierExpr.SetBoundedPool) {
+            var b = (QuantifierExpr.SetBoundedPool)bound;
+            wr.Write("foreach (var @{0} in (", bv.Name);
+            TrExpr(b.Set);
+            wr.Write(").Elements) { ");
+          } else if (bound is QuantifierExpr.SeqBoundedPool) {
+            var b = (QuantifierExpr.SeqBoundedPool)bound;
+            wr.Write("foreach (var @{0} in (", bv.Name);
+            TrExpr(b.Seq);
+            wr.Write(").Elements) { ");
+          } else {
+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type
+          }
+        }
+        wr.Write("if (");
+        TrExpr(e.Range);
+        wr.Write(") { _coll.Add(");
+        TrExpr(e.Term);
+        wr.Write("); }");
+        for (int i = 0; i < n; i++) {
+          wr.Write("}");
+        }
+        wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);
+        wr.Write("})()");
+
       } else if (expr is ITEExpr) {
         ITEExpr e = (ITEExpr)expr;
         wr.Write("(");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 0ce1835f..f2a0a762 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1237,6 +1237,7 @@ ConstAtomExpression<out Expression/*!*/ e>
     "then" Expression<out e0>
     "else" Expression<out e1>                  (. e = new ITEExpr(x, e, e0, e1); .)
   | QuantifierGuts<out e>
+  | ComprehensionExpr<out e>
   )
   .
 
@@ -1391,6 +1392,31 @@ Forall = "forall" | '\u2200'.
 Exists = "exists" | '\u2203'.
 QSep = "::" | '\u2022'.
 
+ComprehensionExpr<out Expression/*!*/ q>
+= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
+     IToken/*!*/ x = Token.NoToken;
+     BoundVar/*!*/ bv;
+     List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+     Expression/*!*/ range;
+     Expression body = null;
+  .)
+  "set"                                        (. x = t; .)
+  (. parseVarScope.PushMarker(); .)
+  IdentTypeOptional<out bv>                    (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)
+  { ","
+    IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)
+  }
+  "|" Expression<out range>
+  [
+    QSep
+    Expression<out body>
+  ]
+  (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
+     q = new SetComprehension(x, bvars, range, body);
+     parseVarScope.PopMarker();
+  .)
+  .
+
 Expressions<.List<Expression/*!*/>/*!*/ args.>
 = (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
   Expression<out e>                            (. args.Add(e); .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ad7f5fb6..d83560e0 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2303,6 +2303,8 @@ namespace Microsoft.Dafny {
   /// <summary>
   /// A ComprehensionExpr has the form:
   ///   BINDER x Attributes | Range(x) :: Term(x)
+  /// When BINDER is "forall" or "exists", the range may be "null" (which stands for the logical value "true").
+  /// For other BINDERs (currently, "set"), the range is non-null.
   /// 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>
@@ -2346,7 +2348,7 @@ namespace Microsoft.Dafny {
     public List<BoundedPool> Bounds;  // initialized and filled in by resolver
     // invariant Bounds == null || Bounds.Count == BoundVars.Count;
 
-    public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, 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));
@@ -2369,7 +2371,7 @@ namespace Microsoft.Dafny {
   public abstract class QuantifierExpr : ComprehensionExpr {
     public readonly Triggers Trigs;
 
-    public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Triggers trigs, Attributes attrs)
+    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));
@@ -2431,7 +2433,23 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class WildcardExpr : Expression {  // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
+  public class SetComprehension : ComprehensionExpr
+  {
+    public readonly bool TermIsImplicit;
+
+    public SetComprehension(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression term)
+      : base(tok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), null) {
+      Contract.Requires(tok != null);
+      Contract.Requires(cce.NonNullElements(bvars));
+      Contract.Requires(1 <= bvars.Count);
+      Contract.Requires(range != null);
+
+      TermIsImplicit = term == null;
+    }
+  }
+
+  public class WildcardExpr : Expression
+  {  // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
     public WildcardExpr(IToken tok)
       : base(tok) {
       Contract.Requires(tok != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 983996d1..e707d859 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
 	const bool T = true;
 	const bool x = false;
 	const int minErrDist = 2;
-
+	
 	public Scanner/*!*/ scanner;
 	public Errors/*!*/  errors;
 
@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);
 		errDist = 0;
 	}
-
-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
-	  Contract.Requires(tok != null);
-	  Contract.Requires(msg != null);
+	
+    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+      Contract.Requires(tok != null);
+      Contract.Requires(msg != null);
 	  errors.SemErr(tok, msg);
 	}
 
@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;
 		}
 	}
-
+	
 	void Expect (int n) {
 		if (la.kind==n) Get(); else { SynErr(n); }
 	}
-
+	
 	bool StartOf (int s) {
 		return set[s, la.kind];
 	}
-
+	
 	void ExpectWeak (int n, int follow) {
 		if (la.kind == n) Get();
 		else {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}
 	}
 
-
+	
 	void Dafny() {
 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
@@ -1898,6 +1898,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 			QuantifierGuts(out e);
 			break;
 		}
+		case 37: {
+			ComprehensionExpr(out e);
+			break;
+		}
 		default: SynErr(140); break;
 		}
 	}
@@ -1956,6 +1960,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 		
 	}
 
+	void ComprehensionExpr(out Expression/*!*/ q) {
+		Contract.Ensures(Contract.ValueAtReturn(out q) != null);
+		IToken/*!*/ x = Token.NoToken;
+		BoundVar/*!*/ bv;
+		List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+		Expression/*!*/ range;
+		Expression body = null;
+		
+		Expect(37);
+		x = t; 
+		parseVarScope.PushMarker(); 
+		IdentTypeOptional(out bv);
+		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 
+		while (la.kind == 19) {
+			Get();
+			IdentTypeOptional(out bv);
+			bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 
+		}
+		Expect(17);
+		Expression(out range);
+		if (la.kind == 105 || la.kind == 106) {
+			QSep();
+			Expression(out body);
+		}
+		q = new SetComprehension(x, bvars, range, body);
+		parseVarScope.PopMarker();
+		
+	}
+
 	void IdentOrFuncExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id;  e = dummyExpr;  List<Expression/*!*/>/*!*/ args; 
 		Ident(out id);
@@ -2138,13 +2171,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	public void Parse() {
 		la = new Token();
-		la.val = "";
+		la.val = "";		
 		Get();
 		Dafny();
 
-		Expect(0);
+    Expect(0);
 	}
-
+	
 	static readonly bool[,]/*!*/ set = {
 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
@@ -2154,15 +2187,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
 		{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
 		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
 		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
-		{x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,T,T,T, T,x,x,x, x},
-		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x}
+		{x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,T,T,T, T,x,x,x, x},
+		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x}
 
 	};
 } // end Parser
@@ -2171,20 +2204,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {
 	public int count = 0;                                    // number of errors detected
 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream
-	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
-	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+  
 	public void SynErr(string filename, int line, int col, int n) {
-		SynErr(filename, line, col, GetSyntaxErrorString(n));
-	}
-
-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
-		Contract.Requires(msg != null);
+    SynErr(filename, line, col, GetSyntaxErrorString(n));
+  }
+	public virtual void SynErr(string filename, int line, int col, string msg) {
+	  Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
-	}
-
-	string GetSyntaxErrorString(int n) {
+  }
+  string GetSyntaxErrorString(int n) {
 		string s;
 		switch (n) {
 			case 0: s = "EOF expected"; break;
@@ -2340,7 +2371,7 @@ public class Errors {
 
 			default: s = "error " + n; break;
 		}
-		return s;
+    return s;
 	}
 
 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors
@@ -2348,9 +2379,8 @@ public class Errors {
 		Contract.Requires(msg != null);
 		SemErr(tok.filename, tok.line, tok.col, msg);
 	}
-
 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
-		Contract.Requires(msg != null);
+	  Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
 	}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6dcf0020..d3c7ecea 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -946,7 +946,28 @@ namespace Microsoft.Dafny {
           PrintExpression(e.Term);
         }
         if (parensNeeded) { wr.Write(")"); }
-        
+
+      } else if (expr is SetComprehension) {
+        var e = (SetComprehension)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("set ");
+        string sep = "";
+        foreach (BoundVar bv in e.BoundVars) {
+          wr.Write("{0}{1}", sep, bv.Name);
+          sep = ", ";
+          PrintType(": ", bv.Type);
+        }
+        wr.Write(" ");
+        PrintAttributes(e.Attributes);
+        wr.Write("| ");
+        PrintExpression(e.Range);
+        if (!e.TermIsImplicit) {
+          wr.Write(" :: ");
+          PrintExpression(e.Term);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
       } else if (expr is WildcardExpr) {
         wr.Write("*");
         
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c7deb42f..d8ca3448 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2247,9 +2247,35 @@ namespace Microsoft.Dafny {
         expr.Type = Type.Bool;
 
         if (prevErrorCount == ErrorCount) {
-          e.Bounds = DiscoverBounds(e, specContext);
+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, specContext ? null : "quantifiers in non-ghost contexts must be compilable");
         }
-        
+
+      } else if (expr is SetComprehension) {
+        var e = (SetComprehension)expr;
+        int prevErrorCount = ErrorCount;
+        scope.PushMarker();
+        foreach (BoundVar v in e.BoundVars) {
+          if (!scope.Push(v.Name, v)) {
+            Error(v, "Duplicate bound-variable name: {0}", v.Name);
+          }
+          ResolveType(v.tok, v.Type);
+        }
+        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 comprehension 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
+
+        ResolveAttributes(e.Attributes, twoState);
+        scope.PopMarker();
+        expr.Type = new SetType(e.Term.Type);
+
+        if (prevErrorCount == ErrorCount) {
+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, "a set comprehension must produce a finite set");
+        }
+
       } else if (expr is WildcardExpr) {
         expr.Type = new SetType(new ObjectType());
         
@@ -2378,34 +2404,36 @@ namespace Microsoft.Dafny {
     }
 
     /// <summary>
-    /// Tries to find a bounded pool for each of the bound variables of "e".  If this process fails, appropriate
-    /// error messages are reported and "null" is returned, unless "friendlyTry" is "true", in which case no
-    /// error messages are reported.
+    /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr".  If this process
+    /// fails, then "null" is returned and:
+    /// if "errorMessage" is non-null, then appropriate error messages are reported and "null" is returned;
+    /// if "errorMessage" is null, no error messages are reported.
     /// Requires "e" to be successfully resolved.
     /// </summary>
-    List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e, bool friendlyTry) {
-      Contract.Requires(e != null);
-      Contract.Requires(e.Type != null);  // a sanity check (but not a complete proof) that "e" has been resolved
-      Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == e.BoundVars.Count);
+    List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, string errorMessage) {
+      Contract.Requires(tok != null);
+      Contract.Requires(bvars != null);
+      Contract.Requires(expr.Type != null);  // a sanity check (but not a complete proof) that "e" has been resolved
+      Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count);
 
       var bounds = new List<QuantifierExpr.BoundedPool>();
-      for (int j = 0; j < e.BoundVars.Count; j++) {
-        var bv = e.BoundVars[j];
-        if (bv.Type == Type.Bool) {
+      for (int j = 0; j < bvars.Count; j++) {
+        var bv = bvars[j];
+        if (bv.Type is BoolType) {
           // easy
           bounds.Add(new QuantifierExpr.BoolBoundedPool());
         } else {
           // 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.LogicalBody(), e is ExistsExpr)) {
+          foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
             var c = conjunct as BinaryExpr;
             if (c == null) {
               goto CHECK_NEXT_CONJUNCT;
             }
             var e0 = c.E0;
             var e1 = c.E1;
-            int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, c.ResolvedOp, ref e0, ref e1);
+            int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);
             if (whereIsBv < 0) {
               goto CHECK_NEXT_CONJUNCT;
             }
@@ -2457,8 +2485,8 @@ namespace Microsoft.Dafny {
           CHECK_NEXT_CONJUNCT: ;
           }
           // we have checked every conjunct in the range expression and still have not discovered good bounds
-          if (!friendlyTry) {
-            Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+          if (errorMessage != null) {
+            Error(tok, "{0}, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", errorMessage, bv.Name);
           }
           return null;
         }
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 817df6cd..0af254f3 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer
 	//    b) part of stream in buffer
 	// 2) non seekable stream (network, console)
-
+  
 	public const int EOF = 65535 + 1; // char.MaxValue + 1;
 	const int MIN_BUFFER_LENGTH = 1024; // 1KB
 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,17 +31,15 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)
 	bool isUserStream;  // was the stream opened by the user?
 
-	[ContractInvariantMethod]
-	void ObjectInvariant(){
-		Contract.Invariant(buf != null);
-		Contract.Invariant(stream != null);
-	}
-
-//  [NotDelayed]
-	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
+[ContractInvariantMethod]
+void ObjectInvariant(){
+  Contract.Invariant(buf != null);
+  Contract.Invariant(stream != null);}
+    [NotDelayed]
+	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
 	  Contract.Requires(s != null);
 		stream = s; this.isUserStream = isUserStream;
-
+		
 		int fl, bl;
 		if (s.CanSeek) {
 			fl = (int) s.Length;
@@ -53,12 +51,12 @@ public class Buffer {
 
 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
 		fileLen = fl;  bufLen = bl;
-
+		
 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
 		if (bufLen == fileLen && s.CanSeek) Close();
 	}
-
+	
 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
 	  Contract.Requires(b != null);
 		buf = b.buf;
@@ -75,14 +73,14 @@ public class Buffer {
 	}
 
 	~Buffer() { Close(); }
-
+	
 	protected void Close() {
 		if (!isUserStream && stream != null) {
 			stream.Close();
 			//stream = null;
 		}
 	}
-
+	
 	public virtual int Read () {
 		if (bufPos < bufLen) {
 			return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;
 		return ch;
 	}
-
+	
 	public string/*!*/ GetString (int beg, int end) {
 	  Contract.Ensures(Contract.Result<string>() != null);
 		int len = 0;
@@ -141,7 +139,7 @@ public class Buffer {
 			}
 		}
 	}
-
+	
 	// Read the next chunk of bytes from the stream, increases the buffer
 	// if needed and updates the fields fileLen and bufLen.
 	// Returns the number of bytes read.
@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 107;
 
 
-	[ContractInvariantMethod]
-	void objectInvariant(){
-		Contract.Invariant(buffer!=null);
-		Contract.Invariant(t != null);
-		Contract.Invariant(start != null);
-		Contract.Invariant(tokens != null);
-		Contract.Invariant(pt != null);
-		Contract.Invariant(tval != null);
-		Contract.Invariant(Filename != null);
-		Contract.Invariant(errorHandler != null);
-	}
-
+[ContractInvariantMethod]
+void objectInvariant(){
+  Contract.Invariant(buffer!=null);
+  Contract.Invariant(t != null);
+  Contract.Invariant(start != null);
+  Contract.Invariant(tokens != null);
+  Contract.Invariant(pt != null);
+  Contract.Invariant(tval != null);
+  Contract.Invariant(Filename != null);
+  Contract.Invariant(errorHandler != null);
+}
 	public Buffer/*!*/ buffer; // scanner buffer
-
+	
 	Token/*!*/ t;          // current token
 	int ch;           // current input character
 	int pos;          // byte position of current character
@@ -239,13 +236,13 @@ public class Scanner {
 
 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)
 	Token/*!*/ pt;         // current peek token
-
+	
 	char[]/*!*/ tval = new char[128]; // text of current token
 	int tlen;         // length of current token
-
+	
 	private string/*!*/ Filename;
 	private Errors/*!*/ errorHandler;
-
+	
 	static Scanner() {
 		start = new Hashtable(128);
 		for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -294,9 +291,9 @@ public class Scanner {
 		start[Buffer.EOF] = -1;
 
 	}
-
-//	[NotDelayed]
-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+	
+	[NotDelayed]
+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
 	  Contract.Requires(fileName != null);
 	  Contract.Requires(errorHandler != null);
 		this.errorHandler = errorHandler;
@@ -306,14 +303,15 @@ public class Scanner {
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
 			buffer = new Buffer(stream, false);
 			Filename = fileName;
+			
 			Init();
 		} catch (IOException) {
 			throw new FatalError("Cannot open file " + fileName);
 		}
 	}
-
-//	[NotDelayed]
-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+	
+	[NotDelayed]
+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
 	  Contract.Requires(s != null);
 	  Contract.Requires(errorHandler != null);
 	  Contract.Requires(fileName != null);
@@ -322,9 +320,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);
 		this.errorHandler = errorHandler;
 		this.Filename = fileName;
+		
 		Init();
 	}
-
+	
 	void Init() {
 		pos = -1; line = 1; col = 0;
 		oldEols = 0;
@@ -345,11 +344,11 @@ public class Scanner {
 	Contract.Ensures(Contract.Result<string>() != null);
 	  int p = buffer.Pos;
 	  int ch = buffer.Read();
-	  // replace isolated '\r' by '\n' in order to make
+      // replace isolated '\r' by '\n' in order to make
 	  // eol handling uniform across Windows, Unix and Mac
 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 	  while (ch != EOL && ch != Buffer.EOF){
-		ch = buffer.Read();
+	    ch = buffer.Read();
 		// replace isolated '\r' by '\n' in order to make
 		// eol handling uniform across Windows, Unix and Mac
 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -360,7 +359,7 @@ public class Scanner {
 	}
 
 	void NextCh() {
-		if (oldEols > 0) { ch = EOL; oldEols--; }
+		if (oldEols > 0) { ch = EOL; oldEols--; } 
 		else {
 //			pos = buffer.Pos;
 //			ch = buffer.Read(); col++;
@@ -368,9 +367,9 @@ public class Scanner {
 //			// eol handling uniform across Windows, Unix and Mac
 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 //			if (ch == EOL) { line++; col = 0; }
-
+			
 			while (true) {
-				pos = buffer.Pos;
+			    pos = buffer.Pos;
 				ch = buffer.Read(); col++;
 				// replace isolated '\r' by '\n' in order to make
 				// eol handling uniform across Windows, Unix and Mac
@@ -420,7 +419,7 @@ public class Scanner {
 				return;
 			  }
 
-
+			
 		}
 
 	}
@@ -559,13 +558,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;
 		t.filename = this.Filename;
 		int state;
-		if (start.ContainsKey(ch)) {
-			Contract.Assert(start[ch] != null);
-			state = (int) start[ch];
-		}
+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
 		else { state = 0; }
 		tlen = 0; AddCh();
-
+		
 		switch (state) {
 			case -1: { t.kind = eofSym; break; } // NextCh already done
 			case 0: {
@@ -773,14 +769,14 @@ public class Scanner {
 		t.val = new String(tval, 0, tlen);
 		return t;
 	}
-
+	
 	private void SetScannerBehindT() {
 		buffer.Pos = t.pos;
 		NextCh();
 		line = t.line; col = t.col;
 		for (int i = 0; i < tlen; i++) NextCh();
 	}
-
+	
 	// get the next token (possibly a token already seen during peeking)
 	public Token/*!*/ Scan () {
 	 Contract.Ensures(Contract.Result<Token>() != null);
@@ -801,7 +797,7 @@ public class Scanner {
 			}
 			pt = pt.next;
 		} while (pt.kind > maxT); // skip pragmas
-
+	
 		return pt;
 	}
 
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 67559aee..bba7b734 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1509,9 +1509,12 @@ namespace Microsoft.Dafny {
         }
         Bpl.Expr r = BplAnd(t0, t1);
         return z == null ? r : BplAnd(r, z);
-      } else if (expr is QuantifierExpr) {
-        QuantifierExpr e = (QuantifierExpr)expr;
-        Bpl.Expr total = IsTotal(e.LogicalBody(), etran);
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        var total = IsTotal(e.Term, etran);
+        if (e.Range != null) {
+          total = BplAnd(IsTotal(e.Range, etran), BplImp(etran.TrExpr(e.Range), total));
+        }
         if (total != Bpl.Expr.True) {
           Bpl.VariableSeq bvars = new Bpl.VariableSeq();
           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1636,9 +1639,12 @@ namespace Microsoft.Dafny {
             break;
         }
         return BplAnd(t0, t1);
-      } else if (expr is QuantifierExpr) {
-        QuantifierExpr e = (QuantifierExpr)expr;
-        Bpl.Expr total = CanCallAssumption(e.LogicalBody(), etran);
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        var total = CanCallAssumption(e.Term, etran);
+        if (e.Range != null) {
+          total = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), total));
+        }
         if (total != Bpl.Expr.True) {
           Bpl.VariableSeq bvars = new Bpl.VariableSeq();
           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1684,6 +1690,18 @@ namespace Microsoft.Dafny {
       }
     }
     
+    Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+      if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
+        return b;
+      } else {
+        return Bpl.Expr.Imp(a, b);
+      }
+    }
+    
     void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {
       Contract.Requires(tok != null);
       Contract.Requires(e != null);
@@ -1970,8 +1988,8 @@ namespace Microsoft.Dafny {
             break;
         }
 
-      } else if (expr is QuantifierExpr) {
-        QuantifierExpr e = (QuantifierExpr)expr;
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
         Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
         foreach (BoundVar bv in e.BoundVars) {
           VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, bv.IsGhost, null);
@@ -1986,8 +2004,18 @@ namespace Microsoft.Dafny {
             builder.Add(new Bpl.AssumeCmd(bv.tok, wh));
           }
         }
-        Expression body = Substitute(e.LogicalBody(), null, substMap);
-        CheckWellformed(body, options, locals, builder, etran);
+
+        Expression body = Substitute(e.Term, null, substMap);
+        if (e.Range == null) {
+          CheckWellformed(body, options, locals, builder, etran);
+        } else {
+          Expression range = Substitute(e.Range, null, substMap);
+          CheckWellformed(range, options, locals, builder, etran);
+
+          Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
+          CheckWellformed(body, options, locals, b, etran);
+          builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(range), b.Collect(expr.tok), null, null));
+        }
 
       } else if (expr is ITEExpr) {
         ITEExpr e = (ITEExpr)expr;
@@ -4443,7 +4471,24 @@ namespace Microsoft.Dafny {
             Contract.Assert(e is ExistsExpr);
             return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(antecedent, body));
           }
-        
+
+        } else if (expr is SetComprehension) {
+          var e = (SetComprehension)expr;
+          // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".
+          Bpl.VariableSeq bvars = new Bpl.VariableSeq();
+          Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);
+          Bpl.QKeyValue kv = TrAttributes(e.Attributes);
+
+          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));
+          translator.otherTmpVarCount++;
+          Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);
+
+          var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));
+          var ebody = Bpl.Expr.And(translator.BplAnd(typeAntecedent, TrExpr(e.Range)), eq);
+          var exst = new Bpl.ExistsExpr(expr.tok, bvars, ebody);
+
+          return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);
+
         } else if (expr is ITEExpr) {
           ITEExpr e = (ITEExpr)expr;
           Bpl.Expr g = TrExpr(e.Test);
@@ -5470,9 +5515,10 @@ namespace Microsoft.Dafny {
         }
         return VarOccursInArgumentToRecursiveFunction(e.E0, n, p) ||
           VarOccursInArgumentToRecursiveFunction(e.E1, n, p);
-      } else if (expr is QuantifierExpr) {
-        var e = (QuantifierExpr)expr;
-        return VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null);
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, null)) ||
+          VarOccursInArgumentToRecursiveFunction(e.Term, n, null);
       } else if (expr is ITEExpr) {
         var e = (ITEExpr)expr;
         return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) ||  // test is not "elevated"
@@ -5640,18 +5686,27 @@ namespace Microsoft.Dafny {
           newExpr = newBin;
         }
         
-      } else if (expr is QuantifierExpr) {
-        QuantifierExpr e = (QuantifierExpr)expr;
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
         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 (newRange != e.Range || newTerm != e.Term || newTrigs != e.Trigs || newAttrs != e.Attributes) {
-          if (expr is ForallExpr) {
-            newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
-          } else {
-            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+        if (e is SetComprehension) {
+          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
+            newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
           }
+        } else if (e is QuantifierExpr) {
+          var q = (QuantifierExpr)e;
+          Triggers newTrigs = SubstTriggers(q.Trigs, receiverReplacement, substMap);
+          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes || newTrigs != q.Trigs) {
+            if (expr is ForallExpr) {
+              newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+            } else {
+              newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+            }
+          }
+        } else {
+          Contract.Assume(false);  // unexpected ComprehensionExpr
         }
         
       } else if (expr is ITEExpr) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2463b0e5..34aea30b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -527,6 +527,19 @@ Execution trace:
 
 Dafny program verifier finished with 2 verified, 1 error
 
+-------------------- Comprehensions.dfy --------------------
+Comprehensions.dfy(9,14): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon9_Then
+    (0,0): anon10_Then
+    (0,0): anon4
+    (0,0): anon11_Then
+    (0,0): anon12_Then
+    (0,0): anon8
+
+Dafny program verifier finished with 6 verified, 1 error
+
 -------------------- Termination.dfy --------------------
 Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
 Execution trace:
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
new file mode 100644
index 00000000..8629a418
--- /dev/null
+++ b/Test/dafny0/Comprehensions.dfy
@@ -0,0 +1,40 @@
+method M()
+{
+  var numbers := set i | 0 <= i && i < 100;
+  var squares := set i | 0 <= i && i < 100 :: Id(i)*i;  // verifying properties about set comprehensions with a term expression is hard
+
+  assert 12 in numbers;
+  assert Id(5) == 5;
+  assert 25 in squares;
+  assert 200 in numbers;  // error
+}
+
+function method Id(x: int): int { x }  // for triggering
+
+// The following mainly test that set comprehensions can be compiled, but one would
+// have to run the resulting program to check that the compiler is doing the right thing.
+method Main()
+{
+  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+  call PrintSet(q);
+  q := set b: bool | true :: if b then 3 else 7;
+  call PrintSet(q);
+  var m := set k | k in q :: 2*k;
+  call PrintSet(m);
+  call PrintSet(set k | k in q && k % 2 == 0);
+  var sq := [30, 40, 20];
+  call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+}
+
+method PrintSet<T>(s: set<T>) {
+  var q := s;
+  while (q != {})
+    decreases q;
+  {
+    var x := choose q;
+    print x, " ";
+    q := q - {x};
+  }
+  print "\n";
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 12d9bcf4..f67429d2 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -15,6 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             FunctionSpecifications.dfy ResolutionErrors.dfy
             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
             Modules0.dfy Modules1.dfy BadFunction.dfy
+            Comprehensions.dfy
             Termination.dfy Use.dfy DTypes.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
             Refinement.dfy RefinementErrors.dfy) do (
-- 
cgit v1.2.3