Dafny: added named expressions and replacement

8 files changed, 826 insertions, 447 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 8f9a7717..958726fd 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -730,10 +730,23 @@ OneStmt<out Statement/*!*/ s>
     SYNC

     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | ReturnStmt<out s>

-  | "..."                              (. s = new SkeletonStatement(t); .)

+  | SkeletonStmt<out s> 

     ";"

   )

   .

+

+SkeletonStmt<out Statement s>

+= (. List<IToken> names = null;

+     List<Expression> exprs = null;

+     IToken tok, dotdotdot;

+     Expression e; .)

+  "..."                                (. dotdotdot = t; .)

+  ["where"                             (. names = new List<IToken>(); exprs = new List<Expression>(); .)

+     Ident<out tok> "=" Expression<out e>        (. names.Add(tok); exprs.Add(e); .)

+     {"," Ident<out tok> "=" Expression<out e> } (. names.Add(tok); exprs.Add(e); .)

+  ]

+                                       (. s = new SkeletonStatement(dotdotdot, names, exprs); .)

+  .

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -1443,8 +1456,6 @@ EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;

      Expression e0, e1;

      e = dummyExpr;

-     BoundVar d;

-     List<BoundVar> letVars;  List<Expression> letRHSs;

   .)

   ( "if"                            (. x = t; .)

     Expression<out e>

@@ -1459,7 +1470,18 @@ EndlessExpression<out Expression e>
   | "assume"                        (. x = t; .)

     Expression<out e0> ";"

     Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

-  | "var"                           (. x = t;

+  | LetExpr<out e>

+  | NamedExpr<out e>

+  )

+  .

+

+LetExpr<out Expression e>

+= (. IToken/*!*/ x;

+     e = dummyExpr;

+     BoundVar d;

+     List<BoundVar> letVars;  List<Expression> letRHSs;

+  .)

+    "var"                           (. x = t;

                                        letVars = new List<BoundVar>();

                                        letRHSs = new List<Expression>(); .)

     IdentTypeOptional<out d>        (. letVars.Add(d); .)

@@ -1471,8 +1493,20 @@ EndlessExpression<out Expression e>
     }

     ";"

     Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)

-  )

   .

+

+NamedExpr<out Expression e>

+= (. IToken/*!*/ x, d;

+     e = dummyExpr;

+     Expression expr;

+  .)

+    "expr"                          (. x = t; .)

+    NoUSIdent<out d>

+    ":"

+    Expression<out e>               (. expr = e;

+                                       e = new NamedExpr(x, d, expr); .)

+  .

+

 MatchExpression<out Expression/*!*/ e>

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

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

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9d426421..c2a4ace3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2495,10 +2495,13 @@ namespace Microsoft.Dafny {
     public readonly Statement S;

     public readonly bool ConditionOmitted;

     public readonly bool BodyOmitted;

+    public readonly List<IToken> NameReplacements;

+    public readonly List<Expression> ExprReplacements;

     public SkeletonStatement(IToken tok)

       : base(tok)

     {

       Contract.Requires(tok != null);

+      S = null;

     }

     public SkeletonStatement(Statement s, bool conditionOmitted, bool bodyOmitted)

       : base(s.Tok)

@@ -2508,6 +2511,13 @@ namespace Microsoft.Dafny {
       ConditionOmitted = conditionOmitted;

       BodyOmitted = bodyOmitted;

     }

+    public SkeletonStatement(IToken tok, List<IToken> nameReplacements, List<Expression> exprReplacements)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      NameReplacements = nameReplacements;

+      ExprReplacements = exprReplacements;

+      

+    }

     public override IEnumerable<Statement> SubStatements {

       get {

         // The SkeletonStatement is really a modification of its inner statement S.  Therefore,

@@ -3373,6 +3383,28 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class NamedExpr : Expression

+  {

+    public readonly string Name;

+    public readonly Expression Body;

+    public NamedExpr(IToken tok, IToken name, Expression body)

+      : base(tok) {

+      Name = name.val;

+      Body = body;

+    }

+

+    public NamedExpr(IToken tok, string p, Expression body)

+      : base(tok) {

+      Name = p;

+      Body = body;

+    }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Body;

+      }

+    }

+  }

+

   /// <summary>

   /// A ComprehensionExpr has the form:

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

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 15ea873c..6adc4df0 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 107;

+	public const int maxT = 109;

 

 	const bool T = true;

 	const bool x = false;

@@ -212,7 +212,7 @@ bool IsAttribute() {
 				defaultModule.TopLevelDecls.Add(at); 

 			} else if (StartOf(2)) {

 				ClassMemberDecl(membersDefaultClass, isGhost, false);

-			} else SynErr(108);

+			} else SynErr(110);

 		}

 		DefaultClassDecl defaultClass = null;

 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

@@ -275,7 +275,7 @@ bool IsAttribute() {
 					module.TopLevelDecls.Add(at); 

 				} else if (StartOf(2)) {

 					ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);

-				} else SynErr(109);

+				} else SynErr(111);

 			}

 			Expect(7);

 			module.BodyEndTok = t;

@@ -291,7 +291,7 @@ bool IsAttribute() {
 			QualifiedName(out idPath);

 			Expect(12);

 			submodule = new AbstractModuleDecl(idPath, id, parent); 

-		} else SynErr(110);

+		} else SynErr(112);

 	}

 

 	void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {

@@ -303,7 +303,7 @@ bool IsAttribute() {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

-		while (!(la.kind == 0 || la.kind == 15)) {SynErr(111); Get();}

+		while (!(la.kind == 0 || la.kind == 15)) {SynErr(113); Get();}

 		Expect(15);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

@@ -334,13 +334,13 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

-		while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(112); Get();}

+		while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(114); Get();}

 		if (la.kind == 17) {

 			Get();

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

 			Get();

 			co = true; 

-		} else SynErr(113);

+		} else SynErr(115);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -355,7 +355,7 @@ bool IsAttribute() {
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

-		while (!(la.kind == 0 || la.kind == 12)) {SynErr(114); Get();}

+		while (!(la.kind == 0 || la.kind == 12)) {SynErr(116); Get();}

 		Expect(12);

 		if (co) {

 		 dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

@@ -384,7 +384,7 @@ bool IsAttribute() {
 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

 		}

 		at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); 

-		while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}

+		while (!(la.kind == 0 || la.kind == 12)) {SynErr(117); Get();}

 		Expect(12);

 	}

 

@@ -412,7 +412,7 @@ bool IsAttribute() {
 		} else if (la.kind == 28 || la.kind == 29) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(116);

+		} else SynErr(118);

 	}

 

 	void Attribute(ref Attributes attrs) {

@@ -483,7 +483,7 @@ bool IsAttribute() {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

-		while (!(la.kind == 0 || la.kind == 20)) {SynErr(117); Get();}

+		while (!(la.kind == 0 || la.kind == 20)) {SynErr(119); Get();}

 		Expect(20);

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

@@ -497,7 +497,7 @@ bool IsAttribute() {
 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

-		while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); Get();}

+		while (!(la.kind == 0 || la.kind == 12)) {SynErr(120); Get();}

 		Expect(12);

 	}

 

@@ -543,7 +543,7 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(119);

+			} else SynErr(121);

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

 			Get();

 			isPredicate = true; 

@@ -572,8 +572,8 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(120);

-		} else SynErr(121);

+			} else SynErr(122);

+		} else SynErr(123);

 		while (StartOf(4)) {

 			FunctionSpec(reqs, reads, ens, decreases);

 		}

@@ -612,7 +612,7 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(122); Get();}

+		while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(124); Get();}

 		if (la.kind == 28) {

 			Get();

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

@@ -623,7 +623,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

-		} else SynErr(123);

+		} else SynErr(125);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

 		   SemErr(t, "constructors cannot be declared 'ghost'");

@@ -650,7 +650,7 @@ bool IsAttribute() {
 		} else if (la.kind == 31) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(124);

+		} else SynErr(126);

 		while (StartOf(5)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

@@ -844,7 +844,7 @@ bool IsAttribute() {
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(125); break;

+		default: SynErr(127); break;

 		}

 	}

 

