Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax

22 files changed, 261 insertions, 361 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 82cd5d47..11a2dfed 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -267,16 +267,10 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

-  (

-    "{"                                      (. bodyStart = t; .)

-    { DatatypeMemberDecl<ctors> ";" }

-    "}"

-  | 

-    "="                                      (. bodyStart = t; .)

-    DatatypeMemberDecl<ctors>

-    { "|" DatatypeMemberDecl<ctors> }

-    ";"

-  )

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

+  DatatypeMemberDecl<ctors>

+  { "|" DatatypeMemberDecl<ctors> }

+  ";"

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

      dt.BodyStartTok = bodyStart;

      dt.BodyEndTok = t;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 7a0d86e3..b650b655 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -707,6 +707,7 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(Ctors));

+      Contract.Invariant(1 <= Ctors.Count);

     }

 

     public DatatypeCtor DefaultCtor;  // set during resolution

@@ -719,8 +720,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(module != null);

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

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

+      Contract.Invariant(1 <= ctors.Count);

       Ctors = ctors;

-

     }

   }

 

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 994d6f70..840344bd 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -345,24 +345,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (la.kind == 23) {

 			GenericParameters(typeArgs);

 		}

-		if (la.kind == 7) {

-			Get();

-			bodyStart = t; 

-			while (la.kind == 1 || la.kind == 7) {

-				DatatypeMemberDecl(ctors);

-				Expect(15);

-			}

-			Expect(8);

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

+		Expect(15);

+		bodyStart = t; 

+		DatatypeMemberDecl(ctors);

+		while (la.kind == 16) {

 			Get();

-			bodyStart = t; 

 			DatatypeMemberDecl(ctors);

-			while (la.kind == 17) {

-				Get();

-				DatatypeMemberDecl(ctors);

-			}

-			Expect(15);

-		} else SynErr(105);

+		}

+		Expect(17);

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

 		dt.BodyStartTok = bodyStart;

 		dt.BodyEndTok = t;

@@ -397,7 +387,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 

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

 			CouplingInvDecl(mmod, mm);

-		} else SynErr(106);

+		} else SynErr(105);

 	}

 

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

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

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

 		}

-		Expect(15);

+		Expect(17);

 	}

 

 	void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {

@@ -469,7 +459,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Formals(true, isFunctionMethod, formals);

 		Expect(22);

 		Type(out returnType);

-		if (la.kind == 15) {

+		if (la.kind == 17) {

 			Get();

 			while (StartOf(3)) {

 				FunctionSpec(reqs, reads, ens, decreases);

@@ -480,7 +470,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

 			FunctionBody(out bb, out bodyStart, out bodyEnd);

 			body = bb; 

-		} else SynErr(107);

+		} else SynErr(106);

 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);

 		f.BodyStartTok = bodyStart;

 		f.BodyEndTok = bodyEnd;

@@ -508,7 +498,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {

 			Get();

 			isRefinement = true; 

-		} else SynErr(108);

+		} else SynErr(107);

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

 		

 		while (la.kind == 7) {

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

 			Formals(false, true, outs);

 		}

-		if (la.kind == 15) {

+		if (la.kind == 17) {

 			Get();

 			while (StartOf(5)) {

 				MethodSpec(req, mod, ens, dec);

@@ -534,7 +524,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

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

 			body = (BlockStmt)bb; 

-		} else SynErr(109);

+		} else SynErr(108);

 		if (isRefinement)

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

 		else 

@@ -568,7 +558,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 		Expect(21);

 		Expression(out e);

-		Expect(15);

+		Expect(17);

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

 	}

 

@@ -729,7 +719,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(110); break;

+		default: SynErr(109); break;

 		}

 	}

 

@@ -764,7 +754,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					mod.Add(fe); 

 				}

 			}

-			Expect(15);

+			Expect(17);

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

 			if (la.kind == 28) {

 				Get();

@@ -773,19 +763,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (la.kind == 29) {

 				Get();

 				Expression(out e);

-				Expect(15);

+				Expect(17);

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

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

 				Get();

 				Expression(out e);

-				Expect(15);

+				Expect(17);

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

-			} else SynErr(111);

+			} else SynErr(110);

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

 			Get();

 			Expressions(decreases);

-			Expect(15);

-		} else SynErr(112);

+			Expect(17);

+		} else SynErr(111);

 	}

 

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

