Merge

8 files changed, 673 insertions, 665 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index b49c011f..78ea8d3d 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -74,7 +74,10 @@ namespace Microsoft.Dafny {
         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

           wr.WriteLine();

-          if (d is DatatypeDecl) {

+          if (d is ArbitraryTypeDecl) {

+            var at = (ArbitraryTypeDecl)d;

+            Error("Arbitrary type ('{0}') cannot be compiled", at.Name);

+          } else if (d is DatatypeDecl) {

             DatatypeDecl dt = (DatatypeDecl)d;

             Indent(indent);

             wr.Write("public abstract class Base_{0}", dt.Name);

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 7019a22b..6b12a288 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -134,7 +134,7 @@ IGNORE cr + lf + tab
 /*------------------------------------------------------------------------*/

 PRODUCTIONS

 Dafny

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

      Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

      List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

      ModuleDecl module;

@@ -157,11 +157,13 @@ Dafny
     "{"                                  (. module.BodyStartTok = t; .)

       { ClassDecl<module, out c>         (. module.TopLevelDecls.Add(c); .)

       | DatatypeDecl<module, out dt>     (. module.TopLevelDecls.Add(dt); .)

+      | ArbitraryTypeDecl<module, out at>(. module.TopLevelDecls.Add(at); .)

       }

     "}"                                  (. module.BodyEndTok = t;

                                             theModules.Add(module); .)

-  | ClassDecl<defaultModule, out c>      (. defaultModule.TopLevelDecls.Add(c); .)

-  | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)

+  | ClassDecl<defaultModule, out c>           (. defaultModule.TopLevelDecls.Add(c); .)

+  | DatatypeDecl<defaultModule, out dt>       (. defaultModule.TopLevelDecls.Add(dt); .)

+  | ArbitraryTypeDecl<defaultModule, out at>  (. defaultModule.TopLevelDecls.Add(at); .)

   | ClassMemberDecl<membersDefaultClass, false>

   }

   (. if (defaultModuleCreatedHere) {

@@ -276,6 +278,14 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   SYNC ";"

   .

+ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>

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

+     Attributes attrs = null;

+  .)

+  "type"

+  { Attribute<ref attrs> }

+  Ident<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

+  .

 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Attributes attrs = null;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 99ebe8da..4faa85f2 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -169,7 +169,7 @@ namespace Microsoft.Dafny {
           return true;

         } else {

           UserDefinedType udt = this as UserDefinedType;

-          return udt != null && udt.ResolvedParam == null && !(udt.ResolvedClass is DatatypeDecl);

+          return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl;

         }

       }

     }

@@ -201,7 +201,6 @@ namespace Microsoft.Dafny {
     }

     public bool IsTypeParameter {

       get {

-        Contract.Ensures(!Contract.Result<bool>() || this is UserDefinedType && ((UserDefinedType)this).ResolvedParam != null);

         UserDefinedType ct = this as UserDefinedType;

         return ct != null && ct.ResolvedParam != null;

       }

@@ -601,7 +600,6 @@ namespace Microsoft.Dafny {
       : base(tok, name, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

-

     }

   }

 

@@ -653,7 +651,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(TypeArgs));

     }

 

-

     public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

@@ -920,6 +917,23 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType

+  {

+    public readonly TypeParameter TheType;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(TheType != null && Name == TheType.Name);

+    }

+

+    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes)

+      : base(tok, name, module, new List<TypeParameter>(), attributes) {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(module != null);

+      TheType = new TypeParameter(tok, name);

+    }

+  }

+

   [ContractClass(typeof(IVariableContracts))]

   public interface IVariable {

     string/*!*/ Name {

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index f723ad2c..d942582f 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -18,7 +18,7 @@ public class Parser {
 	public const int _digits = 2;

 	public const int _arrayToken = 3;

 	public const int _string = 4;

-	public const int maxT = 104;

+	public const int maxT = 105;

 

 	const bool T = true;

 	const bool x = false;

@@ -184,20 +184,20 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 

 

 	void Dafny() {

-		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

+		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

 		List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

 		ModuleDecl module;

 		// to support multiple files, create a default module only if theModules doesn't already contain one

 		DefaultModuleDecl defaultModule = null;

 		foreach (ModuleDecl mdecl in theModules) {

-		 defaultModule = mdecl as DefaultModuleDecl;

-		 if (defaultModule != null) { break; }

+		  defaultModule = mdecl as DefaultModuleDecl;

+		  if (defaultModule != null) { break; }

 		}

 		bool defaultModuleCreatedHere = false;

 		if (defaultModule == null) {

-		 defaultModuleCreatedHere = true;

-		 defaultModule = new DefaultModuleDecl();

+		  defaultModuleCreatedHere = true;

+		  defaultModule = new DefaultModuleDecl();

 		}

 		

 		while (StartOf(1)) {

@@ -215,13 +215,16 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 				module = new ModuleDecl(id, id.val, theImports, attrs); 

 				Expect(7);

 				module.BodyStartTok = t; 

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

+				while (la.kind == 9 || la.kind == 14 || la.kind == 20) {

 					if (la.kind == 9) {

 						ClassDecl(module, out c);

 						module.TopLevelDecls.Add(c); 

-					} else {

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

 						DatatypeDecl(module, out dt);

 						module.TopLevelDecls.Add(dt); 

+					} else {

+						ArbitraryTypeDecl(module, out at);

+						module.TopLevelDecls.Add(at); 

 					}

 				}

 				Expect(8);

@@ -233,6 +236,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			} else if (la.kind == 14) {

 				DatatypeDecl(defaultModule, out dt);

 				defaultModule.TopLevelDecls.Add(dt); 

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

+				ArbitraryTypeDecl(defaultModule, out at);

+				defaultModule.TopLevelDecls.Add(at); 

 			} else {

 				ClassMemberDecl(membersDefaultClass, false);

 			}

@@ -241,14 +247,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

 		 theModules.Add(defaultModule);

 		} else {

-		 // find the default class in the default module, then append membersDefaultClass to its member list

-		 foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-		   DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

-		   if (defaultClass != null) {

-		     defaultClass.Members.AddRange(membersDefaultClass);

-		     break;

-		   }

-		 }

+		  // find the default class in the default module, then append membersDefaultClass to its member list

+		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		    if (defaultClass != null) {

+		      defaultClass.Members.AddRange(membersDefaultClass);

+		      break;

+		    }

+		  }

 		}

 		

 		Expect(0);

@@ -288,13 +294,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

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

 		Expect(9);

 		while (la.kind == 7) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 24) {

 			GenericParameters(typeArgs);

 		}

 		if (la.kind == 10) {

@@ -311,7 +316,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (optionalId == null)

 		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

 		else

-		 c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+		  c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -326,13 +331,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		

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

 		Expect(14);

 		while (la.kind == 7) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 24) {

 			GenericParameters(typeArgs);

 		}

 		Expect(15);

