Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to parallel syntax, other minor fixes

7 files changed, 310 insertions, 275 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 7f48e551..3864df8b 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -2184,6 +2184,8 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         TrExpr(e.ResolvedExpression);

 

+      } else if (expr is NamedExpr) {

+        TrExpr(((NamedExpr)expr).Body);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 78e7675e..54b9b4a4 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -765,14 +765,24 @@ OneStmt<out Statement/*!*/ s>
 SkeletonStmt<out Statement s>

 = (. List<IToken> names = null;

      List<Expression> exprs = null;

-     IToken tok, dotdotdot;

+     IToken tok, dotdotdot, whereTok;

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

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

+     Ident<out tok>                    (. names.Add(tok); .)

+     {"," Ident<out tok>               (. names.Add(tok); .)

+     }

+     ":=" 

+     Expression<out e>                 (. exprs.Add(e); .)

+     {"," Expression<out e>            (. exprs.Add(e); .)

+     }

+                                       (. if (exprs.Count != names.Count) {

+                                            SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");

+                                            names = null; exprs = null;

+                                          }

+                                       .) 

   ]

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

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

   .

 ReturnStmt<out Statement/*!*/ s>

 = (.

@@ -1527,7 +1537,7 @@ NamedExpr<out Expression e>
      e = dummyExpr;

      Expression expr;

   .)

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

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

     NoUSIdent<out d>

     ":"

     Expression<out e>               (. expr = e;

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 9c47278b..350ebd8e 100644
--- a/Dafny/Parser.cs
+++ b/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 = 110;

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

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

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

+		} 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(114); 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(115); 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(116);

+		} 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(117); 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(118); 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(119);

+		} 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(120); 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(121); 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(122);

+			} else SynErr(121);

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

 			Get();

 			isPredicate = true; 

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

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(123);

+			} else SynErr(122);

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

 			Get();

 			isCoPredicate = true; 

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

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(124);

-		} else SynErr(125);

+			} else SynErr(123);

+		} else SynErr(124);

 		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

 		while (StartOf(4)) {

 			FunctionSpec(reqs, reads, ens, decreases);

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

 		IToken bodyEnd = Token.NoToken;

 		

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

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

 		if (la.kind == 28) {

 			Get();

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

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

 			}

 			

-		} else SynErr(127);

+		} else SynErr(126);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

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

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

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(128);

+		} else SynErr(127);

 		while (StartOf(5)) {

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

 		}

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

 			break;

 		}

-		default: SynErr(129); break;

+		default: SynErr(128); break;

 		}

 	}

 

@@ -898,7 +898,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(130); Get();}

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

 		if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

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

 				}

 			}

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

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

 			Expect(12);

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

 			if (la.kind == 33) {

@@ -923,7 +923,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(132); Get();}

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

 				Expect(12);

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

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

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

 				}

 				Expression(out e);

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

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

 				Expect(12);

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

-			} else SynErr(134);

+			} else SynErr(133);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(136);

+		} else SynErr(135);

 	}

 

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

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

 			}

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

-		} else SynErr(137);

+		} else SynErr(136);

 	}

 

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

@@ -1054,10 +1054,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(decreases == null || cce.NonNullElements(decreases));

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

 		if (la.kind == 34) {

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

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			reqs.Add(e); 

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

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

 				}

 			}

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

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

 			Expect(12);

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			ens.Add(e); 

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

@@ -1087,9 +1087,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(143);

+		} else SynErr(142);

 	}

 

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

@@ -1108,7 +1108,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(144);

+		} else SynErr(143);

 	}

 

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

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

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(145);

+		} else SynErr(144);

 	}

 

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

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

 		int breakCount;

 		

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

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

 		switch (la.kind) {

 		case 6: {

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

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

 					breakCount++; 

 				}

-			} else SynErr(147);

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

+			} else SynErr(146);

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

 			Expect(12);

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

 			break;

 		}