@@ -869,7 +869,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(7))) {SynErr(126); Get();}

+		while (!(StartOf(7))) {SynErr(128); Get();}

 		if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

@@ -884,7 +884,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					mod.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(127); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}

 			Expect(12);

 		} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {

 			if (la.kind == 33) {

@@ -894,7 +894,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 34) {

 				Get();

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(128); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(130); Get();}

 				Expect(12);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

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

@@ -903,19 +903,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}

 				Expect(12);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

-			} else SynErr(130);

+			} else SynErr(132);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();}

 			Expect(12);

-		} else SynErr(132);

+		} else SynErr(134);

 	}

 

 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

@@ -1016,17 +1016,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt, path); 

-		} else SynErr(133);

+		} else SynErr(135);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

 		Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

 		if (la.kind == 34) {

-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(134); Get();}

+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(136); Get();}

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}

 			Expect(12);

 			reqs.Add(e); 

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

@@ -1040,20 +1040,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					reads.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(136); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}

 			Expect(12);

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

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();}

 			Expect(12);

 			ens.Add(e); 

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

 			Get();

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}

 			Expect(12);

-		} else SynErr(139);

+		} else SynErr(141);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -1072,7 +1072,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(140);

+		} else SynErr(142);

 	}

 

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

@@ -1083,7 +1083,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new WildcardExpr(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(141);

+		} else SynErr(143);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1100,26 +1100,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(11))) {SynErr(142); Get();}

+		while (!(StartOf(11))) {SynErr(144); Get();}

 		switch (la.kind) {

 		case 6: {

 			BlockStmt(out bs, out bodyStart, out bodyEnd);

 			s = bs; 

 			break;

 		}

-		case 67: {

+		case 68: {

 			AssertStmt(out s);

 			break;

 		}

-		case 55: {

+		case 56: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 68: {

+		case 69: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 1: case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1127,19 +1127,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 60: {

+		case 61: {

 			IfStmt(out s);

 			break;

 		}

-		case 64: {

+		case 65: {

 			WhileStmt(out s);

 			break;

 		}

-		case 66: {

+		case 67: {

 			MatchStmt(out s);

 			break;

 		}

-		case 69: {

+		case 70: {

 			ParallelStmt(out s);

 			break;

 		}

@@ -1163,23 +1163,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					breakCount++; 

 				}

-			} else SynErr(143);

-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(144); Get();}

+			} else SynErr(145);

+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(146); Get();}

 			Expect(12);

 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

-		case 52: {

+		case 53: {

 			ReturnStmt(out s);

 			break;

 		}

 		case 31: {

-			Get();

-			s = new SkeletonStatement(t); 

+			SkeletonStmt(out s);

 			Expect(12);

 			break;

 		}

-		default: SynErr(145); break;

+		default: SynErr(147); break;

 		}

 	}

 

@@ -1187,7 +1186,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(67);

+		Expect(68);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

@@ -1196,7 +1195,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

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

 			Get();

-		} else SynErr(146);

+		} else SynErr(148);

 		Expect(12);

 		if (e == null) {

 		 s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);

@@ -1210,7 +1209,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(55);

+		Expect(56);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

@@ -1219,7 +1218,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

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

 			Get();

-		} else SynErr(147);

+		} else SynErr(149);

 		if (e == null) {

 		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

 		} else {

@@ -1233,7 +1232,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

 		

-		Expect(68);

+		Expect(69);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1264,14 +1263,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(12);

 			rhss.Add(new ExprRhs(e, attrs)); 

-		} else if (la.kind == 21 || la.kind == 53 || la.kind == 54) {

+		} else if (la.kind == 21 || la.kind == 54 || la.kind == 55) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 21) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 53) {

+			if (la.kind == 54) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

@@ -1281,20 +1280,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Rhs(out r, lhs0);

 					rhss.Add(r); 

 				}

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

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

 				Get();

 				x = t; 

-				if (la.kind == 55) {

+				if (la.kind == 56) {

 					Get();

 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(148);

+			} else SynErr(150);

 			Expect(12);

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

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(149);

+		} else SynErr(151);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