@@ -342,7 +346,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

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

 		Expect(17);

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

 		dt.BodyStartTok = bodyStart;

@@ -350,6 +353,19 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		

 	}

 

+	void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) {

+		IToken/*!*/ id;

+		Attributes attrs = null;

+		

+		Expect(20);

+		while (la.kind == 7) {

+			Attribute(ref attrs);

+		}

+		Ident(out id);

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

+		Expect(17);

+	}

+

 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors) {

 		Contract.Requires(cce.NonNullElements(mm));

 		Method/*!*/ m;

@@ -370,21 +386,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 		if (la.kind == 18) {

 			FieldDecl(mmod, mm);

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

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

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 10 || la.kind == 25 || la.kind == 26) {

+		} else if (la.kind == 10 || la.kind == 26 || la.kind == 27) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

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

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

 			CouplingInvDecl(mmod, mm);

-		} else SynErr(108);

+		} else SynErr(106);

 	}

 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

 		Contract.Requires(cce.NonNullElements(typeArgs));

 		IToken/*!*/ id; 

-		Expect(23);

+		Expect(24);

 		Ident(out id);

 		typeArgs.Add(new TypeParameter(id, id.val)); 

 		while (la.kind == 19) {

@@ -392,7 +408,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Ident(out id);

 			typeArgs.Add(new TypeParameter(id, id.val)); 

 		}

-		Expect(24);

+		Expect(25);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -400,7 +416,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Attributes attrs = null;

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

 		

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

 		Expect(18);

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

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

@@ -415,7 +430,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			IdentType(out id, out ty);

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

 		}

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

 		Expect(17);

 	}

 

@@ -435,8 +449,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		Expect(42);

-		if (la.kind == 25) {

+		Expect(43);

+		if (la.kind == 26) {

 			Get();

 			isFunctionMethod = true; 

 		}

@@ -446,11 +460,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 24) {

 			GenericParameters(typeArgs);

 		}

 		Formals(true, isFunctionMethod, formals);

-		Expect(22);

+		Expect(23);

 		Type(out returnType);

 		while (StartOf(3)) {

 			FunctionSpec(reqs, reads, ens, decreases);

@@ -482,45 +496,44 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(StartOf(4))) {SynErr(111); Get();}

-		if (la.kind == 25) {

+		if (la.kind == 26) {

 			Get();

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

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

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			 SemErr(t, "constructors are only allowed in classes");

+			  SemErr(t, "constructors are only allowed in classes");

 			}

 			

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

 			Get();

 			isRefinement = true; 

-		} else SynErr(112);

+		} else SynErr(107);

 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

 		if (isConstructor) {

-		 if (mmod.IsGhost) {

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

-		 }

-		 if (mmod.IsStatic) {

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

-		 }

+		  if (mmod.IsGhost) {

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

+		  }

+		  if (mmod.IsStatic) {

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

+		  }

 		}

 		

 		while (la.kind == 7) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 24) {

 			GenericParameters(typeArgs);

 		}

 		Formals(true, !mmod.IsGhost, ins);

-		if (la.kind == 27) {

+		if (la.kind == 28) {

 			Get();

 			if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 			Formals(false, !mmod.IsGhost, outs);

 		}

-		while (StartOf(5)) {

+		while (StartOf(4)) {

 			MethodSpec(req, mod, ens, dec);

 		}

 		if (la.kind == 7) {

@@ -530,9 +543,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (isRefinement)

 		 m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		else if (isConstructor)

-		 m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

+		  m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

 		else

-		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+		  m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		m.BodyStartTok = bodyStart;

 		m.BodyEndTok = bodyEnd;

 		

@@ -545,7 +558,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken/*!*/ id;

 		Expression/*!*/ e;

 		

-		Expect(20);

+		Expect(21);

 		if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }

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

 		if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

@@ -560,7 +573,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Ident(out id);

 			ids.Add(id); 

 		}

-		Expect(21);

+		Expect(22);

 		Expression(out e);

 		Expect(17);

 		mm.Add(new CouplingInvariant(ids, e, attrs)); 

@@ -576,7 +589,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			FormalsOptionalIds(formals);

 		}

 		ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); 

@@ -584,8 +597,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 

 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

-		Expect(33);

-		if (StartOf(6)) {

+		Expect(34);

+		if (StartOf(5)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			while (la.kind == 19) {

@@ -594,13 +607,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 				formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			}

 		}

-		Expect(34);

+		Expect(35);

 	}

 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

 		Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

 		Ident(out id);

-		Expect(22);

+		Expect(23);

 		Type(out ty);

 	}

 

@@ -628,7 +641,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

 		

 		Ident(out id);