-		case 54: {

+		case 55: {

 			ReturnStmt(out s);

 			break;

 		}

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

 			break;

 		}

-		default: SynErr(149); break;

+		default: SynErr(148); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(150);

+		} else SynErr(149);

 		Expect(12);

 		if (e == null) {

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

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

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

 			Get();

-		} else SynErr(151);

+		} else SynErr(150);

 		if (e == null) {

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

 		} else {

@@ -1299,14 +1299,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 == 55 || la.kind == 56) {

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

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 21) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 55) {

+			if (la.kind == 54) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

@@ -1324,12 +1324,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(152);

+			} else SynErr(151);

 			Expect(12);

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

 			Get();

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

-		} else SynErr(153);

+		} else SynErr(152);

 		if (suchThat != null) {

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

 		} else {

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

 			lhss.Add(d); 

 		}

-		if (la.kind == 55 || la.kind == 56) {

-			if (la.kind == 55) {

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

+			if (la.kind == 54) {

 				Get();

 				assignTok = t;

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

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

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

 					els = bs; 

-				} else SynErr(154);

+				} else SynErr(153);

 			}

 			if (guardOmitted) {

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

@@ -1449,7 +1449,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(155);

+		} else SynErr(154);

 	}

 

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

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

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(156);

+			} else SynErr(155);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

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

@@ -1499,7 +1499,7 @@ 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(157);

+		} else SynErr(156);

 	}

 

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

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

 		AssignmentRhs r;

 		

-		Expect(54);

+		Expect(55);

 		returnTok = t; 

 		if (StartOf(13)) {

 			Rhs(out r, null);

@@ -1581,24 +1581,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void SkeletonStmt(out Statement s) {

 		List<IToken> names = null;

 		List<Expression> exprs = null;

-		IToken tok, dotdotdot;

+		IToken tok, dotdotdot, whereTok;

 		Expression e; 

 		Expect(31);

 		dotdotdot = t; 

 		if (la.kind == 53) {

 			Get();

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

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

 			Ident(out tok);

-			Expect(11);

-			Expression(out e);

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

+			names.Add(tok); 

 			while (la.kind == 21) {

 				Get();

 				Ident(out tok);

-				Expect(11);

+				names.Add(tok); 

+			}

+			Expect(54);

+			Expression(out e);

+			exprs.Add(e); 

+			while (la.kind == 21) {

+				Get();

 				Expression(out e);

+				exprs.Add(e); 

+			}

+			if (exprs.Count != names.Count) {

+			 SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");

+			 names = null; exprs = null;

 			}

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

+			

 		}

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

 	}

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(158);

+		} else SynErr(157);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1695,7 +1704,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 14 || la.kind == 59) {

 				Suffix(ref e);

 			}

-		} else SynErr(159);

+		} else SynErr(158);

 	}

 

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

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(160);

+		} else SynErr(159);

 		Expect(25);

 	}

 

@@ -1753,20 +1762,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (StartOf(15)) {

 			if (la.kind == 33 || la.kind == 67) {

 				Invariant(out invariant);

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

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

 				Expect(12);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(12);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

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

 					}

 				}

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

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

 				Expect(12);

 			}

 		}

@@ -1789,7 +1798,7 @@ 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 == 67)) {SynErr(166); Get();}

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

 		if (la.kind == 33) {

 			Get();

 			isFree = true; 

@@ -1838,7 +1847,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(167);

+		} else SynErr(166);

 	}

 

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

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

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

 			Get();

-		} else SynErr(168);

+		} else SynErr(167);

 	}

 

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

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

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

 			Get();

-		} else SynErr(169);

+		} else SynErr(168);

 	}

 

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

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

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

 			Get();

-		} else SynErr(170);

+		} else SynErr(169);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(171);

+		} else SynErr(170);

 	}

 

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

@@ -2126,7 +2135,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(172); break;

+		default: SynErr(171); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(173);