@@ -1329,8 +1328,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 53 || la.kind == 54) {

-			if (la.kind == 53) {

+		if (la.kind == 54 || la.kind == 55) {

+			if (la.kind == 54) {

 				Get();

 				assignTok = t;

 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

@@ -1346,7 +1345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				Get();

 				assignTok = t; 

-				if (la.kind == 55) {

+				if (la.kind == 56) {

 					Get();

 					suchThatAssume = t; 

 				}

@@ -1385,7 +1384,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(60);

+		Expect(61);

 		x = t; 

 		if (la.kind == 23 || la.kind == 31) {

 			if (la.kind == 23) {

@@ -1395,15 +1394,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardOmitted = true; 

 			}

 			BlockStmt(out thn, out bodyStart, out bodyEnd);

-			if (la.kind == 61) {

+			if (la.kind == 62) {

 				Get();

-				if (la.kind == 60) {

+				if (la.kind == 61) {

 					IfStmt(out s);

 					els = s; 

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

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(150);

+				} else SynErr(152);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1414,7 +1413,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(151);

+		} else SynErr(153);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1430,7 +1429,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(64);

+		Expect(65);

 		x = t; 

 		if (la.kind == 23 || la.kind == 31) {

 			if (la.kind == 23) {

@@ -1446,7 +1445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else if (la.kind == 31) {

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(152);

+			} else SynErr(154);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

@@ -1464,18 +1463,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(153);

+		} else SynErr(155);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

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

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

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

-		Expect(66);

+		Expect(67);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 62) {

+		while (la.kind == 63) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1495,7 +1494,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(69);

+		Expect(70);

 		x = t; 

 		Expect(23);

 		if (la.kind == 1) {

@@ -1528,7 +1527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

 		

-		Expect(52);

+		Expect(53);

 		returnTok = t; 

 		if (StartOf(13)) {

 			Rhs(out r, null);

@@ -1543,6 +1542,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		s = new ReturnStmt(returnTok, rhss); 

 	}

 

+	void SkeletonStmt(out Statement s) {

+		List<IToken> names = null;

+		List<Expression> exprs = null;

+		IToken tok, dotdotdot;

+		Expression e; 

+		Expect(31);

+		dotdotdot = t; 

+		if (la.kind == 52) {

+			Get();

+			names = new List<IToken>(); exprs = new List<Expression>(); 

+			Ident(out tok);

+			Expect(11);

+			Expression(out e);

+			names.Add(tok); exprs.Add(e); 

+			while (la.kind == 21) {

+				Get();

+				Ident(out tok);

+				Expect(11);

+				Expression(out e);

+			}

+			names.Add(tok); exprs.Add(e); 

+		}

+		s = new SkeletonStatement(dotdotdot, names, exprs); 

+	}

+

 	void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {

 		IToken/*!*/ x, newToken;  Expression/*!*/ e;

 		List<Expression> ee = null;

@@ -1552,16 +1576,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 56) {

+		if (la.kind == 57) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 14 || la.kind == 23 || la.kind == 57) {

-				if (la.kind == 57) {

+			if (la.kind == 14 || la.kind == 23 || la.kind == 58) {

+				if (la.kind == 58) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(58);

+					Expect(59);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

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

@@ -1603,7 +1627,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

@@ -1614,7 +1638,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(154);

+		} else SynErr(156);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1626,16 +1650,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 14 || la.kind == 57) {

+			while (la.kind == 14 || la.kind == 58) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 14 || la.kind == 57) {

+			while (la.kind == 14 || la.kind == 58) {

 				Suffix(ref e);

 			}

-		} else SynErr(155);

+		} else SynErr(157);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1658,7 +1682,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(156);

+		} else SynErr(158);

 		Expect(25);

 	}

 

@@ -1669,11 +1693,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 62) {

+		while (la.kind == 63) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(63);

+			Expect(64);

 			body = new List<Statement>(); 

 			while (StartOf(9)) {

 				Stmt(body);

@@ -1691,22 +1715,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;

 		

 		while (StartOf(15)) {

-			if (la.kind == 33 || la.kind == 65) {

+			if (la.kind == 33 || la.kind == 66) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(157); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();}

 				Expect(12);

 				invariants.Add(invariant); 

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

-				while (!(la.kind == 0 || la.kind == 36)) {SynErr(158); Get();}

+				while (!(la.kind == 0 || la.kind == 36)) {SynErr(160); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}

 				Expect(12);

 			} else {

-				while (!(la.kind == 0 || la.kind == 32)) {SynErr(160); Get();}

+				while (!(la.kind == 0 || la.kind == 32)) {SynErr(162); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1721,7 +1745,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(163); Get();}

 				Expect(12);

 			}

 		}

@@ -1729,12 +1753,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 33 || la.kind == 65)) {SynErr(162); Get();}

+		while (!(la.kind == 0 || la.kind == 33 || la.kind == 66)) {SynErr(164); Get();}

 		if (la.kind == 33) {

 			Get();

 			isFree = true; 

 		}

-		Expect(65);

+		Expect(66);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1749,7 +1773,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

-		Expect(62);

+		Expect(63);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 23) {

@@ -1763,7 +1787,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(25);

 		}

-		Expect(63);

+		Expect(64);

 		while (StartOf(9)) {

 			Stmt(body);

 		}

@@ -1778,7 +1802,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(163);

+		} else SynErr(165);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1806,7 +1830,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpression(out e0);

-		while (la.kind == 70 || la.kind == 71) {

+		while (la.kind == 71 || la.kind == 72) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1817,7 +1841,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0);

-		if (la.kind == 72 || la.kind == 73) {

+		if (la.kind == 73 || la.kind == 74) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1826,23 +1850,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 70) {

+		if (la.kind == 71) {

 			Get();

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

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

 			Get();

-		} else SynErr(164);

+		} else SynErr(166);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

 		if (StartOf(16)) {

-			if (la.kind == 74 || la.kind == 75) {

+			if (la.kind == 75 || la.kind == 76) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 74 || la.kind == 75) {

+				while (la.kind == 75 || la.kind == 76) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1853,7 +1877,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 76 || la.kind == 77) {

+				while (la.kind == 77 || la.kind == 78) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1864,11 +1888,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 72) {

+		if (la.kind == 73) {

 			Get();

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

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

 			Get();

-		} else SynErr(165);

+		} else SynErr(167);

 	}

 

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

@@ -1962,25 +1986,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 74) {

+		if (la.kind == 75) {

 			Get();

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

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

 			Get();

-		} else SynErr(166);

+		} else SynErr(168);

 	}

 

 	void OrOp() {

-		if (la.kind == 76) {

+		if (la.kind == 77) {

 			Get();

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

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

 			Get();

-		} else SynErr(167);

+		} else SynErr(169);

 	}

 

 	void Term(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		Factor(out e0);

-		while (la.kind == 87 || la.kind == 88) {

+		while (la.kind == 88 || la.kind == 89) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2008,35 +2032,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 78: {

+		case 79: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 79: {

+		case 80: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 80: {

+		case 81: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 81: {

+		case 82: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Disjoint; 

 			break;

 		}

-		case 82: {

+		case 83: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.In; 

 			break;

 		}

-		case 83: {

+		case 84: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 82) {

+			if (la.kind == 83) {

 				Get();

 				y = t; 

 			}

@@ -2051,29 +2075,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			break;

 		}

-		case 84: {

+		case 85: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 85: {

+		case 86: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 86: {

+		case 87: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(168); break;

+		default: SynErr(170); break;

 		}

 	}

 

 	void Factor(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 48 || la.kind == 89 || la.kind == 90) {

+		while (la.kind == 48 || la.kind == 90 || la.kind == 91) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2082,44 +2106,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 87) {

+		if (la.kind == 88) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Add; 

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

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(169);

+		} else SynErr(171);

 	}

 

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

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

 		switch (la.kind) {

-		case 88: {

+		case 89: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

-		case 83: case 91: {

+		case 84: case 92: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 20: case 40: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {

+		case 20: case 40: case 56: case 61: case 67: case 68: case 101: case 103: case 104: case 105: case 106: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 14 || la.kind == 57) {

+			while (la.kind == 14 || la.kind == 58) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 57: {

+		case 6: case 58: {

 			DisplayExpr(out e);

 			break;

 		}

@@ -2131,14 +2155,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MapExpr(out e);

 			break;

 		}

-		case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {

 			ConstAtomExpression(out e);

-			while (la.kind == 14 || la.kind == 57) {

+			while (la.kind == 14 || la.kind == 58) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(170); break;

+		default: SynErr(172); break;

 		}

 	}

 

@@ -2147,47 +2171,45 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 48) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

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

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Div; 

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

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(171);

+		} else SynErr(173);

 	}

 

 	void NegOp() {

-		if (la.kind == 83) {

+		if (la.kind == 84) {

 			Get();

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

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

 			Get();

-		} else SynErr(172);

+		} else SynErr(174);

 	}

 

 	void EndlessExpression(out Expression e) {

 		IToken/*!*/ x;

 		Expression e0, e1;

 		e = dummyExpr;

-		BoundVar d;

-		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 60: {

+		case 61: {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(99);

+			Expect(100);

 			Expression(out e0);

-			Expect(61);

+			Expect(62);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

-		case 66: {

+		case 67: {

 			MatchExpression(out e);

 			break;

 		}

-		case 101: case 102: case 103: case 104: {

+		case 103: case 104: case 105: case 106: {

 			QuantifierGuts(out e);

 			break;

 		}

@@ -2195,7 +2217,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ComprehensionExpr(out e);

 			break;

 		}

-		case 67: {

+		case 68: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2204,7 +2226,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 55: {

+		case 56: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2214,31 +2236,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			break;

 		}

 		case 20: {

-			Get();

-			x = t;

-			letVars = new List<BoundVar>();

-			letRHSs = new List<Expression>(); 

-			IdentTypeOptional(out d);

-			letVars.Add(d); 

-			while (la.kind == 21) {

-				Get();

-				IdentTypeOptional(out d);

-				letVars.Add(d); 

-			}

-			Expect(53);

-			Expression(out e);

-			letRHSs.Add(e); 

-			while (la.kind == 21) {

-				Get();

-				Expression(out e);

-				letRHSs.Add(e); 

-			}

-			Expect(12);

-			Expression(out e);

-			e = new LetExpr(x, letVars, letRHSs, e); 

+			LetExpr(out e);

+			break;

+		}

+		case 101: {

+			NamedExpr(out e);

 			break;

 		}

-		default: SynErr(173); break;

+		default: SynErr(175); break;

 		}

 	}

 

@@ -2284,24 +2289,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

 			if (!func) { e = new ExprDotName(id, e, id.val); } 

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

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

 			Get();

 			x = t; 

 			if (StartOf(8)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 100) {

+				if (la.kind == 102) {

 					Get();

 					anyDots = true; 

 					if (StartOf(8)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 21 || la.kind == 58) {

+				} else if (la.kind == 21 || la.kind == 59) {

 					while (la.kind == 21) {

 						Get();

 						Expression(out ee);

@@ -2312,15 +2317,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(174);

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

+				} else SynErr(176);

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

 				Get();

 				anyDots = true; 

 				if (StartOf(8)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(175);

+			} else SynErr(177);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2343,8 +2348,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(58);

-		} else SynErr(176);

+			Expect(59);

+		} else SynErr(178);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2360,15 +2365,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

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

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(58);

-		} else SynErr(177);

+			Expect(59);

+		} else SynErr(179);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2394,7 +2399,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 		} else if (StartOf(18)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(178);

+		} else SynErr(180);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2405,14 +2410,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(43);

 		x = t; 

-		if (la.kind == 57) {

+		if (la.kind == 58) {

 			Get();

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

 			if (StartOf(8)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(58);

+			Expect(59);

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

 			BoundVar/*!*/ bv;

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

@@ -2428,7 +2433,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(18)) {

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

-		} else SynErr(179);

+		} else SynErr(181);

 	}

 

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

@@ -2437,17 +2442,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 92: {

+		case 93: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 93: {

+		case 94: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 94: {

+		case 95: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2457,12 +2462,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 95: {

+		case 96: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 96: {

+		case 97: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2471,7 +2476,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 97: {

+		case 98: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2480,7 +2485,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 98: {

+		case 99: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2505,7 +2510,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 			break;

 		}

-		default: SynErr(180); break;

+		default: SynErr(182); break;

 		}

 	}

 

@@ -2524,34 +2529,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

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

 		Expression(out d);

-		Expect(53);

+		Expect(54);

 		Expression(out r);

 		elements.Add(new ExpressionPair(d,r)); 

 		while (la.kind == 21) {

 			Get();

 			Expression(out d);

-			Expect(53);

+			Expect(54);

 			Expression(out r);

 			elements.Add(new ExpressionPair(d,r)); 

 		}

 	}

 

 	void QSep() {

-		if (la.kind == 105) {

+		if (la.kind == 107) {

 			Get();

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

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

 			Get();

-		} else SynErr(181);

+		} else SynErr(183);

 	}

 

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

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

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

 		

-		Expect(66);

+		Expect(67);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 62) {

+		while (la.kind == 63) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2566,13 +2571,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

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

+		if (la.kind == 103 || la.kind == 104) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 103 || la.kind == 104) {

+		} else if (la.kind == 105 || la.kind == 106) {

 			Exists();

 			x = t; 

-		} else SynErr(182);

+		} else SynErr(184);

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

 		QSep();

 		Expression(out body);

@@ -2603,7 +2608,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(19);

 		Expression(out range);

-		if (la.kind == 105 || la.kind == 106) {

+		if (la.kind == 107 || la.kind == 108) {

 			QSep();

 			Expression(out body);

 		}

@@ -2612,13 +2617,57 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 	}

 

+	void LetExpr(out Expression e) {

+		IToken/*!*/ x;

+		e = dummyExpr;

+		BoundVar d;

+		List<BoundVar> letVars;  List<Expression> letRHSs;

+		

+		Expect(20);

+		x = t;

+		letVars = new List<BoundVar>();

+		letRHSs = new List<Expression>(); 

+		IdentTypeOptional(out d);

+		letVars.Add(d); 

+		while (la.kind == 21) {

+			Get();

+			IdentTypeOptional(out d);

+			letVars.Add(d); 

+		}

+		Expect(54);

+		Expression(out e);

+		letRHSs.Add(e); 

+		while (la.kind == 21) {

+			Get();

+			Expression(out e);

+			letRHSs.Add(e); 

+		}

+		Expect(12);

+		Expression(out e);

+		e = new LetExpr(x, letVars, letRHSs, e); 

+	}

+

+	void NamedExpr(out Expression e) {

+		IToken/*!*/ x, d;

+		e = dummyExpr;

+		Expression expr;

+		

+		Expect(101);

+		x = t; 

+		NoUSIdent(out d);

+		Expect(5);

+		Expression(out e);

+		expr = e;

+		e = new NamedExpr(x, d, expr); 

+	}

+

 	void CaseExpression(out MatchCaseExpr/*!*/ c) {

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

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

 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(62);

+		Expect(63);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 23) {

@@ -2632,25 +2681,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(25);

 		}

-		Expect(63);

+		Expect(64);

 		Expression(out body);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

 

 	void Forall() {

-		if (la.kind == 101) {

+		if (la.kind == 103) {

 			Get();

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

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

 			Get();

-		} else SynErr(183);

+		} else SynErr(185);

 	}

 

 	void Exists() {

-		if (la.kind == 103) {

+		if (la.kind == 105) {

 			Get();

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

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

 			Get();

-		} else SynErr(184);

+		} else SynErr(186);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2686,26 +2735,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,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, 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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,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, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,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},

-		{T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,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,x, x,x,x,x, x,x,x,x, x,x,T,T, T,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,x, 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,T,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,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,T,T, T,x,x,T, x,x,x,x, T,x,x,x, 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, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,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,T,T, T,x,x,T, x,x,x,x, T,x,x,x, 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, T,T,T,T, T,T,T,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, T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,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,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, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,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, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,T,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,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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,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, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,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},

+		{T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,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,x,x,x, 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,T,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, 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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,x,T, T,T,T,x, x,x,x},

+		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,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,T,T, x,T,x,x, T,x,x,x, x,T,x,x, x,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,x,T, T,T,T,x, x,x,x},

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,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,T,T, x,T,x,x, T,x,x,x, x,T,x,x, x,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,T,T,T, T,T,T,T, 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, T,T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,x,T, T,T,T,x, x,x,x},

+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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, x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,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,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,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,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,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,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, T,T,x,x, x,x,T,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,T, T,x,x},

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,x,T, T,T,T,x, x,x,x}

 

 	};

 } // end Parser

@@ -2782,139 +2831,141 @@ public class Errors {
 			case 49: s = "\"`\" expected"; break;

 			case 50: s = "\"label\" expected"; break;

 			case 51: s = "\"break\" expected"; break;

-			case 52: s = "\"return\" expected"; break;

-			case 53: s = "\":=\" expected"; break;

-			case 54: s = "\":|\" expected"; break;

-			case 55: s = "\"assume\" expected"; break;

-			case 56: s = "\"new\" expected"; break;

-			case 57: s = "\"[\" expected"; break;

-			case 58: s = "\"]\" expected"; break;

-			case 59: s = "\"choose\" expected"; break;

-			case 60: s = "\"if\" expected"; break;

-			case 61: s = "\"else\" expected"; break;

-			case 62: s = "\"case\" expected"; break;

-			case 63: s = "\"=>\" expected"; break;

-			case 64: s = "\"while\" expected"; break;

-			case 65: s = "\"invariant\" expected"; break;

-			case 66: s = "\"match\" expected"; break;

-			case 67: s = "\"assert\" expected"; break;

-			case 68: s = "\"print\" expected"; break;

-			case 69: s = "\"parallel\" expected"; break;

-			case 70: s = "\"<==>\" expected"; break;

-			case 71: s = "\"\\u21d4\" expected"; break;

-			case 72: s = "\"==>\" expected"; break;

-			case 73: s = "\"\\u21d2\" expected"; break;

-			case 74: s = "\"&&\" expected"; break;

-			case 75: s = "\"\\u2227\" expected"; break;

-			case 76: s = "\"||\" expected"; break;

-			case 77: s = "\"\\u2228\" expected"; break;

-			case 78: s = "\"<=\" expected"; break;

-			case 79: s = "\">=\" expected"; break;

-			case 80: s = "\"!=\" expected"; break;

-			case 81: s = "\"!!\" expected"; break;

-			case 82: s = "\"in\" expected"; break;

-			case 83: s = "\"!\" expected"; break;

-			case 84: s = "\"\\u2260\" expected"; break;

-			case 85: s = "\"\\u2264\" expected"; break;

-			case 86: s = "\"\\u2265\" expected"; break;

-			case 87: s = "\"+\" expected"; break;

-			case 88: s = "\"-\" expected"; break;

-			case 89: s = "\"/\" expected"; break;

-			case 90: s = "\"%\" expected"; break;

-			case 91: s = "\"\\u00ac\" expected"; break;

-			case 92: s = "\"false\" expected"; break;

-			case 93: s = "\"true\" expected"; break;

-			case 94: s = "\"null\" expected"; break;

-			case 95: s = "\"this\" expected"; break;

-			case 96: s = "\"fresh\" expected"; break;

-			case 97: s = "\"allocated\" expected"; break;

-			case 98: s = "\"old\" expected"; break;

-			case 99: s = "\"then\" expected"; break;

-			case 100: s = "\"..\" expected"; break;

-			case 101: s = "\"forall\" expected"; break;

-			case 102: s = "\"\\u2200\" expected"; break;

-			case 103: s = "\"exists\" expected"; break;

-			case 104: s = "\"\\u2203\" expected"; break;

-			case 105: s = "\"::\" expected"; break;

-			case 106: s = "\"\\u2022\" expected"; break;

-			case 107: s = "??? expected"; break;

-			case 108: s = "invalid Dafny"; break;

-			case 109: s = "invalid SubModuleDecl"; break;

-			case 110: s = "invalid SubModuleDecl"; break;

-			case 111: s = "this symbol not expected in ClassDecl"; break;

-			case 112: s = "this symbol not expected in DatatypeDecl"; break;

-			case 113: s = "invalid DatatypeDecl"; break;

+			case 52: s = "\"where\" expected"; break;

+			case 53: s = "\"return\" expected"; break;

+			case 54: s = "\":=\" expected"; break;

+			case 55: s = "\":|\" expected"; break;

+			case 56: s = "\"assume\" expected"; break;

+			case 57: s = "\"new\" expected"; break;

+			case 58: s = "\"[\" expected"; break;

+			case 59: s = "\"]\" expected"; break;

+			case 60: s = "\"choose\" expected"; break;

+			case 61: s = "\"if\" expected"; break;

+			case 62: s = "\"else\" expected"; break;

+			case 63: s = "\"case\" expected"; break;

+			case 64: s = "\"=>\" expected"; break;

+			case 65: s = "\"while\" expected"; break;

+			case 66: s = "\"invariant\" expected"; break;

+			case 67: s = "\"match\" expected"; break;

+			case 68: s = "\"assert\" expected"; break;

+			case 69: s = "\"print\" expected"; break;

+			case 70: s = "\"parallel\" expected"; break;

+			case 71: s = "\"<==>\" expected"; break;

+			case 72: s = "\"\\u21d4\" expected"; break;

+			case 73: s = "\"==>\" expected"; break;

+			case 74: s = "\"\\u21d2\" expected"; break;

+			case 75: s = "\"&&\" expected"; break;

+			case 76: s = "\"\\u2227\" expected"; break;

+			case 77: s = "\"||\" expected"; break;

+			case 78: s = "\"\\u2228\" expected"; break;

+			case 79: s = "\"<=\" expected"; break;

+			case 80: s = "\">=\" expected"; break;

+			case 81: s = "\"!=\" expected"; break;

+			case 82: s = "\"!!\" expected"; break;

+			case 83: s = "\"in\" expected"; break;

+			case 84: s = "\"!\" expected"; break;

+			case 85: s = "\"\\u2260\" expected"; break;

+			case 86: s = "\"\\u2264\" expected"; break;

+			case 87: s = "\"\\u2265\" expected"; break;

+			case 88: s = "\"+\" expected"; break;

+			case 89: s = "\"-\" expected"; break;

+			case 90: s = "\"/\" expected"; break;

+			case 91: s = "\"%\" expected"; break;

+			case 92: s = "\"\\u00ac\" expected"; break;

+			case 93: s = "\"false\" expected"; break;

+			case 94: s = "\"true\" expected"; break;

+			case 95: s = "\"null\" expected"; break;

+			case 96: s = "\"this\" expected"; break;

+			case 97: s = "\"fresh\" expected"; break;

+			case 98: s = "\"allocated\" expected"; break;

+			case 99: s = "\"old\" expected"; break;

+			case 100: s = "\"then\" expected"; break;

+			case 101: s = "\"expr\" expected"; break;

+			case 102: s = "\"..\" expected"; break;

+			case 103: s = "\"forall\" expected"; break;

+			case 104: s = "\"\\u2200\" expected"; break;

+			case 105: s = "\"exists\" expected"; break;

+			case 106: s = "\"\\u2203\" expected"; break;

+			case 107: s = "\"::\" expected"; break;

+			case 108: s = "\"\\u2022\" expected"; break;

+			case 109: s = "??? expected"; break;

+			case 110: s = "invalid Dafny"; break;

+			case 111: s = "invalid SubModuleDecl"; break;

+			case 112: s = "invalid SubModuleDecl"; break;

+			case 113: s = "this symbol not expected in ClassDecl"; break;

 			case 114: s = "this symbol not expected in DatatypeDecl"; break;

-			case 115: s = "this symbol not expected in ArbitraryTypeDecl"; break;

-			case 116: s = "invalid ClassMemberDecl"; break;

-			case 117: s = "this symbol not expected in FieldDecl"; break;

-			case 118: s = "this symbol not expected in FieldDecl"; break;

-			case 119: s = "invalid FunctionDecl"; break;

-			case 120: s = "invalid FunctionDecl"; break;

+			case 115: s = "invalid DatatypeDecl"; break;

+			case 116: s = "this symbol not expected in DatatypeDecl"; break;

+			case 117: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 118: s = "invalid ClassMemberDecl"; break;

+			case 119: s = "this symbol not expected in FieldDecl"; break;

+			case 120: s = "this symbol not expected in FieldDecl"; break;

 			case 121: s = "invalid FunctionDecl"; break;

-			case 122: s = "this symbol not expected in MethodDecl"; break;

-			case 123: s = "invalid MethodDecl"; break;

-			case 124: s = "invalid MethodDecl"; break;

-			case 125: s = "invalid TypeAndToken"; break;

-			case 126: s = "this symbol not expected in MethodSpec"; break;

-			case 127: s = "this symbol not expected in MethodSpec"; break;

+			case 122: s = "invalid FunctionDecl"; break;

+			case 123: s = "invalid FunctionDecl"; break;

+			case 124: s = "this symbol not expected in MethodDecl"; break;

+			case 125: s = "invalid MethodDecl"; break;

+			case 126: s = "invalid MethodDecl"; break;

+			case 127: s = "invalid TypeAndToken"; break;

 			case 128: s = "this symbol not expected in MethodSpec"; break;

 			case 129: s = "this symbol not expected in MethodSpec"; break;

-			case 130: s = "invalid MethodSpec"; break;

+			case 130: s = "this symbol not expected in MethodSpec"; break;

 			case 131: s = "this symbol not expected in MethodSpec"; break;

 			case 132: s = "invalid MethodSpec"; break;

-			case 133: s = "invalid ReferenceType"; break;

-			case 134: s = "this symbol not expected in FunctionSpec"; break;

-			case 135: s = "this symbol not expected in FunctionSpec"; break;

+			case 133: s = "this symbol not expected in MethodSpec"; break;

+			case 134: s = "invalid MethodSpec"; break;

+			case 135: s = "invalid ReferenceType"; break;

 			case 136: s = "this symbol not expected in FunctionSpec"; break;

 			case 137: s = "this symbol not expected in FunctionSpec"; break;

 			case 138: s = "this symbol not expected in FunctionSpec"; break;

-			case 139: s = "invalid FunctionSpec"; break;

-			case 140: s = "invalid PossiblyWildFrameExpression"; break;

-			case 141: s = "invalid PossiblyWildExpression"; break;

-			case 142: s = "this symbol not expected in OneStmt"; break;

-			case 143: s = "invalid OneStmt"; break;

+			case 139: s = "this symbol not expected in FunctionSpec"; break;

+			case 140: s = "this symbol not expected in FunctionSpec"; break;

+			case 141: s = "invalid FunctionSpec"; break;

+			case 142: s = "invalid PossiblyWildFrameExpression"; break;

+			case 143: s = "invalid PossiblyWildExpression"; break;

 			case 144: s = "this symbol not expected in OneStmt"; break;

 			case 145: s = "invalid OneStmt"; break;

-			case 146: s = "invalid AssertStmt"; break;

-			case 147: s = "invalid AssumeStmt"; break;

-			case 148: s = "invalid UpdateStmt"; break;

-			case 149: s = "invalid UpdateStmt"; break;

-			case 150: s = "invalid IfStmt"; break;

-			case 151: s = "invalid IfStmt"; break;

-			case 152: s = "invalid WhileStmt"; break;

-			case 153: s = "invalid WhileStmt"; break;

-			case 154: s = "invalid Rhs"; break;

-			case 155: s = "invalid Lhs"; break;

-			case 156: s = "invalid Guard"; break;

-			case 157: s = "this symbol not expected in LoopSpec"; break;

-			case 158: s = "this symbol not expected in LoopSpec"; break;

+			case 146: s = "this symbol not expected in OneStmt"; break;

+			case 147: s = "invalid OneStmt"; break;

+			case 148: s = "invalid AssertStmt"; break;

+			case 149: s = "invalid AssumeStmt"; break;

+			case 150: s = "invalid UpdateStmt"; break;

+			case 151: s = "invalid UpdateStmt"; break;

+			case 152: s = "invalid IfStmt"; break;

+			case 153: s = "invalid IfStmt"; break;

+			case 154: s = "invalid WhileStmt"; break;

+			case 155: s = "invalid WhileStmt"; break;

+			case 156: s = "invalid Rhs"; break;

+			case 157: s = "invalid Lhs"; break;

+			case 158: s = "invalid Guard"; break;

 			case 159: s = "this symbol not expected in LoopSpec"; break;

 			case 160: s = "this symbol not expected in LoopSpec"; break;

 			case 161: s = "this symbol not expected in LoopSpec"; break;

-			case 162: s = "this symbol not expected in Invariant"; break;

-			case 163: s = "invalid AttributeArg"; break;

-			case 164: s = "invalid EquivOp"; break;

-			case 165: s = "invalid ImpliesOp"; break;

-			case 166: s = "invalid AndOp"; break;

-			case 167: s = "invalid OrOp"; break;

-			case 168: s = "invalid RelOp"; break;

-			case 169: s = "invalid AddOp"; break;

-			case 170: s = "invalid UnaryExpression"; break;

-			case 171: s = "invalid MulOp"; break;

-			case 172: s = "invalid NegOp"; break;

-			case 173: s = "invalid EndlessExpression"; break;

-			case 174: s = "invalid Suffix"; break;

-			case 175: s = "invalid Suffix"; break;

+			case 162: s = "this symbol not expected in LoopSpec"; break;

+			case 163: s = "this symbol not expected in LoopSpec"; break;

+			case 164: s = "this symbol not expected in Invariant"; break;

+			case 165: s = "invalid AttributeArg"; break;

+			case 166: s = "invalid EquivOp"; break;

+			case 167: s = "invalid ImpliesOp"; break;

+			case 168: s = "invalid AndOp"; break;

+			case 169: s = "invalid OrOp"; break;

+			case 170: s = "invalid RelOp"; break;

+			case 171: s = "invalid AddOp"; break;

+			case 172: s = "invalid UnaryExpression"; break;

+			case 173: s = "invalid MulOp"; break;

+			case 174: s = "invalid NegOp"; break;

+			case 175: s = "invalid EndlessExpression"; break;

 			case 176: s = "invalid Suffix"; break;

-			case 177: s = "invalid DisplayExpr"; break;

-			case 178: s = "invalid MultiSetExpr"; break;

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

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

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

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

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

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

+			case 177: s = "invalid Suffix"; break;

+			case 178: s = "invalid Suffix"; break;

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a49a906e..0b922413 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1167,7 +1167,12 @@ namespace Microsoft.Dafny {
         }

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

 

-      } else if (expr is SetComprehension) {

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        wr.Write("expr {0}: ", e.Name);

+        PrintExpression(e.Body);

+ 

+       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         bool parensNeeded = !isRightmost;

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

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0a653f6c..68ab2c20 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -62,8 +62,8 @@ namespace Microsoft.Dafny {
     private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

 

     public void PreResolve(ModuleDefinition m) {

-      Contract.Requires(m != null);

-      Contract.Requires(m.RefinementBase != null);

+      

+      if (m.RefinementBase == null) return;

 

       if (moduleUnderConstruction != null) {

         postTasks.Clear();

@@ -424,6 +424,9 @@ namespace Microsoft.Dafny {
         var e = (LetExpr)expr;

         return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr) expr;

+        return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var tk = Tok(e.tok);

@@ -698,8 +701,12 @@ namespace Microsoft.Dafny {
         } else {

           var nwMember = nw.Members[index];

           if (nwMember is Field) {

-            reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) is not allowed replace an existing declaration in the refinement base", nwMember.Name, nw.Name);

-

+            if (member is Field && TypesAreEqual(((Field)nwMember).Type, ((Field)member).Type)) {

+              if (member.IsGhost || !nwMember.IsGhost)

+                reporter.Error(nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name, nw.Name);

+            } else {

+              reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name);

+            }

           } else if (nwMember is Function) {

             var f = (Function)nwMember;

             bool isPredicate = f is Predicate;

@@ -799,7 +806,228 @@ namespace Microsoft.Dafny {
 

       return nw;

     }

+    private Statement SubstituteNamedExpr(Statement s, string p, Expression E, ref int subCount) {

+      if (s == null) {

+        return null;

+      } else if (s is AssertStmt) {

+        AssertStmt stmt = (AssertStmt)s;

+        return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);

+      } else if (s is AssumeStmt) {

+        AssumeStmt stmt = (AssumeStmt)s;

+        return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);

+      } else if (s is PrintStmt) {

+        throw new NotImplementedException();

+      } else if (s is BreakStmt) {

+        return s;

+      } else if (s is ReturnStmt) {

+        return s;

+      } else if (s is VarDeclStmt) {

+        return s;

+      } else if (s is AssignSuchThatStmt) {

+        return s;

+      } else if (s is UpdateStmt) {

+        UpdateStmt stmt = (UpdateStmt)s;

+        List<Expression> lhs = new List<Expression>();

+        List<AssignmentRhs> rhs = new List<AssignmentRhs>();

+        foreach (Expression l in stmt.Lhss) {

+          lhs.Add(SubstituteNamedExpr(l, p, E, ref subCount));

+        }

+        foreach (AssignmentRhs r in stmt.Rhss) {

+          if (r is HavocRhs) {

+            rhs.Add(r); // no substitution on Havoc (*);

+          } else if (r is ExprRhs) {

+            rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, p, E, ref subCount)));

+          } else if (r is CallRhs) {

+            CallRhs rr = (CallRhs)r;

+            rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, p, E, ref subCount), rr.MethodName, SubstituteNamedExprList(rr.Args, p, E, ref subCount)));

+          } else if (r is TypeRhs) {

+            rhs.Add(r);

+          } else {

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

+            throw new cce.UnreachableException();

+          }

+        }

+        return new UpdateStmt(stmt.Tok, lhs, rhs);

+      } else if (s is AssignStmt) {

+        Contract.Assert(false);  // AssignStmt is not generated by the parser

+        throw new cce.UnreachableException();

+      } else if (s is VarDecl) {

+        return s;

+      } else if (s is CallStmt) {

+        return s;

+      } else if (s is BlockStmt) {

+        BlockStmt stmt = (BlockStmt)s;

+        List<Statement> res = new List<Statement>();

+        foreach (Statement ss in stmt.Body) {

+          res.Add(SubstituteNamedExpr(ss, p, E, ref subCount));

+        }

+        return new BlockStmt(stmt.Tok, res);

+      } else if (s is IfStmt) {

+        IfStmt stmt = (IfStmt)s;

+        return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount),

+                         (BlockStmt)SubstituteNamedExpr(stmt.Thn, p, E, ref subCount),

+                                    SubstituteNamedExpr(stmt.Els, p, E, ref subCount));

