Dafny: Added map comprehensions and updated display syntax

8 files changed, 262 insertions, 37 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 232224b0..fad4e7fa 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1990,6 +1990,11 @@ namespace Microsoft.Dafny {
             wr.Write("Dafny.Helpers.QuantSet(");

             TrExpr(b.Set);

             wr.Write(", ");

+          } else if (bound is QuantifierExpr.MapBoundedPool) {

+            var b = (QuantifierExpr.MapBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantMap(");

+            TrExpr(b.Map);

+            wr.Write(", ");

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSeq(");

@@ -2047,6 +2052,11 @@ namespace Microsoft.Dafny {
             wr.Write("foreach (var @{0} in (", bv.Name);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

+          } else if (bound is QuantifierExpr.MapBoundedPool) {

+            var b = (QuantifierExpr.MapBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Map);

+            wr.Write(").Domain) { ");

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.Name);

@@ -2067,6 +2077,70 @@ namespace Microsoft.Dafny {
         wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);

         wr.Write("})()");

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        // For "map i | R(i) :: Term(i)" where the term has type "V" and i has type "U", emit something like:

+        // ((MapComprehensionDelegate<U, V>)delegate() {

+        //   var _coll = new List<Pair<U,V>>();

+        //   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(new Pair(i, Term(i));

+        //           }

+        //         }

+        //       }

+        //     }

+        //   }

+        //   return Dafny.Map<U, V>.FromElements(_coll);

+        // })()

+        Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

+        var domtypeName = TypeName(((MapType)e.Type).Domain);

+        var rantypeName = TypeName(((MapType)e.Type).Range);

+        wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);

+        wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);

+        var n = e.BoundVars.Count;

+        Contract.Assert(e.Bounds.Count == n && n == 1);

+        var bound = e.Bounds[0];

+        var bv = e.BoundVars[0];

+        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.MapBoundedPool) {

+          var b = (QuantifierExpr.MapBoundedPool)bound;

+          wr.Write("foreach (var @{0} in (", bv.Name);

+          TrExpr(b.Map);

+          wr.Write(").Domain) { ");

+        } 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(") { ");

+        wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.Name);

+        TrExpr(e.Term);

+        wr.Write(")); }");

+        wr.Write("}");

+        wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName);

+        wr.Write("})()");

+

       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         TrExpr(e.Body);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 103cb5c7..97da97e3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1342,14 +1342,28 @@ MultiSetExpr<out Expression e>
   .

 MapExpr<out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-     IToken/*!*/ x = null;  List<ExpressionPair/*!*/>/*!*/ elements;

+     IToken/*!*/ x = Token.NoToken;

+     List<ExpressionPair/*!*/>/*!*/ elements;

      e = dummyExpr;

   .)

   "map"                                        (. x = t; .)

-  ( "{"                                        (. elements = new List<ExpressionPair/*!*/>(); .)

+  ( "["                                        (. elements = new List<ExpressionPair/*!*/>(); .)

       [ MapLiteralExpressions<out elements> ]  (. e = new MapDisplayExpr(x, elements);.)

-    "}"

-  | (. SemErr("map must be followed by braces."); .)

+    "]"

+  | (

+     (. 

+     BoundVar/*!*/ bv;

+     List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+     Expression/*!*/ range;

+     Expression body = null;

+    .)

+      IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

+      "|" Expression<out range>

+      QSep

+      Expression<out body>

+      (. e = new MapComprehension(x, bvars, range, body); .) 

+    )

+  | (. SemErr("map must be followed by literal in brackets or comprehension."); .)

   )

   .

 MapLiteralExpressions<.out List<ExpressionPair> elements.>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b42fcb5a..5fd34e65 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -577,7 +577,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for:

-  ///     set(Arg) or seq(Arg)

+  ///     set(Arg) or seq(Arg) or map(Arg, Range)

   /// </summary>

   public class CollectionTypeProxy : RestrictedTypeProxy {

     public readonly Type Arg;

@@ -3068,6 +3068,11 @@ namespace Microsoft.Dafny {
       public readonly Expression Set;

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

     }

+    public class MapBoundedPool : BoundedPool

+    {

+      public readonly Expression Map;

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

+    }

     public class SeqBoundedPool : BoundedPool

     {

       public readonly Expression Seq;

@@ -3162,6 +3167,17 @@ namespace Microsoft.Dafny {
       TermIsImplicit = term == null;

     }

   }

+  public class MapComprehension : ComprehensionExpr

+  {

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

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

+      Contract.Requires(tok != null);

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

+      Contract.Requires(1 <= bvars.Count);

+      Contract.Requires(range != null);

+      Contract.Requires(term != null);

+    }

+  }

 

   public class WildcardExpr : Expression

   {  // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 817df12b..fe4d58a9 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2303,21 +2303,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void MapExpr(out Expression e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-		IToken/*!*/ x = null;  List<ExpressionPair/*!*/>/*!*/ elements;

+		IToken/*!*/ x = Token.NoToken;

+		List<ExpressionPair/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

 		Expect(42);

 		x = t; 

-		if (la.kind == 6) {

+		if (la.kind == 55) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(9)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(7);

+			Expect(56);

+		} else if (la.kind == 1) {

+			BoundVar/*!*/ bv;

+			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+			Expression/*!*/ range;

+			Expression body = null;

+			

+			IdentTypeOptional(out bv);

+			bvars.Add(bv); 

+			Expect(18);

+			Expression(out range);

+			QSep();

+			Expression(out body);

+			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

-			SemErr("map must be followed by braces."); 

+			SemErr("map must be followed by literal in brackets or comprehension."); 

 		} else SynErr(177);

 	}

 

@@ -2426,6 +2440,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

+	void QSep() {

+		if (la.kind == 106) {

+			Get();

+		} else if (la.kind == 107) {

+			Get();

+		} else SynErr(179);

+	}

+

 	void MatchExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

@@ -2454,7 +2476,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 104 || la.kind == 105) {

 			Exists();

 			x = t; 

-		} else SynErr(179);