+		} else SynErr(172);

 	}

 

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

@@ -2168,7 +2177,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 20: case 40: case 57: case 62: case 68: case 69: case 102: case 104: case 105: case 106: case 107: {

+		case 20: case 40: case 51: case 57: case 62: case 68: case 69: case 103: case 104: case 105: case 106: {

 			EndlessExpression(out e);

 			break;

 		}

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

 			break;

 		}

-		default: SynErr(174); break;

+		default: SynErr(173); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(175);

+		} else SynErr(174);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(176);

+		} else SynErr(175);

 	}

 

 	void EndlessExpression(out Expression e) {

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

 			break;

 		}

-		case 104: case 105: case 106: case 107: {

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

 			QuantifierGuts(out e);

 			break;

 		}

@@ -2275,11 +2284,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LetExpr(out e);

 			break;

 		}

-		case 102: {

+		case 51: {

 			NamedExpr(out e);

 			break;

 		}

-		default: SynErr(177); break;

+		default: SynErr(176); break;

 		}

 	}

 

@@ -2331,14 +2340,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (StartOf(8)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 103) {

+				if (la.kind == 102) {

 					Get();

 					anyDots = true; 

 					if (StartOf(8)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

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

 						

 					}

-				} else SynErr(178);

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

+				} else SynErr(177);

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

 				Get();

 				anyDots = true; 

 				if (StartOf(8)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(179);

+			} else SynErr(178);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(60);

-		} else SynErr(180);

+		} else SynErr(179);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(60);

-		} else SynErr(181);

+		} else SynErr(180);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2435,7 +2444,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(182);

+		} else SynErr(181);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2469,7 +2478,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(183);

+		} else SynErr(182);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(184); break;

+		default: SynErr(183); break;

 		}

 	}

 

@@ -2565,24 +2574,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

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

 		Expression(out d);

-		Expect(55);

+		Expect(54);

 		Expression(out r);

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

 		while (la.kind == 21) {

 			Get();

 			Expression(out d);

-			Expect(55);

+			Expect(54);

 			Expression(out r);

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

 		}

 	}

 

 	void QSep() {

-		if (la.kind == 108) {

+		if (la.kind == 107) {

 			Get();

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

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

 			Get();

-		} else SynErr(185);

+		} else SynErr(184);

 	}

 

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

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

 		Expression/*!*/ body;

 		

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

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

 			Forall();

 			x = t;  univ = true; 

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

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

 			Exists();

 			x = t; 

-		} else SynErr(186);

+		} else SynErr(185);

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

 		QSep();

 		Expression(out body);

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

 		Expect(19);

 		Expression(out range);

-		if (la.kind == 108 || la.kind == 109) {

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

 			QSep();

 			Expression(out body);

 		}

@@ -2670,7 +2679,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out d);

 			letVars.Add(d); 

 		}

-		Expect(55);

+		Expect(54);

 		Expression(out e);

 		letRHSs.Add(e); 

 		while (la.kind == 21) {

@@ -2688,7 +2697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		Expression expr;

 		

-		Expect(102);

+		Expect(51);

 		x = t; 

 		NoUSIdent(out d);

 		Expect(5);

@@ -2723,19 +2732,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void Forall() {

-		if (la.kind == 104) {

+		if (la.kind == 103) {

 			Get();

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

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

 			Get();

-		} else SynErr(187);

+		} else SynErr(186);

 	}

 

 	void Exists() {

-		if (la.kind == 106) {

+		if (la.kind == 105) {

 			Get();

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

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

 			Get();

-		} else SynErr(188);

+		} else SynErr(187);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2771,26 +2780,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,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,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,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, 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,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},

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

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

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

 

 	};

 } // end Parser