+      } else if (s is AlternativeStmt) {

+        return s;

+      } else if (s is WhileStmt) {

+        WhileStmt stmt = (WhileStmt)s;

+        return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, p, E, ref subCount));

+      } else if (s is AlternativeLoopStmt) {

+        return s;

+      } else if (s is ParallelStmt) {

+        return s;

+      } else if (s is MatchStmt) {

+        return s;

+      } else if (s is SkeletonStatement) {

+        return s;

+      } else {

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

+        throw new cce.UnreachableException();

+      }

+

+    }

+    private Expression SubstituteNamedExpr(Expression expr, string p, Expression E, ref int subCount) {

+      if (expr == null) {

+        return null;

+      }

+      if (expr is NamedExpr) {

+        NamedExpr n = (NamedExpr)expr;

+        if (n.Name == p) {

+          subCount++;

+          return new NamedExpr(n.tok, n.Name, E);

+        } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount));

+      } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {

+        return expr;

+      } else if (expr is DisplayExpression) {

+        DisplayExpression e = (DisplayExpression)expr;

+        List<Expression> newElements = SubstituteNamedExprList(e.Elements, p, E, ref subCount);

+        if (expr is SetDisplayExpr) {

+          return new SetDisplayExpr(expr.tok, newElements);

+        } else if (expr is MultiSetDisplayExpr) {

+          return new MultiSetDisplayExpr(expr.tok, newElements);

+        } else {

+          return new SeqDisplayExpr(expr.tok, newElements);

+        }

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr fse = (FieldSelectExpr)expr;

+        Expression substE = SubstituteNamedExpr(fse.Obj, p, E, ref subCount);

+        return new FieldSelectExpr(fse.tok, substE, fse.FieldName);

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr sse = (SeqSelectExpr)expr;

+        Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);

