Dafny: fixed resolution bug for inductive datatypes (previous check did not handle generic datatypes correctly)

Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now)
author: Unknown <leino@LEINO6.redmond.corp.microsoft.com> 2012-04-25 16:37:12 -0700
committer: Unknown <leino@LEINO6.redmond.corp.microsoft.com> 2012-04-25 16:37:12 -0700
commit: a732a632287074e74a1dd394149b36e83526a0cf (patch)
tree: 9770cb8127d4bf9d8348a5da54922d32f3d29fdb
parent: 032662d0adb823376b1abd49a0c46ba3276f8721 (diff)
17 files changed, 937 insertions, 723 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 454b47be..581a699e 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -81,8 +81,8 @@ namespace Microsoft.Dafny {
           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;
+          } else if (d is IndDatatypeDecl) {
+            var dt = (IndDatatypeDecl)d;
             Indent(indent);
             wr.Write("public abstract class Base_{0}", dt.Name);
             if (dt.TypeArgs.Count != 0) {
@@ -91,6 +91,9 @@ namespace Microsoft.Dafny {
             wr.WriteLine(" { }");
             CompileDatatypeConstructors(dt, indent);
             CompileDatatypeStruct(dt, indent);
+          } else if (d is CoDatatypeDecl) {
+            // TODO
+            throw new NotImplementedException();
           } else {
             ClassDecl cl = (ClassDecl)d;
             Indent(indent);
@@ -202,10 +205,7 @@ namespace Microsoft.Dafny {
         //   }
         // }
         Indent(indent);
-        wr.Write("public class {0}", DtCtorName(ctor));
-        if (dt.TypeArgs.Count != 0) {
-          wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
-        }
+        wr.Write("public class {0}", DtCtorName(ctor, dt.TypeArgs));
         wr.Write(" : Base_{0}", dt.Name);
         if (dt.TypeArgs.Count != 0) {
           wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
@@ -239,10 +239,7 @@ namespace Microsoft.Dafny {
         // Equals method
         Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
         Indent(ind + IndentAmount);
-        wr.Write("var oth = other as {0}", DtCtorName(ctor));
-        if (dt.TypeArgs.Count != 0) {
-          wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
-        }
+        wr.Write("var oth = other as {0}", DtCtorName(ctor, dt.TypeArgs));
         wr.WriteLine(";");
         Indent(ind + IndentAmount);
         wr.Write("return oth != null");
@@ -270,7 +267,7 @@ namespace Microsoft.Dafny {
       }
     }
 
-    void CompileDatatypeStruct(DatatypeDecl dt, int indent) {
+    void CompileDatatypeStruct(IndDatatypeDecl dt, int indent) {
       Contract.Requires(dt != null);
 
       // public struct Dt<T> {
@@ -320,10 +317,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("public static Base_{0} Default {{", DtT);
       Indent(ind + IndentAmount);
       wr.Write("get { return ");
-      wr.Write("new {0}", DtCtorName(cce.NonNull(dt.DefaultCtor)));
-      if (dt.TypeArgs.Count != 0) {
-        wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
-      }
+      wr.Write("new {0}", DtCtorName(cce.NonNull(dt.DefaultCtor), dt.TypeArgs));
       wr.Write("(");
       string sep = "";
       foreach (Formal f in dt.DefaultCtor.Formals) {
@@ -390,11 +384,34 @@ namespace Microsoft.Dafny {
     }
 
     string DtCtorName(DatatypeCtor ctor) {
-      Contract.Requires(ctor != null);Contract.Ensures(Contract.Result<string>() != null);
+      Contract.Requires(ctor != null);
+      Contract.Ensures(Contract.Result<string>() != null);
 
       return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;
     }
 
+    string DtCtorName(DatatypeCtor ctor, List<TypeParameter> typeParams) {
+      Contract.Requires(ctor != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+
+      var s = DtCtorName(ctor);
+      if (typeParams != null && typeParams.Count != 0) {
+        s += "<" + TypeParameters(typeParams) + ">";
+      }
+      return s;
+    }
+
+    string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs) {
+      Contract.Requires(ctor != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+
+      var s = DtCtorName(ctor);
+      if (typeArgs != null && typeArgs.Count != 0) {
+        s += "<" + TypeNames(typeArgs) + ">";
+      }
+      return s;
+    }
+
     public bool HasMain(Program program) {
       foreach (var module in program.Modules) {
         foreach (var decl in module.TopLevelDecls) {
@@ -528,8 +545,9 @@ namespace Microsoft.Dafny {
           wr.WriteLine("throw new System.Exception();");
         } else {
           int i = 0;
+          var sourceType = (UserDefinedType)me.Source.Type;
           foreach (MatchCaseExpr mc in me.Cases) {
-            MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
             CompileReturnBody(mc.Body, indent + IndentAmount);
             i++;
           }
@@ -1085,6 +1103,8 @@ namespace Microsoft.Dafny {
         //   ...
         // }
         if (s.Cases.Count != 0) {
+          var sourceType = (UserDefinedType)s.Source.Type;
+
           SpillLetVariableDecls(s.Source, indent);
           string source = "_source" + tmpVarCount;
           tmpVarCount++;
@@ -1095,7 +1115,7 @@ namespace Microsoft.Dafny {
 
           int i = 0;
           foreach (MatchCaseStmt mc in s.Cases) {
-            MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);
+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);
             TrStmtList(mc.Body, indent);
             i++;
           }
@@ -1344,8 +1364,9 @@ namespace Microsoft.Dafny {
       }
     }
 
-    void MatchCasePrelude(string source, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {
+    void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {
       Contract.Requires(source != null);
+      Contract.Requires(sourceType != null);
       Contract.Requires(ctor != null);
       Contract.Requires(cce.NonNullElements(arguments));
       // if (source._D is Dt_Ctor0) {
@@ -1356,7 +1377,7 @@ namespace Microsoft.Dafny {
       if (caseIndex == caseCount - 1) {
         wr.Write("true");
       } else {
-        wr.Write("{0}._D is {1}", source, DtCtorName(ctor));
+        wr.Write("{0}._D is {1}", source, DtCtorName(ctor, sourceType.TypeArgs));
       }
       wr.WriteLine(") {");
 
@@ -1368,7 +1389,7 @@ namespace Microsoft.Dafny {
           // FormalType f0 = ((Dt_Ctor0)source._D).a0;
           Indent(indent + IndentAmount);
           wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",
-            TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k));
+            TypeName(bv.Type), bv.Name, DtCtorName(ctor, sourceType.TypeArgs), source, FormalName(arg, k));
           k++;
         }
       }
@@ -1561,10 +1582,7 @@ namespace Microsoft.Dafny {
         if (dtv.InferredTypeArgs.Count != 0) {
           wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));
         }
-        wr.Write("(new {0}", DtCtorName(dtv.Ctor));
-        if (dtv.InferredTypeArgs.Count != 0) {
-          wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));
-        }
+        wr.Write("(new {0}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));
         wr.Write("(");
         string sep = "";
         for (int i = 0; i < dtv.Arguments.Count; i++) {
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index c6609b4c..1390d5ca 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -171,7 +171,7 @@ Dafny
                                               theModules.Add(module); .)
     | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .)
       ClassDecl<defaultModule, out c>           (. defaultModule.TopLevelDecls.Add(c); .)
-    | (. if (isGhost) { SemErr(t, "a datatype is not allowed to be declared as 'ghost'"); } .)
+    | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .)
       DatatypeDecl<defaultModule, out dt>       (. defaultModule.TopLevelDecls.Add(dt); .)
     | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .)
       ArbitraryTypeDecl<defaultModule, out at>  (. defaultModule.TopLevelDecls.Add(at); .)
@@ -241,9 +241,12 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
      List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
      IToken bodyStart = Token.NoToken;  // dummy assignment
+     bool co = false;
   .)
   SYNC
-  "datatype"
+  ( "datatype"
+  | "codatatype"     (. co = true; .)
+  )
   { Attribute<ref attrs> }
   Ident<out id>
   [ GenericParameters<typeArgs> ]
@@ -251,7 +254,11 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
   DatatypeMemberDecl<ctors>
   { "|" DatatypeMemberDecl<ctors> }
   SYNC ";"
-  (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+  (. if (co) {
+       dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+     } else {
+       dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+     }
      dt.BodyStartTok = bodyStart;
      dt.BodyEndTok = t;
   .)
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index f5955d11..ffe39618 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -232,6 +232,21 @@ namespace Microsoft.Dafny {
         }
       }
     }
+    public bool IsIndDatatype {
+      get {
+        return AsIndDatatype != null;
+      }
+    }
+    public IndDatatypeDecl AsIndDatatype {
+      get {
+        UserDefinedType udt = this as UserDefinedType;
+        if (udt == null) {
+          return null;
+        } else {
+          return udt.ResolvedClass as IndDatatypeDecl;
+        }
+      }
+    }
     public bool IsTypeParameter {
       get {
         UserDefinedType ct = this as UserDefinedType;
@@ -774,7 +789,7 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class DatatypeDecl : TopLevelDecl {
+  public abstract class DatatypeDecl : TopLevelDecl {
     public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;
     [ContractInvariantMethod]
     void ObjectInvariant() {
@@ -782,8 +797,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(1 <= Ctors.Count);
     }
 
-    public DatatypeCtor DefaultCtor;  // set during resolution
-
     public DatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,
       [Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)
       : base(tok, name, module, typeArgs, attributes) {
@@ -797,7 +810,39 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class DatatypeCtor : Declaration, TypeParameter.ParentType {
+  public class IndDatatypeDecl : DatatypeDecl
+  {
+    public DatatypeCtor DefaultCtor;  // set during resolution
+    public bool[] TypeParametersUsedInConstructionByDefaultCtor;  // set during resolution; has same length as
+
+    public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,
+      [Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)
+      : base(tok, name, module, typeArgs, ctors, attributes) {
+      Contract.Requires(tok != null);
+      Contract.Requires(name != null);
+      Contract.Requires(module != null);
+      Contract.Requires(cce.NonNullElements(typeArgs));
+      Contract.Requires(cce.NonNullElements(ctors));
+      Contract.Requires(1 <= ctors.Count);
+    }
+  }
+
+  public class CoDatatypeDecl : DatatypeDecl
+  {
+    public CoDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,
+      [Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)
+      : base(tok, name, module, typeArgs, ctors, attributes) {
+      Contract.Requires(tok != null);
+      Contract.Requires(name != null);
+      Contract.Requires(module != null);
+      Contract.Requires(cce.NonNullElements(typeArgs));
+      Contract.Requires(cce.NonNullElements(ctors));
+      Contract.Requires(1 <= ctors.Count);
+    }
+  }
+
+  public class DatatypeCtor : Declaration, TypeParameter.ParentType
+  {
     public readonly List<Formal/*!*/>/*!*/ Formals;
     [ContractInvariantMethod]
     void ObjectInvariant() {
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 8e0d2e31..a063e26b 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;
 	public const int _lbrace = 6;
 	public const int _rbrace = 7;
-	public const int maxT = 106;
+	public const int maxT = 107;
 
 	const bool T = true;
 	const bool x = false;
@@ -231,10 +231,10 @@ bool IsAttribute() {
 					if (la.kind == 12) {
 						ClassDecl(module, out c);
 						module.TopLevelDecls.Add(c); 
-					} else if (la.kind == 15) {
+					} else if (la.kind == 15 || la.kind == 16) {
 						DatatypeDecl(module, out dt);
 						module.TopLevelDecls.Add(dt); 
-					} else if (la.kind == 21) {
+					} else if (la.kind == 22) {
 						ArbitraryTypeDecl(module, out at);
 						module.TopLevelDecls.Add(at); 
 					} else {
@@ -249,17 +249,17 @@ bool IsAttribute() {
 				if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } 
 				ClassDecl(defaultModule, out c);
 				defaultModule.TopLevelDecls.Add(c); 
-			} else if (la.kind == 15) {
-				if (isGhost) { SemErr(t, "a datatype is not allowed to be declared as 'ghost'"); } 
+			} else if (la.kind == 15 || la.kind == 16) {
+				if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } 
 				DatatypeDecl(defaultModule, out dt);
 				defaultModule.TopLevelDecls.Add(dt); 
-			} else if (la.kind == 21) {
+			} else if (la.kind == 22) {
 				if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } 
 				ArbitraryTypeDecl(defaultModule, out at);
 				defaultModule.TopLevelDecls.Add(at); 
 			} else if (StartOf(3)) {
 				ClassMemberDecl(membersDefaultClass, isGhost, false);
-			} else SynErr(107);
+			} else SynErr(108);
 		}
 		if (defaultModuleCreatedHere) {
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
@@ -294,7 +294,7 @@ bool IsAttribute() {
 		IToken/*!*/ id; 
 		Ident(out id);
 		ids.Add(id.val); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			Ident(out id);
 			ids.Add(id.val); 
@@ -310,13 +310,13 @@ bool IsAttribute() {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
 		IToken bodyStart;
 		
-		while (!(la.kind == 0 || la.kind == 12)) {SynErr(108); Get();}
+		while (!(la.kind == 0 || la.kind == 12)) {SynErr(109); Get();}
 		Expect(12);
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
 		Ident(out id);
-		if (la.kind == 22) {
+		if (la.kind == 23) {
 			GenericParameters(typeArgs);
 		}
 		Expect(6);
@@ -339,26 +339,36 @@ bool IsAttribute() {
 		List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
 		List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
 		IToken bodyStart = Token.NoToken;  // dummy assignment
+		bool co = false;
 		
-		while (!(la.kind == 0 || la.kind == 15)) {SynErr(109); Get();}
-		Expect(15);
+		while (!(la.kind == 0 || la.kind == 15 || la.kind == 16)) {SynErr(110); Get();}
+		if (la.kind == 15) {
+			Get();
+		} else if (la.kind == 16) {
+			Get();
+			co = true; 
+		} else SynErr(111);
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
 		Ident(out id);
-		if (la.kind == 22) {
+		if (la.kind == 23) {
 			GenericParameters(typeArgs);
 		}
-		Expect(16);
+		Expect(17);
 		bodyStart = t; 
 		DatatypeMemberDecl(ctors);
-		while (la.kind == 17) {
+		while (la.kind == 18) {
 			Get();
 			DatatypeMemberDecl(ctors);
 		}
-		while (!(la.kind == 0 || la.kind == 18)) {SynErr(110); Get();}
-		Expect(18);
-		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+		while (!(la.kind == 0 || la.kind == 19)) {SynErr(112); Get();}
+		Expect(19);
+		if (co) {
+		 dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+		} else {
+		 dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+		}
 		dt.BodyStartTok = bodyStart;
 		dt.BodyEndTok = t;
 		
@@ -368,14 +378,14 @@ bool IsAttribute() {
 		IToken/*!*/ id;
 		Attributes attrs = null;
 		
-		Expect(21);
+		Expect(22);
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
 		Ident(out id);
 		at = new ArbitraryTypeDecl(id, id.val, module, attrs); 
-		while (!(la.kind == 0 || la.kind == 18)) {SynErr(111); Get();}
-		Expect(18);
+		while (!(la.kind == 0 || la.kind == 19)) {SynErr(113); Get();}
+		Expect(19);
 	}
 
 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {
@@ -397,29 +407,29 @@ bool IsAttribute() {
 				mmod.IsUnlimited = true; 
 			}
 		}
-		if (la.kind == 19) {
+		if (la.kind == 20) {
 			FieldDecl(mmod, mm);
-		} else if (la.kind == 42 || la.kind == 43) {
+		} else if (la.kind == 43 || la.kind == 44) {
 			FunctionDecl(mmod, out f);
 			mm.Add(f); 
-		} else if (la.kind == 24 || la.kind == 25) {
+		} else if (la.kind == 25 || la.kind == 26) {
 			MethodDecl(mmod, allowConstructors, out m);
 			mm.Add(m); 
-		} else SynErr(112);
+		} else SynErr(114);
 	}
 
 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
 		Contract.Requires(cce.NonNullElements(typeArgs));
 		IToken/*!*/ id; 
-		Expect(22);
+		Expect(23);
 		Ident(out id);
 		typeArgs.Add(new TypeParameter(id, id.val)); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			Ident(out id);
 			typeArgs.Add(new TypeParameter(id, id.val)); 
 		}
-		Expect(23);
+		Expect(24);
 	}
 
 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -427,8 +437,8 @@ bool IsAttribute() {
 		Attributes attrs = null;
 		IToken/*!*/ id;  Type/*!*/ ty;
 		
-		while (!(la.kind == 0 || la.kind == 19)) {SynErr(113); Get();}
-		Expect(19);
+		while (!(la.kind == 0 || la.kind == 20)) {SynErr(115); Get();}
+		Expect(20);
 		if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
 		
@@ -437,13 +447,13 @@ bool IsAttribute() {
 		}
 		IdentType(out id, out ty);
 		mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			IdentType(out id, out ty);
 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 
 		}
-		while (!(la.kind == 0 || la.kind == 18)) {SynErr(114); Get();}
-		Expect(18);
+		while (!(la.kind == 0 || la.kind == 19)) {SynErr(116); Get();}
+		Expect(19);
 	}
 
 	void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
@@ -465,9 +475,9 @@ bool IsAttribute() {
 		IToken bodyEnd = Token.NoToken;
 		bool signatureOmitted = false;
 		
-		if (la.kind == 42) {
+		if (la.kind == 43) {
 			Get();
-			if (la.kind == 24) {
+			if (la.kind == 25) {
 				Get();
 				isFunctionMethod = true; 
 			}
@@ -477,22 +487,22 @@ bool IsAttribute() {
 				Attribute(ref attrs);
 			}
 			Ident(out id);
-			if (la.kind == 22 || la.kind == 33) {
-				if (la.kind == 22) {
+			if (la.kind == 23 || la.kind == 34) {
+				if (la.kind == 23) {
 					GenericParameters(typeArgs);
 				}
 				Formals(true, isFunctionMethod, formals, out openParen);
 				Expect(5);
 				Type(out returnType);
-			} else if (la.kind == 27) {
+			} else if (la.kind == 28) {
 				Get();
 				signatureOmitted = true;
 				openParen = Token.NoToken; 
-			} else SynErr(115);
-		} else if (la.kind == 43) {
+			} else SynErr(117);
+		} else if (la.kind == 44) {
 			Get();
 			isPredicate = true; 
-			if (la.kind == 24) {
+			if (la.kind == 25) {
 				Get();
 				isFunctionMethod = true; 
 			}
@@ -503,22 +513,22 @@ bool IsAttribute() {
 			}
 			Ident(out id);
 			if (StartOf(4)) {
-				if (la.kind == 22) {
+				if (la.kind == 23) {
 					GenericParameters(typeArgs);
 				}
-				if (la.kind == 33) {
+				if (la.kind == 34) {
 					Formals(true, isFunctionMethod, formals, out openParen);
 					if (la.kind == 5) {
 						Get();
 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 
 					}
 				}
-			} else if (la.kind == 27) {
+			} else if (la.kind == 28) {
 				Get();
 				signatureOmitted = true;
 				openParen = Token.NoToken; 
-			} else SynErr(116);
-		} else SynErr(117);
+			} else SynErr(118);
+		} else SynErr(119);
 		while (StartOf(5)) {
 			FunctionSpec(reqs, reads, ens, decreases);
 		}
@@ -557,10 +567,10 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;
 		IToken bodyEnd = Token.NoToken;
 		
-		while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(118); Get();}
-		if (la.kind == 24) {
+		while (!(la.kind == 0 || la.kind == 25 || la.kind == 26)) {SynErr(120); Get();}
+		if (la.kind == 25) {
 			Get();
-		} else if (la.kind == 25) {
+		} else if (la.kind == 26) {
 			Get();
 			if (allowConstructor) {
 			 isConstructor = true;
@@ -568,7 +578,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");
 			}
 			
-		} else SynErr(119);
+		} else SynErr(121);
 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
 		if (isConstructor) {
 		 if (mmod.IsGhost) {
@@ -583,20 +593,20 @@ bool IsAttribute() {
 			Attribute(ref attrs);
 		}
 		Ident(out id);
-		if (la.kind == 22 || la.kind == 33) {
-			if (la.kind == 22) {
+		if (la.kind == 23 || la.kind == 34) {
+			if (la.kind == 23) {
 				GenericParameters(typeArgs);
 			}
 			Formals(true, !mmod.IsGhost, ins, out openParen);
-			if (la.kind == 26) {
+			if (la.kind == 27) {
 				Get();
 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 
 				Formals(false, !mmod.IsGhost, outs, out openParen);
 			}
-		} else if (la.kind == 27) {
+		} else if (la.kind == 28) {
 			Get();
 			signatureOmitted = true; openParen = Token.NoToken; 
-		} else SynErr(120);
+		} else SynErr(122);
 		while (StartOf(6)) {
 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
 		}
@@ -625,7 +635,7 @@ bool IsAttribute() {
 			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)); 
@@ -633,17 +643,17 @@ bool IsAttribute() {
 
 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 
-		Expect(33);
+		Expect(34);
 		if (StartOf(7)) {
 			TypeIdentOptional(out id, out name, out ty, out isGhost);
 			formals.Add(new Formal(id, name, ty, true, isGhost)); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				TypeIdentOptional(out id, out name, out ty, out isGhost);
 				formals.Add(new Formal(id, name, ty, true, isGhost)); 
 			}
 		}
-		Expect(34);
+		Expect(35);
 	}
 
 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -727,22 +737,22 @@ bool IsAttribute() {
 		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);
@@ -753,7 +763,7 @@ bool IsAttribute() {
 			
 			break;
 		}
-		case 39: {
+		case 40: {
 			Get();
 			tok = t;  gt = new List<Type/*!*/>(); 
 			GenericInstantiation(gt);
@@ -764,7 +774,7 @@ bool IsAttribute() {
 			
 			break;
 		}
-		case 40: {
+		case 41: {
 			Get();
 			tok = t;  gt = new List<Type/*!*/>(); 
 			GenericInstantiation(gt);
@@ -775,28 +785,28 @@ bool IsAttribute() {
 			
 			break;
 		}
-		case 1: case 3: case 41: {
+		case 1: case 3: case 42: {
 			ReferenceType(out tok, out ty);
 			break;
 		}
-		default: SynErr(121); break;
+		default: SynErr(123); break;
 		}
 	}
 
 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 
-		Expect(33);
+		Expect(34);
 		openParen = t; 
 		if (la.kind == 1 || la.kind == 8) {
 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
 				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,
@@ -804,8 +814,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;
 		
-		while (!(StartOf(8))) {SynErr(122); Get();}
-		if (la.kind == 28) {
+		while (!(StartOf(8))) {SynErr(124); Get();}
+		if (la.kind == 29) {
 			Get();
 			while (IsAttribute()) {
 				Attribute(ref modAttrs);
@@ -813,44 +823,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (StartOf(9)) {
 				FrameExpression(out fe);
 				mod.Add(fe); 
-				while (la.kind == 20) {
+				while (la.kind == 21) {
 					Get();
 					FrameExpression(out fe);
 					mod.Add(fe); 
 				}
 			}
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(123); Get();}
-			Expect(18);
-		} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {
-			if (la.kind == 29) {
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(125); Get();}
+			Expect(19);
+		} 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 == 18)) {SynErr(124); Get();}
-				Expect(18);
+				while (!(la.kind == 0 || la.kind == 19)) {SynErr(126); Get();}
+				Expect(19);
 				req.Add(new MaybeFreeExpression(e, isFree)); 
-			} else if (la.kind == 31) {
+			} else if (la.kind == 32) {
 				Get();
 				while (IsAttribute()) {
 					Attribute(ref ensAttrs);
 				}
 				Expression(out e);
-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}
-				Expect(18);
+				while (!(la.kind == 0 || la.kind == 19)) {SynErr(127); Get();}
+				Expect(19);
 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 
-			} else SynErr(126);
-		} else if (la.kind == 32) {
+			} else SynErr(128);
+		} else if (la.kind == 33) {
 			Get();
 			while (IsAttribute()) {
 				Attribute(ref decAttrs);
 			}
 			DecreasesList(decreases, false);
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();}
-			Expect(18);
-		} else SynErr(128);
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(129); Get();}
+			Expect(19);
+		} else SynErr(130);
 	}
 
 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -870,7 +880,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	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 == 46) {
+		if (la.kind == 47) {
 			Get();
 			Ident(out id);
 			fieldName = id.val; 
@@ -891,7 +901,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 decreases.Add(e);
 		}
 		
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			PossiblyWildExpression(out e);
 			if (!allowWildcard && e is WildcardExpr) {
@@ -905,15 +915,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 
-		Expect(22);
+		Expect(23);
 		Type(out ty);
 		gt.Add(ty); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			Type(out ty);
 			gt.Add(ty); 
 		}
-		Expect(23);
+		Expect(24);
 	}
 
 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -921,7 +931,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		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) {
@@ -940,48 +950,48 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 1) {
 			Ident(out tok);
 			gt = new List<Type/*!*/>(); 
-			if (la.kind == 22) {
+			if (la.kind == 23) {
 				GenericInstantiation(gt);
 			}
 			ty = new UserDefinedType(tok, tok.val, gt); 
-		} else SynErr(129);
+		} else SynErr(131);
 	}
 
 	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(130); Get();}
+		if (la.kind == 31) {
+			while (!(la.kind == 0 || la.kind == 31)) {SynErr(132); Get();}
 			Get();
 			Expression(out e);
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(131); Get();}
-			Expect(18);
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(133); Get();}
+			Expect(19);
 			reqs.Add(e); 
-		} else if (la.kind == 44) {
+		} else if (la.kind == 45) {
 			Get();
 			if (StartOf(11)) {
 				PossiblyWildFrameExpression(out fe);
 				reads.Add(fe); 
-				while (la.kind == 20) {
+				while (la.kind == 21) {
 					Get();
 					PossiblyWildFrameExpression(out fe);
 					reads.Add(fe); 
 				}
 			}
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(132); Get();}
-			Expect(18);
-		} else if (la.kind == 31) {
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(134); Get();}
+			Expect(19);
+		} else if (la.kind == 32) {
 			Get();
 			Expression(out e);
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}
-			Expect(18);
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(135); Get();}
+			Expect(19);
 			ens.Add(e); 
-		} else if (la.kind == 32) {
+		} else if (la.kind == 33) {
 			Get();
 			DecreasesList(decreases, false);
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();}
-			Expect(18);
-		} else SynErr(135);
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(136); Get();}
+			Expect(19);
+		} else SynErr(137);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -995,23 +1005,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 
-		if (la.kind == 45) {
+		if (la.kind == 46) {
 			Get();
 			fe = new FrameExpression(new WildcardExpr(t), null); 
 		} else if (StartOf(9)) {
 			FrameExpression(out fe);
-		} else SynErr(136);
+		} else SynErr(138);
 	}
 
 	void PossiblyWildExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
 		e = dummyExpr; 
-		if (la.kind == 45) {
+		if (la.kind == 46) {
 			Get();
 			e = new WildcardExpr(t); 
 		} else if (StartOf(9)) {
 			Expression(out e);
-		} else SynErr(137);
+		} else SynErr(139);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1028,50 +1038,50 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;
 		int breakCount;
 		
-		while (!(StartOf(12))) {SynErr(138); Get();}
+		while (!(StartOf(12))) {SynErr(140); Get();}
 		switch (la.kind) {
 		case 6: {
 			BlockStmt(out bs, out bodyStart, out bodyEnd);
 			s = bs; 
 			break;
 		}
-		case 64: {
+		case 65: {
 			AssertStmt(out s);
 			break;
 		}
-		case 65: {
+		case 66: {
 			AssumeStmt(out s);
 			break;
 		}
-		case 66: {
+		case 67: {
 			PrintStmt(out s);
 			break;
 		}
-		case 1: case 2: case 17: case 33: case 91: case 92: case 93: case 94: case 95: case 96: case 97: {
+		case 1: case 2: case 18: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
 			UpdateStmt(out s);
 			break;
 		}
-		case 8: case 19: {
+		case 8: case 20: {
 			VarDeclStatement(out s);
 			break;
 		}
-		case 57: {
+		case 58: {
 			IfStmt(out s);
 			break;
 		}
-		case 61: {
+		case 62: {
 			WhileStmt(out s);
 			break;
 		}
-		case 63: {
+		case 64: {
 			MatchStmt(out s);
 			break;
 		}
-		case 67: {
+		case 68: {
 			ParallelStmt(out s);
 			break;
 		}
-		case 47: {
+		case 48: {
 			Get();
 			x = t; 
 			Ident(out id);
@@ -1080,34 +1090,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LabelNode(x, id.val, s.Labels); 
 			break;
 		}
-		case 48: {
+		case 49: {
 			Get();
 			x = t; breakCount = 1; label = null; 
 			if (la.kind == 1) {
 				Ident(out id);
 				label = id.val; 
-			} else if (la.kind == 18 || la.kind == 48) {
-				while (la.kind == 48) {
+			} else if (la.kind == 19 || la.kind == 49) {
+				while (la.kind == 49) {
 					Get();
 					breakCount++; 
 				}
-			} else SynErr(139);
-			while (!(la.kind == 0 || la.kind == 18)) {SynErr(140); Get();}
-			Expect(18);
+			} else SynErr(141);
+			while (!(la.kind == 0 || la.kind == 19)) {SynErr(142); Get();}
+			Expect(19);
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 
 			break;
 		}
-		case 49: {
+		case 50: {
 			ReturnStmt(out s);
 			break;
 		}
-		case 27: {
+		case 28: {
 			Get();
 			s = new SkeletonStatement(t); 
-			Expect(18);
+			Expect(19);
 			break;
 		}
-		default: SynErr(141); break;
+		default: SynErr(143); break;
 		}
 	}
 
@@ -1115,17 +1125,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
 		Expression/*!*/ e = null; Attributes attrs = null;
 		
-		Expect(64);
+		Expect(65);
 		x = t; s = null;
 		while (IsAttribute()) {
 			Attribute(ref attrs);
 		}
 		if (StartOf(9)) {
 			Expression(out e);
-		} else if (la.kind == 27) {
+		} else if (la.kind == 28) {
 			Get();
-		} else SynErr(142);
-		Expect(18);
+		} else SynErr(144);
+		Expect(19);
 		if (e == null) {
 		 s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
 		} else {
@@ -1136,10 +1146,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void AssumeStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(65);
+		Expect(66);
 		x = t; 
 		Expression(out e);
-		Expect(18);
+		Expect(19);
 		s = new AssumeStmt(x, e); 
 	}
 
@@ -1147,16 +1157,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;
 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
 		
-		Expect(66);
+		Expect(67);
 		x = t; 
 		AttributeArg(out arg);
 		args.Add(arg); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			AttributeArg(out arg);
 			args.Add(arg); 
 		}
-		Expect(18);
+		Expect(19);
 		s = new PrintStmt(x, args); 
 	}
 
@@ -1171,39 +1181,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		Lhs(out e);
 		x = e.tok; 
-		if (la.kind == 6 || la.kind == 18) {
+		if (la.kind == 6 || la.kind == 19) {
 			while (la.kind == 6) {
 				Attribute(ref attrs);
 			}
-			Expect(18);
+			Expect(19);
 			rhss.Add(new ExprRhs(e, attrs)); 
-		} else if (la.kind == 20 || la.kind == 50 || la.kind == 51) {
+		} else if (la.kind == 21 || la.kind == 51 || la.kind == 52) {
 			lhss.Add(e);  lhs0 = e; 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				Lhs(out e);
 				lhss.Add(e); 
 			}
-			if (la.kind == 50) {
+			if (la.kind == 51) {
 				Get();
 				x = t; 
 				Rhs(out r, lhs0);
 				rhss.Add(r); 
-				while (la.kind == 20) {
+				while (la.kind == 21) {
 					Get();
 					Rhs(out r, lhs0);
 					rhss.Add(r); 
 				}
-			} else if (la.kind == 51) {
+			} else if (la.kind == 52) {
 				Get();
 				x = t; 
 				Expression(out suchThat);
-			} else SynErr(143);
-			Expect(18);
+			} else SynErr(145);
+			Expect(19);
 		} else if (la.kind == 5) {
 			Get();
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
-		} else SynErr(144);
+		} else SynErr(146);
 		if (suchThat != null) {
 		 s = new AssignSuchThatStmt(x, lhss, suchThat);
 		} else {
@@ -1224,17 +1234,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();
 			isGhost = true;  x = t; 
 		}
-		Expect(19);
+		Expect(20);
 		if (!isGhost) { x = t; } 
 		LocalIdentTypeOptional(out d, isGhost);
 		lhss.Add(d); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			LocalIdentTypeOptional(out d, isGhost);
 			lhss.Add(d); 
 		}
-		if (la.kind == 50 || la.kind == 51) {
-			if (la.kind == 50) {
+		if (la.kind == 51 || la.kind == 52) {
+			if (la.kind == 51) {
 				Get();
 				assignTok = t;
 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1242,7 +1252,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				
 				Rhs(out r, lhs0);
 				rhss.Add(r); 
-				while (la.kind == 20) {
+				while (la.kind == 21) {
 					Get();
 					Rhs(out r, lhs0);
 					rhss.Add(r); 
@@ -1253,7 +1263,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Expression(out suchThat);
 			}
 		}
-		Expect(18);
+		Expect(19);
 		ConcreteUpdateStatement update;
 		if (suchThat != null) {
 		 var ies = new List<Expression>();
@@ -1285,25 +1295,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		ifStmt = dummyStmt;  // to please the compiler
 		
-		Expect(57);
+		Expect(58);
 		x = t; 
-		if (la.kind == 27 || la.kind == 33) {
-			if (la.kind == 33) {
+		if (la.kind == 28 || la.kind == 34) {
+			if (la.kind == 34) {
 				Guard(out guard);
 			} else {
 				Get();
 				guardOmitted = true; 
 			}
 			BlockStmt(out thn, out bodyStart, out bodyEnd);
-			if (la.kind == 58) {
+			if (la.kind == 59) {
 				Get();
-				if (la.kind == 57) {
+				if (la.kind == 58) {
 					IfStmt(out s);
 					els = s; 
 				} else if (la.kind == 6) {
 					BlockStmt(out bs, out bodyStart, out bodyEnd);
 					els = bs; 
-				} else SynErr(145);
+				} else SynErr(147);
 			}
 			if (guardOmitted) {
 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1314,7 +1324,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {
 			AlternativeBlock(out alternatives);
 			ifStmt = new AlternativeStmt(x, alternatives); 
-		} else SynErr(146);
+		} else SynErr(148);
 	}
 
 	void WhileStmt(out Statement/*!*/ stmt) {
@@ -1330,10 +1340,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		stmt = dummyStmt;  // to please the compiler
 		
-		Expect(61);
+		Expect(62);
 		x = t; 
-		if (la.kind == 27 || la.kind == 33) {
-			if (la.kind == 33) {
+		if (la.kind == 28 || la.kind == 34) {
+			if (la.kind == 34) {
 				Guard(out guard);
 				Contract.Assume(guard == null || cce.Owner.None(guard)); 
 			} else {
@@ -1343,10 +1353,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
 			if (la.kind == 6) {
 				BlockStmt(out body, out bodyStart, out bodyEnd);
-			} else if (la.kind == 27) {
+			} else if (la.kind == 28) {
 				Get();
 				bodyOmitted = true; 
-			} else SynErr(147);
+			} else SynErr(149);
 			if (guardOmitted || bodyOmitted) {
 			 if (decreases.Count != 0) {
 			   SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");
@@ -1367,18 +1377,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
 			AlternativeBlock(out alternatives);
 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 
-		} else SynErr(148);
+		} else SynErr(150);
 	}
 
 	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(63);
+		Expect(64);
 		x = t; 
 		Expression(out e);
 		Expect(6);
-		while (la.kind == 59) {
+		while (la.kind == 60) {
 			CaseStatement(out c);
 			cases.Add(c); 
 		}
@@ -1398,9 +1408,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;
 		IToken bodyStart, bodyEnd;
 		
-		Expect(67);
+		Expect(68);
 		x = t; 
-		Expect(33);
+		Expect(34);
 		if (la.kind == 1) {
 			List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; 
 			QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1410,16 +1420,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (bvars == null) { bvars = new List<BoundVar>(); }
 		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(18);
+			Expect(19);
 			ens.Add(new MaybeFreeExpression(e, isFree)); 
 		}
 		BlockStmt(out block, out bodyStart, out bodyEnd);
@@ -1431,18 +1441,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;
 		AssignmentRhs r;
 		
-		Expect(49);
+		Expect(50);
 		returnTok = t; 
 		if (StartOf(14)) {
 			Rhs(out r, null);
 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				Rhs(out r, null);
 				rhss.Add(r); 
 			}
 		}
-		Expect(18);
+		Expect(19);
 		s = new ReturnStmt(returnTok, rhss); 
 	}
 
@@ -1455,27 +1465,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler
 		Attributes attrs = null;
 		
-		if (la.kind == 52) {
+		if (la.kind == 53) {
 			Get();
 			newToken = t; 
 			TypeAndToken(out x, out ty);
-			if (la.kind == 53 || la.kind == 55) {
-				if (la.kind == 53) {
+			if (la.kind == 54 || la.kind == 56) {
+				if (la.kind == 54) {
 					Get();
 					ee = new List<Expression>(); 
 					Expressions(ee);
-					Expect(54);
+					Expect(55);
 					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(9)) {
 						Expressions(args);
 					}
-					Expect(34);
+					Expect(35);
 					initCall = new CallStmt(x, new List<Expression>(),
 					                       receiverForInitCall, x.val, args); 
 				}
@@ -1486,18 +1496,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);
 			}
 			
-		} else if (la.kind == 56) {
+		} else if (la.kind == 57) {
 			Get();
 			x = t; 
 			Expression(out e);
 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 
-		} else if (la.kind == 45) {
+		} else if (la.kind == 46) {
 			Get();
 			r = new HavocRhs(t); 
 		} else if (StartOf(9)) {
 			Expression(out e);
 			r = new ExprRhs(e); 
-		} else SynErr(149);
+		} else SynErr(151);
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
@@ -1509,23 +1519,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		if (la.kind == 1) {
 			DottedIdentifiersAndFunction(out e);
-			while (la.kind == 53 || la.kind == 55) {
+			while (la.kind == 54 || la.kind == 56) {
 				Suffix(ref e);
 			}
 		} else if (StartOf(15)) {
 			ConstAtomExpression(out e);
 			Suffix(ref e);
-			while (la.kind == 53 || la.kind == 55) {
+			while (la.kind == 54 || la.kind == 56) {
 				Suffix(ref e);
 			}
-		} else SynErr(150);
+		} else SynErr(152);
 	}
 
 	void Expressions(List<Expression/*!*/>/*!*/ args) {
 		Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; 
 		Expression(out e);
 		args.Add(e); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			Expression(out e);
 			args.Add(e); 
@@ -1534,15 +1544,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void Guard(out Expression e) {
 		Expression/*!*/ ee;  e = null; 
-		Expect(33);
-		if (la.kind == 45) {
+		Expect(34);
+		if (la.kind == 46) {
 			Get();
 			e = null; 
 		} else if (StartOf(9)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(151);
-		Expect(34);
+		} else SynErr(153);
+		Expect(35);
 	}
 
 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {
@@ -1552,11 +1562,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;
 		
 		Expect(6);
-		while (la.kind == 59) {
+		while (la.kind == 60) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(60);
+			Expect(61);
 			body = new List<Statement>(); 
 			while (StartOf(10)) {
 				Stmt(body);
@@ -1574,22 +1584,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;
 		
 		while (StartOf(16)) {
-			if (la.kind == 29 || la.kind == 62) {
+			if (la.kind == 30 || la.kind == 63) {
 				Invariant(out invariant);
-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(152); Get();}
-				Expect(18);
+				while (!(la.kind == 0 || la.kind == 19)) {SynErr(154); Get();}
+				Expect(19);
 				invariants.Add(invariant); 
-			} else if (la.kind == 32) {
-				while (!(la.kind == 0 || la.kind == 32)) {SynErr(153); Get();}
+			} else if (la.kind == 33) {
+				while (!(la.kind == 0 || la.kind == 33)) {SynErr(155); Get();}
 				Get();
 				while (IsAttribute()) {
 					Attribute(ref decAttrs);
 				}
 				DecreasesList(decreases, true);
-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
-				Expect(18);
+				while (!(la.kind == 0 || la.kind == 19)) {SynErr(156); Get();}
+				Expect(19);
 			} else {
-				while (!(la.kind == 0 || la.kind == 28)) {SynErr(155); Get();}
+				while (!(la.kind == 0 || la.kind == 29)) {SynErr(157); Get();}
 				Get();
 				while (IsAttribute()) {
 					Attribute(ref modAttrs);
@@ -1598,26 +1608,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				if (StartOf(9)) {
 					FrameExpression(out fe);
 					mod.Add(fe); 
-					while (la.kind == 20) {
+					while (la.kind == 21) {
 						Get();
 						FrameExpression(out fe);
 						mod.Add(fe); 
 					}
 				}
-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}
-				Expect(18);
+				while (!(la.kind == 0 || la.kind == 19)) {SynErr(158); Get();}
+				Expect(19);
 			}
 		}
 	}
 
 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {
 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 
-		while (!(la.kind == 0 || la.kind == 29 || la.kind == 62)) {SynErr(157); Get();}
-		if (la.kind == 29) {
+		while (!(la.kind == 0 || la.kind == 30 || la.kind == 63)) {SynErr(159); Get();}
+		if (la.kind == 30) {
 			Get();
 			isFree = true; 
 		}
-		Expect(62);
+		Expect(63);
 		while (IsAttribute()) {
 			Attribute(ref attrs);
 		}
@@ -1632,21 +1642,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;
 		List<Statement/*!*/> body = new List<Statement/*!*/>();
 		
-		Expect(59);
+		Expect(60);
 		x = t; 
 		Ident(out id);
-		if (la.kind == 33) {
+		if (la.kind == 34) {
 			Get();
 			IdentTypeOptional(out bv);
 			arguments.Add(bv); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				IdentTypeOptional(out bv);
 				arguments.Add(bv); 
 			}
-			Expect(34);
+			Expect(35);
 		}
-		Expect(60);
+		Expect(61);
 		while (StartOf(10)) {
 			Stmt(body);
 		}
@@ -1661,7 +1671,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {
 			Expression(out e);
 			arg = new Attributes.Argument(t, e); 
-		} else SynErr(158);
+		} else SynErr(160);
 	}
 
 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1672,7 +1682,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		IdentTypeOptional(out bv);
 		bvars.Add(bv); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			IdentTypeOptional(out bv);
 			bvars.Add(bv); 
@@ -1680,7 +1690,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
-		if (la.kind == 17) {
+		if (la.kind == 18) {
 			Get();
 			Expression(out range);
 		}
@@ -1689,7 +1699,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		ImpliesExpression(out e0);
-		while (la.kind == 68 || la.kind == 69) {
+		while (la.kind == 69 || la.kind == 70) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1700,7 +1710,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		LogicalExpression(out e0);
-		if (la.kind == 70 || la.kind == 71) {
+		if (la.kind == 71 || la.kind == 72) {
 			ImpliesOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1709,23 +1719,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void EquivOp() {
-		if (la.kind == 68) {
+		if (la.kind == 69) {
 			Get();
-		} else if (la.kind == 69) {
+		} else if (la.kind == 70) {
 			Get();
-		} else SynErr(159);
+		} else SynErr(161);
 	}
 
 	void LogicalExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(17)) {
-			if (la.kind == 72 || la.kind == 73) {
+			if (la.kind == 73 || la.kind == 74) {
 				AndOp();
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 
-				while (la.kind == 72 || la.kind == 73) {
+				while (la.kind == 73 || la.kind == 74) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1736,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 
-				while (la.kind == 74 || la.kind == 75) {
+				while (la.kind == 75 || la.kind == 76) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1747,11 +1757,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 70) {
+		if (la.kind == 71) {
 			Get();
-		} else if (la.kind == 71) {
+		} else if (la.kind == 72) {
 			Get();
-		} else SynErr(160);
+		} else SynErr(162);
 	}
 
 	void RelationalExpression(out Expression/*!*/ e) {
@@ -1845,25 +1855,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void AndOp() {
-		if (la.kind == 72) {
+		if (la.kind == 73) {
 			Get();
-		} else if (la.kind == 73) {
+		} else if (la.kind == 74) {
 			Get();
-		} else SynErr(161);
+		} else SynErr(163);
 	}
 
 	void OrOp() {
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
-		} else if (la.kind == 75) {
+		} else if (la.kind == 76) {
 			Get();
-		} else SynErr(162);
+		} else SynErr(164);
 	}
 
 	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 == 86 || la.kind == 87) {
+		while (la.kind == 87 || la.kind == 88) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -1876,50 +1886,50 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken y;
 		
 		switch (la.kind) {
-		case 76: {
+		case 77: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Eq; 
 			break;
 		}
-		case 22: {
+		case 23: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Lt; 
 			break;
 		}
-		case 23: {
+		case 24: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 77: {
+		case 78: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 78: {
+		case 79: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 79: {
+		case 80: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 80: {
+		case 81: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Disjoint; 
 			break;
 		}
-		case 81: {
+		case 82: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.In; 
 			break;
 		}
-		case 82: {
+		case 83: {
 			Get();
 			x = t;  y = Token.NoToken; 
-			if (la.kind == 81) {
+			if (la.kind == 82) {
 				Get();
 				y = t; 
 			}
@@ -1934,29 +1944,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 85: {
+		case 86: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(163); break;
+		default: SynErr(165); 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 == 45 || la.kind == 88 || la.kind == 89) {
+		while (la.kind == 46 || la.kind == 89 || la.kind == 90) {
 			MulOp(out x, out op);
 			UnaryExpression(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -1965,82 +1975,82 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 86) {
+		if (la.kind == 87) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Add; 
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Sub; 
-		} else SynErr(164);
+		} else SynErr(166);
 	}
 
 	void UnaryExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
 		switch (la.kind) {
-		case 87: {
+		case 88: {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 
 			break;
 		}
-		case 82: case 90: {
+		case 83: case 91: {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 
 			break;
 		}
-		case 19: case 38: case 57: case 63: case 64: case 65: case 100: case 101: case 102: case 103: {
+		case 20: case 39: case 58: case 64: case 65: case 66: case 101: case 102: case 103: case 104: {
 			EndlessExpression(out e);
 			break;
 		}
 		case 1: {
 			DottedIdentifiersAndFunction(out e);
-			while (la.kind == 53 || la.kind == 55) {
+			while (la.kind == 54 || la.kind == 56) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		case 6: case 53: {
+		case 6: case 54: {
 			DisplayExpr(out e);
 			break;
 		}
-		case 39: {
+		case 40: {
 			MultiSetExpr(out e);
 			break;
 		}
-		case 2: case 17: case 33: case 91: case 92: case 93: case 94: case 95: case 96: case 97: {
+		case 2: case 18: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
 			ConstAtomExpression(out e);
-			while (la.kind == 53 || la.kind == 55) {
+			while (la.kind == 54 || la.kind == 56) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		default: SynErr(165); break;
+		default: SynErr(167); 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 == 45) {
+		if (la.kind == 46) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mul; 
-		} else if (la.kind == 88) {
+		} else if (la.kind == 89) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Div; 
-		} else if (la.kind == 89) {
+		} else if (la.kind == 90) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mod; 
-		} else SynErr(166);
+		} else SynErr(168);
 	}
 
 	void NegOp() {
-		if (la.kind == 82) {
+		if (la.kind == 83) {
 			Get();
-		} else if (la.kind == 90) {
+		} else if (la.kind == 91) {
 			Get();
-		} else SynErr(167);
+		} else SynErr(169);
 	}
 
 	void EndlessExpression(out Expression e) {
@@ -2051,73 +2061,73 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;
 		
 		switch (la.kind) {
-		case 57: {
+		case 58: {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(98);
+			Expect(99);
 			Expression(out e0);
-			Expect(58);
+			Expect(59);
 			Expression(out e1);
 			e = new ITEExpr(x, e, e0, e1); 
 			break;
 		}
-		case 63: {
+		case 64: {
 			MatchExpression(out e);
 			break;
 		}
-		case 100: case 101: case 102: case 103: {
+		case 101: case 102: case 103: case 104: {
 			QuantifierGuts(out e);
 			break;
 		}
-		case 38: {
+		case 39: {
 			ComprehensionExpr(out e);
 			break;
 		}
-		case 64: {
+		case 65: {
 			Get();
 			x = t; 
 			Expression(out e0);
-			Expect(18);
+			Expect(19);
 			Expression(out e1);
 			e = new AssertExpr(x, e0, e1); 
 			break;
 		}
-		case 65: {
+		case 66: {
 			Get();
 			x = t; 
 			Expression(out e0);
-			Expect(18);
+			Expect(19);
 			Expression(out e1);
 			e = new AssumeExpr(x, e0, e1); 
 			break;
 		}
-		case 19: {
+		case 20: {
 			Get();
 			x = t;
 			letVars = new List<BoundVar>();
 			letRHSs = new List<Expression>(); 
 			IdentTypeOptional(out d);
 			letVars.Add(d); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				IdentTypeOptional(out d);
 				letVars.Add(d); 
 			}
-			Expect(50);
+			Expect(51);
 			Expression(out e);
 			letRHSs.Add(e); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				Expression(out e);
 				letRHSs.Add(e); 
 			}
-			Expect(18);
+			Expect(19);
 			Expression(out e);
 			e = new LetExpr(x, letVars, letRHSs, e); 
 			break;
 		}
-		default: SynErr(168); break;
+		default: SynErr(170); break;
 		}
 	}
 
@@ -2128,18 +2138,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		Ident(out id);
 		idents.Add(id); 
-		while (la.kind == 55) {
+		while (la.kind == 56) {
 			Get();
 			Ident(out id);
 			idents.Add(id); 
 		}
-		if (la.kind == 33) {
+		if (la.kind == 34) {
 			Get();
 			openParen = t;  args = new List<Expression>(); 
 			if (StartOf(9)) {
 				Expressions(args);
 			}
-			Expect(34);
+			Expect(35);
 		}
 		e = new IdentifierSequence(idents, openParen, args); 
 	}
@@ -2150,38 +2160,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> multipleIndices = null;
 		bool func = false;
 		
-		if (la.kind == 55) {
+		if (la.kind == 56) {
 			Get();
 			Ident(out id);
-			if (la.kind == 33) {
+			if (la.kind == 34) {
 				Get();
 				IToken openParen = t;  args = new List<Expression/*!*/>();  func = true; 
 				if (StartOf(9)) {
 					Expressions(args);
 				}
-				Expect(34);
+				Expect(35);
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 
 			}
 			if (!func) { e = new ExprDotName(id, e, id.val); } 
-		} else if (la.kind == 53) {
+		} else if (la.kind == 54) {
 			Get();
 			x = t; 
 			if (StartOf(9)) {
 				Expression(out ee);
 				e0 = ee; 
-				if (la.kind == 99) {
+				if (la.kind == 100) {
 					Get();
 					anyDots = true; 
 					if (StartOf(9)) {
 						Expression(out ee);
 						e1 = ee; 
 					}
-				} else if (la.kind == 50) {
+				} else if (la.kind == 51) {
 					Get();
 					Expression(out ee);
 					e1 = ee; 
-				} else if (la.kind == 20 || la.kind == 54) {
-					while (la.kind == 20) {
+				} else if (la.kind == 21 || la.kind == 55) {
+					while (la.kind == 21) {
 						Get();
 						Expression(out ee);
 						if (multipleIndices == null) {
@@ -2191,15 +2201,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(169);
-			} else if (la.kind == 99) {
+				} else SynErr(171);
+			} else if (la.kind == 100) {
 				Get();
 				anyDots = true; 
 				if (StartOf(9)) {
 					Expression(out ee);
 					e1 = ee; 
 				}
-			} else SynErr(170);
+			} else SynErr(172);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			 // make sure an array class with this dimensionality exists
@@ -2222,8 +2232,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }
 			}
 			
-			Expect(54);
-		} else SynErr(171);
+			Expect(55);
+		} else SynErr(173);
 	}
 
 	void DisplayExpr(out Expression e) {
@@ -2239,15 +2249,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			e = new SetDisplayExpr(x, elements);
 			Expect(7);
-		} else if (la.kind == 53) {
+		} else if (la.kind == 54) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(9)) {
 				Expressions(elements);
 			}
 			e = new SeqDisplayExpr(x, elements); 
-			Expect(54);
-		} else SynErr(172);
+			Expect(55);
+		} else SynErr(174);
 	}
 
 	void MultiSetExpr(out Expression e) {
@@ -2255,7 +2265,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
 		e = dummyExpr;
 		
-		Expect(39);
+		Expect(40);
 		x = t; 
 		if (la.kind == 6) {
 			Get();
@@ -2265,15 +2275,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			e = new MultiSetDisplayExpr(x, elements);
 			Expect(7);
-		} 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);
+			Expect(35);
 		} else if (StartOf(19)) {
 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 
-		} else SynErr(173);
+		} else SynErr(175);
 	}
 
 	void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2282,17 +2292,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;
 		
 		switch (la.kind) {
-		case 91: {
+		case 92: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 92: {
+		case 93: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 93: {
+		case 94: {
 			Get();
 			e = new LiteralExpr(t); 
 			break;
@@ -2302,55 +2312,55 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 
 			break;
 		}
-		case 94: {
+		case 95: {
 			Get();
 			e = new ThisExpr(t); 
 			break;
 		}
-		case 95: {
+		case 96: {
 			Get();
 			x = t; 
-			Expect(33);
-			Expression(out e);
 			Expect(34);
+			Expression(out e);
+			Expect(35);
 			e = new FreshExpr(x, e); 
 			break;
 		}
-		case 96: {
+		case 97: {
 			Get();
 			x = t; 
-			Expect(33);
-			Expression(out e);
 			Expect(34);
+			Expression(out e);
+			Expect(35);
 			e = new AllocatedExpr(x, e); 
 			break;
 		}
-		case 97: {
+		case 98: {
 			Get();
 			x = t; 
-			Expect(33);
-			Expression(out e);
 			Expect(34);
+			Expression(out e);
+			Expect(35);
 			e = new OldExpr(x, e); 
 			break;
 		}
-		case 17: {
+		case 18: {
 			Get();
 			x = t; 
 			Expression(out e);
 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 
-			Expect(17);
+			Expect(18);
 			break;
 		}
-		case 33: {
+		case 34: {
 			Get();
 			x = t; 
 			Expression(out e);
 			e = new ParensExpression(x, e); 
-			Expect(34);
+			Expect(35);
 			break;
 		}
-		default: SynErr(174); break;
+		default: SynErr(176); break;
 		}
 	}
 
@@ -2369,10 +2379,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
 		
-		Expect(63);
+		Expect(64);
 		x = t; 
 		Expression(out e);
-		while (la.kind == 59) {
+		while (la.kind == 60) {
 			CaseExpression(out c);
 			cases.Add(c); 
 		}
@@ -2387,13 +2397,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;
 		Expression/*!*/ body;
 		
-		if (la.kind == 100 || la.kind == 101) {
+		if (la.kind == 101 || la.kind == 102) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 102 || la.kind == 103) {
+		} else if (la.kind == 103 || la.kind == 104) {
 			Exists();
 			x = t; 
-		} else SynErr(175);
+		} else SynErr(177);
 		QuantifierDomain(out bvars, out attrs, out range);
 		QSep();
 		Expression(out body);
@@ -2413,18 +2423,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;
 		Expression body = null;
 		
-		Expect(38);
+		Expect(39);
 		x = t; 
 		IdentTypeOptional(out bv);
 		bvars.Add(bv); 
-		while (la.kind == 20) {
+		while (la.kind == 21) {
 			Get();
 			IdentTypeOptional(out bv);
 			bvars.Add(bv); 
 		}
-		Expect(17);
+		Expect(18);
 		Expression(out range);
-		if (la.kind == 104 || la.kind == 105) {
+		if (la.kind == 105 || la.kind == 106) {
 			QSep();
 			Expression(out body);
 		}
@@ -2439,47 +2449,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;
 		Expression/*!*/ body;
 		
-		Expect(59);
+		Expect(60);
 		x = t; 
 		Ident(out id);
-		if (la.kind == 33) {
+		if (la.kind == 34) {
 			Get();
 			IdentTypeOptional(out bv);
 			arguments.Add(bv); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				IdentTypeOptional(out bv);
 				arguments.Add(bv); 
 			}
-			Expect(34);
+			Expect(35);
 		}
-		Expect(60);
+		Expect(61);
 		Expression(out body);
 		c = new MatchCaseExpr(x, id.val, arguments, body); 
 	}
 
 	void Forall() {
-		if (la.kind == 100) {
+		if (la.kind == 101) {
 			Get();
-		} else if (la.kind == 101) {
+		} else if (la.kind == 102) {
 			Get();
-		} else SynErr(176);
+		} else SynErr(178);
 	}
 
 	void Exists() {
-		if (la.kind == 102) {
+		if (la.kind == 103) {
 			Get();
-		} else if (la.kind == 103) {
+		} else if (la.kind == 104) {
 			Get();
-		} else SynErr(177);
+		} else SynErr(179);
 	}
 
 	void QSep() {
-		if (la.kind == 104) {
+		if (la.kind == 105) {
 			Get();
-		} else if (la.kind == 105) {
+		} else if (la.kind == 106) {
 			Get();
-		} else SynErr(178);
+		} else SynErr(180);
 	}
 
 	void AttributeBody(ref Attributes attrs) {
@@ -2493,7 +2503,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (StartOf(20)) {
 			AttributeArg(out aArg);
 			aArgs.Add(aArg); 
-			while (la.kind == 20) {
+			while (la.kind == 21) {
 				Get();
 				AttributeArg(out aArg);
 				aArgs.Add(aArg); 
@@ -2515,27 +2525,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,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,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,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,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,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,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, 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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,x,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, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, 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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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,T,x, T,x,x,x, T,x,x,T, T,x,T,T, T,x,x,x, x,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, 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,x,x,x, T,T,x,x, T,T,T,T, T,x,x,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, T,x,x,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, T,x,x,x, T,x,T,T, x,T,T,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,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, 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,T,x, T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,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,T,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,T,T,x, x,x,T,x, T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,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,T,x, 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, x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,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,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,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, 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
@@ -2576,169 +2586,171 @@ public class Errors {
 			case 13: s = "\"static\" expected"; break;
 			case 14: s = "\"unlimited\" expected"; break;
 			case 15: s = "\"datatype\" expected"; break;
-			case 16: s = "\"=\" expected"; break;
-			case 17: s = "\"|\" expected"; break;
-			case 18: s = "\";\" expected"; break;
-			case 19: s = "\"var\" expected"; break;
-			case 20: s = "\",\" expected"; break;
-			case 21: s = "\"type\" expected"; break;
-			case 22: s = "\"<\" expected"; break;
-			case 23: s = "\">\" expected"; break;
-			case 24: s = "\"method\" expected"; break;
-			case 25: s = "\"constructor\" expected"; break;
-			case 26: s = "\"returns\" expected"; break;
-			case 27: s = "\"...\" 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 = "\"predicate\" 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 = "\":|\" expected"; break;
-			case 52: s = "\"new\" expected"; break;
-			case 53: s = "\"[\" expected"; break;
-			case 54: s = "\"]\" expected"; break;
-			case 55: s = "\".\" expected"; break;
-			case 56: s = "\"choose\" expected"; break;
-			case 57: s = "\"if\" expected"; break;
-			case 58: s = "\"else\" expected"; break;
-			case 59: s = "\"case\" expected"; break;
-			case 60: s = "\"=>\" expected"; break;
-			case 61: s = "\"while\" expected"; break;
-			case 62: s = "\"invariant\" expected"; break;
-			case 63: s = "\"match\" expected"; break;
-			case 64: s = "\"assert\" expected"; break;
-			case 65: s = "\"assume\" expected"; break;
-			case 66: s = "\"print\" expected"; break;
-			case 67: s = "\"parallel\" expected"; break;
-			case 68: s = "\"<==>\" expected"; break;
-			case 69: s = "\"\\u21d4\" expected"; break;
-			case 70: s = "\"==>\" expected"; break;
-			case 71: s = "\"\\u21d2\" expected"; break;
-			case 72: s = "\"&&\" expected"; break;
-			case 73: s = "\"\\u2227\" expected"; break;
-			case 74: s = "\"||\" expected"; break;
-			case 75: s = "\"\\u2228\" 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 = "\"!!\" expected"; break;
-			case 81: s = "\"in\" expected"; break;
-			case 82: s = "\"!\" expected"; break;
-			case 83: s = "\"\\u2260\" expected"; break;
-			case 84: s = "\"\\u2264\" expected"; break;
-			case 85: s = "\"\\u2265\" expected"; break;
-			case 86: s = "\"+\" expected"; break;
-			case 87: s = "\"-\" expected"; break;
-			case 88: s = "\"/\" expected"; break;
-			case 89: s = "\"%\" expected"; break;
-			case 90: s = "\"\\u00ac\" expected"; break;
-			case 91: s = "\"false\" expected"; break;
-			case 92: s = "\"true\" expected"; break;
-			case 93: s = "\"null\" expected"; break;
-			case 94: s = "\"this\" expected"; break;
-			case 95: s = "\"fresh\" expected"; break;
-			case 96: s = "\"allocated\" expected"; break;
-			case 97: s = "\"old\" expected"; break;
-			case 98: s = "\"then\" expected"; break;
-			case 99: s = "\"..\" expected"; break;
-			case 100: s = "\"forall\" expected"; break;
-			case 101: s = "\"\\u2200\" expected"; break;
-			case 102: s = "\"exists\" expected"; break;
-			case 103: s = "\"\\u2203\" expected"; break;
-			case 104: s = "\"::\" expected"; break;
-			case 105: s = "\"\\u2022\" expected"; break;
-			case 106: s = "??? expected"; break;
-			case 107: s = "invalid Dafny"; break;
-			case 108: s = "this symbol not expected in ClassDecl"; break;
-			case 109: s = "this symbol not expected in DatatypeDecl"; break;
+			case 16: s = "\"codatatype\" expected"; break;
+			case 17: s = "\"=\" expected"; break;
+			case 18: s = "\"|\" expected"; break;
+			case 19: s = "\";\" expected"; break;
+			case 20: s = "\"var\" expected"; break;
+			case 21: s = "\",\" expected"; break;
+			case 22: s = "\"type\" 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 = "\"...\" 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 = "\"predicate\" expected"; break;
+			case 45: s = "\"reads\" expected"; break;
+			case 46: s = "\"*\" expected"; break;
+			case 47: s = "\"`\" expected"; break;
+			case 48: s = "\"label\" expected"; break;
+			case 49: s = "\"break\" expected"; break;
+			case 50: s = "\"return\" expected"; break;
+			case 51: s = "\":=\" expected"; break;
+			case 52: s = "\":|\" expected"; break;
+			case 53: s = "\"new\" expected"; break;
+			case 54: s = "\"[\" expected"; break;
+			case 55: s = "\"]\" expected"; break;
+			case 56: s = "\".\" expected"; break;
+			case 57: s = "\"choose\" expected"; break;
+			case 58: s = "\"if\" expected"; break;
+			case 59: s = "\"else\" expected"; break;
+			case 60: s = "\"case\" expected"; break;
+			case 61: s = "\"=>\" expected"; break;
+			case 62: s = "\"while\" expected"; break;
+			case 63: s = "\"invariant\" expected"; break;
+			case 64: s = "\"match\" expected"; break;
+			case 65: s = "\"assert\" expected"; break;
+			case 66: s = "\"assume\" expected"; break;
+			case 67: s = "\"print\" expected"; break;
+			case 68: s = "\"parallel\" expected"; break;
+			case 69: s = "\"<==>\" expected"; break;
+			case 70: s = "\"\\u21d4\" expected"; break;
+			case 71: s = "\"==>\" expected"; break;
+			case 72: s = "\"\\u21d2\" expected"; break;
+			case 73: s = "\"&&\" expected"; break;
+			case 74: s = "\"\\u2227\" expected"; break;
+			case 75: s = "\"||\" expected"; break;
+			case 76: s = "\"\\u2228\" expected"; break;
+			case 77: s = "\"==\" expected"; break;
+			case 78: s = "\"<=\" expected"; break;
+			case 79: s = "\">=\" expected"; break;
+			case 80: s = "\"!=\" expected"; break;
+			case 81: s = "\"!!\" expected"; break;
+			case 82: s = "\"in\" expected"; break;
+			case 83: s = "\"!\" expected"; break;
+			case 84: s = "\"\\u2260\" expected"; break;
+			case 85: s = "\"\\u2264\" expected"; break;
+			case 86: s = "\"\\u2265\" expected"; break;
+			case 87: s = "\"+\" expected"; break;
+			case 88: s = "\"-\" expected"; break;
+			case 89: s = "\"/\" expected"; break;
+			case 90: s = "\"%\" expected"; break;
+			case 91: s = "\"\\u00ac\" expected"; break;
+			case 92: s = "\"false\" expected"; break;
+			case 93: s = "\"true\" expected"; break;
+			case 94: s = "\"null\" expected"; break;
+			case 95: s = "\"this\" expected"; break;
+			case 96: s = "\"fresh\" expected"; break;
+			case 97: s = "\"allocated\" expected"; break;
+			case 98: s = "\"old\" expected"; break;
+			case 99: s = "\"then\" expected"; break;
+			case 100: s = "\"..\" expected"; break;
+			case 101: s = "\"forall\" expected"; break;
+			case 102: s = "\"\\u2200\" expected"; break;
+			case 103: s = "\"exists\" expected"; break;
+			case 104: s = "\"\\u2203\" expected"; break;
+			case 105: s = "\"::\" expected"; break;
+			case 106: s = "\"\\u2022\" expected"; break;
+			case 107: s = "??? expected"; break;
+			case 108: s = "invalid Dafny"; break;
+			case 109: s = "this symbol not expected in ClassDecl"; break;
 			case 110: s = "this symbol not expected in DatatypeDecl"; break;
-			case 111: s = "this symbol not expected in ArbitraryTypeDecl"; break;
-			case 112: s = "invalid ClassMemberDecl"; break;
-			case 113: s = "this symbol not expected in FieldDecl"; break;
-			case 114: s = "this symbol not expected in FieldDecl"; break;
-			case 115: s = "invalid FunctionDecl"; break;
-			case 116: s = "invalid FunctionDecl"; break;
+			case 111: s = "invalid DatatypeDecl"; break;
+			case 112: s = "this symbol not expected in DatatypeDecl"; break;
+			case 113: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+			case 114: s = "invalid ClassMemberDecl"; break;
+			case 115: s = "this symbol not expected in FieldDecl"; break;
+			case 116: s = "this symbol not expected in FieldDecl"; break;
 			case 117: s = "invalid FunctionDecl"; break;
-			case 118: s = "this symbol not expected in MethodDecl"; break;
-			case 119: s = "invalid MethodDecl"; break;
-			case 120: s = "invalid MethodDecl"; break;
-			case 121: s = "invalid TypeAndToken"; break;
-			case 122: s = "this symbol not expected in MethodSpec"; break;
-			case 123: s = "this symbol not expected in MethodSpec"; break;
+			case 118: s = "invalid FunctionDecl"; break;
+			case 119: s = "invalid FunctionDecl"; break;
+			case 120: s = "this symbol not expected in MethodDecl"; break;
+			case 121: s = "invalid MethodDecl"; break;
+			case 122: s = "invalid MethodDecl"; break;
+			case 123: s = "invalid TypeAndToken"; break;
 			case 124: s = "this symbol not expected in MethodSpec"; break;
 			case 125: s = "this symbol not expected in MethodSpec"; break;
-			case 126: s = "invalid MethodSpec"; break;
+			case 126: s = "this symbol not expected in MethodSpec"; break;
 			case 127: s = "this symbol not expected in MethodSpec"; break;
 			case 128: s = "invalid MethodSpec"; break;
-			case 129: s = "invalid ReferenceType"; break;
-			case 130: s = "this symbol not expected in FunctionSpec"; break;
-			case 131: s = "this symbol not expected in FunctionSpec"; break;
+			case 129: s = "this symbol not expected in MethodSpec"; break;
+			case 130: s = "invalid MethodSpec"; break;
+			case 131: s = "invalid ReferenceType"; break;
 			case 132: s = "this symbol not expected in FunctionSpec"; break;
 			case 133: s = "this symbol not expected in FunctionSpec"; break;
 			case 134: s = "this symbol not expected in FunctionSpec"; break;
-			case 135: s = "invalid FunctionSpec"; break;
-			case 136: s = "invalid PossiblyWildFrameExpression"; break;
-			case 137: s = "invalid PossiblyWildExpression"; break;
-			case 138: s = "this symbol not expected in OneStmt"; break;
-			case 139: s = "invalid OneStmt"; break;
+			case 135: s = "this symbol not expected in FunctionSpec"; break;
+			case 136: s = "this symbol not expected in FunctionSpec"; break;
+			case 137: s = "invalid FunctionSpec"; break;
+			case 138: s = "invalid PossiblyWildFrameExpression"; break;
+			case 139: s = "invalid PossiblyWildExpression"; break;
 			case 140: s = "this symbol not expected in OneStmt"; break;
 			case 141: s = "invalid OneStmt"; break;
-			case 142: s = "invalid AssertStmt"; break;
-			case 143: s = "invalid UpdateStmt"; break;
-			case 144: s = "invalid UpdateStmt"; break;
-			case 145: s = "invalid IfStmt"; break;
-			case 146: s = "invalid IfStmt"; break;
-			case 147: s = "invalid WhileStmt"; break;
-			case 148: s = "invalid WhileStmt"; break;
-			case 149: s = "invalid Rhs"; break;
-			case 150: s = "invalid Lhs"; break;
-			case 151: s = "invalid Guard"; break;
-			case 152: s = "this symbol not expected in LoopSpec"; break;
-			case 153: s = "this symbol not expected in LoopSpec"; break;
+			case 142: s = "this symbol not expected in OneStmt"; break;
+			case 143: s = "invalid OneStmt"; break;
+			case 144: s = "invalid AssertStmt"; break;
+			case 145: s = "invalid UpdateStmt"; break;
+			case 146: s = "invalid UpdateStmt"; break;
+			case 147: s = "invalid IfStmt"; break;
+			case 148: s = "invalid IfStmt"; break;
+			case 149: s = "invalid WhileStmt"; break;
+			case 150: s = "invalid WhileStmt"; break;
+			case 151: s = "invalid Rhs"; break;
+			case 152: s = "invalid Lhs"; break;
+			case 153: s = "invalid Guard"; break;
 			case 154: s = "this symbol not expected in LoopSpec"; break;
 			case 155: s = "this symbol not expected in LoopSpec"; break;
 			case 156: s = "this symbol not expected in LoopSpec"; break;
-			case 157: s = "this symbol not expected in Invariant"; break;
-			case 158: s = "invalid AttributeArg"; break;
-			case 159: s = "invalid EquivOp"; break;
-			case 160: s = "invalid ImpliesOp"; break;
-			case 161: s = "invalid AndOp"; break;
-			case 162: s = "invalid OrOp"; break;
-			case 163: s = "invalid RelOp"; break;
-			case 164: s = "invalid AddOp"; break;
-			case 165: s = "invalid UnaryExpression"; break;
-			case 166: s = "invalid MulOp"; break;
-			case 167: s = "invalid NegOp"; break;
-			case 168: s = "invalid EndlessExpression"; break;
-			case 169: s = "invalid Suffix"; break;
-			case 170: s = "invalid Suffix"; break;
+			case 157: s = "this symbol not expected in LoopSpec"; break;
+			case 158: s = "this symbol not expected in LoopSpec"; break;
+			case 159: s = "this symbol not expected in Invariant"; break;
+			case 160: s = "invalid AttributeArg"; break;
+			case 161: s = "invalid EquivOp"; break;
+			case 162: s = "invalid ImpliesOp"; break;
+			case 163: s = "invalid AndOp"; break;
+			case 164: s = "invalid OrOp"; break;
+			case 165: s = "invalid RelOp"; break;
+			case 166: s = "invalid AddOp"; break;
+			case 167: s = "invalid UnaryExpression"; break;
+			case 168: s = "invalid MulOp"; break;
+			case 169: s = "invalid NegOp"; break;
+			case 170: s = "invalid EndlessExpression"; break;
 			case 171: s = "invalid Suffix"; break;
-			case 172: s = "invalid DisplayExpr"; break;
-			case 173: s = "invalid MultiSetExpr"; break;
-			case 174: s = "invalid ConstAtomExpression"; break;
-			case 175: s = "invalid QuantifierGuts"; break;
-			case 176: s = "invalid Forall"; break;
-			case 177: s = "invalid Exists"; break;
-			case 178: s = "invalid QSep"; break;
+			case 172: s = "invalid Suffix"; break;
+			case 173: s = "invalid Suffix"; break;
+			case 174: s = "invalid DisplayExpr"; break;
+			case 175: s = "invalid MultiSetExpr"; break;
+			case 176: s = "invalid ConstAtomExpression"; break;
+			case 177: s = "invalid QuantifierGuts"; break;
+			case 178: s = "invalid Forall"; break;
+			case 179: s = "invalid Exists"; break;
+			case 180: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 015bd490..2c6fb96a 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -158,7 +158,7 @@ namespace Microsoft.Dafny {
     public void PrintDatatype(DatatypeDecl dt, int indent) {
       Contract.Requires(dt != null);
       Indent(indent);
-      PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs);
+      PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
       wr.Write(" =");
       string sep = "";
       foreach (DatatypeCtor ctor in dt.Ctors) {
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index a10cb4bf..c73ffda8 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -136,11 +136,17 @@ namespace Microsoft.Dafny {
       if (d is ArbitraryTypeDecl) {
         var dd = (ArbitraryTypeDecl)d;
         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
-      } else if (d is DatatypeDecl) {
-        var dd = (DatatypeDecl)d;
+      } else if (d is IndDatatypeDecl) {
+        var dd = (IndDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
         var ctors = dd.Ctors.ConvertAll(CloneCtor);
-        var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+        return dt;
+      } else if (d is CoDatatypeDecl) {
+        var dd = (CoDatatypeDecl)d;
+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+        var ctors = dd.Ctors.ConvertAll(CloneCtor);
+        var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
         return dt;
       } else if (d is ClassDecl) {
         var dd = (ClassDecl)d;
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index adf530aa..8ab946dc 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -173,7 +173,6 @@ namespace Microsoft.Dafny {
       Rewriter rewriter = new AutoContractsRewriter();
       var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);
       var moduleNameInfo = new ModuleNameInformation[h];
-      var datatypeDependencies = new Graph<DatatypeDecl>();
       foreach (var m in mm) {
         rewriter.PreResolve(m);
         if (m.RefinementBase != null) {
@@ -181,15 +180,13 @@ namespace Microsoft.Dafny {
           transformer.Construct(m);
         }
         moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);
-//      }
 
-      // resolve top-level declarations
-//      foreach (ModuleDecl m in mm) {
         // set up environment
         ModuleNameInformation info = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo);
         classes = info.Classes;
         allDatatypeCtors = info.Ctors;
         // resolve
+        var datatypeDependencies = new Graph<IndDatatypeDecl>();
         ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
         // tear down
@@ -362,9 +359,9 @@ namespace Microsoft.Dafny {
       return info;
     }
 
-    public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
+    public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
       Contract.Requires(declarations != null);
-      Contract.Requires(cce.NonNullElements(datatypeDependencies));
+      Contract.Requires(datatypeDependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));
       foreach (TopLevelDecl d in declarations) {
         Contract.Assert(d != null);
         allTypeParameters.PushMarker();
@@ -380,26 +377,28 @@ namespace Microsoft.Dafny {
       }
     }
 
-    public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
+    public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
       Contract.Requires(declarations != null);
       Contract.Requires(cce.NonNullElements(datatypeDependencies));
+
+      // Resolve the meat of classes, and the type parameters of all top-level type declarations
       foreach (TopLevelDecl d in declarations) {
         Contract.Assert(d != null);
         allTypeParameters.PushMarker();
         ResolveTypeParameters(d.TypeArgs, false, d);
-        if (d is ArbitraryTypeDecl) {
-          // nothing to do
-        } else if (d is ClassDecl) {
+        if (d is ClassDecl) {
           ResolveClassMemberBodies((ClassDecl)d);
-        } else {
-          DatatypeDecl dtd = (DatatypeDecl)d;
-          if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
-            // do the following check once per SCC, so call it on each SCC representative
-            SccStratosphereCheck(dtd, datatypeDependencies);
-          }
         }
         allTypeParameters.PopMarker();
       }
+
+      // Perform the stratosphere check on inductive datatypes
+      foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
+        if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
+          // do the following check once per SCC, so call it on each SCC representative
+          SccStratosphereCheck(dtd, datatypeDependencies);
+        }
+      }
     }
 
     ClassDecl currentClass;
@@ -485,10 +484,10 @@ namespace Microsoft.Dafny {
     /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
-    void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)
+    void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies)
     {
       Contract.Requires(dt != null);
-      Contract.Requires(cce.NonNullElements(dependencies));
+      Contract.Requires(dependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
       foreach (DatatypeCtor ctor in dt.Ctors) {
 
         ctor.EnclosingDatatype = dt;
@@ -497,47 +496,72 @@ namespace Microsoft.Dafny {
         ResolveCtorSignature(ctor, dt.TypeArgs);
         allTypeParameters.PopMarker();
 
-        foreach (Formal p in ctor.Formals) {
-          DatatypeDecl dependee = p.Type.AsDatatype;
-          if (dependee != null) {
-            dependencies.AddEdge(dt, dependee);
+        if (dt is IndDatatypeDecl) {
+          foreach (Formal p in ctor.Formals) {
+            AddDatatypeDependencyEdge((IndDatatypeDecl)dt, p.Type, dependencies);
           }
         }
       }
     }
 
+    void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
+      Contract.Requires(dt != null);
+      Contract.Requires(tp != null);
+      Contract.Requires(dependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+
+      var dependee = tp.AsIndDatatype;
+      if (dependee != null && dt.Module == dependee.Module) {
+        dependencies.AddEdge((IndDatatypeDecl)dt, dependee);
+        foreach (var ta in ((UserDefinedType)tp).TypeArgs) {
+          AddDatatypeDependencyEdge(dt, ta, dependencies);
+        }
+      }
+    }
+
     /// <summary>
     /// Check that the SCC of 'startingPoint' can be carved up into stratospheres in such a way that each
     /// datatype has some value that can be constructed from datatypes in lower stratospheres only.
     /// The algorithm used here is quadratic in the number of datatypes in the SCC.  Since that number is
     /// deemed to be rather small, this seems okay.
+    /// 
+    /// As a side effect of this checking, the DefaultCtor field is filled in (for every inductive datatype
+    /// that passes the check).  It may be that several constructors could be used as the default, but
+    /// only the first one encountered as recorded.  This particular choice is slightly more than an
+    /// implementation detail, because it affects how certain cycles among inductive datatypes (having
+    /// to do with the types used to instantiate type parameters of datatypes) are used.
+    /// 
+    /// The role of the SCC here is simply to speed up this method.  It would still be correct if the
+    /// equivalence classes in the given SCC were unions of actual SCC's.  In particular, this method
+    /// would still work if "dependencies" consisted of one large SCC containing all the inductive
+    /// datatypes in the module.
     /// </summary>
-    void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)
+    void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies)
     {
       Contract.Requires(startingPoint != null);
-      Contract.Requires(cce.NonNullElements(dependencies));
-      List<DatatypeDecl> scc = dependencies.GetSCC(startingPoint);
-      List<DatatypeDecl> cleared = new List<DatatypeDecl>();  // this is really a set
+      Contract.Requires(dependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+
+      var scc = dependencies.GetSCC(startingPoint);
+      int totalCleared = 0;
       while (true) {
         int clearedThisRound = 0;
-        foreach (DatatypeDecl dt in scc) {
-          if (cleared.Contains(dt)) {
+        foreach (var dt in scc) {
+          if (dt.DefaultCtor != null) {
             // previously cleared
-          } else if (StratosphereCheck(dt, dependencies, cleared)) {
+          } else if (ComputeDefaultCtor(dt)) {
+            Contract.Assert(dt.DefaultCtor != null);  // should have been set by the successful call to StratosphereCheck)
             clearedThisRound++;
-            cleared.Add(dt);
-            // (it would be nice if the List API allowed us to remove 'dt' from 'scc' here; then we wouldn't have to check 'cleared.Contains(dt)' above and below)
+            totalCleared++;
           }
         }
-        if (cleared.Count == scc.Count) {
+        if (totalCleared == scc.Count) {
           // all is good
           return;
         } else if (clearedThisRound != 0) {
           // some progress was made, so let's keep going
         } else {
           // whatever is in scc-cleared now failed to pass the test
-          foreach (DatatypeDecl dt in scc) {
-            if (!cleared.Contains(dt)) {
+          foreach (var dt in scc) {
+            if (dt.DefaultCtor == null) {
               Error(dt, "because of cyclic dependencies among constructor argument types, no instances of datatype '{0}' can be constructed", dt.Name);
             }
           }
@@ -547,33 +571,29 @@ namespace Microsoft.Dafny {
     }
 
     /// <summary>
-    /// Check that the datatype has some constructor all whose argument types go to a lower stratum, which means
-    /// go to a different SCC or to a type in 'goodOnes'.
+    /// Check that the datatype has some constructor all whose argument types can be constructed.
     /// Returns 'true' and sets dt.DefaultCtor if that is the case.
     /// </summary>
-    bool StratosphereCheck(DatatypeDecl dt, Graph<DatatypeDecl/*!*/>/*!*/ dependencies, List<DatatypeDecl/*!*/>/*!*/ goodOnes) {
+    bool ComputeDefaultCtor(IndDatatypeDecl dt) {
       Contract.Requires(dt != null);
-      Contract.Requires(cce.NonNullElements(dependencies));
-      Contract.Requires(cce.NonNullElements(goodOnes));
+      Contract.Requires(dt.DefaultCtor == null);  // the intention is that this method be called only when DefaultCtor hasn't already been set
+      Contract.Ensures(!Contract.Result<bool>() || dt.DefaultCtor != null);
+
       // Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
-      DatatypeDecl stratumRepresentative = dependencies.GetSCCRepresentative(dt);
       foreach (DatatypeCtor ctor in dt.Ctors) {
+        var typeParametersUsed = new List<TypeParameter>();
         foreach (Formal p in ctor.Formals) {
-          DatatypeDecl dependee = p.Type.AsDatatype;
-          if (dependee == null) {
-            // the type is not a datatype, which means it's in the lowest stratum (below all datatypes)
-          } else if (dependencies.GetSCCRepresentative(dependee) != stratumRepresentative) {
-            // the argument type goes to a different stratum, which must be a "lower" one, so this argument is fine
-          } else if (goodOnes.Contains(dependee)) {
-            // the argument type is in the same SCC, but has already passed the test, so it is to be considered as
-            // being in a lower stratum
-          } else {
-            // the argument type is in the same stratum as 'dt', so this constructor is not what we're looking for
+          if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) {
+            // the argument type (has a component which) is not yet known to be constructable
             goto NEXT_OUTER_ITERATION;
           }
         }
         // this constructor satisfies the requirements, so the datatype is allowed
         dt.DefaultCtor = ctor;
+        dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count];
+        for (int i = 0; i < dt.TypeArgs.Count; i++) {
+          dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
+        }
         return true;
         NEXT_OUTER_ITERATION: {}
       }
@@ -581,6 +601,30 @@ namespace Microsoft.Dafny {
       return false;
     }
 
+    bool CheckCanBeConstructed(Type tp, List<TypeParameter> typeParametersUsed) {
+      var dependee = tp.AsIndDatatype;
+      if (dependee == null) {
+        // the type is not an inductive datatype, which means it is always possible to construct it
+        if (tp.IsTypeParameter) {
+          typeParametersUsed.Add(((UserDefinedType)tp).ResolvedParam);
+        }
+        return true;
+      } else if (dependee.DefaultCtor == null) {
+        // the type is an inductive datatype that we don't yet know how to construct
+        return false;
+      }
+      // also check the type arguments of the inductive datatype
+      Contract.Assert(((UserDefinedType)tp).TypeArgs.Count == dependee.TypeParametersUsedInConstructionByDefaultCtor.Length);
+      var i = 0;
+      foreach (var ta in ((UserDefinedType)tp).TypeArgs) {  // note, "tp" is known to be a UserDefinedType, because that follows from tp being an inductive datatype
+        if (dependee.TypeParametersUsedInConstructionByDefaultCtor[i] && !CheckCanBeConstructed(ta, typeParametersUsed)) {
+          return false;
+        }
+        i++;
+      }
+      return true;
+    }
+
     void ResolveAttributes(Attributes attrs, bool twoState) {
       // order does not matter much for resolution, so resolve them in reverse order
       for (; attrs != null; attrs = attrs.Prev) {
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index ca2ae13c..ffc6f4b0 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 = 106;
-	const int noSym = 106;
+	const int maxT = 107;
+	const int noSym = 107;
 
 
 	[ContractInvariantMethod]
@@ -496,52 +496,53 @@ public class Scanner {
 			case "static": t.kind = 13; break;
 			case "unlimited": t.kind = 14; break;
 			case "datatype": t.kind = 15; break;
-			case "var": t.kind = 19; break;
-			case "type": t.kind = 21; break;
-			case "method": t.kind = 24; break;
-			case "constructor": t.kind = 25; break;
-			case "returns": t.kind = 26; 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 "predicate": 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 = 52; break;
-			case "choose": t.kind = 56; break;
-			case "if": t.kind = 57; break;
-			case "else": t.kind = 58; break;
-			case "case": t.kind = 59; break;
-			case "while": t.kind = 61; break;
-			case "invariant": t.kind = 62; break;
-			case "match": t.kind = 63; break;
-			case "assert": t.kind = 64; break;
-			case "assume": t.kind = 65; break;
-			case "print": t.kind = 66; break;
-			case "parallel": t.kind = 67; break;
-			case "in": t.kind = 81; break;
-			case "false": t.kind = 91; break;
-			case "true": t.kind = 92; break;
-			case "null": t.kind = 93; break;
-			case "this": t.kind = 94; break;
-			case "fresh": t.kind = 95; break;
-			case "allocated": t.kind = 96; break;
-			case "old": t.kind = 97; break;
-			case "then": t.kind = 98; break;
-			case "forall": t.kind = 100; break;
-			case "exists": t.kind = 102; break;
+			case "codatatype": t.kind = 16; break;
+			case "var": t.kind = 20; break;
+			case "type": t.kind = 22; break;
+			case "method": t.kind = 25; break;
+			case "constructor": t.kind = 26; break;
+			case "returns": t.kind = 27; 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 "predicate": t.kind = 44; break;
+			case "reads": t.kind = 45; break;
+			case "label": t.kind = 48; break;
+			case "break": t.kind = 49; break;
+			case "return": t.kind = 50; break;
+			case "new": t.kind = 53; break;
+			case "choose": t.kind = 57; break;
+			case "if": t.kind = 58; break;
+			case "else": t.kind = 59; break;
+			case "case": t.kind = 60; break;
+			case "while": t.kind = 62; break;
+			case "invariant": t.kind = 63; break;
+			case "match": t.kind = 64; break;
+			case "assert": t.kind = 65; break;
+			case "assume": t.kind = 66; break;
+			case "print": t.kind = 67; break;
+			case "parallel": t.kind = 68; break;
+			case "in": t.kind = 82; break;
+			case "false": t.kind = 92; break;
+			case "true": t.kind = 93; break;
+			case "null": t.kind = 94; break;
+			case "this": t.kind = 95; break;
+			case "fresh": t.kind = 96; break;
+			case "allocated": t.kind = 97; break;
+			case "old": t.kind = 98; break;
+			case "then": t.kind = 99; break;
+			case "forall": t.kind = 101; break;
+			case "exists": t.kind = 103; break;
 			default: break;
 		}
 	}
@@ -647,81 +648,81 @@ public class Scanner {
 				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
 				else {t.kind = 3; break;}
 			case 19:
-				{t.kind = 18; break;}
+				{t.kind = 19; break;}
 			case 20:
-				{t.kind = 20; break;}
+				{t.kind = 21; break;}
 			case 21:
-				{t.kind = 27; break;}
+				{t.kind = 28; break;}
 			case 22:
-				{t.kind = 33; break;}
-			case 23:
 				{t.kind = 34; break;}
+			case 23:
+				{t.kind = 35; break;}
 			case 24:
-				{t.kind = 45; break;}
-			case 25:
 				{t.kind = 46; break;}
+			case 25:
+				{t.kind = 47; break;}
 			case 26:
-				{t.kind = 50; break;}
-			case 27:
 				{t.kind = 51; break;}
+			case 27:
+				{t.kind = 52; break;}
 			case 28:
-				{t.kind = 53; break;}
-			case 29:
 				{t.kind = 54; break;}
+			case 29:
+				{t.kind = 55; break;}
 			case 30:
-				{t.kind = 60; break;}
+				{t.kind = 61; break;}
 			case 31:
 				if (ch == '>') {AddCh(); goto case 32;}
 				else {goto case 0;}
 			case 32:
-				{t.kind = 68; break;}
-			case 33:
 				{t.kind = 69; break;}
-			case 34:
+			case 33:
 				{t.kind = 70; break;}
-			case 35:
+			case 34:
 				{t.kind = 71; break;}
+			case 35:
+				{t.kind = 72; break;}
 			case 36:
 				if (ch == '&') {AddCh(); goto case 37;}
 				else {goto case 0;}
 			case 37:
-				{t.kind = 72; break;}
-			case 38:
 				{t.kind = 73; break;}
-			case 39:
+			case 38:
 				{t.kind = 74; break;}
-			case 40:
+			case 39:
 				{t.kind = 75; break;}
+			case 40:
+				{t.kind = 76; break;}
 			case 41:
-				{t.kind = 78; break;}
-			case 42:
 				{t.kind = 79; break;}
-			case 43:
+			case 42:
 				{t.kind = 80; break;}
+			case 43:
+				{t.kind = 81; break;}
 			case 44:
-				{t.kind = 83; break;}
-			case 45:
 				{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 50:
+			case 49:
 				{t.kind = 89; break;}
-			case 51:
+			case 50:
 				{t.kind = 90; break;}
+			case 51:
+				{t.kind = 91; break;}
 			case 52:
-				{t.kind = 101; break;}
+				{t.kind = 102; break;}
 			case 53:
-				{t.kind = 103; break;}
-			case 54:
 				{t.kind = 104; break;}
-			case 55:
+			case 54:
 				{t.kind = 105; break;}
+			case 55:
+				{t.kind = 106; break;}
 			case 56:
 				recEnd = pos; recKind = 5;
 				if (ch == '=') {AddCh(); goto case 26;}
@@ -729,43 +730,43 @@ public class Scanner {
 				else if (ch == ':') {AddCh(); goto case 54;}
 				else {t.kind = 5; break;}
 			case 57:
-				recEnd = pos; recKind = 16;
+				recEnd = pos; recKind = 17;
 				if (ch == '>') {AddCh(); goto case 30;}
 				else if (ch == '=') {AddCh(); goto case 63;}
-				else {t.kind = 16; break;}
+				else {t.kind = 17; break;}
 			case 58:
-				recEnd = pos; recKind = 17;
+				recEnd = pos; recKind = 18;
 				if (ch == '|') {AddCh(); goto case 39;}
-				else {t.kind = 17; break;}
+				else {t.kind = 18; break;}
 			case 59:
-				recEnd = pos; recKind = 22;
+				recEnd = pos; recKind = 23;
 				if (ch == '=') {AddCh(); goto case 64;}
-				else {t.kind = 22; break;}
+				else {t.kind = 23; break;}
 			case 60:
-				recEnd = pos; recKind = 23;
+				recEnd = pos; recKind = 24;
 				if (ch == '=') {AddCh(); goto case 41;}
-				else {t.kind = 23; break;}
+				else {t.kind = 24; break;}
 			case 61:
-				recEnd = pos; recKind = 55;
+				recEnd = pos; recKind = 56;
 				if (ch == '.') {AddCh(); goto case 65;}
-				else {t.kind = 55; break;}
+				else {t.kind = 56; break;}
 			case 62:
-				recEnd = pos; recKind = 82;
+				recEnd = pos; recKind = 83;
 				if (ch == '=') {AddCh(); goto case 42;}
 				else if (ch == '!') {AddCh(); goto case 43;}
-				else {t.kind = 82; break;}
+				else {t.kind = 83; break;}
 			case 63:
-				recEnd = pos; recKind = 76;
+				recEnd = pos; recKind = 77;
 				if (ch == '>') {AddCh(); goto case 34;}
-				else {t.kind = 76; break;}
+				else {t.kind = 77; break;}
 			case 64:
-				recEnd = pos; recKind = 77;
+				recEnd = pos; recKind = 78;
 				if (ch == '=') {AddCh(); goto case 31;}
-				else {t.kind = 77; break;}
+				else {t.kind = 78; break;}
 			case 65:
-				recEnd = pos; recKind = 99;
+				recEnd = pos; recKind = 100;
 				if (ch == '.') {AddCh(); goto case 21;}
-				else {t.kind = 99; break;}
+				else {t.kind = 100; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 589a43e2..ed69d5db 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -66,7 +66,6 @@ TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, g
 TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
@@ -92,6 +91,7 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 34 resolution/type errors detected in TypeTests.dfy
 
 -------------------- NatTypes.dfy --------------------
@@ -1263,6 +1263,12 @@ Execution trace:
 
 Dafny program verifier finished with 32 verified, 6 errors
 
+-------------------- Coinductive.dfy --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(51,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+3 resolution/type errors detected in Coinductive.dfy
+
 -------------------- TypeAntecedents.dfy --------------------
 TypeAntecedents.dfy(32,13): Error: assertion violation
 Execution trace:
@@ -1848,3 +1854,6 @@ Execution trace:
     (0,0): anon11_Then
 
 Dafny program verifier finished with 19 verified, 2 errors
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled assembly into Compilation.dll
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
new file mode 100644
index 00000000..fdb8c06b
--- /dev/null
+++ b/Test/dafny0/Coinductive.dfy
@@ -0,0 +1,55 @@
+// --------------------------------------------------
+
+module TestInductiveDatatypes
+{
+  // The following types test for cycles that go via instantiated type arguments
+
+  datatype Record<T> = Ctor(T);
+
+  datatype RecInt = Ctor(Record<int>);  // this is fine
+  datatype Rec_Forever = Ctor(Record<Rec_Forever>);  // error
+  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil;  // this is okay
+
+  datatype D<T> = Ctor(E<D<T>>);  // error: illegal cycle
+  datatype E<T> = Ctor(T);
+
+  // the following is okay
+  datatype MD<T> = Ctor(ME<T>);
+  datatype ME<T> = Ctor(T);
+  method M()
+  {
+    var d: MD<MD<int>>;
+  }
+
+  datatype A = Ctor(B);  // superficially looks like a cycle, but can still be constructed
+  datatype B = Ctor(List<A>);
+  datatype List<T> = Nil | Cons(T, List);
+}
+
+// --------------------------------------------------
+
+module TestCoinductiveDatatypes
+{
+  codatatype InfList<T> = Done | Continue(T, InfList);
+
+  codatatype Stream<T> = More(T, Stream<T>);
+
+  codatatype BinaryTreeForever<T> = BNode(val: T, left: BinaryTreeForever<T>, right: BinaryTreeForever<T>);
+
+  datatype List<T> = Nil | Cons(T, List);
+
+  codatatype BestBushEver<T> = Node(value: T, branches: List<BestBushEver<T>>);
+
+  codatatype LazyRecord<T> = Lazy(contents: T);
+  class MyClass<T> { }
+  datatype GenericDt<T> = Blue | Green(T);
+  datatype GenericRecord<T> = Rec(T);
+
+  datatype FiniteEnough_Class = Ctor(MyClass<FiniteEnough_Class>);
+  datatype FiniteEnough_Co = Ctor(LazyRecord<FiniteEnough_Co>);
+  datatype FiniteEnough_Dt = Ctor(GenericDt<FiniteEnough_Dt>);  // fine
+  datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>);  // error
+
+}
+
+// --------------------------------------------------
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
new file mode 100644
index 00000000..301a4e94
--- /dev/null
+++ b/Test/dafny0/Compilation.dfy
@@ -0,0 +1,13 @@
+// The tests in this file are designed to run through the compiler.  They contain
+// program snippets that are tricky to compile or whose compilation once was buggy.
+
+datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
+
+method M<U>(x: MyDt<int>)
+{
+  match (x) {
+    case Cons(head, tail) =>
+      var y: int := head;
+    case Nil =>
+  }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 608b7358..f9cd5a89 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,8 +17,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy
             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
-            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy NoTypeArgs.dfy
-            SplitExpr.dfy
+            TypeParameters.dfy Datatypes.dfy Coinductive.dfy
+            TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
@@ -34,3 +34,5 @@ for %%f in (SmallTests.dfy LetExpr.dfy) do (
   %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
   %DAFNY_EXE% /compile:0 %* out.tmp.dfy
 )
+
+%DAFNY_EXE% %* Compilation.dfy
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 56b56000..f16b09b5 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
 ]\\)*" . font-lock-comment-face)
 
    `(,(dafny-regexp-opt '(
-        "class" "datatype" "type" "function" "predicate" "ghost" "var" "method" "constructor" "unlimited"
+        "class" "datatype" "codatatype" "type" "function" "predicate" "ghost" "var" "method" "constructor" "unlimited"
         "module" "imports" "static" "refines"
         "returns" "requires" "ensures" "modifies" "reads" "free"
         "invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 41923a98..012058f6 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -17,7 +17,7 @@ namespace Demo
         StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
 
         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below
-          "class", "ghost", "static", "var", "method", "constructor", "datatype", "type",
+          "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
           "assert", "assume", "new", "this", "object", "refines",
           "unlimited", "module", "imports",
           "if", "then", "else", "while", "invariant",
@@ -267,6 +267,7 @@ namespace Demo
           | "method"
           | "constructor"
           | "datatype"
+          | "codatatype"
           | "type"
           | "assert"
           | "assume"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 650c01bd..48faa5ec 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -242,6 +242,7 @@ namespace DafnyLanguage
                 case "case":
                 case "choose":
                 case "class":
+                case "codatatype":
                 case "constructor":
                 case "datatype":
                 case "decreases":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index b23e2dc4..4126d2f2 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
 \usepackage{listings}
 
 \lstdefinelanguage{dafny}{
-  morekeywords={class,datatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
+  morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
       function,predicate,unlimited,
       ghost,var,static,refines,
       method,constructor,returns,module,imports,in,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 37038f35..6af28094 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -6,7 +6,7 @@
 syntax clear
 syntax case match
 syntax keyword dafnyFunction function predicate method constructor
-syntax keyword dafnyTypeDef class datatype type
+syntax keyword dafnyTypeDef class datatype codatatype type
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
 syntax keyword dafnyStatement havoc assume assert return new print break label
author	Unknown <leino@LEINO6.redmond.corp.microsoft.com>	2012-04-25 16:37:12 -0700
committer	Unknown <leino@LEINO6.redmond.corp.microsoft.com>	2012-04-25 16:37:12 -0700
commit	a732a632287074e74a1dd394149b36e83526a0cf (patch)
tree	9770cb8127d4bf9d8348a5da54922d32f3d29fdb
parent	032662d0adb823376b1abd49a0c46ba3276f8721 (diff)