-		if (la.kind == 22) {

+		if (la.kind == 23) {

 			Get();

 			Type(out ty);

 			optType = ty; 

@@ -640,7 +653,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

 		

 		Ident(out id);

-		if (la.kind == 22) {

+		if (la.kind == 23) {

 			Get();

 			Type(out ty);

 			optType = ty; 

@@ -658,13 +671,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			isGhost = true; 

 		}

 		TypeAndToken(out id, out ty);

-		if (la.kind == 22) {

+		if (la.kind == 23) {

 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

 			if (udt != null && udt.TypeArgs.Count == 0) {

-			 name = udt.Name;

+			  name = udt.Name;

 			} else {

-			 SemErr(id, "invalid formal-parameter name in datatype constructor");

+			  SemErr(id, "invalid formal-parameter name in datatype constructor");

 			}

 			

 			Type(out ty);

@@ -672,7 +685,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (name != null) {

 		 identName = name;

 		} else {

-		 identName = "#" + anonymousIds++;

+		  identName = "#" + anonymousIds++;

 		}

 		

 	}

@@ -682,22 +695,22 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 35: {

+		case 36: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 36: {

+		case 37: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 37: {

+		case 38: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 38: {

+		case 39: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -708,7 +721,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			

 			break;

 		}

-		case 39: {

+		case 40: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -719,7 +732,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			

 			break;

 		}

-		case 40: {

+		case 41: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -730,17 +743,17 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			

 			break;

 		}

-		case 1: case 3: case 41: {

+		case 1: case 3: case 42: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(113); break;

+		default: SynErr(108); break;

 		}

 	}

 

 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

-		Expect(33);

+		Expect(34);

 		if (la.kind == 1 || la.kind == 11) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

@@ -750,7 +763,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}

-		Expect(34);

+		Expect(35);

 	}

 

 	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

@@ -758,10 +771,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		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;

 		

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

-		if (la.kind == 28) {

+		if (la.kind == 29) {

 			Get();

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

 				while (la.kind == 19) {

@@ -770,32 +782,28 @@ List<Expression/*!*/>/*!*/ decreases) {
 					mod.Add(fe); 

 				}

 			}

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

 			Expect(17);

-		} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {

-			if (la.kind == 29) {

+		} else if (la.kind == 30 || la.kind == 31 || la.kind == 32) {

+			if (la.kind == 30) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 30) {

+			if (la.kind == 31) {

 				Get();

 				Expression(out e);

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

 				Expect(17);

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

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

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

 				Get();

 				Expression(out e);

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

 				Expect(17);

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

-			} else SynErr(118);

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

+			} else SynErr(109);

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

 			Get();

 			DecreasesList(decreases, false);

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

 			Expect(17);

-		} else SynErr(120);

+		} else SynErr(110);

 	}

 

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

@@ -804,7 +812,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Expect(7);

 		bodyStart = t; 

-		while (StartOf(9)) {

+		while (StartOf(7)) {

 			Stmt(body);

 		}

 		Expect(8);

@@ -815,7 +823,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void FrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; 

 		Expression(out e);

-		if (la.kind == 45) {

+		if (la.kind == 46) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -829,7 +837,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (!allowWildcard && e is WildcardExpr) {

 		 SemErr(e.tok, "'decreases *' is only allowed on loops");

 		} else {

-		 decreases.Add(e);

+		  decreases.Add(e);

 		}

 		

 		while (la.kind == 19) {

@@ -838,7 +846,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (!allowWildcard && e is WildcardExpr) {

 			 SemErr(e.tok, "'decreases *' is only allowed on loops");

 			} else {

-			 decreases.Add(e);

+			  decreases.Add(e);

 			}

 			

 		}

@@ -846,7 +854,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(23);

+		Expect(24);

 		Type(out ty);

 		gt.Add(ty); 

 		while (la.kind == 19) {

@@ -854,7 +862,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(24);

+		Expect(25);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -862,7 +870,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type/*!*/>/*!*/ gt;

 		

-		if (la.kind == 41) {

+		if (la.kind == 42) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

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

@@ -874,33 +882,31 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}

 			int dims = 1;

 			if (tok.val.Length != 5) {

-			 dims = int.Parse(tok.val.Substring(5));

+			  dims = int.Parse(tok.val.Substring(5));

 			}

 			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

 			

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

 			Ident(out tok);

 			gt = new List<Type/*!*/>(); 

-			if (la.kind == 23) {

+			if (la.kind == 24) {

 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(121);

+		} else SynErr(111);

 	}

 

 	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 == 30) {

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

+		if (la.kind == 31) {

 			Get();

 			Expression(out e);

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

 			Expect(17);

 			reqs.Add(e); 

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

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

 			Get();

-			if (StartOf(10)) {

+			if (StartOf(8)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

 				while (la.kind == 19) {

@@ -909,20 +915,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 					reads.Add(fe); 

 				}

 			}

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

 			Expect(17);

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

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

 			Get();

 			Expression(out e);

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

 			Expect(17);

 			ens.Add(e); 

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

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

 			Get();

 			DecreasesList(decreases, false);

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

 			Expect(17);

-		} else SynErr(127);

+		} else SynErr(112);

 	}

 

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

@@ -936,23 +939,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

-		if (la.kind == 44) {

+		if (la.kind == 45) {

 			Get();

 			fe = new FrameExpression(new WildcardExpr(t), null); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(6)) {

 			FrameExpression(out fe);

-		} else SynErr(128);

+		} else SynErr(113);

 	}

 

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

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

 		e = dummyExpr; 

-		if (la.kind == 44) {

+		if (la.kind == 45) {

 			Get();

 			e = new WildcardExpr(t); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(6)) {

 			Expression(out e);

-		} else SynErr(129);

+		} else SynErr(114);

 	}

 

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

@@ -968,25 +971,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

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

 		switch (la.kind) {

 		case 7: {

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

 			break;

 		}

-		case 62: {

+		case 63: {

 			AssertStmt(out s);

 			break;

 		}

-		case 63: {

+		case 64: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 64: {

+		case 65: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {

+		case 1: case 2: case 16: case 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -994,59 +996,58 @@ List<Expression/*!*/>/*!*/ decreases) {
 			VarDeclStatement(out s);

 			break;

 		}

-		case 55: {

+		case 56: {

 			IfStmt(out s);

 			break;

 		}

-		case 59: {

+		case 60: {

 			WhileStmt(out s);

 			break;

 		}

-		case 61: {

+		case 62: {

 			MatchStmt(out s);

 			break;

 		}

-		case 65: {

+		case 66: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 46: {

+		case 47: {

 			Get();

 			x = t; 

 			Ident(out id);

-			Expect(22);

+			Expect(23);

 			OneStmt(out s);

 			s.Labels = new LabelNode(x, id.val, s.Labels); 

 			break;

 		}

-		case 47: {

+		case 48: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			} else if (la.kind == 17 || la.kind == 47) {

-				while (la.kind == 47) {

+			} else if (la.kind == 17 || la.kind == 48) {

+				while (la.kind == 48) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(131);

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

+			} else SynErr(115);

 			Expect(17);

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

 			break;

 		}

-		case 48: {

+		case 49: {

 			ReturnStmt(out s);

 			break;

 		}

-		default: SynErr(133); break;

+		default: SynErr(116); break;

 		}

 	}

 

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

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

-		Expect(62);

+		Expect(63);

 		x = t; 

 		Expression(out e);

 		Expect(17);

@@ -1055,7 +1056,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 

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

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

-		Expect(63);

+		Expect(64);

 		x = t; 

 		Expression(out e);

 		Expect(17);

@@ -1066,7 +1067,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

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

 		

-		Expect(64);

+		Expect(65);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1091,14 +1092,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 17) {

 			Get();

 			rhss.Add(new ExprRhs(e)); 

-		} else if (la.kind == 19 || la.kind == 49) {

+		} else if (la.kind == 19 || la.kind == 50) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 19) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			Expect(49);

+			Expect(50);

 			x = t; 

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

@@ -1108,10 +1109,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 				rhss.Add(r); 

 			}

 			Expect(17);

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

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

 			Get();

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

-		} else SynErr(134);

+		} else SynErr(117);

 		s = new UpdateStmt(x, lhss, rhss); 

 	}

 

@@ -1135,7 +1136,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 49) {

+		if (la.kind == 50) {

 			Get();

 			assignTok = t;

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

@@ -1152,13 +1153,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(17);

 		UpdateStmt update;

 		if (rhss.Count == 0) {

-		 update = null;

+		  update = null;

 		} else {

-		 var ies = new List<Expression>();

-		 foreach (var lhs in lhss) {

-		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

-		 }

-		 update = new UpdateStmt(assignTok, ies, rhss);

+		  var ies = new List<Expression>();

+		  foreach (var lhs in lhss) {

+		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

+		  }

+		  update = new UpdateStmt(assignTok, ies, rhss);

 		}

 		s = new VarDeclStmt(x, lhss, update);

 		

@@ -1174,26 +1175,26 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(55);

+		Expect(56);

 		x = t; 

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			Guard(out guard);

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

-			if (la.kind == 56) {

+			if (la.kind == 57) {

 				Get();

-				if (la.kind == 55) {

+				if (la.kind == 56) {

 					IfStmt(out s);

 					els = s; 

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

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

 					els = s; 

-				} else SynErr(135);

+				} else SynErr(118);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(136);

+		} else SynErr(119);

 	}

 

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

@@ -1207,30 +1208,30 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(59);

+		Expect(60);

 		x = t; 

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			Guard(out guard);

 			Contract.Assume(guard == null || cce.Owner.None(guard)); 

 			LoopSpec(out invariants, out decreases, out mod);

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

 			stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); 

-		} else if (StartOf(12)) {

+		} else if (StartOf(9)) {

 			LoopSpec(out invariants, out decreases, out mod);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); 

-		} else SynErr(137);

+		} else SynErr(120);

 	}

 

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