+        Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, p, E, ref subCount);

+        Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, p, E, ref subCount);

+        return new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr sse = (SeqUpdateExpr)expr;

+        Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);

+        Expression index = SubstituteNamedExpr(sse.Index, p, E, ref subCount);

+        Expression val = SubstituteNamedExpr(sse.Value, p, E, ref subCount);

+        return new SeqUpdateExpr(sse.tok, seq, index, val);

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr mse = (MultiSelectExpr)expr;

+        Expression array = SubstituteNamedExpr(mse.Array, p, E, ref subCount);

+        List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, p, E, ref subCount);

+        return new MultiSelectExpr(mse.tok, array, newArgs);

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+        Expression receiver = SubstituteNamedExpr(e.Receiver, p, E, ref subCount);

+        List<Expression> newArgs = SubstituteNamedExprList(e.Args, p, E, ref subCount);

+        return new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);

+      } else if (expr is DatatypeValue) {

+        DatatypeValue dtv = (DatatypeValue)expr;

+        List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, p, E, ref subCount);

+        return new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);

+      } else if (expr is OldExpr) {

+        OldExpr e = (OldExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new OldExpr(expr.tok, se);

+      } else if (expr is FreshExpr) {

+        FreshExpr e = (FreshExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new FreshExpr(expr.tok, se);

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new AllocatedExpr(expr.tok, se);

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new UnaryExpr(expr.tok, e.Op, se);

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+        Expression e0 = SubstituteNamedExpr(e.E0, p, E, ref subCount);

+        Expression e1 = SubstituteNamedExpr(e.E1, p, E, ref subCount);

+        return new BinaryExpr(expr.tok, e.Op, e0, e1);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        var rhss = SubstituteNamedExprList(e.RHSs, p, E, ref subCount);

+        var body = SubstituteNamedExpr(e.Body, p, E, ref subCount);

+        return new LetExpr(e.tok, e.Vars, rhss, body);

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

+        Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, p, E, ref subCount);

+        Expression newTerm = SubstituteNamedExpr(e.Term, p, E, ref subCount);

+        Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, p, E, ref subCount);

+        if (e is SetComprehension) {

+          return new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+        } else if (e is MapComprehension) {

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

+        } else if (e is QuantifierExpr) {

+          var q = (QuantifierExpr)e;

+          if (expr is ForallExpr) {

+            return new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+          } else {

+            return new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+          }

+        } else {

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

+          throw new cce.UnreachableException();

+        }

+

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        Expression g = SubstituteNamedExpr(e.Guard, p, E, ref subCount);

+        Expression b = SubstituteNamedExpr(e.Body, p, E, ref subCount);

+        if (expr is AssertExpr) {

+          return new AssertExpr(e.tok, g, b);

+        } else {

+          return new AssumeExpr(e.tok, g, b);

+        }

+      } else if (expr is ITEExpr) {

+        ITEExpr e = (ITEExpr)expr;

+        Expression test = SubstituteNamedExpr(e.Test, p, E, ref subCount);

+        Expression thn = SubstituteNamedExpr(e.Thn, p, E, ref subCount);

+        Expression els = SubstituteNamedExpr(e.Els, p, E, ref subCount);

+        return new ITEExpr(expr.tok, test, thn, els);

+      } else if (expr is ConcreteSyntaxExpression) {

+        if (expr is ParensExpression) {

+          return SubstituteNamedExpr(((ParensExpression)expr).E, p, E, ref subCount);

+        } else if (expr is IdentifierSequence) {

+          return expr;

+        } else if (expr is ExprDotName) {

+          ExprDotName edn = (ExprDotName)expr;

+          return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, p, E, ref subCount), edn.SuffixName);