+		} else SynErr(180);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2524,7 +2546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 103) {

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void Exists() {

@@ -2532,14 +2554,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 105) {

 			Get();

-		} else SynErr(181);

-	}

-

-	void QSep() {

-		if (la.kind == 106) {

-			Get();

-		} else if (la.kind == 107) {

-			Get();

 		} else SynErr(182);

 	}

 

@@ -2800,10 +2814,10 @@ public class Errors {
 			case 176: s = "invalid MultiSetExpr"; break;

 			case 177: s = "invalid MapExpr"; break;

 			case 178: s = "invalid ConstAtomExpression"; break;

-			case 179: s = "invalid QuantifierGuts"; break;

-			case 180: s = "invalid Forall"; break;

-			case 181: s = "invalid Exists"; break;

-			case 182: s = "invalid QSep"; break;

+			case 179: s = "invalid QSep"; break;

+			case 180: s = "invalid QuantifierGuts"; break;

+			case 181: s = "invalid Forall"; break;

+			case 182: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 38ec17fc..6cf71fa1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1190,6 +1190,24 @@ namespace Microsoft.Dafny {
         }

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

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        bool parensNeeded = !isRightmost;

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

+        wr.Write("map ");

+        string sep = "";

+        foreach (BoundVar bv in e.BoundVars) {

+          wr.Write("{0}{1}", sep, bv.Name);

+          sep = ", ";

+          PrintType(": ", bv.Type);

+        }

+        PrintAttributes(e.Attributes);

+        wr.Write(" | ");

+        PrintExpression(e.Range);

+        wr.Write(" :: ");

+        PrintExpression(e.Term);

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

+

       } else if (expr is WildcardExpr) {

         wr.Write("*");

 

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 29a4943a..d966a76f 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -353,6 +353,8 @@ namespace Microsoft.Dafny {
           return new ForallExpr(tk, bvs, range, term, null);

         } else if (e is ExistsExpr) {

           return new ExistsExpr(tk, bvs, range, term, null);

+        } else if (e is MapComprehension) {

+          return new MapComprehension(tk, bvs, range, term);

         } else {

           Contract.Assert(e is SetComprehension);

           return new SetComprehension(tk, bvs, range, term);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 4402e5b1..7be3fca2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3067,6 +3067,42 @@ namespace Microsoft.Dafny {
           }

         }

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        int prevErrorCount = ErrorCount;

+        scope.PushMarker();

+        if (e.BoundVars.Count != 1) {

+          Error(e.tok, "a map comprehension must have exactly one bound variable.");

+        }

+        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, null, true);

+        }

+        ResolveExpression(e.Range, twoState);

+        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);

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

+

+        ResolveAttributes(e.Attributes, twoState);

+        scope.PopMarker();

+        expr.Type = new MapType(e.BoundVars[0].Type,e.Term.Type);

+