@@ -865,7 +855,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(113);

+		} else SynErr(112);

 	}

 

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

@@ -874,7 +864,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 29) {

 			Get();

 			Expression(out e);

-			Expect(15);

+			Expect(17);

 			reqs.Add(e); 

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

 			Get();

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

 				}

 			}

-			Expect(15);

+			Expect(17);

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

 			Get();

 			Expression(out e);

-			Expect(15);

+			Expect(17);

 			ens.Add(e); 

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

 			Get();

 			Expressions(decreases);

-			Expect(15);

-		} else SynErr(114);

+			Expect(17);

+		} else SynErr(113);

 	}

 

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

@@ -908,7 +898,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchExpression(out e);

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(115);

+		} else SynErr(114);

 		Expect(8);

 		bodyEnd = t; 

 	}

@@ -920,7 +910,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(116);

+		} else SynErr(115);

 	}

 

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

@@ -931,7 +921,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new WildcardExpr(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(117);

+		} else SynErr(116);

 	}

 

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

@@ -982,7 +972,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchExpression(out e);

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(118);

+		} else SynErr(117);

 	}

 

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

@@ -1033,20 +1023,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			} else if (la.kind == 15 || la.kind == 48) {

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

 				while (la.kind == 48) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(119);

-			Expect(15);

+			} else SynErr(118);

+			Expect(17);

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

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

 			Get();

 			x = t; 

-			Expect(15);

+			Expect(17);

 			s = new ReturnStmt(x); 

-		} else SynErr(120);

+		} else SynErr(119);

 	}

 

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

@@ -1054,7 +1044,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(63);

 		x = t; 

 		Expression(out e);

-		Expect(15);

+		Expect(17);

 		s = new AssertStmt(x, e); 

 	}

 

@@ -1063,7 +1053,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(64);

 		x = t; 

 		Expression(out e);

-		Expect(15);

+		Expect(17);

 		s = new AssumeStmt(x, e); 

 	}

 

@@ -1080,7 +1070,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			AttributeArg(out arg);

 			args.Add(arg); 

 		}

-		Expect(15);

+		Expect(17);

 		s = new PrintStmt(x, args); 

 	}

 

@@ -1093,7 +1083,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Lhs(out e);

 		x = e.tok; 

-		if (la.kind == 15) {

+		if (la.kind == 17) {

 			Get();

 			rhss.Add(new ExprRhs(e)); 

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

@@ -1112,11 +1102,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Rhs(out r, lhs0);

 				rhss.Add(r); 

 			}

-			Expect(15);

+			Expect(17);

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

 			Get();

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

-		} else SynErr(121);

+		} else SynErr(120);

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

 	}

 

@@ -1125,7 +1115,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(56);

 		x = t; 

 		Lhs(out lhs);

-		Expect(15);

+		Expect(17);

 		s = new AssignStmt(x, lhs); 

 	}

 

@@ -1160,7 +1150,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				rhss.Add(r); 

 			}

 		}

-		Expect(15);

+		Expect(17);

 		UpdateStmt update;

 		if (rhss.Count == 0) {

 		  update = null;

@@ -1198,13 +1188,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 				} else if (la.kind == 7) {

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

 					els = s; 

-				} else SynErr(122);

+				} else SynErr(121);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(123);

+		} else SynErr(122);

 	}

 

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

@@ -1229,7 +1219,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases);

 			AlternativeBlock(out alternatives);

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

-		} else SynErr(124);

+		} else SynErr(123);

 	}

 

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

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

 		Expect(62);

 		Expression(out collection);

-		if (la.kind == 17) {

+		if (la.kind == 16) {

 			Get();

 			Expression(out range);

 		}

@@ -1291,7 +1281,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 56) {

 			HavocStmt(out s);

 			bodyAssign = s; 

-		} else SynErr(125);

+		} else SynErr(124);

 		Expect(8);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

@@ -1315,7 +1305,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(126);

+		} else SynErr(125);

 	}

 

 	void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {

@@ -1365,7 +1355,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(127);

+		} else SynErr(126);

 	}

 

 	void Guard(out Expression e) {

@@ -1377,7 +1367,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(128);

+		} else SynErr(127);

 		Expect(33);

 	}

 

@@ -1417,7 +1407,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expect(60);

 				Expression(out e);

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

-				Expect(15);