+        } else if (expr is ChainingExpression) {

+          ChainingExpression ch = (ChainingExpression)expr;

+          return SubstituteNamedExpr(ch.E, p, E, ref subCount);

+        } else {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        }

+      } else {

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

+      }

+    }

 

+    private List<Expression> SubstituteNamedExprList(List<Expression> list, string p, Expression E, ref int subCount) {

+      List<Expression> res = new List<Expression>();

+      foreach (Expression e in list) {

+        res.Add(SubstituteNamedExpr(e, p, E, ref subCount));

+      }

+      return res;

+    }

     void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {

       Contract.Requires(tok != null);

       Contract.Requires(old != null);

@@ -915,7 +1143,8 @@ namespace Microsoft.Dafny {
            *   while (G) LoopSpec ...      while (*) LoopSpec' Body     while (G) Merge(LoopSpec,LoopSpec') Body

            *   while (G) LoopSpec Body     while (*) LoopSpec' Body'    while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')

            *   

-           *   ...; S                      StmtThatDoesNotMatchS; S'    StatementThatDoesNotMatchS; Merge( ...;S , S')

+           *   ... where x = e; S          StmtThatDoesNotMatchS; S'    StatementThatDoesNotMatchS[e/x]; Merge( ... where x = e; S , S')

+           *   ... where x = e; S          StmtThatMatchesS; S'         StmtThatMatchesS; S'

            * 

            * Note, LoopSpec must contain only invariant declarations (as the parser ensures for the first three cases).

            * Note, there is an implicit "...;" at the end of every block in a skeleton.