@@ -2869,8 +2878,8 @@ public class Errors {
 			case 51: s = "\"label\" expected"; break;

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

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

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

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

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

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

 			case 56: s = "\":|\" expected"; break;

 			case 57: s = "\"assume\" expected"; break;

 			case 58: s = "\"new\" expected"; break;

@@ -2917,93 +2926,92 @@ public class Errors {
 			case 99: s = "\"allocated\" expected"; break;

 			case 100: s = "\"old\" expected"; break;

 			case 101: s = "\"then\" expected"; break;

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

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

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

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

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

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

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

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

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

-			case 111: s = "invalid Dafny"; 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 = "invalid SubModuleDecl"; break;

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

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

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

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

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

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

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

+			case 114: s = "this symbol not expected in DatatypeDecl"; 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 = "this symbol not expected in FieldDecl"; break;

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

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

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

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

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

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

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

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

 			case 127: s = "invalid MethodDecl"; break;

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

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

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

+			case 129: s = "this symbol not expected in 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 = "this symbol not expected in MethodSpec"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 			case 152: s = "invalid UpdateStmt"; break;

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

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

 			case 154: s = "invalid IfStmt"; break;

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

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

 			case 156: s = "invalid WhileStmt"; break;

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

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

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

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

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

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

+			case 159: s = "invalid Guard"; 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 LoopSpec"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 5ddc1fac..a5fab242 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -809,15 +809,15 @@ namespace Microsoft.Dafny {
 

       return nw;

     }

-    private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {

+    private Statement SubstituteNamedExpr(Statement s, Dictionary<string, Expression> sub, SortedSet<string> subs) {

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

+        return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);

       } else if (s is AssumeStmt) {

         AssumeStmt stmt = (AssumeStmt)s;

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

+        return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);

       } else if (s is PrintStmt) {

         throw new NotImplementedException();

       } else if (s is BreakStmt) {

@@ -833,16 +833,16 @@ namespace Microsoft.Dafny {
         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));

+          lhs.Add(SubstituteNamedExpr(l, sub, subs));

         }

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

+            rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, sub, subs)));

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

+            rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, sub, subs), rr.MethodName, SubstituteNamedExprList(rr.Args, sub, subs)));

           } else if (r is TypeRhs) {

             rhs.Add(r);

           } else {

@@ -862,19 +862,19 @@ namespace Microsoft.Dafny {
         BlockStmt stmt = (BlockStmt)s;

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

         foreach (Statement ss in stmt.Body) {

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

+          res.Add(SubstituteNamedExpr(ss, sub, subs));

         }

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

+        return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs),

+                         (BlockStmt)SubstituteNamedExpr(stmt.Thn, sub, subs),

+                                    SubstituteNamedExpr(stmt.Els, sub, subs));

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

+        return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, sub, subs));

       } else if (s is AlternativeLoopStmt) {

         return s;

       } else if (s is ParallelStmt) {

@@ -889,21 +889,22 @@ namespace Microsoft.Dafny {
       }

 

     }

-    private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) {

+    private Expression SubstituteNamedExpr(Expression expr, Dictionary<string, Expression> sub, SortedSet<string> subs) {

       if (expr == null) {

         return null;

       }

       if (expr is NamedExpr) {

         NamedExpr n = (NamedExpr)expr;

-        if (n.Name == p.val) {

-          subCount++;

-          return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p);

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

+        Expression E;

+        if (sub.TryGetValue(n.Name, out E)) {

+          subs.Add(n.Name);

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

+        } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, sub, subs));

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

+        List<Expression> newElements = SubstituteNamedExprList(e.Elements, sub, subs);

         if (expr is SetDisplayExpr) {

           return new SetDisplayExpr(expr.tok, newElements);

         } else if (expr is MultiSetDisplayExpr) {

@@ -913,65 +914,65 @@ namespace Microsoft.Dafny {
         }

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr fse = (FieldSelectExpr)expr;

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

+        Expression substE = SubstituteNamedExpr(fse.Obj, sub, subs);

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

+        Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);

+        Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, sub, subs);