+				Expect(17);

 			} else {

 				Get();

 				PossiblyWildExpression(out e);

@@ -1427,7 +1417,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					PossiblyWildExpression(out e);

 					decreases.Add(e); 

 				}

-				Expect(15);

+				Expect(17);

 			}

 		}

 	}

@@ -1467,7 +1457,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(129);

+		} else SynErr(128);

 	}

 

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

@@ -1497,7 +1487,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(130);

+		} else SynErr(129);

 	}

 

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

@@ -1535,7 +1525,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(131);

+		} else SynErr(130);

 	}

 

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

@@ -1618,7 +1608,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(132);

+		} else SynErr(131);

 	}

 

 	void OrOp() {

@@ -1626,7 +1616,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(133);

+		} else SynErr(132);

 	}

 

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

@@ -1702,7 +1692,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(134); break;

+		default: SynErr(133); break;

 		}

 	}

 

@@ -1724,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 84) {

 			Get();

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

-		} else SynErr(135);

+		} else SynErr(134);

 	}

 

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

@@ -1751,7 +1741,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(136);

+		} else SynErr(135);

 	}

 

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

@@ -1765,7 +1755,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 86) {

 			Get();

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

-		} else SynErr(137);

+		} else SynErr(136);

 	}

 

 	void NegOp() {

@@ -1773,7 +1763,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(138);

+		} else SynErr(137);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1794,7 +1784,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			QuantifierGuts(out e);

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

 			ComprehensionExpr(out e);

-		} else SynErr(139);

+		} else SynErr(138);

 	}

 

 	void DottedIdentifiersAndFunction(out Expression e) {

@@ -1867,12 +1857,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(140);

+				} else SynErr(139);

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

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(141);

+			} else SynErr(140);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(53);

-		} else SynErr(142);

+		} else SynErr(141);

 	}

 

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

@@ -1957,12 +1947,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new OldExpr(x, e); 

 			break;

 		}

-		case 17: {

+		case 16: {

 			Get();

 			x = t; 

 			Expression(out e);

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

-			Expect(17);

+			Expect(16);

 			break;

 		}

 		case 7: {

@@ -1993,7 +1983,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(33);

 			break;

 		}

-		default: SynErr(143); break;

+		default: SynErr(142); break;

 		}

 	}

 

@@ -2024,7 +2014,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 100 || la.kind == 101) {

 			Exists();

 			x = t; 

-		} else SynErr(144);

+		} else SynErr(143);

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

 		while (la.kind == 19) {

@@ -2035,7 +2025,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		while (la.kind == 7) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

-		if (la.kind == 17) {

+		if (la.kind == 16) {

 			Get();

 			Expression(out range);

 		}

@@ -2066,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

 		}

-		Expect(17);

+		Expect(16);

 		Expression(out range);

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

 			QSep();

@@ -2082,7 +2072,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(145);

+		} else SynErr(144);

 	}

 

 	void Exists() {

@@ -2090,7 +2080,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(146);

+		} else SynErr(145);

 	}

 

 	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

@@ -2103,7 +2093,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			es = new List<Expression/*!*/>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(147);

+		} else SynErr(146);

 		Expect(8);

 	}

 

@@ -2112,7 +2102,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(148);

+		} else SynErr(147);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2155,17 +2145,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,x,x,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,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 } // end Parser