+		Expect(62);

 		x = t; 

 		Expression(out e);

 		Expect(7);

-		while (la.kind == 57) {

+		while (la.kind == 58) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1250,19 +1251,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Statement/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(65);

+		Expect(66);

 		x = t; 

-		Expect(33);

+		Expect(34);

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

 		if (range == null) { range = new LiteralExpr(x, true); } 

-		Expect(34);

-		while (la.kind == 29 || la.kind == 31) {

+		Expect(35);

+		while (la.kind == 30 || la.kind == 32) {

 			isFree = false; 

-			if (la.kind == 29) {

+			if (la.kind == 30) {

 				Get();

 				isFree = true; 

 			}

-			Expect(31);

+			Expect(32);

 			Expression(out e);

 			Expect(17);

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

@@ -1276,9 +1277,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

 		

-		Expect(48);

+		Expect(49);

 		returnTok = t; 

-		if (StartOf(13)) {

+		if (StartOf(10)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 19) {

@@ -1299,27 +1300,27 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> args;

 		r = null;  // to please compiler

 		

-		if (la.kind == 50) {

+		if (la.kind == 51) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

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

-				if (la.kind == 51) {

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

+				if (la.kind == 52) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(52);

+					Expect(53);

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

 					

 				} else {

 					Get();

 					Ident(out x);

-					Expect(33);

+					Expect(34);

 					args = new List<Expression/*!*/>(); 

-					if (StartOf(8)) {

+					if (StartOf(6)) {

 						Expressions(args);

 					}

-					Expect(34);

+					Expect(35);

 					initCall = new CallStmt(x, new List<Expression>(),

 					                       receiverForInitCall, x.val, args); 

 				}

@@ -1327,21 +1328,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (ee != null) {

 			 r = new TypeRhs(newToken, ty, ee);

 			} else {

-			 r = new TypeRhs(newToken, ty, initCall);

+			  r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 

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

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

 			Get();

 			r = new HavocRhs(t); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(6)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(138);

+		} else SynErr(121);

 	}

 

 	void Lhs(out Expression e) {

@@ -1349,16 +1350,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 51 || la.kind == 53) {

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(14)) {

+		} else if (StartOf(11)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 51 || la.kind == 53) {

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(139);

+		} else SynErr(122);

 	}

 

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

@@ -1374,15 +1375,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

-		Expect(33);

-		if (la.kind == 44) {

+		Expect(34);

+		if (la.kind == 45) {

 			Get();

 			e = null; 

-		} else if (StartOf(8)) {

+		} else if (StartOf(6)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(140);

-		Expect(34);

+		} else SynErr(123);

+		Expect(35);

 	}

 

 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {

@@ -1392,13 +1393,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Statement> body;

 		

 		Expect(7);

-		while (la.kind == 57) {

+		while (la.kind == 58) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(58);

+			Expect(59);

 			body = new List<Statement>(); 

-			while (StartOf(9)) {

+			while (StartOf(7)) {

 				Stmt(body);

 			}

 			alternatives.Add(new GuardedAlternative(x, e, body)); 

@@ -1407,29 +1408,30 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {

-		FrameExpression/*!*/ fe;

+		bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

 		invariants = new List<MaybeFreeExpression/*!*/>();

-		MaybeFreeExpression invariant = null;

 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(15)) {

-			if (la.kind == 29 || la.kind == 60) {

-				Invariant(out invariant);

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

+		while (StartOf(12)) {

+			if (la.kind == 30 || la.kind == 61) {

+				isFree = false; 

+				if (la.kind == 30) {

+					Get();

+					isFree = true; 

+				}

+				Expect(61);

+				Expression(out e);

+				invariants.Add(new MaybeFreeExpression(e, isFree)); 

 				Expect(17);

-				invariants.Add(invariant); 

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

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

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

 				Get();

 				DecreasesList(decreases, true);

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

 				Expect(17);

 			} else {

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

 				Get();

 				mod = mod ?? new List<FrameExpression>(); 

-				if (StartOf(8)) {

+				if (StartOf(6)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

 					while (la.kind == 19) {

@@ -1438,24 +1440,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 						mod.Add(fe); 

 					}

 				}

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

 				Expect(17);

 			}

 		}

 	}

 

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

-		bool isFree = false; Expression/*!*/ e; invariant = null; 

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

-		if (la.kind == 29) {

-			Get();

-			isFree = true; 

-		}

-		Expect(60);

-		Expression(out e);

-		invariant = new MaybeFreeExpression(e, isFree); 

-	}

-

 	void CaseStatement(out MatchCaseStmt/*!*/ c) {

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

 		IToken/*!*/ x, id;

@@ -1463,10 +1452,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		BoundVar/*!*/ bv;

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

 		

-		Expect(57);

+		Expect(58);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -1475,10 +1464,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(34);

+			Expect(35);

 		}

-		Expect(58);

-		while (StartOf(9)) {

+		Expect(59);

+		while (StartOf(7)) {

 			Stmt(body);

 		}

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

@@ -1489,10 +1478,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 4) {

 			Get();

 			arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(6)) {

 			Expression(out e);

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

-		} else SynErr(147);

+		} else SynErr(124);

 	}

 

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

@@ -1520,7 +1509,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void EquivExpression(out Expression/*!*/ e0) {

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

 		ImpliesExpression(out e0);

-		while (la.kind == 66 || la.kind == 67) {

+		while (la.kind == 67 || la.kind == 68) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1531,7 +1520,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void ImpliesExpression(out Expression/*!*/ e0) {

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

 		LogicalExpression(out e0);

-		if (la.kind == 68 || la.kind == 69) {

+		if (la.kind == 69 || la.kind == 70) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1540,23 +1529,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void EquivOp() {

-		if (la.kind == 66) {

+		if (la.kind == 67) {

 			Get();

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

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

 			Get();

-		} else SynErr(148);

+		} else SynErr(125);

 	}

 

 	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 == 70 || la.kind == 71) {

+		if (StartOf(13)) {

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

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

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

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

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

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1567,7 +1556,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				x = t; 

 				RelationalExpression(out e1);

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

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

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

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1578,11 +1567,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 68) {

+		if (la.kind == 69) {

 			Get();

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

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

 			Get();

-		} else SynErr(149);

+		} else SynErr(126);

 	}

 

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

@@ -1591,23 +1580,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> chain = null;

 		List<BinaryExpr.Opcode> ops = null;

 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

-		              // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

-		              // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

-		              // 3 ("illegal")     indicates illegal chain

-		              // 4 ("disjoint")    indicates chain of disjoint set operators

+		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

+		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

+		               // 3 ("illegal")     indicates illegal chain

+		               // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(17)) {

+		if (StartOf(14)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

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

 			if (op == BinaryExpr.Opcode.Disjoint)

-			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

-			while (StartOf(17)) {

+			while (StartOf(14)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -1661,11 +1650,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

 				if (op == BinaryExpr.Opcode.Disjoint) {

-				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

-				 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

 				}

 				else

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

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

 				

 			}

 		}

@@ -1676,25 +1665,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void AndOp() {

-		if (la.kind == 70) {

+		if (la.kind == 71) {

 			Get();

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

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

 			Get();

-		} else SynErr(150);

+		} else SynErr(127);

 	}

 

 	void OrOp() {

-		if (la.kind == 72) {

+		if (la.kind == 73) {

 			Get();

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

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

 			Get();

-		} else SynErr(151);

+		} else SynErr(128);

 	}

 

 	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 == 84 || la.kind == 85) {

+		while (la.kind == 85 || la.kind == 86) {

 			AddOp(out x, out op);

 			Factor(out e1);

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

@@ -1707,87 +1696,87 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken y;

 		

 		switch (la.kind) {

-		case 74: {

+		case 75: {

 			Get();

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

 			break;

 		}

-		case 23: {

+		case 24: {

 			Get();

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

 			break;

 		}

-		case 24: {

+		case 25: {

 			Get();

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

 			break;

 		}

-		case 75: {

+		case 76: {

 			Get();

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

 			break;

 		}

-		case 76: {

+		case 77: {

 			Get();

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

 			break;

 		}

-		case 77: {

+		case 78: {

 			Get();

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

 			break;

 		}

-		case 78: {

+		case 79: {

 			Get();

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

 			break;

 		}

-		case 79: {

+		case 80: {

 			Get();

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

 			break;

 		}

-		case 80: {

+		case 81: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 79) {

+			if (la.kind == 80) {

 				Get();

 				y = t; 

 			}

 			if (y == Token.NoToken) {

 			 SemErr(x, "invalid RelOp");

 			} else if (y.pos != x.pos + 1) {

-			 SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

+			  SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

 			} else {

-			 x.val = "!in";

-			 op = BinaryExpr.Opcode.NotIn;

+			  x.val = "!in";

+			  op = BinaryExpr.Opcode.NotIn;

 			}

 			

 			break;

 		}

-		case 81: {

+		case 82: {

 			Get();

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

 			break;

 		}

-		case 82: {

+		case 83: {

 			Get();

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

 			break;

 		}

-		case 83: {

+		case 84: {

 			Get();

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

 			break;

 		}

-		default: SynErr(152); break;

+		default: SynErr(129); 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 == 44 || la.kind == 86 || la.kind == 87) {

+		while (la.kind == 45 || la.kind == 87 || la.kind == 88) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

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

@@ -1796,82 +1785,82 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	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 == 84) {

+		if (la.kind == 85) {

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(153);

+		} else SynErr(130);

 	}

 

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

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

 		switch (la.kind) {

-		case 85: {

+		case 86: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

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

 			break;

 		}

-		case 80: case 88: {

+		case 81: case 89: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

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

 			break;

 		}

-		case 18: case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {

+		case 18: case 39: case 56: case 62: case 63: case 64: case 99: case 100: case 101: case 102: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 51 || la.kind == 53) {

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 7: case 51: {

+		case 7: case 52: {

 			DisplayExpr(out e);

 			break;

 		}

-		case 39: {

+		case 40: {

 			MultiSetExpr(out e);

 			break;

 		}

-		case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {

+		case 2: case 16: case 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {

 			ConstAtomExpression(out e);

-			while (la.kind == 51 || la.kind == 53) {

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(154); break;

+		default: SynErr(131); break;

 		}

 	}

 

 	void MulOp(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 == 44) {

+		if (la.kind == 45) {

 			Get();

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

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

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

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(155);

+		} else SynErr(132);

 	}

 

 	void NegOp() {

-		if (la.kind == 80) {

+		if (la.kind == 81) {

 			Get();

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

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

 			Get();

-		} else SynErr(156);

+		} else SynErr(133);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1882,30 +1871,30 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 55: {

+		case 56: {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(96);

+			Expect(97);

 			Expression(out e0);

-			Expect(56);

+			Expect(57);

 			Expression(out e1);

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

 			break;

 		}

-		case 61: {

+		case 62: {

 			MatchExpression(out e);

 			break;

 		}

-		case 98: case 99: case 100: case 101: {

+		case 99: case 100: case 101: case 102: {

 			QuantifierGuts(out e);

 			break;

 		}

-		case 38: {

+		case 39: {

 			ComprehensionExpr(out e);

 			break;

 		}

-		case 62: {

+		case 63: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -1914,7 +1903,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 63: {

+		case 64: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -1935,7 +1924,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				IdentTypeOptional(out d);

 				letVars.Add(d); 

 			}

-			Expect(49);

+			Expect(50);

 			Expression(out e);

 			letRHSs.Add(e); 

 			while (la.kind == 19) {

@@ -1948,7 +1937,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(157); break;

+		default: SynErr(134); break;

 		}

 	}

 

@@ -1959,18 +1948,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 53) {

+		while (la.kind == 54) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

 		}

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				Expressions(args);

 			}

-			Expect(34);

+			Expect(35);

 		}

 		e = new IdentifierSequence(idents, openParen, args); 

 	}

@@ -1981,37 +1970,37 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 53) {

+		if (la.kind == 54) {

 			Get();

 			Ident(out id);

-			if (la.kind == 33) {

+			if (la.kind == 34) {

 				Get();

 				args = new List<Expression/*!*/>();  func = true; 

-				if (StartOf(8)) {

+				if (StartOf(6)) {

 					Expressions(args);

 				}

-				Expect(34);

+				Expect(35);

 				e = new FunctionCallExpr(id, id.val, e, args); 

 			}

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

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

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

 			Get();

 			x = t; 

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 97) {

+				if (la.kind == 98) {

 					Get();

 					anyDots = true; 

-					if (StartOf(8)) {

+					if (StartOf(6)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 19 || la.kind == 52) {

+				} else if (la.kind == 19 || la.kind == 53) {

 					while (la.kind == 19) {

 						Get();

 						Expression(out ee);

@@ -2022,39 +2011,39 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(158);

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

+				} else SynErr(135);

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

 				Get();

 				anyDots = true; 

-				if (StartOf(8)) {

+				if (StartOf(6)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(159);

+			} else SynErr(136);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			} else {

-			 if (!anyDots && e0 == null) {

-			   /* a parsing error occurred */

-			   e0 = dummyExpr;

-			 }

-			 Contract.Assert(anyDots || e0 != null);

-			 if (anyDots) {

-			   //Contract.Assert(e0 != null || e1 != null);

-			   e = new SeqSelectExpr(x, false, e, e0, e1);

-			 } else if (e1 == null) {

-			   Contract.Assert(e0 != null);

-			   e = new SeqSelectExpr(x, true, e, e0, null);

-			 } else {

-			   Contract.Assert(e0 != null);

-			   e = new SeqUpdateExpr(x, e, e0, e1);

-			 }

+			  if (!anyDots && e0 == null) {

+			    /* a parsing error occurred */

+			    e0 = dummyExpr;

+			  }

+			  Contract.Assert(anyDots || e0 != null);

+			  if (anyDots) {

+			    //Contract.Assert(e0 != null || e1 != null);

+			    e = new SeqSelectExpr(x, false, e, e0, e1);

+			  } else if (e1 == null) {

+			    Contract.Assert(e0 != null);

+			    e = new SeqSelectExpr(x, true, e, e0, null);

+			  } else {

+			    Contract.Assert(e0 != null);

+			    e = new SeqUpdateExpr(x, e, e0, e1);

+			  }

 			}

 			

-			Expect(52);

-		} else SynErr(160);

+			Expect(53);

+		} else SynErr(137);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2065,20 +2054,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 7) {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(8);

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

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

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(52);

-		} else SynErr(161);

+			Expect(53);

+		} else SynErr(138);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2086,25 +2075,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(39);

+		Expect(40);

 		x = t; 

 		if (la.kind == 7) {

 			Get();

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

-			if (StartOf(8)) {

+			if (StartOf(6)) {

 				Expressions(elements);

 			}

 			e = new MultiSetDisplayExpr(x, elements);

 			Expect(8);

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

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

 			Get();

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

 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

-			Expect(34);

-		} else if (StartOf(18)) {

+			Expect(35);

+		} else if (StartOf(15)) {

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

-		} else SynErr(162);

+		} else SynErr(139);

 	}

 

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

@@ -2113,17 +2102,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 89: {

+		case 90: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 90: {

+		case 91: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 91: {

+		case 92: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2133,35 +2122,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 92: {

+		case 93: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 93: {

+		case 94: {

 			Get();

 			x = t; 

-			Expect(33);

-			Expression(out e);

 			Expect(34);

+			Expression(out e);

+			Expect(35);

 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 94: {

+		case 95: {

 			Get();

 			x = t; 

-			Expect(33);

-			Expression(out e);

 			Expect(34);

+			Expression(out e);

+			Expect(35);

 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 95: {

+		case 96: {

 			Get();

 			x = t; 

-			Expect(33);

-			Expression(out e);

 			Expect(34);

+			Expression(out e);

+			Expect(35);

 			e = new OldExpr(x, e); 

 			break;

 		}

@@ -2173,15 +2162,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(16);

 			break;

 		}

-		case 33: {

+		case 34: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new ParensExpression(x, e); 

-			Expect(34);

+			Expect(35);

 			break;

 		}

-		default: SynErr(163); break;

+		default: SynErr(140); break;

 		}

 	}

 

@@ -2190,8 +2179,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		try {

 		 n = BigInteger.Parse(t.val);

 		} catch (System.FormatException) {

-		 SemErr("incorrectly formatted number");

-		 n = BigInteger.Zero;

+		  SemErr("incorrectly formatted number");

+		  n = BigInteger.Zero;

 		}

 		

 	}

@@ -2200,10 +2189,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

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

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 57) {

+		while (la.kind == 58) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2218,20 +2207,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 98 || la.kind == 99) {

+		if (la.kind == 99 || la.kind == 100) {

 			Forall();

 			x = t;  univ = true; 

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

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

 			Exists();

 			x = t; 

-		} else SynErr(164);

+		} else SynErr(141);

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

 		QSep();

 		Expression(out body);

 		if (univ) {

 		 q = new ForallExpr(x, bvars, range, body, attrs);

 		} else {

-		 q = new ExistsExpr(x, bvars, range, body, attrs);

+		  q = new ExistsExpr(x, bvars, range, body, attrs);

 		}

 		

 	}

@@ -2244,7 +2233,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(38);

+		Expect(39);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

@@ -2255,7 +2244,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}

 		Expect(16);

 		Expression(out range);

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

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

 			QSep();

 			Expression(out body);

 		}

@@ -2270,10 +2259,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(57);

+		Expect(58);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 34) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -2282,35 +2271,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(34);

+			Expect(35);

 		}

-		Expect(58);

+		Expect(59);

 		Expression(out body);

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

 	}

 

 	void Forall() {

-		if (la.kind == 98) {

+		if (la.kind == 99) {

 			Get();

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

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

 			Get();

-		} else SynErr(165);

+		} else SynErr(142);

 	}

 

 	void Exists() {

-		if (la.kind == 100) {

+		if (la.kind == 101) {

 			Get();

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

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

 			Get();

-		} else SynErr(166);

+		} else SynErr(143);

 	}

 

 	void QSep() {

-		if (la.kind == 102) {

+		if (la.kind == 103) {

 			Get();

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

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

 			Get();

-		} else SynErr(167);

+		} else SynErr(144);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2318,10 +2307,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();

 		Attributes.Argument/*!*/ aArg;

 		

-		Expect(22);

+		Expect(23);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(19)) {

+		if (StartOf(16)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 19) {

@@ -2340,32 +2329,28 @@ List<Expression/*!*/>/*!*/ decreases) {
 		la.val = "";

 		Get();

 		Dafny();

-		Expect(0);

 

 		Expect(0);

 	}

 

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

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

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

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

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

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

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

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

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

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

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

@@ -2410,154 +2395,131 @@ public class Errors {
 			case 17: s = "\";\" expected"; break;

 			case 18: s = "\"var\" expected"; break;

 			case 19: s = "\",\" expected"; break;

-			case 20: s = "\"replaces\" expected"; break;

-			case 21: s = "\"by\" expected"; break;

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

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

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

-			case 25: s = "\"method\" expected"; break;

-			case 26: s = "\"constructor\" expected"; break;

-			case 27: s = "\"returns\" expected"; break;

-			case 28: s = "\"modifies\" expected"; break;

-			case 29: s = "\"free\" expected"; break;

-			case 30: s = "\"requires\" expected"; break;

-			case 31: s = "\"ensures\" expected"; break;

-			case 32: s = "\"decreases\" expected"; break;

-			case 33: s = "\"(\" expected"; break;

-			case 34: s = "\")\" expected"; break;

-			case 35: s = "\"bool\" expected"; break;

-			case 36: s = "\"nat\" expected"; break;

-			case 37: s = "\"int\" expected"; break;

-			case 38: s = "\"set\" expected"; break;

-			case 39: s = "\"multiset\" expected"; break;

-			case 40: s = "\"seq\" expected"; break;

-			case 41: s = "\"object\" expected"; break;

-			case 42: s = "\"function\" expected"; break;

-			case 43: s = "\"reads\" expected"; break;

-			case 44: s = "\"*\" expected"; break;

-			case 45: s = "\"`\" expected"; break;

-			case 46: s = "\"label\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+			case 20: s = "\"type\" expected"; break;

+			case 21: s = "\"replaces\" expected"; break;

+			case 22: s = "\"by\" expected"; break;

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

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

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

+			case 26: s = "\"method\" expected"; break;

+			case 27: s = "\"constructor\" expected"; break;

+			case 28: s = "\"returns\" expected"; break;

+			case 29: s = "\"modifies\" expected"; break;

+			case 30: s = "\"free\" expected"; break;

+			case 31: s = "\"requires\" expected"; break;

+			case 32: s = "\"ensures\" expected"; break;

+			case 33: s = "\"decreases\" expected"; break;

+			case 34: s = "\"(\" expected"; break;

+			case 35: s = "\")\" expected"; break;

+			case 36: s = "\"bool\" expected"; break;

+			case 37: s = "\"nat\" expected"; break;

+			case 38: s = "\"int\" expected"; break;

+			case 39: s = "\"set\" expected"; break;

+			case 40: s = "\"multiset\" expected"; break;

+			case 41: s = "\"seq\" expected"; break;

+			case 42: s = "\"object\" expected"; break;

+			case 43: s = "\"function\" expected"; break;

+			case 44: s = "\"reads\" expected"; break;

+			case 45: s = "\"*\" expected"; break;

+			case 46: s = "\"`\" expected"; break;

+			case 47: s = "\"label\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

@@ -2587,5 +2549,4 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}

 }

 

-

 }
\ No newline at end of file
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 5b9ba1d6..9f012509 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -62,7 +62,13 @@ namespace Microsoft.Dafny {
       int i = 0;

       foreach (TopLevelDecl d in classes) {

         Contract.Assert(d != null);

-        if (d is DatatypeDecl) {

+        if (d is ArbitraryTypeDecl) {

+          var at = (ArbitraryTypeDecl)d;

+          if (i++ != 0) { wr.WriteLine(); }

+          Indent(indent);

+          PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

+          wr.WriteLine(";");

+        } else if (d is DatatypeDecl) {

           if (i++ != 0) { wr.WriteLine(); }

           PrintDatatype((DatatypeDecl)d, indent);

         } else {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 55c2f48b..f54c633b 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -195,7 +195,10 @@ namespace Microsoft.Dafny {
           classes.Add(d.Name, d);

         }

 

-        if (d is ClassDecl) {

+        if (d is ArbitraryTypeDecl) {

+          // nothing more to register

+

+        } else if (d is ClassDecl) {

           ClassDecl cl = (ClassDecl)d;

 

           // register the names of the class members

@@ -293,7 +296,9 @@ namespace Microsoft.Dafny {
         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, true, d);

-        if (d is ClassDecl) {

+        if (d is ArbitraryTypeDecl) {

+          // nothing to do

+        } else if (d is ClassDecl) {

           ResolveClassMemberTypes((ClassDecl)d);

         } else {

           ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);

@@ -309,7 +314,9 @@ namespace Microsoft.Dafny {
         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, false, d);

-        if (d is ClassDecl) {

+        if (d is ArbitraryTypeDecl) {

+          // nothing to do

+        } else if (d is ClassDecl) {

           ResolveClassMemberBodies((ClassDecl)d);

         } else {

           DatatypeDecl dtd = (DatatypeDecl)d;

@@ -872,10 +879,12 @@ namespace Microsoft.Dafny {
           TopLevelDecl d;

           if (!classes.TryGetValue(t.Name, out d)) {

             Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name);

-          } else if (cce.NonNull(d).TypeArgs.Count == t.TypeArgs.Count) {

-            t.ResolvedClass = d;

-          } else {

+          } else if (d.TypeArgs.Count != t.TypeArgs.Count) {

             Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

+          } else if (d is ArbitraryTypeDecl) {

+            t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve as type parameter

+          } else {

+            t.ResolvedClass = d;

           }

         }

 

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index f0eb1937..72239d5e 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 = 104;

-	const int noSym = 104;

+	const int maxT = 105;

+	const int noSym = 105;

 

 

 	[ContractInvariantMethod]

@@ -497,51 +497,52 @@ public class Scanner {
 			case "unlimited": t.kind = 13; break;

 			case "datatype": t.kind = 14; break;

 			case "var": t.kind = 18; break;

-			case "replaces": t.kind = 20; break;

-			case "by": t.kind = 21; break;

-			case "method": t.kind = 25; break;

-			case "constructor": t.kind = 26; break;

-			case "returns": t.kind = 27; break;

-			case "modifies": t.kind = 28; break;

-			case "free": t.kind = 29; break;

-			case "requires": t.kind = 30; break;

-			case "ensures": t.kind = 31; break;

-			case "decreases": t.kind = 32; break;

-			case "bool": t.kind = 35; break;

-			case "nat": t.kind = 36; break;

-			case "int": t.kind = 37; break;

-			case "set": t.kind = 38; break;

-			case "multiset": t.kind = 39; break;

-			case "seq": t.kind = 40; break;

-			case "object": t.kind = 41; break;

-			case "function": t.kind = 42; break;

-			case "reads": t.kind = 43; break;

-			case "label": t.kind = 46; break;

-			case "break": t.kind = 47; break;

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

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

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

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

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

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

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

-			case "invariant": t.kind = 60; break;

-			case "match": t.kind = 61; break;

-			case "assert": t.kind = 62; break;

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

-			case "print": t.kind = 64; break;

-			case "parallel": t.kind = 65; break;

-			case "in": t.kind = 79; break;

-			case "false": t.kind = 89; break;

-			case "true": t.kind = 90; break;

-			case "null": t.kind = 91; break;

-			case "this": t.kind = 92; break;

-			case "fresh": t.kind = 93; break;

-			case "allocated": t.kind = 94; break;

-			case "old": t.kind = 95; break;

-			case "then": t.kind = 96; break;

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

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

+			case "type": t.kind = 20; break;

+			case "replaces": t.kind = 21; break;

+			case "by": t.kind = 22; break;

+			case "method": t.kind = 26; break;

+			case "constructor": t.kind = 27; break;

+			case "returns": t.kind = 28; break;

+			case "modifies": t.kind = 29; break;

+			case "free": t.kind = 30; break;

+			case "requires": t.kind = 31; break;

+			case "ensures": t.kind = 32; break;

+			case "decreases": t.kind = 33; break;

+			case "bool": t.kind = 36; break;

+			case "nat": t.kind = 37; break;

+			case "int": t.kind = 38; break;

+			case "set": t.kind = 39; break;

+			case "multiset": t.kind = 40; break;

+			case "seq": t.kind = 41; break;

+			case "object": t.kind = 42; break;

+			case "function": t.kind = 43; break;

+			case "reads": t.kind = 44; break;

+			case "label": t.kind = 47; break;

+			case "break": t.kind = 48; break;

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

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

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

+			case "if": t.kind = 56; break;

+			case "else": t.kind = 57; break;

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

+			case "while": t.kind = 60; break;

+			case "invariant": t.kind = 61; break;

+			case "match": t.kind = 62; break;

+			case "assert": t.kind = 63; break;

+			case "assume": t.kind = 64; break;

+			case "print": t.kind = 65; break;

+			case "parallel": t.kind = 66; break;

+			case "in": t.kind = 80; break;

+			case "false": t.kind = 90; break;

+			case "true": t.kind = 91; break;

+			case "null": t.kind = 92; break;

+			case "this": t.kind = 93; break;

+			case "fresh": t.kind = 94; break;

+			case "allocated": t.kind = 95; break;

+			case "old": t.kind = 96; break;

+			case "then": t.kind = 97; break;

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

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

 			default: break;

 		}

 	}

@@ -651,75 +652,75 @@ public class Scanner {
 			case 20:

 				{t.kind = 19; break;}

 			case 21:

-				{t.kind = 33; break;}

-			case 22:

 				{t.kind = 34; break;}

+			case 22:

+				{t.kind = 35; break;}

 			case 23:

-				{t.kind = 44; break;}

-			case 24:

 				{t.kind = 45; break;}

+			case 24:

+				{t.kind = 46; break;}

 			case 25:

-				{t.kind = 49; break;}

+				{t.kind = 50; break;}

 			case 26:

-				{t.kind = 51; break;}

-			case 27:

 				{t.kind = 52; break;}

+			case 27:

+				{t.kind = 53; break;}

 			case 28:

-				{t.kind = 58; break;}

+				{t.kind = 59; break;}

 			case 29:

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

 				else {goto case 0;}

 			case 30:

-				{t.kind = 66; break;}

-			case 31:

 				{t.kind = 67; break;}

-			case 32:

+			case 31:

 				{t.kind = 68; break;}

-			case 33:

+			case 32:

 				{t.kind = 69; break;}

+			case 33:

+				{t.kind = 70; break;}

 			case 34:

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

 				else {goto case 0;}

 			case 35:

-				{t.kind = 70; break;}

-			case 36:

 				{t.kind = 71; break;}

-			case 37:

+			case 36:

 				{t.kind = 72; break;}

-			case 38:

+			case 37:

 				{t.kind = 73; break;}

+			case 38:

+				{t.kind = 74; break;}

 			case 39:

-				{t.kind = 76; break;}

-			case 40:

 				{t.kind = 77; break;}

-			case 41:

+			case 40:

 				{t.kind = 78; break;}

+			case 41:

+				{t.kind = 79; break;}

 			case 42:

-				{t.kind = 81; break;}

-			case 43:

 				{t.kind = 82; break;}

-			case 44:

+			case 43:

 				{t.kind = 83; break;}

-			case 45:

+			case 44:

 				{t.kind = 84; break;}

-			case 46:

+			case 45:

 				{t.kind = 85; break;}

-			case 47:

+			case 46:

 				{t.kind = 86; break;}

-			case 48:

+			case 47:

 				{t.kind = 87; break;}

-			case 49:

+			case 48:

 				{t.kind = 88; break;}

+			case 49:

+				{t.kind = 89; break;}

 			case 50:

-				{t.kind = 97; break;}

+				{t.kind = 98; break;}

 			case 51:

-				{t.kind = 99; break;}

+				{t.kind = 100; break;}

 			case 52:

-				{t.kind = 101; break;}

-			case 53:

 				{t.kind = 102; break;}

-			case 54:

+			case 53:

 				{t.kind = 103; break;}

+			case 54:

+				{t.kind = 104; break;}

 			case 55:

 				recEnd = pos; recKind = 15;

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

@@ -730,35 +731,35 @@ public class Scanner {
 				if (ch == '|') {AddCh(); goto case 37;}

 				else {t.kind = 16; break;}

 			case 57:

-				recEnd = pos; recKind = 22;

+				recEnd = pos; recKind = 23;

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

 				else if (ch == ':') {AddCh(); goto case 53;}

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

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

 			case 58:

-				recEnd = pos; recKind = 23;

+				recEnd = pos; recKind = 24;

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

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

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

 			case 59:

-				recEnd = pos; recKind = 24;

+				recEnd = pos; recKind = 25;

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

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

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

 			case 60:

-				recEnd = pos; recKind = 53;

+				recEnd = pos; recKind = 54;

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

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

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

 			case 61:

-				recEnd = pos; recKind = 80;

+				recEnd = pos; recKind = 81;

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

 				else if (ch == '!') {AddCh(); goto case 41;}

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

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

 			case 62:

-				recEnd = pos; recKind = 74;

+				recEnd = pos; recKind = 75;

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

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

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

 			case 63:

-				recEnd = pos; recKind = 75;

+				recEnd = pos; recKind = 76;

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

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

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

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 5f382eb6..ce64e202 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -302,7 +302,9 @@ namespace Microsoft.Dafny {
       }

 

       foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {

-        if (d is DatatypeDecl) {

+        if (d is ArbitraryTypeDecl) {

+          // nothing to do--this is treated just like a type parameter

+        } else if (d is DatatypeDecl) {

           AddDatatype((DatatypeDecl)d);

         } else {

           AddClassMembers((ClassDecl)d);

@@ -310,7 +312,9 @@ namespace Microsoft.Dafny {
       }

       foreach (ModuleDecl m in program.Modules) {

         foreach (TopLevelDecl d in m.TopLevelDecls) {

-          if (d is DatatypeDecl) {

+          if (d is ArbitraryTypeDecl) {

+            // nothing to do--this is treated just like a type parameter

+          } else if (d is DatatypeDecl) {

             AddDatatype((DatatypeDecl)d);

           } else {

             AddClassMembers((ClassDecl)d);