+        Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, sub, subs);

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

+        Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);

+        Expression index = SubstituteNamedExpr(sse.Index, sub, subs);

+        Expression val = SubstituteNamedExpr(sse.Value, sub, subs);

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

+        Expression array = SubstituteNamedExpr(mse.Array, sub, subs);

+        List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, sub, subs);

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

+        Expression receiver = SubstituteNamedExpr(e.Receiver, sub, subs);

+        List<Expression> newArgs = SubstituteNamedExprList(e.Args, sub, subs);

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

+        List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, sub, subs);

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

+        Expression se = SubstituteNamedExpr(e.E, sub, subs);

         return new OldExpr(expr.tok, se);

       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

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

+        Expression se = SubstituteNamedExpr(e.E, sub, subs);

         return new FreshExpr(expr.tok, se);

       } else if (expr is AllocatedExpr) {

         AllocatedExpr e = (AllocatedExpr)expr;

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

+        Expression se = SubstituteNamedExpr(e.E, sub, subs);

         return new AllocatedExpr(expr.tok, se);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

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

+        Expression se = SubstituteNamedExpr(e.E, sub, subs);

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

+        Expression e0 = SubstituteNamedExpr(e.E0, sub, subs);

+        Expression e1 = SubstituteNamedExpr(e.E1, sub, subs);

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

+        var rhss = SubstituteNamedExprList(e.RHSs, sub, subs);

+        var body = SubstituteNamedExpr(e.Body, sub, subs);

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

+        Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, sub, subs);

+        Expression newTerm = SubstituteNamedExpr(e.Term, sub, subs);

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

         if (e is SetComprehension) {

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

         } else if (e is MapComprehension) {

@@ -990,8 +991,8 @@ namespace Microsoft.Dafny {
 

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

+        Expression g = SubstituteNamedExpr(e.Guard, sub, subs);

+        Expression b = SubstituteNamedExpr(e.Body, sub, subs);

         if (expr is AssertExpr) {

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

         } else {

@@ -999,21 +1000,21 @@ namespace Microsoft.Dafny {
         }

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

+        Expression test = SubstituteNamedExpr(e.Test, sub, subs);

+        Expression thn = SubstituteNamedExpr(e.Thn, sub, subs);

+        Expression els = SubstituteNamedExpr(e.Els, sub, subs);

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

+          return SubstituteNamedExpr(((ParensExpression)expr).E, sub, subs);

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

+          return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, sub, subs), edn.SuffixName);

         } else if (expr is ChainingExpression) {

           ChainingExpression ch = (ChainingExpression)expr;

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

+          return SubstituteNamedExpr(ch.E, sub, subs);

         } else {

           Contract.Assert(false);

           throw new cce.UnreachableException();

@@ -1024,10 +1025,10 @@ namespace Microsoft.Dafny {
       }

     }

 

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

+    private List<Expression> SubstituteNamedExprList(List<Expression> list, Dictionary<string, Expression> sub, SortedSet<string> subCount) {

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

       foreach (Expression e in list) {

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

+        res.Add(SubstituteNamedExpr(e, sub, subCount));

       }

       return res;

     }