@@ -2205,9 +2195,9 @@ public class Errors {
 			case 12: s = "\"static\" expected"; break;

 			case 13: s = "\"unlimited\" expected"; break;

 			case 14: s = "\"datatype\" expected"; break;

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

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

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

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

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

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

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

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

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

@@ -2295,50 +2285,49 @@ public class Errors {
 			case 102: s = "\"::\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 115: s = "invalid FunctionBody"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 8a2513da..5ee2f0c9 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -152,16 +152,17 @@ namespace Microsoft.Dafny {
       Contract.Requires(dt != null);

       Indent(indent);

       PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs);

-      if (dt.Ctors.Count == 0) {

-        wr.WriteLine(" { }");

-      } else {

-        wr.WriteLine(" {");

-        int ind = indent + IndentAmount;

-        foreach (DatatypeCtor ctor in dt.Ctors) {

-          PrintCtor(ctor, ind);

+      wr.Write(" = ");

+      string sep = "";

+      foreach (DatatypeCtor ctor in dt.Ctors) {

+        wr.Write(sep);

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

+        if (ctor.Formals.Count != 0) {

+          PrintFormals(ctor.Formals);

         }

-        Indent(indent);  wr.WriteLine("}");

+        sep = " | ";

       }

+      wr.WriteLine(";");

     }

     

     public void PrintAttributes(Attributes a) {

@@ -245,16 +246,6 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void PrintCtor(DatatypeCtor ctor, int indent) {

-      Contract.Requires(ctor != null);

-      Indent(indent);

-      PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List<TypeParameter>());

-      if (ctor.Formals.Count != 0) {

-        PrintFormals(ctor.Formals);

-      }

-      wr.WriteLine(";");

-    }

-    

     // ----------------------------- PrintMethod -----------------------------

 

     const int IndentAmount = 2;

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 50529816..083c0c0c 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -259,9 +259,9 @@ public class Scanner {
 		start[97] = 10; 

 		start[123] = 17; 

 		start[125] = 18; 

-		start[59] = 19; 

 		start[61] = 57; 

 		start[124] = 58; 

+		start[59] = 19; 

 		start[44] = 20; 

 		start[58] = 59; 

 		start[60] = 60; 

@@ -645,7 +645,7 @@ public class Scanner {
 			case 18:

 				{t.kind = 8; break;}

 			case 19:

-				{t.kind = 15; break;}

+				{t.kind = 17; break;}

 			case 20:

 				{t.kind = 19; break;}

 			case 21:

@@ -724,14 +724,14 @@ public class Scanner {
 			case 56:

 				{t.kind = 103; break;}

 			case 57:

-				recEnd = pos; recKind = 16;

+				recEnd = pos; recKind = 15;

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

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

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

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

 			case 58:

-				recEnd = pos; recKind = 17;

+				recEnd = pos; recKind = 16;

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

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

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

 			case 59:

 				recEnd = pos; recKind = 22;

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

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bf3ba197..5cfee29d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -46,16 +46,9 @@ class MyClass<T, U> {
   }

 }

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype WildData {

-  Something;

-  JustAboutAnything(bool, myName: set<int>, int, WildData);

-  More(List<int>);

-}

+datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>);

 

 class C {

   var w: WildData;

@@ -65,7 +58,7 @@ class C {
 Dafny program verifier finished with 0 verified, 0 errors

 

 -------------------- TypeTests.dfy --------------------

-TypeTests.dfy(95,9): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(84,9): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -73,21 +66,20 @@ 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(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed

-TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-TypeTests.dfy(55,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(64,6): Error: Duplicate local-variable name: z

-TypeTests.dfy(66,6): Error: Duplicate local-variable name: x

-TypeTests.dfy(69,8): Error: Duplicate local-variable name: x

-TypeTests.dfy(72,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(79,17): Error: member F in class C does not refer to a method

-TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

-TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

-TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-22 resolution/type errors detected in TypeTests.dfy

+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

+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x

+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

+TypeTests.dfy(68,17): Error: member F in class C does not refer to a method

+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

+TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(79,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type

+TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+21 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -114,16 +106,16 @@ NatTypes.dfy(54,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(71,16): Error: assertion violation

+NatTypes.dfy(68,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

@@ -192,14 +184,14 @@ Execution trace:
     (0,0): anon6

     (0,0): anon14_Then

     (0,0): anon11

-SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.

+SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(267,19): anon3_Else

+    SmallTests.dfy(266,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -379,7 +371,7 @@ Execution trace:
 Dafny program verifier finished with 23 verified, 34 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

-FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition

+FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon10_Else

     (0,0): anon11_Else

@@ -387,13 +379,13 @@ Execution trace:
     (0,0): anon13_Else

     (0,0): anon7

     (0,0): anon9

-FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition

+FunctionSpecifications.dfy(37,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon12_Else

     (0,0): anon15_Else

     (0,0): anon16_Then

     (0,0): anon11

-FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(50,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Then

@@ -557,10 +549,10 @@ Modules0.dfy(187,12): Error: match source expression 'l' has already been used a
 13 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

-Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

+Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0

 Execution trace:

     (0,0): anon0

-Modules1.dfy(61,3): Error: failure to decrease termination measure

+Modules1.dfy(58,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

 

@@ -755,57 +747,57 @@ Execution trace:
 Dafny program verifier finished with 18 verified, 10 errors

 

 -------------------- Termination.dfy --------------------

-Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(103,3): anon7_LoopHead

+    Termination.dfy(100,3): anon7_LoopHead

     (0,0): anon7_LoopBody

-    Termination.dfy(103,3): anon8_Else

+    Termination.dfy(100,3): anon8_Else

     (0,0): anon3

-    Termination.dfy(103,3): anon9_Else

+    Termination.dfy(100,3): anon9_Else

     (0,0): anon5

-Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(111,3): anon9_LoopHead

+    Termination.dfy(108,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(111,3): anon10_Else

+    Termination.dfy(108,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(111,3): anon12_Else

+    Termination.dfy(108,3): anon12_Else

     (0,0): anon7

-Termination.dfy(120,3): Error: decreases expression might not decrease

+Termination.dfy(117,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(120,3): anon9_LoopHead

+    Termination.dfy(117,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(120,3): anon10_Else

+    Termination.dfy(117,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(120,3): anon12_Else

+    Termination.dfy(117,3): anon12_Else

     (0,0): anon7

-Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

+Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

-    Termination.dfy(120,3): anon9_LoopHead

+    Termination.dfy(117,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(120,3): anon10_Else

+    Termination.dfy(117,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(120,3): anon12_Else

+    Termination.dfy(117,3): anon12_Else

     (0,0): anon7

-Termination.dfy(249,35): Error: cannot prove termination; try supplying a decreases clause

+Termination.dfy(246,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

-Termination.dfy(289,3): Error: decreases expression might not decrease

+Termination.dfy(286,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(289,3): anon10_LoopHead

+    Termination.dfy(286,3): anon10_LoopHead

     (0,0): anon10_LoopBody

-    Termination.dfy(289,3): anon11_Else

-    Termination.dfy(289,3): anon12_Else

+    Termination.dfy(286,3): anon11_Else

+    Termination.dfy(286,3): anon12_Else

     (0,0): anon13_Else

     (0,0): anon8

 

@@ -818,20 +810,20 @@ Execution trace:
 DTypes.dfy(53,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(123,13): Error: assertion violation

-DTypes.dfy(94,3): Related location: Related location

+DTypes.dfy(117,13): Error: assertion violation

+DTypes.dfy(89,30): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(129,13): Error: assertion violation

-DTypes.dfy(93,3): Related location: Related location

+DTypes.dfy(123,13): Error: assertion violation

+DTypes.dfy(89,20): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(139,12): Error: assertion violation

-DTypes.dfy(134,6): Related location: Related location

-DTypes.dfy(93,3): Related location: Related location

+DTypes.dfy(133,12): Error: assertion violation

+DTypes.dfy(128,6): Related location: Related location

+DTypes.dfy(89,20): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(160,12): Error: assertion violation

+DTypes.dfy(154,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -883,7 +875,7 @@ Execution trace:
 Dafny program verifier finished with 33 verified, 5 errors

 

 -------------------- Datatypes.dfy --------------------

-Datatypes.dfy(82,20): Error: assertion violation

+Datatypes.dfy(79,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon20_Else

@@ -897,11 +889,11 @@ Execution trace:
 Dafny program verifier finished with 17 verified, 1 error

 

 -------------------- TypeAntecedents.dfy --------------------

-TypeAntecedents.dfy(34,13): Error: assertion violation

+TypeAntecedents.dfy(32,13): Error: assertion violation

 Execution trace:

     (0,0): anon0

-TypeAntecedents.dfy(60,1): Error BP5003: A postcondition might not hold on this return path.

-TypeAntecedents.dfy(59,15): Related location: This is the postcondition that might not hold.

+TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this return path.

+TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon15_Then

@@ -913,7 +905,7 @@ Execution trace:
     (0,0): anon20_Then

     (0,0): anon21_Then

     (0,0): anon14

-TypeAntecedents.dfy(68,16): Error: assertion violation

+TypeAntecedents.dfy(63,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon15_Else

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index b402c335..55d107c5 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -74,10 +74,7 @@ class Node { }
 class CP<T,U> {

 }

 

-datatype Data {

-  Lemon;

-  Kiwi(int);

-}

+datatype Data = Lemon | Kiwi(int);

 

 function G(d: Data): int

   requires d != Data.Lemon;

@@ -89,10 +86,7 @@ function G(d: Data): int
 

 // -------- some things about induction ---------------------------------

 

-datatype Tree<T> {

-  Leaf(T);

-  Branch(Tree<T>, Tree<T>);

-}

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

 

 class DatatypeInduction<T> {

   function LeafCount<G>(tree: Tree<G>): int

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 9a16a91a..99e5e920 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -1,7 +1,4 @@
-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

 class Node {

   var data: int;

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index 21ce5468..13171c47 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -6,10 +6,7 @@ function Fib(n: int): int
   Fib(n-2) + Fib(n-1)

 }

 

-datatype List {

-  Nil;

-  Cons(int, List);

-}

+datatype List = Nil | Cons(int, List);

 

 function Sum(a: List): int

   ensures 0 <= Sum(a);

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 01e14585..c14aece6 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -138,7 +138,7 @@ method SpecialFunctions()
 

 // ---------------------- illegal match expressions ---------------

 

-datatype Tree { Nil; Cons(int, Tree, Tree); }

+datatype Tree = Nil | Cons(int, Tree, Tree);

 

 function NestedMatch0(tree: Tree): int

 {

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index ff84b84b..ad17c7d8 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -5,10 +5,7 @@ module A imports B {
       decreases 5, 4, 3;

     { z.G() }  // fine; this goes to a different module

   }

-  datatype Y {

-    Cons(int, Y);

-    Empty;

-  }

+  datatype Y = Cons(int, Y) | Empty;

 }

 

 class C {

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index e4d0cbe7..53d3bf03 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -44,7 +44,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
 

 function method FenEric<T>(t0: T, t1: T): T;

 

-datatype Pair<T> { Pr(T, T); }

+datatype Pair<T> = Pr(T, T);

 

 method K(n: nat, i: int) {

   match (Pair.Pr(n, i)) {

@@ -55,10 +55,7 @@ method K(n: nat, i: int) {
   }

 }

 

-datatype List<T> {

-  Nil;

-  Cons(nat, T, List<T>);

-}

+datatype List<T> = Nil | Cons(nat, T, List<T>);

 

 method MatchIt(list: List<object>) returns (k: nat)

 {

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index e1416094..ac3a4792 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -39,16 +39,12 @@ class MyClass<T,U> {
 

 // some datatype stuff:

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype WildData {

-  Something();

-  JustAboutAnything(bool, myName: set<int>, int, WildData);

+datatype WildData =

+  Something() |

+  JustAboutAnything(bool, myName: set<int>, int, WildData) |

   More(List<int>);

-}

 

 class C {

   var w: WildData;

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index fcc764aa..b4dc6599 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -227,11 +227,10 @@ class AllocatedTests {
   }

 }

 

-datatype Lindgren {

-  Pippi(Node);

-  Longstocking(seq<object>, Lindgren);

+datatype Lindgren =

+  Pippi(Node) |

+  Longstocking(seq<object>, Lindgren) |

   HerrNilsson;

-}

 

 // --------------------------------------------------

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 155fbaef..d4d1dfcf 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -92,10 +92,7 @@ class Termination {
     ensures a == List.Cons(val, b);

 }

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

 method FailureToProveTermination0(N: int)

 {

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 38050b88..2bedd37d 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -1,10 +1,8 @@
 // -------- This is an example of what was once logically (although not trigger-ly) unsound ---

 

-datatype Wrapper<T> {

-  Wrap(T);

-}

-datatype Unit { It; }

-datatype Color { Yellow; Blue; }

+datatype Wrapper<T> = Wrap(T);

+datatype Unit = It;

+datatype Color = Yellow | Blue;

 

 function F(a: Wrapper<Unit>): bool

   ensures a == Wrapper.Wrap(Unit.It);

@@ -49,10 +47,7 @@ class MyClass {
   function H(): int { 5 }

 }

 

-datatype List {

-  Nil;

-  Cons(MyClass, List);

-}

+datatype List =  Nil | Cons(MyClass, List);

 

 method M(list: List, S: set<MyClass>) returns (ret: int)

   modifies S;

@@ -97,8 +92,6 @@ function NF(): MyClass;
 

 function TakesADatatype(a: List): int { 12 }

 

-datatype GenData<T> {

-  Pair(T, T);

-}

+datatype GenData<T> = Pair(T, T);

 

 function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 21f0dda8..9df11a67 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -13,37 +13,26 @@ class C {
   }

 }

 

-datatype D {

-  A;

-}

-

-datatype Nothing {  // error: no grounding constructor

-}

+datatype D = A;

 

-datatype NeverendingList {  // error: no grounding constructor

-  Cons(int, NeverendingList);

-}

+datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor

 

-datatype MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(TheCounterpart<T>, C);

-}

 

-datatype TheCounterpart<T> {

-  TreeLike(TheCounterpart<T>, TheCounterpart<T>);

+datatype TheCounterpart<T> =

+  TreeLike(TheCounterpart<T>, TheCounterpart<T>) |

   More(MutuallyRecursiveDataType<T>);

-}

 

 // these 'ReverseOrder_' order tests may be called white-box unit tests

-datatype ReverseOrder_MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype ReverseOrder_MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(ReverseOrder_TheCounterpart<T>, C);

-}

 

-datatype ReverseOrder_TheCounterpart<T> {

-  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>);

+datatype ReverseOrder_TheCounterpart<T> =

+  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |

   More(ReverseOrder_MutuallyRecursiveDataType<T>);

-}

 

 // ---------------------

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 2c90769b..de5a3358 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -136,10 +136,7 @@ class IntegerInduction {
   }

 }

 

-datatype Tree<T> {

-  Leaf(T);

-  Branch(Tree<T>, Tree<T>);

-}

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

 

 class DatatypeInduction<T> {

   function LeafCount<T>(tree: Tree<T>): int

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 3a455077..fdce6dc7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -1,16 +1,16 @@
 // Datatypes

 

-datatype Bool { False; True; }

+datatype Bool = False | True;

 

-datatype Nat { Zero; Suc(Nat); }

+datatype Nat = Zero | Suc(Nat);

 

-datatype List { Nil; Cons(Nat, List); }

+datatype List = Nil | Cons(Nat, List);

 

-datatype Pair { Pair(Nat, Nat); }

+datatype Pair = Pair(Nat, Nat);

 

-datatype PList { PNil; PCons(Pair, PList); }

+datatype PList = PNil | PCons(Pair, PList);

 

-datatype Tree { Leaf; Node(Tree, Nat, Tree); }

+datatype Tree = Leaf | Node(Tree, Nat, Tree);

 

 // Boolean functions

 

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 95cdab89..8da32b05 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -10,6 +10,8 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

+datatype Path = Empty | Extend(Path, Node);

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -265,8 +267,3 @@ class Main {
     }

   }

 }

-

-datatype Path {

-  Empty;

-  Extend(Path, Node);

-}

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 11c8c878..ad39e3f2 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,13 +1,9 @@
-datatype List {

-  Nil;

-  Cons(Expr, List);

-}

+datatype List = Nil | Cons(Expr, List);

 

-datatype Expr {

-  Const(int);

-  Var(int);

+datatype Expr =

+  Const(int) |

+  Var(int) |

   Nary(int, List);

-}

 

 static function Subst(e: Expr, v: int, val: int): Expr

 {

@@ -48,11 +44,10 @@ static ghost method Lemma(l: List, v: int, val: int)
 

 // -------------------------------

 

-datatype Expression {

-  Const(int);

-  Var(int);

+datatype Expression =

+  Const(int) |

+  Var(int) |

   Nary(int, seq<Expression>);

-}

 

 static function Substitute(e: Expression, v: int, val: int): Expression

   decreases e;

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index f363a023..a94283e6 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -1,13 +1,8 @@
 // ------------------ generic list, non-generic tree

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype Tree {

-  Node(int, List<Tree>);

-}

+datatype Tree = Node(int, List<Tree>);

 

 static function Inc(t: Tree): Tree

 {

@@ -24,9 +19,7 @@ static function ForestInc(forest: List<Tree>): List<Tree>
 

 // ------------------ generic list, generic tree (but GInc defined only for GTree<int>

 

-datatype GTree<T> {

-  Node(T, List<GTree<T>>);

-}

+datatype GTree<T> = Node(T, List<GTree<T>>);

 

 static function GInc(t: GTree<int>): GTree<int>

 {

@@ -43,14 +36,9 @@ static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
 

 // ------------------ non-generic structures

 

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

+datatype TreeList = Nil | Cons(OneTree, TreeList);

 

-datatype OneTree {

-  Node(int, TreeList);

-}

+datatype OneTree = Node(int, TreeList);

 

 static function XInc(t: OneTree): OneTree

 {