@@ -924,23 +1153,26 @@ namespace Microsoft.Dafny {
            */

           if (cur is SkeletonStatement) {

             var S = ((SkeletonStatement)cur).S;

+            var c = (SkeletonStatement) cur;

             if (S == null) {

-              if (i + 1 == skeleton.Body.Count) {

-                // this "...;" is the last statement of the skeleton, so treat it like the default case

+              var nxt = i + 1 == skeleton.Body.Count ? null : skeleton.Body[i+1];

+              if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {

+                // "...; ...;" is the same as just "...;", so skip this one

               } else {

-                var nxt = skeleton.Body[i+1];

-                if (nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {

-                  // "...; ...;" is the same as just "...;", so skip this one

-                } else {

-                  // skip up until the next thing that matches "nxt"

-                  while (!PotentialMatch(nxt, oldS)) {

-                    // loop invariant:  oldS == oldStmt.Body[j]

-                    body.Add(CloneStmt(oldS));

-                    j++;

-                    if (j == oldStmt.Body.Count) { break; }

-                    oldS = oldStmt.Body[j];

-                  }

+                int subCount = 0;

+                // skip up until the next thing that matches "nxt"

+                while (nxt == null || !PotentialMatch(nxt, oldS)) {

+                  // loop invariant:  oldS == oldStmt.Body[j]

+                  var s = CloneStmt(oldS);

+                  if (c.NameReplacements != null)

+                    s = SubstituteNamedExpr(s, c.NameReplacements[0].val, c.ExprReplacements[0], ref subCount);

+                  body.Add(s);

+                  j++;

+                  if (j == oldStmt.Body.Count) { break; }

+                  oldS = oldStmt.Body[j];

                 }

+                if (c.NameReplacements != null && subCount == 0)

+                  reporter.Error(c.NameReplacements[0], "did not find expression labeld {0}", c.NameReplacements[0].val);

               }

               i++;

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0a18b783..b226c3fe 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -369,7 +369,7 @@ namespace Microsoft.Dafny {
       foreach (var kv in m.StaticMembers) {

         info.StaticMembers[kv.Key] = kv.Value;

       }

-

+      info.IsGhost = m.IsGhost;

       return info;

     }

     ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {

@@ -3903,7 +3903,11 @@ namespace Microsoft.Dafny {
         scope.PopMarker();

         expr.Type = e.Body.Type;

 

-      } else if (expr is QuantifierExpr) {

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        ResolveExpression(e.Body, twoState);

+        e.Type = e.Body.Type;

+      }else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

         scope.PushMarker();

@@ -4347,6 +4351,9 @@ namespace Microsoft.Dafny {
           }

           return;

         }

+      } else if (expr is NamedExpr) {

+        if (moduleInfo.IsGhost) return;

+        else CheckIsNonGhost(((NamedExpr)expr).Body);

       }

 

       foreach (var ee in expr.SubExpressions) {

@@ -5380,6 +5387,8 @@ namespace Microsoft.Dafny {
           return true;

         }

         return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);

+      }  else if (expr is NamedExpr) {

+         return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);

       } else if (expr is ComprehensionExpr) {

         if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {

           return true;  // the quantifier cannot be compiled if the resolver found no bounds

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 32c92a8b..efd31cbe 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 107;

-	const int noSym = 107;

+	const int maxT = 109;

+	const int noSym = 109;

 

 

 	[ContractInvariantMethod]

@@ -519,30 +519,32 @@ public class Scanner {
 			case "reads": t.kind = 47; break;

 			case "label": t.kind = 50; break;

 			case "break": t.kind = 51; break;

-			case "return": t.kind = 52; break;

-			case "assume": t.kind = 55; break;

-			case "new": t.kind = 56; break;

-			case "choose": t.kind = 59; break;

-			case "if": t.kind = 60; break;

-			case "else": t.kind = 61; break;

-			case "case": t.kind = 62; break;

-			case "while": t.kind = 64; break;

-			case "invariant": t.kind = 65; break;

-			case "match": t.kind = 66; break;

-			case "assert": t.kind = 67; break;

-			case "print": t.kind = 68; break;

-			case "parallel": t.kind = 69; break;

-			case "in": t.kind = 82; break;

-			case "false": t.kind = 92; break;

-			case "true": t.kind = 93; break;

-			case "null": t.kind = 94; break;

-			case "this": t.kind = 95; break;

-			case "fresh": t.kind = 96; break;

-			case "allocated": t.kind = 97; break;

-			case "old": t.kind = 98; break;

-			case "then": t.kind = 99; break;

-			case "forall": t.kind = 101; break;

-			case "exists": t.kind = 103; break;

+			case "where": t.kind = 52; break;

+			case "return": t.kind = 53; break;

+			case "assume": t.kind = 56; break;

+			case "new": t.kind = 57; break;

+			case "choose": t.kind = 60; break;

+			case "if": t.kind = 61; break;

+			case "else": t.kind = 62; break;

+			case "case": t.kind = 63; break;

+			case "while": t.kind = 65; break;

+			case "invariant": t.kind = 66; break;

+			case "match": t.kind = 67; break;

+			case "assert": t.kind = 68; break;

+			case "print": t.kind = 69; break;

+			case "parallel": t.kind = 70; break;

+			case "in": t.kind = 83; break;

+			case "false": t.kind = 93; break;

+			case "true": t.kind = 94; break;

+			case "null": t.kind = 95; break;

+			case "this": t.kind = 96; break;

+			case "fresh": t.kind = 97; break;

+			case "allocated": t.kind = 98; break;

+			case "old": t.kind = 99; break;

+			case "then": t.kind = 100; break;

+			case "expr": t.kind = 101; break;

+			case "forall": t.kind = 103; break;

+			case "exists": t.kind = 105; break;

 			default: break;

 		}

 	}

@@ -662,67 +664,67 @@ public class Scanner {
 			case 25:

 				{t.kind = 49; break;}

 			case 26:

-				{t.kind = 53; break;}

-			case 27:

 				{t.kind = 54; break;}

+			case 27:

+				{t.kind = 55; break;}

 			case 28:

-				{t.kind = 57; break;}

-			case 29:

 				{t.kind = 58; break;}

+			case 29:

+				{t.kind = 59; break;}

 			case 30:

-				{t.kind = 63; break;}

+				{t.kind = 64; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 70; break;}

-			case 33:

 				{t.kind = 71; break;}

-			case 34:

+			case 33:

 				{t.kind = 72; break;}

-			case 35:

+			case 34:

 				{t.kind = 73; break;}

+			case 35:

+				{t.kind = 74; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 74; break;}

-			case 38:

 				{t.kind = 75; break;}

-			case 39:

+			case 38:

 				{t.kind = 76; break;}

-			case 40:

+			case 39:

 				{t.kind = 77; break;}

+			case 40:

+				{t.kind = 78; break;}

 			case 41:

-				{t.kind = 79; break;}

-			case 42:

 				{t.kind = 80; break;}

-			case 43:

+			case 42:

 				{t.kind = 81; break;}

+			case 43:

+				{t.kind = 82; break;}

 			case 44:

-				{t.kind = 84; break;}

-			case 45:

 				{t.kind = 85; break;}

-			case 46:

+			case 45:

 				{t.kind = 86; break;}

-			case 47:

+			case 46:

 				{t.kind = 87; break;}

-			case 48:

+			case 47:

 				{t.kind = 88; break;}

-			case 49:

+			case 48:

 				{t.kind = 89; break;}

-			case 50:

+			case 49:

 				{t.kind = 90; break;}

-			case 51:

+			case 50:

 				{t.kind = 91; break;}

+			case 51:

+				{t.kind = 92; break;}

 			case 52:

-				{t.kind = 102; break;}

-			case 53:

 				{t.kind = 104; break;}

+			case 53:

+				{t.kind = 106; break;}

 			case 54:

-				{t.kind = 105; break;}

+				{t.kind = 107; break;}

 			case 55:

-				{t.kind = 106; break;}

+				{t.kind = 108; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 26;}

@@ -751,22 +753,22 @@ public class Scanner {
 				if (ch == '=') {AddCh(); goto case 41;}

 				else {t.kind = 27; break;}

 			case 62:

-				recEnd = pos; recKind = 83;

+				recEnd = pos; recKind = 84;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

-				else {t.kind = 83; break;}

+				else {t.kind = 84; break;}

 			case 63:

 				recEnd = pos; recKind = 24;

 				if (ch == '>') {AddCh(); goto case 34;}

 				else {t.kind = 24; break;}

 			case 64:

-				recEnd = pos; recKind = 100;

+				recEnd = pos; recKind = 102;

 				if (ch == '.') {AddCh(); goto case 23;}

-				else {t.kind = 100; break;}

+				else {t.kind = 102; break;}

 			case 65:

-				recEnd = pos; recKind = 78;

+				recEnd = pos; recKind = 79;

 				if (ch == '=') {AddCh(); goto case 31;}

-				else {t.kind = 78; break;}

+				else {t.kind = 79; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index aecd8e3d..5d0baaed 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2049,6 +2049,8 @@ namespace Microsoft.Dafny {
         }

         return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));

 

+      } else if (expr is NamedExpr) {

+        return CanCallAssumption(((NamedExpr)expr).Body, etran);

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = CanCallAssumption(e.Term, etran);

@@ -2078,7 +2080,9 @@ namespace Microsoft.Dafny {
         total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));

         total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));

         return total;

-      } else if (expr is ConcreteSyntaxExpression) {

+      } else if (expr is NamedExpr) {

+        return CanCallAssumption(((NamedExpr)expr).Body, etran);

+       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

         return CanCallAssumption(e.ResolvedExpression, etran);

       } else {

@@ -2512,6 +2516,8 @@ namespace Microsoft.Dafny {
         CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);

         result = null;

 

+      } else if (expr is NamedExpr) {

+        CheckWellformedWithResult(((NamedExpr)expr).Body, options, result, resultType, locals, builder, etran);

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);

@@ -6006,6 +6012,8 @@ namespace Microsoft.Dafny {
           var e = (LetExpr)expr;

           return TrExpr(GetSubstitutedBody(e));

 

+        } else if (expr is NamedExpr) {

+          return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

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

@@ -7673,6 +7681,12 @@ namespace Microsoft.Dafny {
           newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

         }

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        var body = Substitute(e.Body, receiverReplacement, substMap);

+        if (body != e.Body) {

+          newExpr = new NamedExpr(e.tok, e.Name, body);

+        }

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

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