+        if (prevErrorCount == ErrorCount) {

+          var missingBounds = new List<BoundVar>();

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          if (missingBounds.Count != 0) {

+            e.MissingBounds = missingBounds;

+            foreach (var bv in e.MissingBounds) {

+              Error(expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+            }

+          }

+        }

+

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

 

@@ -4251,6 +4287,9 @@ namespace Microsoft.Dafny {
       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));

       } else if (expr is WildcardExpr) {

         return false;

       } else if (expr is PredicateExpr) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3f3d89f1..0189c11b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1730,19 +1730,29 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         bool isSequence = e.Seq.Type is SeqType;

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

-        Bpl.Expr seq = etran.TrExpr(e.Seq);

-        Bpl.Expr e0 = null;

-        if (e.E0 != null) {

-          e0 = etran.TrExpr(e.E0);

-          total = BplAnd(total, IsTotal(e.E0, etran));

-          total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));

-        }

-        if (e.E1 != null) {

-          total = BplAnd(total, IsTotal(e.E1, etran));

-          total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));

+        if (e.Seq.Type is MapType) {

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

+          Bpl.Expr map = etran.TrExpr(e.Seq);

+          var e0 = etran.TrExpr(e.E0);

+          Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), map);

+          inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type));

+          total = BplAnd(total, inDomain);

+          return total;

+        } else {

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

+          Bpl.Expr seq = etran.TrExpr(e.Seq);

+          Bpl.Expr e0 = null;

+          if (e.E0 != null) {

+            e0 = etran.TrExpr(e.E0);

+            total = BplAnd(total, IsTotal(e.E0, etran));

+            total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));

+          }

+          if (e.E1 != null) {

+            total = BplAnd(total, IsTotal(e.E1, etran));

+            total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));

+          }

+          return total;

         }

-        return total;

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

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

@@ -5475,7 +5485,7 @@ namespace Microsoft.Dafny {
               x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);

             } else if (e.Seq.Type is MapType) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);

-              x = Bpl.Expr.Select(x, translator.FunctionCall(e.tok, BuiltinFunction.Box, null, e0));

+              x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));

             } else { Contract.Assert(false); x = null; }

             if (!ModeledAsBoxType(elmtType)) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);

@@ -5839,6 +5849,36 @@ namespace Microsoft.Dafny {
 

           return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);

 

+        } else if (expr is MapComprehension) {

+          var e = (MapComprehension)expr;

+          // Translate "map x | R :: T" into

+          // Map#Glue(lambda y: BoxType :: [unbox(y)/x]R,

+          //          lambda y: BoxType :: [unbox(y)/x]T)".

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

+          var bv = e.BoundVars[0];

+          TrBoundVariables(e.BoundVars, bvars);

+          

+          Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

+

+          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));

+          translator.otherTmpVarCount++;

+

+          Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, this);

+          Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar))

+            : (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar));

+

+

+          Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();

+          subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));

+

+          var ebody = translator.BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(Substitute(e.Range, null, subst)));

+          Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, ebody);

+          ebody = TrExpr(Substitute(e.Term, null, subst));

+          Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type));

+

+          

+          return translator.FunctionCall(e.tok, BuiltinFunction.MapGlue, null, l1, l2);

+

         } else if (expr is PredicateExpr) {

           var e = (PredicateExpr)expr;

           return TrExpr(e.Body);

@@ -6301,6 +6341,7 @@ namespace Microsoft.Dafny {
       MapBuild,

       MapDisjoint,

       MapUnion,

+      MapGlue,

 

       IndexField,

       MultiIndexField,

@@ -6485,6 +6526,9 @@ namespace Microsoft.Dafny {
         case BuiltinFunction.MapElements:

           Contract.Assert(args.Length == 1);

           return FunctionCall(tok, "Map#Elements", typeInstantiation, args);

+        case BuiltinFunction.MapGlue:

+          Contract.Assert(args.Length == 2);

+          return FunctionCall(tok, "Map#Glue", predef.MapType(tok, predef.BoxType, predef.BoxType), args);

         case BuiltinFunction.MapEqual:

           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation == null);

@@ -7427,6 +7471,10 @@ namespace Microsoft.Dafny {
           if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

             newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

           }

+        } else if (e is MapComprehension) {

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

+            newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+          }

         } else if (e is QuantifierExpr) {

           var q = (QuantifierExpr)e;

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

@@ -7437,7 +7485,7 @@ namespace Microsoft.Dafny {
             }

           }

         } else {

-          Contract.Assume(false);  // unexpected ComprehensionExpr

+          Contract.Assert(false);  // unexpected ComprehensionExpr

         }

 

       } else if (expr is PredicateExpr) {