@@ -1162,20 +1163,34 @@ namespace Microsoft.Dafny {
               if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {

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

               } else {

-                int subCount = 0;

+                SortedSet<string> substitutions = null;

+                Dictionary<string, Expression> subExprs = null;

+                if (c.NameReplacements != null) {

+                  subExprs = new Dictionary<string, Expression>();

+                  substitutions = new SortedSet<string>();

+                  Contract.Assert(c.NameReplacements.Count == c.ExprReplacements.Count);

+                  for (int k = 0; k < c.NameReplacements.Count; k++) {

+                    if (subExprs.ContainsKey(c.NameReplacements[k].val)) {

+                      reporter.Error(c.NameReplacements[k], "replacement definition must contain at most one definition for a given label");

+                    } else subExprs.Add(c.NameReplacements[k].val, c.ExprReplacements[k]);

+                  }

+                }

                 // 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], c.ExprReplacements[0], ref subCount);

+                  if (subExprs != null) 

+                    s = SubstituteNamedExpr(s, subExprs, substitutions);

                   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 labeled {0}", c.NameReplacements[0].val);

+                if (subExprs != null && substitutions.Count < subExprs.Count) {

+                  foreach (var s in substitutions)

+                    subExprs.Remove(s);

+                  reporter.Error(c.Tok, "could not find labeled expression(s): " + Util.Comma(", ", subExprs.Keys, x => x));

+                }

               }

               i++;

 

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 71210c9f..16804d8c 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -4421,8 +4421,9 @@ namespace Microsoft.Dafny {
           return;

         }

       } else if (expr is NamedExpr) {

-        if (moduleInfo.IsGhost) return;

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

+        if (!moduleInfo.IsGhost) 

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

+        return;

       }

 

       foreach (var ee in expr.SubExpressions) {

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 1bfa80a0..0433519d 100644
--- a/Dafny/Scanner.cs
+++ b/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 = 110;

-	const int noSym = 110;

+	const int maxT = 109;

+	const int noSym = 109;

 

 

 	[ContractInvariantMethod]

@@ -521,7 +521,7 @@ public class Scanner {
 			case "label": t.kind = 51; break;

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

 			case "where": t.kind = 53; break;

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

+			case "return": t.kind = 55; break;

 			case "assume": t.kind = 57; break;

 			case "new": t.kind = 58; break;

 			case "choose": t.kind = 61; break;

@@ -543,9 +543,8 @@ public class Scanner {
 			case "allocated": t.kind = 99; break;

 			case "old": t.kind = 100; break;

 			case "then": t.kind = 101; break;

-			case "expr": t.kind = 102; break;

-			case "forall": t.kind = 104; break;

-			case "exists": t.kind = 106; break;

+			case "forall": t.kind = 103; break;

+			case "exists": t.kind = 105; break;

 			default: break;

 		}

 	}

@@ -665,7 +664,7 @@ public class Scanner {
 			case 25:

 				{t.kind = 50; break;}

 			case 26:

-				{t.kind = 55; break;}

+				{t.kind = 54; break;}

 			case 27:

 				{t.kind = 56; break;}

 			case 28:

@@ -719,13 +718,13 @@ public class Scanner {
 			case 51:

 				{t.kind = 93; break;}

 			case 52:

-				{t.kind = 105; break;}

+				{t.kind = 104; break;}

 			case 53:

-				{t.kind = 107; break;}

+				{t.kind = 106; break;}

 			case 54:

-				{t.kind = 108; break;}

+				{t.kind = 107; break;}

 			case 55:

-				{t.kind = 109; break;}

+				{t.kind = 108; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 26;}

@@ -763,9 +762,9 @@ public class Scanner {
 				if (ch == '>') {AddCh(); goto case 34;}

 				else {t.kind = 24; break;}

 			case 64:

-				recEnd = pos; recKind = 103;

+				recEnd = pos; recKind = 102;

 				if (ch == '.') {AddCh(); goto case 23;}

-				else {t.kind = 103; break;}

+				else {t.kind = 102; break;}

 			case 65:

 				recEnd = pos; recKind = 80;

 				if (ch == '=') {AddCh(); goto case 31;}

diff --git a/Dafny/Util.cs b/Dafny/Util.cs
index e057727a..8db3ebc8 100644
--- a/Dafny/Util.cs
+++ b/Dafny/Util.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Dafny {
   class Util

   {

      public delegate string ToString<T>(T t);

-     public static string Comma<T>(string comma, List<T> l, ToString<T> f) {

+     public static string Comma<T>(string comma, IEnumerable<T> l, ToString<T> f) {

        string res = "";

        string c = "";

        foreach(var t in l) {