From a0ccbb8461b68eb4a61ba78e0efced94423e93c7 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 19 Apr 2011 16:48:32 -0700
Subject: Dafny: added type "nat"

---
 Dafny/Dafny.atg     |   1 +
 Dafny/DafnyAst.cs   |  20 +-
 Dafny/Parser.cs     | 685 +++++++++++++++++++++++++++-------------------------
 Dafny/Resolver.cs   |  57 +++--
 Dafny/Scanner.cs    | 265 ++++++++++----------
 Dafny/Translator.cs | 163 +++++++++----
 6 files changed, 653 insertions(+), 538 deletions(-)

(limited to 'Dafny')

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 7d7a496c..e32f0745 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -516,6 +516,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
      List<Type/*!*/>/*!*/ gt;
   .)
   ( "bool"                          (. tok = t; .)
+  | "nat"                           (. tok = t;  ty = new NatType(); .)
   | "int"                           (. tok = t;  ty = new IntType(); .)
   | "set"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
     GenericInstantiation<gt>        (. if (gt.Count != 1) {
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 045f879a..69756d76 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -135,6 +135,10 @@ namespace Microsoft.Dafny {
       }
     }
 
+    public bool IsSubrangeType {
+      get { return this is NatType; }
+    }
+
     public bool IsRefType {
       get {
         if (this is ObjectType) {
@@ -197,7 +201,16 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class ObjectType : BasicType {
+  public class NatType : IntType
+  {
+    [Pure]
+    public override string ToString() {
+      return "nat";
+    }
+  }
+
+  public class ObjectType : BasicType
+  {
     [Pure]
     public override string ToString() {
       return "object";
@@ -218,9 +231,8 @@ namespace Microsoft.Dafny {
   }
 
   public class SetType : CollectionType {
-    public SetType(Type arg) :base(arg){
+    public SetType(Type arg) : base(arg) {
       Contract.Requires(arg != null);
-
     }
     [Pure]
     public override string ToString() {
@@ -231,7 +243,7 @@ namespace Microsoft.Dafny {
   }
 
   public class SeqType : CollectionType {
-    public SeqType(Type arg):base(arg) {
+    public SeqType(Type arg) : base(arg) {
       Contract.Requires(arg != null);
 
     }
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 988b73e2..72e66d1d 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -20,12 +20,12 @@ public class Parser {
 	public const int _digits = 2;
 	public const int _arrayToken = 3;
 	public const int _string = 4;
-	public const int maxT = 105;
+	public const int maxT = 106;
 
 	const bool T = true;
 	const bool x = false;
 	const int minErrDist = 2;
-	
+
 	public Scanner/*!*/ scanner;
 	public Errors/*!*/  errors;
 
@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);
 		errDist = 0;
 	}
-	
-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
-      Contract.Requires(tok != null);
-      Contract.Requires(msg != null);
+
+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+	  Contract.Requires(tok != null);
+	  Contract.Requires(msg != null);
 	  errors.SemErr(tok, msg);
 	}
 
@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;
 		}
 	}
-	
+
 	void Expect (int n) {
 		if (la.kind==n) Get(); else { SynErr(n); }
 	}
-	
+
 	bool StartOf (int s) {
 		return set[s, la.kind];
 	}
-	
+
 	void ExpectWeak (int n, int follow) {
 		if (la.kind == n) Get();
 		else {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}
 	}
 
-	
+
 	void Dafny() {
 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
@@ -394,7 +394,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}
 		if (la.kind == 16) {
 			FieldDecl(mmod, mm);
-		} else if (la.kind == 37) {
+		} else if (la.kind == 38) {
 			FunctionDecl(mmod, out f);
 			mm.Add(f); 
 		} else if (la.kind == 10 || la.kind == 23) {
@@ -402,7 +402,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 
 		} else if (la.kind == 18) {
 			CouplingInvDecl(mmod, mm);
-		} else SynErr(106);
+		} else SynErr(107);
 	}
 
 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -457,7 +457,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken bodyStart = Token.NoToken;
 		IToken bodyEnd = Token.NoToken;
 		
-		Expect(37);
+		Expect(38);
 		if (la.kind == 23) {
 			Get();
 			isFunctionMethod = true; 
@@ -486,7 +486,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(108);
 		parseVarScope.PopMarker();
 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
 		f.BodyStartTok = bodyStart;
@@ -515,7 +515,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {
 			Get();
 			isRefinement = true; 
-		} else SynErr(108);
+		} else SynErr(109);
 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
 		
 		while (la.kind == 7) {
@@ -542,7 +542,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(110);
 		parseVarScope.PopMarker();
 		if (isRefinement)
 		  m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -634,18 +634,18 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  Expression/*!*/ e0;  Expression/*!*/ e1 = dummyExpr;
 		e = dummyExpr;
 		
-		if (la.kind == 54) {
+		if (la.kind == 55) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(66);
+			Expect(67);
 			Expression(out e0);
-			Expect(55);
+			Expect(56);
 			Expression(out e1);
 			e = new ITEExpr(x, e, e0, e1); 
 		} else if (StartOf(8)) {
 			EquivExpression(out e);
-		} else SynErr(110);
+		} else SynErr(111);
 	}
 
 	void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
@@ -709,13 +709,23 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
 		List<Type/*!*/>/*!*/ gt;
 		
-		if (la.kind == 32) {
+		switch (la.kind) {
+		case 32: {
 			Get();
 			tok = t; 
-		} else if (la.kind == 33) {
+			break;
+		}
+		case 33: {
+			Get();
+			tok = t;  ty = new NatType(); 
+			break;
+		}
+		case 34: {
 			Get();
 			tok = t;  ty = new IntType(); 
-		} else if (la.kind == 34) {
+			break;
+		}
+		case 35: {
 			Get();
 			tok = t;  gt = new List<Type/*!*/>(); 
 			GenericInstantiation(gt);
@@ -724,7 +734,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}
 			ty = new SetType(gt[0]);
 			
-		} else if (la.kind == 35) {
+			break;
+		}
+		case 36: {
 			Get();
 			tok = t;  gt = new List<Type/*!*/>(); 
 			GenericInstantiation(gt);
@@ -733,9 +745,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}
 			ty = new SeqType(gt[0]);
 			
-		} else if (la.kind == 1 || la.kind == 3 || la.kind == 36) {
+			break;
+		}
+		case 1: case 3: case 37: {
 			ReferenceType(out tok, out ty);
-		} else SynErr(111);
+			break;
+		}
+		default: SynErr(112); break;
+		}
 	}
 
 	void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
@@ -785,12 +802,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);
 				Expect(15);
 				ens.Add(new MaybeFreeExpression(e, isFree)); 
-			} else SynErr(112);
+			} else SynErr(113);
 		} else if (la.kind == 29) {
 			Get();
 			Expressions(decreases);
 			Expect(15);
-		} else SynErr(113);
+		} else SynErr(114);
 	}
 
 	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -812,7 +829,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void FrameExpression(out FrameExpression/*!*/ fe) {
 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; 
 		Expression(out e);
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			Get();
 			Ident(out id);
 			fieldName = id.val; 
@@ -849,7 +866,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
 		List<Type/*!*/>/*!*/ gt;
 		
-		if (la.kind == 36) {
+		if (la.kind == 37) {
 			Get();
 			tok = t;  ty = new ObjectType(); 
 		} else if (la.kind == 3) {
@@ -872,7 +889,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);
 			}
 			ty = new UserDefinedType(tok, tok.val, gt); 
-		} else SynErr(114);
+		} else SynErr(115);
 	}
 
 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -883,7 +900,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expression(out e);
 			Expect(15);
 			reqs.Add(e); 
-		} else if (la.kind == 38) {
+		} else if (la.kind == 39) {
 			Get();
 			if (StartOf(11)) {
 				PossiblyWildFrameExpression(out fe);
@@ -904,51 +921,51 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			Expressions(decreases);
 			Expect(15);
-		} else SynErr(115);
+		} else SynErr(116);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 
 		Expect(7);
 		bodyStart = t; 
-		if (la.kind == 41) {
+		if (la.kind == 42) {
 			MatchExpression(out e);
 		} else if (StartOf(9)) {
 			Expression(out e);
-		} else SynErr(116);
+		} else SynErr(117);
 		Expect(8);
 		bodyEnd = t; 
 	}
 
 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 
-		if (la.kind == 39) {
+		if (la.kind == 40) {
 			Get();
 			fe = new FrameExpression(new WildcardExpr(t), null); 
 		} else if (StartOf(9)) {
 			FrameExpression(out fe);
-		} else SynErr(117);
+		} else SynErr(118);
 	}
 
 	void PossiblyWildExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
 		e = dummyExpr; 
-		if (la.kind == 39) {
+		if (la.kind == 40) {
 			Get();
 			e = new WildcardExpr(t); 
 		} else if (StartOf(9)) {
 			Expression(out e);
-		} else SynErr(118);
+		} else SynErr(119);
 	}
 
 	void MatchExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
 		
-		Expect(41);
+		Expect(42);
 		x = t; 
 		Expression(out e);
-		while (la.kind == 42) {
+		while (la.kind == 43) {
 			CaseExpression(out c);
 			cases.Add(c); 
 		}
@@ -960,7 +977,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
 		Expression/*!*/ body;
 		
-		Expect(42);
+		Expect(43);
 		x = t;  parseVarScope.PushMarker(); 
 		Ident(out id);
 		if (la.kind == 30) {
@@ -976,7 +993,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			Expect(31);
 		}
-		Expect(43);
+		Expect(44);
 		MatchOrExpr(out body);
 		c = new MatchCaseExpr(x, id.val, arguments, body);
 		parseVarScope.PopMarker(); 
@@ -988,11 +1005,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			MatchOrExpr(out e);
 			Expect(31);
-		} else if (la.kind == 41) {
+		} else if (la.kind == 42) {
 			MatchExpression(out e);
 		} else if (StartOf(9)) {
 			Expression(out e);
-		} else SynErr(119);
+		} else SynErr(120);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1008,7 +1025,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ss.Add(s); 
 		} else if (la.kind == 11 || la.kind == 16) {
 			VarDeclStmts(ss);
-		} else SynErr(120);
+		} else SynErr(121);
 	}
 
 	void OneStmt(out Statement/*!*/ s) {
@@ -1016,51 +1033,51 @@ List<Expression/*!*/>/*!*/ decreases) {
 		s = dummyStmt;  /* to please the compiler */
 		
 		switch (la.kind) {
-		case 62: {
+		case 63: {
 			AssertStmt(out s);
 			break;
 		}
-		case 63: {
+		case 64: {
 			AssumeStmt(out s);
 			break;
 		}
-		case 64: {
+		case 65: {
 			UseStmt(out s);
 			break;
 		}
-		case 65: {
+		case 66: {
 			PrintStmt(out s);
 			break;
 		}
-		case 1: case 30: case 97: case 98: {
+		case 1: case 30: case 98: case 99: {
 			AssignStmt(out s, true);
 			break;
 		}
-		case 53: {
+		case 54: {
 			HavocStmt(out s);
 			break;
 		}
-		case 58: {
+		case 59: {
 			CallStmt(out s);
 			break;
 		}
-		case 54: {
+		case 55: {
 			IfStmt(out s);
 			break;
 		}
-		case 56: {
+		case 57: {
 			WhileStmt(out s);
 			break;
 		}
-		case 41: {
+		case 42: {
 			MatchStmt(out s);
 			break;
 		}
-		case 59: {
+		case 60: {
 			ForeachStmt(out s);
 			break;
 		}
-		case 44: {
+		case 45: {
 			Get();
 			x = t; 
 			Ident(out id);
@@ -1068,7 +1085,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			s = new LabelStmt(x, id.val); 
 			break;
 		}
-		case 45: {
+		case 46: {
 			Get();
 			x = t; 
 			if (la.kind == 1) {
@@ -1079,14 +1096,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 			s = new BreakStmt(x, label); 
 			break;
 		}
-		case 46: {
+		case 47: {
 			Get();
 			x = t; 
 			Expect(15);
 			s = new ReturnStmt(x); 
 			break;
 		}
-		default: SynErr(121); break;
+		default: SynErr(122); break;
 		}
 	}
 
@@ -1109,7 +1126,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void AssertStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(62);
+		Expect(63);
 		x = t; 
 		Expression(out e);
 		Expect(15);
@@ -1118,7 +1135,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void AssumeStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(63);
+		Expect(64);
 		x = t; 
 		Expression(out e);
 		Expect(15);
@@ -1127,7 +1144,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void UseStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(64);
+		Expect(65);
 		x = t; 
 		Expression(out e);
 		Expect(15);
@@ -1138,7 +1155,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;
 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
 		
-		Expect(65);
+		Expect(66);
 		x = t; 
 		AttributeArg(out arg);
 		args.Add(arg); 
@@ -1160,7 +1177,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		CallStmt initCall = null;
 		
 		LhsExpr(out lhs);
-		Expect(47);
+		Expect(48);
 		x = t; 
 		AssignRhs(out rhs, out ty, out initCall, lhs);
 		if (ty == null) {
@@ -1184,7 +1201,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void HavocStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ lhs; 
-		Expect(53);
+		Expect(54);
 		x = t; 
 		LhsExpr(out lhs);
 		Expect(15);
@@ -1197,10 +1214,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<IdentifierExpr/*!*/> lhs = new List<IdentifierExpr/*!*/>();
 		List<AutoVarDecl/*!*/> newVars = new List<AutoVarDecl/*!*/>();
 		
-		Expect(58);
+		Expect(59);
 		x = t; 
 		CallStmtSubExpr(out e);
-		if (la.kind == 17 || la.kind == 47) {
+		if (la.kind == 17 || la.kind == 48) {
 			if (la.kind == 17) {
 				Get();
 				e = ConvertToLocal(e);
@@ -1219,7 +1236,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					Ident(out id);
 					RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 
 				}
-				Expect(47);
+				Expect(48);
 				CallStmtSubExpr(out e);
 			} else {
 				Get();
@@ -1254,19 +1271,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Statement els = null;
 		IToken bodyStart, bodyEnd;
 		
-		Expect(54);
+		Expect(55);
 		x = t; 
 		Guard(out guard);
 		BlockStmt(out thn, out bodyStart, out bodyEnd);
-		if (la.kind == 55) {
+		if (la.kind == 56) {
 			Get();
-			if (la.kind == 54) {
+			if (la.kind == 55) {
 				IfStmt(out s);
 				els = s; 
 			} else if (la.kind == 7) {
 				BlockStmt(out s, out bodyStart, out bodyEnd);
 				els = s; 
-			} else SynErr(122);
+			} else SynErr(123);
 		}
 		ifStmt = new IfStmt(x, guard, thn, els); 
 	}
@@ -1280,18 +1297,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Statement/*!*/ body;
 		IToken bodyStart, bodyEnd;
 		
-		Expect(56);
+		Expect(57);
 		x = t; 
 		Guard(out guard);
 		Contract.Assume(guard == null || cce.Owner.None(guard)); 
-		while (la.kind == 26 || la.kind == 29 || la.kind == 57) {
-			if (la.kind == 26 || la.kind == 57) {
+		while (la.kind == 26 || la.kind == 29 || la.kind == 58) {
+			if (la.kind == 26 || la.kind == 58) {
 				isFree = false; 
 				if (la.kind == 26) {
 					Get();
 					isFree = true; 
 				}
-				Expect(57);
+				Expect(58);
 				Expression(out e);
 				invariants.Add(new MaybeFreeExpression(e, isFree)); 
 				Expect(15);
@@ -1315,11 +1332,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);
 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;
 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 
-		Expect(41);
+		Expect(42);
 		x = t; 
 		Expression(out e);
 		Expect(7);
-		while (la.kind == 42) {
+		while (la.kind == 43) {
 			CaseStatement(out c);
 			cases.Add(c); 
 		}
@@ -1336,7 +1353,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		AssignStmt bodyAssign = null;
 		
 		parseVarScope.PushMarker(); 
-		Expect(59);
+		Expect(60);
 		x = t;
 		range = new LiteralExpr(x, true);
 		ty = new InferredTypeProxy();
@@ -1347,20 +1364,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			Type(out ty);
 		}
-		Expect(60);
+		Expect(61);
 		Expression(out collection);
 		parseVarScope.Push(boundVar.val, boundVar.val); 
-		if (la.kind == 61) {
+		if (la.kind == 62) {
 			Get();
 			Expression(out range);
 		}
 		Expect(31);
 		Expect(7);
-		while (la.kind == 62 || la.kind == 63 || la.kind == 64) {
-			if (la.kind == 62) {
+		while (la.kind == 63 || la.kind == 64 || la.kind == 65) {
+			if (la.kind == 63) {
 				AssertStmt(out s);
 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 
-			} else if (la.kind == 63) {
+			} else if (la.kind == 64) {
 				AssumeStmt(out s);
 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 
 			} else {
@@ -1371,10 +1388,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (StartOf(13)) {
 			AssignStmt(out s, false);
 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 
-		} else if (la.kind == 53) {
+		} else if (la.kind == 54) {
 			HavocStmt(out s);
 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 
-		} else SynErr(123);
+		} else SynErr(124);
 		Expect(8);
 		if (bodyAssign != null) {
 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1396,15 +1413,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 		initCall = null;
 		List<Expression> args;
 		
-		if (la.kind == 48) {
+		if (la.kind == 49) {
 			Get();
 			TypeAndToken(out x, out ty);
-			if (la.kind == 49 || la.kind == 51) {
-				if (la.kind == 49) {
+			if (la.kind == 50 || la.kind == 52) {
+				if (la.kind == 50) {
 					Get();
 					ee = new List<Expression>(); 
 					Expressions(ee);
-					Expect(50);
+					Expect(51);
 					UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
 					
 				} else {
@@ -1420,7 +1437,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					                       receiverForInitCall, x.val, args); 
 				}
 			}
-		} else if (la.kind == 52) {
+		} else if (la.kind == 53) {
 			Get();
 			x = t; 
 			Expression(out e);
@@ -1430,7 +1447,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {
 			Expression(out e);
 			ee = new List<Expression>() { e }; 
-		} else SynErr(124);
+		} else SynErr(125);
 		if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; } 
 	}
 
@@ -1438,10 +1455,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 
 		if (la.kind == 1) {
 			IdentOrFuncExpression(out e);
-		} else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
+		} else if (la.kind == 30 || la.kind == 98 || la.kind == 99) {
 			ObjectExpression(out e);
-		} else SynErr(125);
-		while (la.kind == 49 || la.kind == 51) {
+		} else SynErr(126);
+		while (la.kind == 50 || la.kind == 52) {
 			SelectOrCallSuffix(ref e);
 		}
 	}
@@ -1458,7 +1475,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Type(out ty);
 			optionalType = ty; 
 		}
-		if (la.kind == 47) {
+		if (la.kind == 48) {
 			Get();
 			AssignRhs(out rhs, out newType, out initCall, new IdentifierExpr(id, id.val));
 		}
@@ -1481,13 +1498,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void Guard(out Expression e) {
 		Expression/*!*/ ee;  e = null; 
 		Expect(30);
-		if (la.kind == 39) {
+		if (la.kind == 40) {
 			Get();
 			e = null; 
 		} else if (StartOf(9)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(126);
+		} else SynErr(127);
 		Expect(31);
 	}
 
@@ -1497,7 +1514,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
 		List<Statement/*!*/> body = new List<Statement/*!*/>();
 		
-		Expect(42);
+		Expect(43);
 		x = t;  parseVarScope.PushMarker(); 
 		Ident(out id);
 		if (la.kind == 30) {
@@ -1513,7 +1530,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			Expect(31);
 		}
-		Expect(43);
+		Expect(44);
 		parseVarScope.PushMarker(); 
 		while (StartOf(10)) {
 			Stmt(body);
@@ -1527,11 +1544,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 
 		if (la.kind == 1) {
 			IdentOrFuncExpression(out e);
-		} else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
+		} else if (la.kind == 30 || la.kind == 98 || la.kind == 99) {
 			ObjectExpression(out e);
 			SelectOrCallSuffix(ref e);
-		} else SynErr(127);
-		while (la.kind == 49 || la.kind == 51) {
+		} else SynErr(128);
+		while (la.kind == 50 || la.kind == 52) {
 			SelectOrCallSuffix(ref e);
 		}
 	}
@@ -1544,13 +1561,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {
 			Expression(out e);
 			arg = new Attributes.Argument(e); 
-		} else SynErr(128);
+		} else SynErr(129);
 	}
 
 	void EquivExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		ImpliesExpression(out e0);
-		while (la.kind == 67 || la.kind == 68) {
+		while (la.kind == 68 || la.kind == 69) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1561,7 +1578,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void ImpliesExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		LogicalExpression(out e0);
-		if (la.kind == 69 || la.kind == 70) {
+		if (la.kind == 70 || la.kind == 71) {
 			ImpliesOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1570,23 +1587,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 67) {
+		if (la.kind == 68) {
 			Get();
-		} else if (la.kind == 68) {
+		} else if (la.kind == 69) {
 			Get();
-		} else SynErr(129);
+		} else SynErr(130);
 	}
 
 	void LogicalExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(14)) {
-			if (la.kind == 71 || la.kind == 72) {
+			if (la.kind == 72 || la.kind == 73) {
 				AndOp();
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 
-				while (la.kind == 71 || la.kind == 72) {
+				while (la.kind == 72 || la.kind == 73) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1597,7 +1614,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 
-				while (la.kind == 73 || la.kind == 74) {
+				while (la.kind == 74 || la.kind == 75) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1608,11 +1625,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 69) {
+		if (la.kind == 70) {
 			Get();
-		} else if (la.kind == 70) {
+		} else if (la.kind == 71) {
 			Get();
-		} else SynErr(130);
+		} else SynErr(131);
 	}
 
 	void RelationalExpression(out Expression/*!*/ e0) {
@@ -1626,25 +1643,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void AndOp() {
-		if (la.kind == 71) {
+		if (la.kind == 72) {
 			Get();
-		} else if (la.kind == 72) {
+		} else if (la.kind == 73) {
 			Get();
-		} else SynErr(131);
+		} else SynErr(132);
 	}
 
 	void OrOp() {
-		if (la.kind == 73) {
+		if (la.kind == 74) {
 			Get();
-		} else if (la.kind == 74) {
+		} else if (la.kind == 75) {
 			Get();
-		} else SynErr(132);
+		} else SynErr(133);
 	}
 
 	void Term(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 
 		Factor(out e0);
-		while (la.kind == 84 || la.kind == 85) {
+		while (la.kind == 85 || la.kind == 86) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -1654,7 +1671,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 
 		switch (la.kind) {
-		case 75: {
+		case 76: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Eq; 
 			break;
@@ -1669,59 +1686,59 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 76: {
+		case 77: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 77: {
+		case 78: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 78: {
+		case 79: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 79: {
+		case 80: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Disjoint; 
 			break;
 		}
-		case 60: {
+		case 61: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.In; 
 			break;
 		}
-		case 80: {
+		case 81: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.NotIn; 
 			break;
 		}
-		case 81: {
+		case 82: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 82: {
+		case 83: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(133); break;
+		default: SynErr(134); 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 == 39 || la.kind == 86 || la.kind == 87) {
+		while (la.kind == 40 || la.kind == 87 || la.kind == 88) {
 			MulOp(out x, out op);
 			UnaryExpression(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -1730,23 +1747,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 84) {
+		if (la.kind == 85) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Add; 
-		} else if (la.kind == 85) {
+		} else if (la.kind == 86) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Sub; 
-		} else SynErr(134);
+		} else SynErr(135);
 	}
 
 	void UnaryExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 
-		} else if (la.kind == 88 || la.kind == 89) {
+		} else if (la.kind == 89 || la.kind == 90) {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
@@ -1755,29 +1772,29 @@ List<Expression/*!*/>/*!*/ decreases) {
 			SelectExpression(out e);
 		} else if (StartOf(16)) {
 			ConstAtomExpression(out e);
-		} else SynErr(135);
+		} else SynErr(136);
 	}
 
 	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 == 39) {
+		if (la.kind == 40) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mul; 
-		} else if (la.kind == 86) {
+		} else if (la.kind == 87) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Div; 
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mod; 
-		} else SynErr(136);
+		} else SynErr(137);
 	}
 
 	void NegOp() {
-		if (la.kind == 88) {
+		if (la.kind == 89) {
 			Get();
-		} else if (la.kind == 89) {
+		} else if (la.kind == 90) {
 			Get();
-		} else SynErr(137);
+		} else SynErr(138);
 	}
 
 	void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1785,17 +1802,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		e = dummyExpr;
 		
 		switch (la.kind) {
-		case 90: {
+		case 91: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 91: {
+		case 92: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 92: {
+		case 93: {
 			Get();
 			e = new LiteralExpr(t); 
 			break;
@@ -1805,11 +1822,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LiteralExpr(t, n); 
 			break;
 		}
-		case 93: {
+		case 94: {
 			Get();
 			x = t; 
 			Ident(out dtName);
-			Expect(51);
+			Expect(52);
 			Ident(out id);
 			elements = new List<Expression/*!*/>(); 
 			if (la.kind == 30) {
@@ -1822,7 +1839,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new DatatypeValue(t, dtName.val, id.val, elements); 
 			break;
 		}
-		case 94: {
+		case 95: {
 			Get();
 			x = t; 
 			Expect(30);
@@ -1831,7 +1848,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new FreshExpr(x, e); 
 			break;
 		}
-		case 95: {
+		case 96: {
 			Get();
 			x = t; 
 			Expect(30);
@@ -1840,12 +1857,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AllocatedExpr(x, e); 
 			break;
 		}
-		case 61: {
+		case 62: {
 			Get();
 			x = t; 
 			Expression(out e);
 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 
-			Expect(61);
+			Expect(62);
 			break;
 		}
 		case 7: {
@@ -1858,17 +1875,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(8);
 			break;
 		}
-		case 49: {
+		case 50: {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(9)) {
 				Expressions(elements);
 			}
 			e = new SeqDisplayExpr(x, elements); 
-			Expect(50);
+			Expect(51);
 			break;
 		}
-		default: SynErr(138); break;
+		default: SynErr(139); break;
 		}
 	}
 
@@ -1907,10 +1924,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void ObjectExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
-		if (la.kind == 97) {
+		if (la.kind == 98) {
 			Get();
 			e = new ThisExpr(t); 
-		} else if (la.kind == 98) {
+		} else if (la.kind == 99) {
 			Get();
 			x = t; 
 			Expect(30);
@@ -1923,9 +1940,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 				QuantifierGuts(out e);
 			} else if (StartOf(9)) {
 				Expression(out e);
-			} else SynErr(139);
+			} else SynErr(140);
 			Expect(31);
-		} else SynErr(140);
+		} else SynErr(141);
 	}
 
 	void SelectOrCallSuffix(ref Expression/*!*/ e) {
@@ -1934,7 +1951,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> multipleIndices = null;
 		bool func = false;
 		
-		if (la.kind == 51) {
+		if (la.kind == 52) {
 			Get();
 			Ident(out id);
 			if (la.kind == 30) {
@@ -1947,24 +1964,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 				e = new FunctionCallExpr(id, id.val, e, args); 
 			}
 			if (!func) { e = new FieldSelectExpr(id, e, id.val); } 
-		} else if (la.kind == 49) {
+		} else if (la.kind == 50) {
 			Get();
 			x = t; 
 			if (StartOf(9)) {
 				Expression(out ee);
 				e0 = ee; 
-				if (la.kind == 96) {
+				if (la.kind == 97) {
 					Get();
 					anyDots = true; 
 					if (StartOf(9)) {
 						Expression(out ee);
 						e1 = ee; 
 					}
-				} else if (la.kind == 47) {
+				} else if (la.kind == 48) {
 					Get();
 					Expression(out ee);
 					e1 = ee; 
-				} else if (la.kind == 17 || la.kind == 50) {
+				} else if (la.kind == 17 || la.kind == 51) {
 					while (la.kind == 17) {
 						Get();
 						Expression(out ee);
@@ -1975,12 +1992,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(141);
-			} else if (la.kind == 96) {
+				} else SynErr(142);
+			} else if (la.kind == 97) {
 				Get();
 				Expression(out ee);
 				anyDots = true;  e1 = ee; 
-			} else SynErr(142);
+			} else SynErr(143);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			} else {
@@ -2001,8 +2018,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  }
 			}
 			
-			Expect(50);
-		} else SynErr(143);
+			Expect(51);
+		} else SynErr(144);
 	}
 
 	void QuantifierGuts(out Expression/*!*/ q) {
@@ -2014,13 +2031,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Triggers trigs = null;
 		Expression/*!*/ body;
 		
-		if (la.kind == 99 || la.kind == 100) {
+		if (la.kind == 100 || la.kind == 101) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 101 || la.kind == 102) {
+		} else if (la.kind == 102 || la.kind == 103) {
 			Exists();
 			x = t; 
-		} else SynErr(144);
+		} else SynErr(145);
 		parseVarScope.PushMarker(); 
 		IdentTypeOptional(out bv);
 		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 
@@ -2044,19 +2061,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void Forall() {
-		if (la.kind == 99) {
+		if (la.kind == 100) {
 			Get();
-		} else if (la.kind == 100) {
+		} else if (la.kind == 101) {
 			Get();
-		} else SynErr(145);
+		} else SynErr(146);
 	}
 
 	void Exists() {
-		if (la.kind == 101) {
+		if (la.kind == 102) {
 			Get();
-		} else if (la.kind == 102) {
+		} else if (la.kind == 103) {
 			Get();
-		} else SynErr(146);
+		} else SynErr(147);
 	}
 
 	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2069,16 +2086,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 			es = new List<Expression/*!*/>(); 
 			Expressions(es);
 			trigs = new Triggers(es, trigs); 
-		} else SynErr(147);
+		} else SynErr(148);
 		Expect(8);
 	}
 
 	void QSep() {
-		if (la.kind == 103) {
+		if (la.kind == 104) {
 			Get();
-		} else if (la.kind == 104) {
+		} else if (la.kind == 105) {
 			Get();
-		} else SynErr(148);
+		} else SynErr(149);
 	}
 
 	void AttributeBody(ref Attributes attrs) {
@@ -2105,33 +2122,33 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	public void Parse() {
 		la = new Token();
-		la.val = "";		
+		la.val = "";
 		Get();
 		Dafny();
 
-    Expect(0);
+		Expect(0);
 	}
-	
+
 	static readonly bool[,]/*!*/ set = {
-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,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,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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,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, 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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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, x,T,T,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,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,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
-		{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,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,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,x,x, T,T,T,T, T,T,T,T, x,T,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, 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,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
-		{x,T,x,x, x,x,x,x, x,x,x,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,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,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,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, 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,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,x,x,x, x,x,x,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,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,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,x,x,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,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,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, 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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,x, x,T,T,T, T,T,T,T, T,x,T,T, 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,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,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x},
+		{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,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, 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,x, x,T,T,T, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x},
+		{x,T,x,x, x,x,x,x, x,x,x,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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,x,x,x, x,x,x,x, 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,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,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x}
 
 	};
 } // end Parser
@@ -2140,18 +2157,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {
 	public int count = 0;                                    // number of errors detected
 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream
-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  
+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
 	public void SynErr(string filename, int line, int col, int n) {
-    SynErr(filename, line, col, GetSyntaxErrorString(n));
-  }
-	public virtual void SynErr(string filename, int line, int col, string msg) {
-	  Contract.Requires(msg != null);
+		SynErr(filename, line, col, GetSyntaxErrorString(n));
+	}
+
+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
-  }
-  string GetSyntaxErrorString(int n) {
+	}
+
+	string GetSyntaxErrorString(int n) {
 		string s;
 		switch (n) {
 			case 0: s = "EOF expected"; break;
@@ -2187,126 +2206,127 @@ public class Errors {
 			case 30: s = "\"(\" expected"; break;
 			case 31: s = "\")\" expected"; break;
 			case 32: s = "\"bool\" expected"; break;
-			case 33: s = "\"int\" expected"; break;
-			case 34: s = "\"set\" expected"; break;
-			case 35: s = "\"seq\" expected"; break;
-			case 36: s = "\"object\" expected"; break;
-			case 37: s = "\"function\" expected"; break;
-			case 38: s = "\"reads\" expected"; break;
-			case 39: s = "\"*\" expected"; break;
-			case 40: s = "\"`\" expected"; break;
-			case 41: s = "\"match\" expected"; break;
-			case 42: s = "\"case\" expected"; break;
-			case 43: s = "\"=>\" expected"; break;
-			case 44: s = "\"label\" expected"; break;
-			case 45: s = "\"break\" expected"; break;
-			case 46: s = "\"return\" expected"; break;
-			case 47: s = "\":=\" expected"; break;
-			case 48: s = "\"new\" expected"; break;
-			case 49: s = "\"[\" expected"; break;
-			case 50: s = "\"]\" expected"; break;
-			case 51: s = "\".\" expected"; break;
-			case 52: s = "\"choose\" expected"; break;
-			case 53: s = "\"havoc\" expected"; break;
-			case 54: s = "\"if\" expected"; break;
-			case 55: s = "\"else\" expected"; break;
-			case 56: s = "\"while\" expected"; break;
-			case 57: s = "\"invariant\" expected"; break;
-			case 58: s = "\"call\" expected"; break;
-			case 59: s = "\"foreach\" expected"; break;
-			case 60: s = "\"in\" expected"; break;
-			case 61: s = "\"|\" expected"; break;
-			case 62: s = "\"assert\" expected"; break;
-			case 63: s = "\"assume\" expected"; break;
-			case 64: s = "\"use\" expected"; break;
-			case 65: s = "\"print\" expected"; break;
-			case 66: s = "\"then\" expected"; break;
-			case 67: s = "\"<==>\" expected"; break;
-			case 68: s = "\"\\u21d4\" expected"; break;
-			case 69: s = "\"==>\" expected"; break;
-			case 70: s = "\"\\u21d2\" expected"; break;
-			case 71: s = "\"&&\" expected"; break;
-			case 72: s = "\"\\u2227\" expected"; break;
-			case 73: s = "\"||\" expected"; break;
-			case 74: s = "\"\\u2228\" expected"; break;
-			case 75: s = "\"==\" expected"; break;
-			case 76: s = "\"<=\" expected"; break;
-			case 77: s = "\">=\" expected"; break;
-			case 78: s = "\"!=\" expected"; break;
-			case 79: s = "\"!!\" expected"; break;
-			case 80: s = "\"!in\" expected"; break;
-			case 81: s = "\"\\u2260\" expected"; break;
-			case 82: s = "\"\\u2264\" expected"; break;
-			case 83: s = "\"\\u2265\" expected"; break;
-			case 84: s = "\"+\" expected"; break;
-			case 85: s = "\"-\" expected"; break;
-			case 86: s = "\"/\" expected"; break;
-			case 87: s = "\"%\" expected"; break;
-			case 88: s = "\"!\" expected"; break;
-			case 89: s = "\"\\u00ac\" expected"; break;
-			case 90: s = "\"false\" expected"; break;
-			case 91: s = "\"true\" expected"; break;
-			case 92: s = "\"null\" expected"; break;
-			case 93: s = "\"#\" expected"; break;
-			case 94: s = "\"fresh\" expected"; break;
-			case 95: s = "\"allocated\" expected"; break;
-			case 96: s = "\"..\" expected"; break;
-			case 97: s = "\"this\" expected"; break;
-			case 98: s = "\"old\" expected"; break;
-			case 99: s = "\"forall\" expected"; break;
-			case 100: s = "\"\\u2200\" expected"; break;
-			case 101: s = "\"exists\" expected"; break;
-			case 102: s = "\"\\u2203\" expected"; break;
-			case 103: s = "\"::\" expected"; break;
-			case 104: s = "\"\\u2022\" expected"; break;
-			case 105: s = "??? expected"; break;
-			case 106: s = "invalid ClassMemberDecl"; break;
-			case 107: s = "invalid FunctionDecl"; break;
-			case 108: s = "invalid MethodDecl"; break;
+			case 33: s = "\"nat\" expected"; break;
+			case 34: s = "\"int\" expected"; break;
+			case 35: s = "\"set\" expected"; break;
+			case 36: s = "\"seq\" expected"; break;
+			case 37: s = "\"object\" expected"; break;
+			case 38: s = "\"function\" expected"; break;
+			case 39: s = "\"reads\" expected"; break;
+			case 40: s = "\"*\" expected"; break;
+			case 41: s = "\"`\" expected"; break;
+			case 42: s = "\"match\" expected"; break;
+			case 43: s = "\"case\" expected"; break;
+			case 44: s = "\"=>\" expected"; break;
+			case 45: s = "\"label\" expected"; break;
+			case 46: s = "\"break\" expected"; break;
+			case 47: s = "\"return\" expected"; break;
+			case 48: s = "\":=\" expected"; break;
+			case 49: s = "\"new\" expected"; break;
+			case 50: s = "\"[\" expected"; break;
+			case 51: s = "\"]\" expected"; break;
+			case 52: s = "\".\" expected"; break;
+			case 53: s = "\"choose\" expected"; break;
+			case 54: s = "\"havoc\" expected"; break;
+			case 55: s = "\"if\" expected"; break;
+			case 56: s = "\"else\" expected"; break;
+			case 57: s = "\"while\" expected"; break;
+			case 58: s = "\"invariant\" expected"; break;
+			case 59: s = "\"call\" expected"; break;
+			case 60: s = "\"foreach\" expected"; break;
+			case 61: s = "\"in\" expected"; break;
+			case 62: s = "\"|\" expected"; break;
+			case 63: s = "\"assert\" expected"; break;
+			case 64: s = "\"assume\" expected"; break;
+			case 65: s = "\"use\" expected"; break;
+			case 66: s = "\"print\" expected"; break;
+			case 67: s = "\"then\" 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 = "\"\\u2260\" expected"; break;
+			case 83: s = "\"\\u2264\" expected"; break;
+			case 84: s = "\"\\u2265\" expected"; break;
+			case 85: s = "\"+\" expected"; break;
+			case 86: s = "\"-\" expected"; break;
+			case 87: s = "\"/\" expected"; break;
+			case 88: s = "\"%\" expected"; break;
+			case 89: s = "\"!\" 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 = "\"#\" expected"; break;
+			case 95: s = "\"fresh\" expected"; break;
+			case 96: s = "\"allocated\" expected"; break;
+			case 97: s = "\"..\" expected"; break;
+			case 98: s = "\"this\" expected"; break;
+			case 99: s = "\"old\" 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 ClassMemberDecl"; break;
+			case 108: s = "invalid FunctionDecl"; break;
 			case 109: s = "invalid MethodDecl"; break;
-			case 110: s = "invalid Expression"; break;
-			case 111: s = "invalid TypeAndToken"; break;
-			case 112: s = "invalid MethodSpec"; break;
+			case 110: s = "invalid MethodDecl"; break;
+			case 111: s = "invalid Expression"; break;
+			case 112: s = "invalid TypeAndToken"; break;
 			case 113: s = "invalid MethodSpec"; break;
-			case 114: s = "invalid ReferenceType"; break;
-			case 115: s = "invalid FunctionSpec"; break;
-			case 116: s = "invalid FunctionBody"; break;
-			case 117: s = "invalid PossiblyWildFrameExpression"; break;
-			case 118: s = "invalid PossiblyWildExpression"; break;
-			case 119: s = "invalid MatchOrExpr"; break;
-			case 120: s = "invalid Stmt"; break;
-			case 121: s = "invalid OneStmt"; break;
-			case 122: s = "invalid IfStmt"; break;
-			case 123: s = "invalid ForeachStmt"; break;
-			case 124: s = "invalid AssignRhs"; break;
-			case 125: s = "invalid SelectExpression"; break;
-			case 126: s = "invalid Guard"; break;
-			case 127: s = "invalid CallStmtSubExpr"; 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 ConstAtomExpression"; break;
-			case 139: s = "invalid ObjectExpression"; break;
+			case 114: s = "invalid MethodSpec"; break;
+			case 115: s = "invalid ReferenceType"; break;
+			case 116: s = "invalid FunctionSpec"; break;
+			case 117: s = "invalid FunctionBody"; break;
+			case 118: s = "invalid PossiblyWildFrameExpression"; break;
+			case 119: s = "invalid PossiblyWildExpression"; break;
+			case 120: s = "invalid MatchOrExpr"; break;
+			case 121: s = "invalid Stmt"; break;
+			case 122: s = "invalid OneStmt"; break;
+			case 123: s = "invalid IfStmt"; break;
+			case 124: s = "invalid ForeachStmt"; break;
+			case 125: s = "invalid AssignRhs"; break;
+			case 126: s = "invalid SelectExpression"; break;
+			case 127: s = "invalid Guard"; break;
+			case 128: s = "invalid CallStmtSubExpr"; 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 ConstAtomExpression"; break;
 			case 140: s = "invalid ObjectExpression"; break;
-			case 141: s = "invalid SelectOrCallSuffix"; break;
+			case 141: s = "invalid ObjectExpression"; break;
 			case 142: s = "invalid SelectOrCallSuffix"; break;
 			case 143: s = "invalid SelectOrCallSuffix"; 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 144: s = "invalid SelectOrCallSuffix"; break;
+			case 145: s = "invalid QuantifierGuts"; break;
+			case 146: s = "invalid Forall"; break;
+			case 147: s = "invalid Exists"; break;
+			case 148: s = "invalid AttributeOrTrigger"; break;
+			case 149: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
-    return s;
+		return s;
 	}
 
 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors
@@ -2314,8 +2334,9 @@ public class Errors {
 		Contract.Requires(msg != null);
 		SemErr(tok.filename, tok.line, tok.col, msg);
 	}
+
 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
-	  Contract.Requires(msg != null);
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
 	}
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 6fe3a3c1..22a58a39 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -281,7 +281,7 @@ namespace Microsoft.Dafny {
       foreach (MemberDecl member in cl.Members) {
         member.EnclosingClass = cl;
         if (member is Field) {
-          ResolveType(((Field)member).Type);
+          ResolveType(member.tok, ((Field)member).Type);
           
         } else if (member is Function) {
           Function f = (Function)member;
@@ -581,9 +581,9 @@ namespace Microsoft.Dafny {
         if (!scope.Push(p.Name, p)) {
           Error(p, "Duplicate parameter name: {0}", p.Name);
         }
-        ResolveType(p.Type);
+        ResolveType(p.tok, p.Type);
       }
-      ResolveType(f.ResultType);
+      ResolveType(f.tok, f.ResultType);
       scope.PopMarker();
     }
 
@@ -679,14 +679,14 @@ namespace Microsoft.Dafny {
         if (!scope.Push(p.Name, p)) {
           Error(p, "Duplicate parameter name: {0}", p.Name);
         }
-        ResolveType(p.Type);
+        ResolveType(p.tok, p.Type);
       }
       // resolve out-parameters
       foreach (Formal p in m.Outs) {
         if (!scope.Push(p.Name, p)) {
           Error(p, "Duplicate parameter name: {0}", p.Name);
         }
-        ResolveType(p.Type);
+        ResolveType(p.tok, p.Type);
       }
       scope.PopMarker();
     }
@@ -756,21 +756,29 @@ namespace Microsoft.Dafny {
         if (!scope.Push(p.Name, p)) {
           Error(p, "Duplicate parameter name: {0}", p.Name);
         }
-        ResolveType(p.Type);
+        ResolveType(p.tok, p.Type);
       }
       scope.PopMarker();
     }
 
-    public void ResolveType(Type type) {
+    public void ResolveType(IToken tok, Type type) {
       Contract.Requires(type != null);
       if (type is BasicType) {
         // nothing to resolve
       } else if (type is CollectionType) {
-        ResolveType(((CollectionType)type).Arg);
+        var t = (CollectionType)type;
+        var argType = t.Arg;
+        ResolveType(tok, argType);
+        if (argType.IsSubrangeType) {
+          Error(tok, "sorry, cannot instantiate collection type with a subrange type");
+        }
       } else if (type is UserDefinedType) {
         UserDefinedType t = (UserDefinedType)type;
         foreach (Type tt in t.TypeArgs) {
-          ResolveType(tt);
+          ResolveType(t.tok, tt);
+          if (tt.IsSubrangeType) {
+            Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
+          }
         }
         TypeParameter tp = allTypeParameters.Find(t.Name);
         if (tp != null) {
@@ -793,7 +801,7 @@ namespace Microsoft.Dafny {
       } else if (type is TypeProxy) {
         TypeProxy t = (TypeProxy)type;
         if (t.T != null) {
-          ResolveType(t.T);
+          ResolveType(tok, t.T);
         }
         
       } else {
@@ -965,8 +973,12 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected proxy type
       }
       
-      // do the merge
-      proxy.T = t;
+      // do the merge, but never infer a subrange type
+      if (t is NatType) {
+        proxy.T = Type.Int;
+      } else {
+        proxy.T = t;
+      }
       return true;
     }
     
@@ -1241,7 +1253,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is VarDecl) {
         VarDecl s = (VarDecl)stmt;
         if (s.OptionalType != null) {
-          ResolveType(s.OptionalType);
+          ResolveType(stmt.Tok, s.OptionalType);
           s.type = s.OptionalType;
         }
         if (s.Rhs != null) {
@@ -1343,7 +1355,7 @@ namespace Microsoft.Dafny {
         scope.PushMarker();
         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
         Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed
-        ResolveType(s.BoundVar.Type);
+        ResolveType(s.BoundVar.tok, s.BoundVar.Type);
         int prevErrorCount = ErrorCount;
         
         ResolveExpression(s.Range, true, true);
@@ -1437,7 +1449,7 @@ namespace Microsoft.Dafny {
             if (!scope.Push(v.Name, v)) {
               Error(v, "Duplicate parameter name: {0}", v.Name);
             }
-            ResolveType(v.Type);
+            ResolveType(v.tok, v.Type);
             if (ctor != null && i < ctor.Formals.Count) {
               Formal formal = ctor.Formals[i];
               Type st = SubstType(formal.Type, subst);
@@ -1609,7 +1621,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(method != null);
       Contract.Ensures(Contract.Result<Type>() != null);
 
-      ResolveType(rr.EType);
+      ResolveType(stmt.Tok, rr.EType);
       if (rr.ArrayDimensions == null) {
         if (!rr.EType.IsRefType) {
           Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
@@ -1619,6 +1631,9 @@ namespace Microsoft.Dafny {
         rr.Type = rr.EType;
       } else {
         int i = 0;
+        if (rr.EType.IsSubrangeType) {
+          Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");
+        }
         foreach (Expression dim in rr.ArrayDimensions) {
           Contract.Assert(dim != null);
           ResolveExpression(dim, true, specContext);
@@ -1807,7 +1822,7 @@ namespace Microsoft.Dafny {
             subst.Add(dt.TypeArgs[i], t);
           }
           expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
-          ResolveType(expr.Type);
+          ResolveType(expr.tok, expr.Type);
           
           DatatypeCtor ctor;
           if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
@@ -2196,7 +2211,7 @@ namespace Microsoft.Dafny {
           if (!scope.Push(v.Name, v)) {
             Error(v, "Duplicate bound-variable name: {0}", v.Name);
           }
-          ResolveType(v.Type);
+          ResolveType(v.tok, v.Type);
         }
         ResolveExpression(e.Body, twoState, specContext);
         Contract.Assert(e.Body.Type != null);  // follows from postcondition of ResolveExpression
@@ -2304,7 +2319,7 @@ namespace Microsoft.Dafny {
             if (!scope.Push(v.Name, v)) {
               Error(v, "Duplicate parameter name: {0}", v.Name);
             }
-            ResolveType(v.Type);
+            ResolveType(v.tok, v.Type);
             if (ctor != null && i < ctor.Formals.Count) {
               Formal formal = ctor.Formals[i];
               Type st = SubstType(formal.Type, subst);
@@ -2360,7 +2375,7 @@ namespace Microsoft.Dafny {
           bounds.Add(new QuantifierExpr.BoolBoundedPool());
         } else {
           // Go through the conjuncts of the range expression look for bounds.
-          Expression lowerBound = null;
+          Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
           Expression upperBound = null;
           foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {
             var c = conjunct as BinaryExpr;
@@ -2388,7 +2403,7 @@ namespace Microsoft.Dafny {
                 }
                 break;
               case BinaryExpr.ResolvedOpcode.EqCommon:
-                if (bv.Type == Type.Int) {
+                if (bv.Type is IntType) {
                   var otherOperand = whereIsBv == 0 ? e1 : e0;
                   bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
                   goto CHECK_NEXT_BOUND_VARIABLE;
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index e3c84a73..2846e17a 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer
 	//    b) part of stream in buffer
 	// 2) non seekable stream (network, console)
-  
+
 	public const int EOF = 65535 + 1; // char.MaxValue + 1;
 	const int MIN_BUFFER_LENGTH = 1024; // 1KB
 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)
 	bool isUserStream;  // was the stream opened by the user?
 
-[ContractInvariantMethod]
-void ObjectInvariant(){
-  Contract.Invariant(buf != null);
-  Contract.Invariant(stream != null);}
-    [NotDelayed]
-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+	[ContractInvariantMethod]
+	void ObjectInvariant(){
+		Contract.Invariant(buf != null);
+		Contract.Invariant(stream != null);
+	}
+
+//  [NotDelayed]
+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
 	  Contract.Requires(s != null);
 		stream = s; this.isUserStream = isUserStream;
-		
+
 		int fl, bl;
 		if (s.CanSeek) {
 			fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
 
 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
 		fileLen = fl;  bufLen = bl;
-		
+
 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
 		if (bufLen == fileLen && s.CanSeek) Close();
 	}
-	
+
 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
 	  Contract.Requires(b != null);
 		buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}
 
 	~Buffer() { Close(); }
-	
+
 	protected void Close() {
 		if (!isUserStream && stream != null) {
 			stream.Close();
 			//stream = null;
 		}
 	}
-	
+
 	public virtual int Read () {
 		if (bufPos < bufLen) {
 			return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;
 		return ch;
 	}
-	
+
 	public string/*!*/ GetString (int beg, int end) {
 	  Contract.Ensures(Contract.Result<string>() != null);
 		int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}
 		}
 	}
-	
+
 	// Read the next chunk of bytes from the stream, increases the buffer
 	// if needed and updates the fields fileLen and bufLen.
 	// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 105;
-	const int noSym = 105;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
-  Contract.Invariant(buffer!=null);
-  Contract.Invariant(t != null);
-  Contract.Invariant(start != null);
-  Contract.Invariant(tokens != null);
-  Contract.Invariant(pt != null);
-  Contract.Invariant(tval != null);
-  Contract.Invariant(Filename != null);
-  Contract.Invariant(errorHandler != null);
-}
+	const int maxT = 106;
+	const int noSym = 106;
+
+
+	[ContractInvariantMethod]
+	void objectInvariant(){
+		Contract.Invariant(buffer!=null);
+		Contract.Invariant(t != null);
+		Contract.Invariant(start != null);
+		Contract.Invariant(tokens != null);
+		Contract.Invariant(pt != null);
+		Contract.Invariant(tval != null);
+		Contract.Invariant(Filename != null);
+		Contract.Invariant(errorHandler != null);
+	}
+
 	public Buffer/*!*/ buffer; // scanner buffer
-	
+
 	Token/*!*/ t;          // current token
 	int ch;           // current input character
 	int pos;          // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
 
 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)
 	Token/*!*/ pt;         // current peek token
-	
+
 	char[]/*!*/ tval = new char[128]; // text of current token
 	int tlen;         // length of current token
-	
+
 	private string/*!*/ Filename;
 	private Errors/*!*/ errorHandler;
-	
+
 	static Scanner() {
 		start = new Hashtable(128);
 		for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -291,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;
 
 	}
-	
-	[NotDelayed]
-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+//	[NotDelayed]
+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
 	  Contract.Requires(fileName != null);
 	  Contract.Requires(errorHandler != null);
 		this.errorHandler = errorHandler;
@@ -303,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
 			buffer = new Buffer(stream, false);
 			Filename = fileName;
-			
 			Init();
 		} catch (IOException) {
 			throw new FatalError("Cannot open file " + fileName);
 		}
 	}
-	
-	[NotDelayed]
-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+//	[NotDelayed]
+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
 	  Contract.Requires(s != null);
 	  Contract.Requires(errorHandler != null);
 	  Contract.Requires(fileName != null);
@@ -320,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);
 		this.errorHandler = errorHandler;
 		this.Filename = fileName;
-		
 		Init();
 	}
-	
+
 	void Init() {
 		pos = -1; line = 1; col = 0;
 		oldEols = 0;
@@ -344,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);
 	  int p = buffer.Pos;
 	  int ch = buffer.Read();
-      // replace isolated '\r' by '\n' in order to make
+	  // replace isolated '\r' by '\n' in order to make
 	  // eol handling uniform across Windows, Unix and Mac
 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 	  while (ch != EOL && ch != Buffer.EOF){
-	    ch = buffer.Read();
+		ch = buffer.Read();
 		// replace isolated '\r' by '\n' in order to make
 		// eol handling uniform across Windows, Unix and Mac
 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -359,7 +360,7 @@ void objectInvariant(){
 	}
 
 	void NextCh() {
-		if (oldEols > 0) { ch = EOL; oldEols--; } 
+		if (oldEols > 0) { ch = EOL; oldEols--; }
 		else {
 //			pos = buffer.Pos;
 //			ch = buffer.Read(); col++;
@@ -367,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac
 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 //			if (ch == EOL) { line++; col = 0; }
-			
+
 			while (true) {
-			    pos = buffer.Pos;
+				pos = buffer.Pos;
 				ch = buffer.Read(); col++;
 				// replace isolated '\r' by '\n' in order to make
 				// eol handling uniform across Windows, Unix and Mac
@@ -419,7 +420,7 @@ void objectInvariant(){
 				return;
 			  }
 
-			
+
 		}
 
 	}
@@ -506,41 +507,42 @@ void objectInvariant(){
 			case "ensures": t.kind = 28; break;
 			case "decreases": t.kind = 29; break;
 			case "bool": t.kind = 32; break;
-			case "int": t.kind = 33; break;
-			case "set": t.kind = 34; break;
-			case "seq": t.kind = 35; break;
-			case "object": t.kind = 36; break;
-			case "function": t.kind = 37; break;
-			case "reads": t.kind = 38; break;
-			case "match": t.kind = 41; break;
-			case "case": t.kind = 42; break;
-			case "label": t.kind = 44; break;
-			case "break": t.kind = 45; break;
-			case "return": t.kind = 46; break;
-			case "new": t.kind = 48; break;
-			case "choose": t.kind = 52; break;
-			case "havoc": t.kind = 53; break;
-			case "if": t.kind = 54; break;
-			case "else": t.kind = 55; break;
-			case "while": t.kind = 56; break;
-			case "invariant": t.kind = 57; break;
-			case "call": t.kind = 58; break;
-			case "foreach": t.kind = 59; break;
-			case "in": t.kind = 60; break;
-			case "assert": t.kind = 62; break;
-			case "assume": t.kind = 63; break;
-			case "use": t.kind = 64; break;
-			case "print": t.kind = 65; break;
-			case "then": t.kind = 66; break;
-			case "false": t.kind = 90; break;
-			case "true": t.kind = 91; break;
-			case "null": t.kind = 92; break;
-			case "fresh": t.kind = 94; break;
-			case "allocated": t.kind = 95; break;
-			case "this": t.kind = 97; break;
-			case "old": t.kind = 98; break;
-			case "forall": t.kind = 99; break;
-			case "exists": t.kind = 101; break;
+			case "nat": t.kind = 33; break;
+			case "int": t.kind = 34; break;
+			case "set": t.kind = 35; break;
+			case "seq": t.kind = 36; break;
+			case "object": t.kind = 37; break;
+			case "function": t.kind = 38; break;
+			case "reads": t.kind = 39; break;
+			case "match": t.kind = 42; break;
+			case "case": t.kind = 43; break;
+			case "label": t.kind = 45; break;
+			case "break": t.kind = 46; break;
+			case "return": t.kind = 47; break;
+			case "new": t.kind = 49; break;
+			case "choose": t.kind = 53; break;
+			case "havoc": t.kind = 54; break;
+			case "if": t.kind = 55; break;
+			case "else": t.kind = 56; break;
+			case "while": t.kind = 57; break;
+			case "invariant": t.kind = 58; break;
+			case "call": t.kind = 59; break;
+			case "foreach": t.kind = 60; break;
+			case "in": t.kind = 61; break;
+			case "assert": t.kind = 63; break;
+			case "assume": t.kind = 64; break;
+			case "use": t.kind = 65; break;
+			case "print": t.kind = 66; break;
+			case "then": t.kind = 67; break;
+			case "false": t.kind = 91; break;
+			case "true": t.kind = 92; break;
+			case "null": t.kind = 93; break;
+			case "fresh": t.kind = 95; break;
+			case "allocated": t.kind = 96; break;
+			case "this": t.kind = 98; break;
+			case "old": t.kind = 99; break;
+			case "forall": t.kind = 100; break;
+			case "exists": t.kind = 102; break;
 			default: break;
 		}
 	}
@@ -557,10 +559,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;
 		t.filename = this.Filename;
 		int state;
-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+		if (start.ContainsKey(ch)) {
+			Contract.Assert(start[ch] != null);
+			state = (int) start[ch];
+		}
 		else { state = 0; }
 		tlen = 0; AddCh();
-		
+
 		switch (state) {
 			case -1: { t.kind = eofSym; break; } // NextCh already done
 			case 0: {
@@ -651,78 +656,78 @@ void objectInvariant(){
 			case 22:
 				{t.kind = 31; break;}
 			case 23:
-				{t.kind = 39; break;}
-			case 24:
 				{t.kind = 40; break;}
+			case 24:
+				{t.kind = 41; break;}
 			case 25:
-				{t.kind = 43; break;}
+				{t.kind = 44; break;}
 			case 26:
-				{t.kind = 47; break;}
+				{t.kind = 48; break;}
 			case 27:
-				{t.kind = 49; break;}
-			case 28:
 				{t.kind = 50; break;}
+			case 28:
+				{t.kind = 51; break;}
 			case 29:
 				if (ch == '>') {AddCh(); goto case 30;}
 				else {goto case 0;}
 			case 30:
-				{t.kind = 67; break;}
-			case 31:
 				{t.kind = 68; break;}
-			case 32:
+			case 31:
 				{t.kind = 69; break;}
-			case 33:
+			case 32:
 				{t.kind = 70; break;}
+			case 33:
+				{t.kind = 71; break;}
 			case 34:
 				if (ch == '&') {AddCh(); goto case 35;}
 				else {goto case 0;}
 			case 35:
-				{t.kind = 71; break;}
-			case 36:
 				{t.kind = 72; break;}
-			case 37:
+			case 36:
 				{t.kind = 73; break;}
-			case 38:
+			case 37:
 				{t.kind = 74; break;}
+			case 38:
+				{t.kind = 75; break;}
 			case 39:
-				{t.kind = 77; break;}
-			case 40:
 				{t.kind = 78; break;}
-			case 41:
+			case 40:
 				{t.kind = 79; break;}
+			case 41:
+				{t.kind = 80; break;}
 			case 42:
 				if (ch == 'n') {AddCh(); goto case 43;}
 				else {goto case 0;}
 			case 43:
-				{t.kind = 80; break;}
-			case 44:
 				{t.kind = 81; break;}
-			case 45:
+			case 44:
 				{t.kind = 82; break;}
-			case 46:
+			case 45:
 				{t.kind = 83; break;}
-			case 47:
+			case 46:
 				{t.kind = 84; break;}
-			case 48:
+			case 47:
 				{t.kind = 85; break;}
-			case 49:
+			case 48:
 				{t.kind = 86; break;}
-			case 50:
+			case 49:
 				{t.kind = 87; break;}
+			case 50:
+				{t.kind = 88; break;}
 			case 51:
-				{t.kind = 89; break;}
+				{t.kind = 90; break;}
 			case 52:
-				{t.kind = 93; break;}
+				{t.kind = 94; break;}
 			case 53:
-				{t.kind = 96; break;}
+				{t.kind = 97; break;}
 			case 54:
-				{t.kind = 100; break;}
+				{t.kind = 101; break;}
 			case 55:
-				{t.kind = 102; break;}
-			case 56:
 				{t.kind = 103; break;}
-			case 57:
+			case 56:
 				{t.kind = 104; break;}
+			case 57:
+				{t.kind = 105; break;}
 			case 58:
 				recEnd = pos; recKind = 20;
 				if (ch == '=') {AddCh(); goto case 26;}
@@ -741,40 +746,40 @@ void objectInvariant(){
 				else if (ch == '=') {AddCh(); goto case 66;}
 				else {goto case 0;}
 			case 62:
-				recEnd = pos; recKind = 51;
+				recEnd = pos; recKind = 52;
 				if (ch == '.') {AddCh(); goto case 53;}
-				else {t.kind = 51; break;}
+				else {t.kind = 52; break;}
 			case 63:
-				recEnd = pos; recKind = 61;
+				recEnd = pos; recKind = 62;
 				if (ch == '|') {AddCh(); goto case 37;}
-				else {t.kind = 61; break;}
+				else {t.kind = 62; break;}
 			case 64:
-				recEnd = pos; recKind = 88;
+				recEnd = pos; recKind = 89;
 				if (ch == '=') {AddCh(); goto case 40;}
 				else if (ch == '!') {AddCh(); goto case 41;}
 				else if (ch == 'i') {AddCh(); goto case 42;}
-				else {t.kind = 88; break;}
+				else {t.kind = 89; break;}
 			case 65:
-				recEnd = pos; recKind = 76;
+				recEnd = pos; recKind = 77;
 				if (ch == '=') {AddCh(); goto case 29;}
-				else {t.kind = 76; break;}
+				else {t.kind = 77; break;}
 			case 66:
-				recEnd = pos; recKind = 75;
+				recEnd = pos; recKind = 76;
 				if (ch == '>') {AddCh(); goto case 32;}
-				else {t.kind = 75; break;}
+				else {t.kind = 76; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
 		return t;
 	}
-	
+
 	private void SetScannerBehindT() {
 		buffer.Pos = t.pos;
 		NextCh();
 		line = t.line; col = t.col;
 		for (int i = 0; i < tlen; i++) NextCh();
 	}
-	
+
 	// get the next token (possibly a token already seen during peeking)
 	public Token/*!*/ Scan () {
 	 Contract.Ensures(Contract.Result<Token>() != null);
@@ -795,7 +800,7 @@ void objectInvariant(){
 			}
 			pt = pt.next;
 		} while (pt.kind > maxT); // skip pragmas
-	
+
 		return pt;
 	}
 
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 33b6d39d..2bb5a51e 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -960,7 +960,7 @@ namespace Microsoft.Dafny {
       } else {
         // check well-formedness of the preconditions, and then assume each one of them
         foreach (MaybeFreeExpression p in m.Req) {
-          CheckWellformed(p.E, new WFOptions(), null, localVariables, builder, etran);
+          CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
           builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
         }
         // Note: the modifies clauses are not checked for well-formedness (is that sound?), because it used to
@@ -968,7 +968,7 @@ namespace Microsoft.Dafny {
         // absolutely well-defined.
         // check well-formedness of the decreases clauses
         foreach (Expression p in m.Decreases) {
-          CheckWellformed(p, new WFOptions(), null, localVariables, builder, etran);
+          CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
         }
 
         // play havoc with the heap according to the modifies clause
@@ -992,7 +992,7 @@ namespace Microsoft.Dafny {
 
         // check wellformedness of postconditions
         foreach (MaybeFreeExpression p in m.Ens) {
-          CheckWellformed(p.E, new WFOptions(), null, localVariables, builder, etran);
+          CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
           builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
         }
 
@@ -1292,7 +1292,7 @@ namespace Microsoft.Dafny {
       // check well-formedness of the preconditions (including termination, but no reads checks), and then
       // assume each one of them
       foreach (Expression p in f.Req) {
-        CheckWellformed(p, new WFOptions(f, null, false), null, locals, builder, etran);
+        CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
         builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
       }
       // Note: the reads clauses are not checked for well-formedness (is that sound?), because it used to
@@ -1300,7 +1300,7 @@ namespace Microsoft.Dafny {
       // absolutely well-defined.
       // check well-formedness of the decreases clauses (including termination, but no reads checks)
       foreach (Expression p in f.Decreases) {
-        CheckWellformed(p, new WFOptions(f, null, false), null, locals, builder, etran);
+        CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
       }
       // Generate:
       //   if (*) {
@@ -1311,7 +1311,7 @@ namespace Microsoft.Dafny {
       // Here go the postconditions (termination checks included, but no reads checks)
       StmtListBuilder postCheckBuilder = new StmtListBuilder();
       foreach (Expression p in f.Ens) {
-        CheckWellformed(p, new WFOptions(f, f, false), null, locals, postCheckBuilder, etran);
+        CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);
         // assume the postcondition for the benefit of checking the remaining postconditions
         postCheckBuilder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
       }
@@ -1327,7 +1327,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
 
         DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);
-        CheckWellformed(f.Body, new WFOptions(f, null, true), funcAppl, locals, bodyCheckBuilder, etran);
+        CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
 
         // check that postconditions hold
         foreach (Expression p in f.Ens) {
@@ -1443,7 +1443,12 @@ namespace Microsoft.Dafny {
         // create a substitution map from each formal parameter to the corresponding actual parameter
         Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
         for (int i = 0; i < e.Function.Formals.Count; i++) {
-          substMap.Add(e.Function.Formals[i], e.Args[i]);
+          var formal = e.Function.Formals[i];
+          var s = CheckSubrange_Expr(e.Args[i].tok, etran.TrExpr(e.Args[i]), formal.Type);
+          if (s != null) {
+            r = BplAnd(r, s);
+          }
+          substMap.Add(formal, e.Args[i]);
         }
         // check that the preconditions for the call hold
         foreach (Expression p in e.Function.Req) {
@@ -1453,7 +1458,16 @@ namespace Microsoft.Dafny {
         return r;
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
-        return IsTotal(dtv.Arguments, etran);
+        var r = IsTotal(dtv.Arguments, etran);
+        for (int i = 0; i < dtv.Ctor.Formals.Count; i++) {
+          var formal = dtv.Ctor.Formals[i];
+          var arg = dtv.Arguments[i];
+          var s = CheckSubrange_Expr(arg.tok, etran.TrExpr(arg), formal.Type);
+          if (s != null) {
+            r = BplAnd(r, s);
+          }
+        }
+        return r;
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
@@ -1727,10 +1741,14 @@ namespace Microsoft.Dafny {
         args.Add(Bpl.Expr.Literal(0));
         kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null);
       }
-      CheckWellformed(expr, new WFOptions(kv), null, locals, builder, etran);
+      CheckWellformed(expr, new WFOptions(kv), locals, builder, etran);
       builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));
     }
 
+    void CheckWellformed(Expression expr, WFOptions options, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+      CheckWellformedWithResult(expr, options, null, null, locals, builder, etran);
+    }
+
     /// <summary>
     /// Adds to "builder" code that checks the well-formedness of "expr".  Any local variables introduced
     /// in this code are added to "locals".
@@ -1738,9 +1756,11 @@ namespace Microsoft.Dafny {
     /// assume the equivalent of "result == expr".
     /// See class WFOptions for descriptions of the specified options.
     /// </summary>
-    void CheckWellformed(Expression expr, WFOptions options, Bpl.Expr result, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+    void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr result, Type resultType,
+                                   Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
       Contract.Requires(expr != null);
       Contract.Requires(options != null);
+      Contract.Requires((result == null) == (resultType == null));
       Contract.Requires(locals != null);
       Contract.Requires(builder != null);
       Contract.Requires(etran != null);
@@ -1751,11 +1771,11 @@ namespace Microsoft.Dafny {
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         foreach (Expression el in e.Elements) {
-          CheckWellformed(el, options, null, locals, builder, etran);
+          CheckWellformed(el, options, locals, builder, etran);
         }
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr e = (FieldSelectExpr)expr;
-        CheckWellformed(e.Obj, options, null, locals, builder, etran);
+        CheckWellformed(e.Obj, options, locals, builder, etran);
         CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);
         if (options.DoReadsChecks && e.Field.IsMutable) {
           builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));
@@ -1763,16 +1783,16 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr e = (SeqSelectExpr)expr;
         bool isSequence = e.Seq.Type is SeqType;
-        CheckWellformed(e.Seq, options, null, locals, builder, etran);
+        CheckWellformed(e.Seq, options, locals, builder, etran);
         Bpl.Expr seq = etran.TrExpr(e.Seq);
         Bpl.Expr e0 = null;
         if (e.E0 != null) {
           e0 = etran.TrExpr(e.E0);
-          CheckWellformed(e.E0, options, null, locals, builder, etran);
+          CheckWellformed(e.E0, options, locals, builder, etran);
           builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range", options.AssertKv));
         }
         if (e.E1 != null) {
-          CheckWellformed(e.E1, options, null, locals, builder, etran);
+          CheckWellformed(e.E1, options, locals, builder, etran);
           builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array"), options.AssertKv));
         }
         if (options.DoReadsChecks && cce.NonNull(e.Seq.Type).IsArrayType) {
@@ -1782,11 +1802,11 @@ namespace Microsoft.Dafny {
         }
       } else if (expr is MultiSelectExpr) {
         MultiSelectExpr e = (MultiSelectExpr)expr;
-        CheckWellformed(e.Array, options, null, locals, builder, etran);
+        CheckWellformed(e.Array, options, locals, builder, etran);
         Bpl.Expr array = etran.TrExpr(e.Array);
         int i = 0;
         foreach (Expression idx in e.Indices) {
-          CheckWellformed(idx, options, null, locals, builder, etran);
+          CheckWellformed(idx, options, locals, builder, etran);
 
           Bpl.Expr index = etran.TrExpr(idx);
           Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
@@ -1797,23 +1817,23 @@ namespace Microsoft.Dafny {
         }
       } else if (expr is SeqUpdateExpr) {
         SeqUpdateExpr e = (SeqUpdateExpr)expr;
-        CheckWellformed(e.Seq, options, null, locals, builder, etran);
+        CheckWellformed(e.Seq, options, locals, builder, etran);
         Bpl.Expr seq = etran.TrExpr(e.Seq);
         Bpl.Expr index = etran.TrExpr(e.Index);
-        CheckWellformed(e.Index, options, null, locals, builder, etran);
+        CheckWellformed(e.Index, options, locals, builder, etran);
         builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv));
-        CheckWellformed(e.Value, options, null, locals, builder, etran);
+        CheckWellformed(e.Value, options, locals, builder, etran);
       } else if (expr is FunctionCallExpr) {
         FunctionCallExpr e = (FunctionCallExpr)expr;
         Contract.Assert(e.Function != null);  // follows from the fact that expr has been successfully resolved
         // check well-formedness of receiver
-        CheckWellformed(e.Receiver, options, null, locals, builder, etran);
+        CheckWellformed(e.Receiver, options, locals, builder, etran);
         if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
           CheckNonNull(expr.tok, e.Receiver, builder, etran, options.AssertKv);
         }
         // check well-formedness of the other parameters
         foreach (Expression arg in e.Args) {
-          CheckWellformed(arg, options, null, locals, builder, etran);
+          CheckWellformed(arg, options, locals, builder, etran);
         }
         // create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
         Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
@@ -1827,6 +1847,7 @@ namespace Microsoft.Dafny {
           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?
           Expression ee = e.Args[i];
+          CheckSubrange(ee.tok, etran.TrExpr(ee), p.Type, builder);
           Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type));
           builder.Add(cmd);
         }
@@ -1893,21 +1914,24 @@ namespace Microsoft.Dafny {
 
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
-        foreach (Expression arg in dtv.Arguments) {
-          CheckWellformed(arg, options, null, locals, builder, etran);
+        for (int i = 0; i < dtv.Ctor.Formals.Count; i++) {
+          var formal = dtv.Ctor.Formals[i];
+          var arg = dtv.Arguments[i];
+          CheckWellformed(arg, options, locals, builder, etran);
+          CheckSubrange(arg.tok, etran.TrExpr(arg), formal.Type, builder);
         }
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
-        CheckWellformed(e.E, options, null, locals, builder, etran.Old);
+        CheckWellformed(e.E, options, locals, builder, etran.Old);
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
-        CheckWellformed(e.E, options, null, locals, builder, etran);
+        CheckWellformed(e.E, options, locals, builder, etran);
       } else if (expr is AllocatedExpr) {
         AllocatedExpr e = (AllocatedExpr)expr;
-        CheckWellformed(e.E, options, null, locals, builder, etran);
+        CheckWellformed(e.E, options, locals, builder, etran);
       } else if (expr is UnaryExpr) {
         UnaryExpr e = (UnaryExpr)expr;
-        CheckWellformed(e.E, options, null, locals, builder, etran);
+        CheckWellformed(e.E, options, locals, builder, etran);
         if (e.Op == UnaryExpr.Opcode.SetChoose) {
           Bpl.Expr emptySet = FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
           builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E), emptySet), "choose is defined only on nonempty sets"));
@@ -1916,30 +1940,30 @@ namespace Microsoft.Dafny {
         }
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
-        CheckWellformed(e.E0, options, null, locals, builder, etran);
+        CheckWellformed(e.E0, options, locals, builder, etran);
         switch (e.ResolvedOp) {
           case BinaryExpr.ResolvedOpcode.And:
           case BinaryExpr.ResolvedOpcode.Imp:
             {
               Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
-              CheckWellformed(e.E1, options, null, locals, b, etran);
+              CheckWellformed(e.E1, options, locals, b, etran);
               builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null));
             }
             break;
           case BinaryExpr.ResolvedOpcode.Or:
             {
               Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
-              CheckWellformed(e.E1, options, null, locals, b, etran);
+              CheckWellformed(e.E1, options, locals, b, etran);
               builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null));
             }
             break;
           case BinaryExpr.ResolvedOpcode.Div:
           case BinaryExpr.ResolvedOpcode.Mod:
-            CheckWellformed(e.E1, options, null, locals, builder, etran);
+            CheckWellformed(e.E1, options, locals, builder, etran);
             builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero", options.AssertKv));
             break;
           default:
-            CheckWellformed(e.E1, options, null, locals, builder, etran);
+            CheckWellformed(e.E1, options, locals, builder, etran);
             break;
         }
 
@@ -1960,20 +1984,20 @@ namespace Microsoft.Dafny {
           }
         }
         Expression body = Substitute(e.Body, null, substMap);
-        CheckWellformed(body, options, null, locals, builder, etran);
+        CheckWellformed(body, options, locals, builder, etran);
 
       } else if (expr is ITEExpr) {
         ITEExpr e = (ITEExpr)expr;
-        CheckWellformed(e.Test, options, null, locals, builder, etran);
+        CheckWellformed(e.Test, options, locals, builder, etran);
         Bpl.StmtListBuilder bThen = new Bpl.StmtListBuilder();
         Bpl.StmtListBuilder bElse = new Bpl.StmtListBuilder();
-        CheckWellformed(e.Thn, options, null, locals, bThen, etran);
-        CheckWellformed(e.Els, options, null, locals, bElse, etran);
+        CheckWellformed(e.Thn, options, locals, bThen, etran);
+        CheckWellformed(e.Els, options, locals, bElse, etran);
         builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
       
       } else if (expr is MatchExpr) {
         MatchExpr me = (MatchExpr)expr;
-        CheckWellformed(me.Source, options, null, locals, builder, etran);
+        CheckWellformed(me.Source, options, locals, builder, etran);
         Bpl.Expr src = etran.TrExpr(me.Source);
         Bpl.IfCmd ifcmd = null;
         StmtListBuilder elsBldr = new StmtListBuilder();
@@ -1984,7 +2008,7 @@ namespace Microsoft.Dafny {
           Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
           Bpl.Expr ct = CtorInvocation(mc, etran, locals, b);
           // generate:  if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...
-          CheckWellformed(mc.Body, options, result, locals, b, etran);
+          CheckWellformedWithResult(mc.Body, options, result, resultType, locals, b, etran);
           ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);
           els = null;
         }
@@ -1996,7 +2020,10 @@ namespace Microsoft.Dafny {
       }
 
       if (result != null) {
-        builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, etran.TrExpr(expr))));
+        Contract.Assert(resultType != null);
+        var bResult = etran.TrExpr(expr);
+        CheckSubrange(expr.tok, bResult, resultType, builder);
+        builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult)));
         builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));
       }
     }
@@ -3250,7 +3277,9 @@ namespace Microsoft.Dafny {
         Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?
         Expression actual = s.Args[i];
         TrStmt_CheckWellformed(actual, builder, locals, etran, true);
-        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, etran.TrExpr(actual), cce.NonNull(actual.Type), s.Method.Ins[i].Type));
+        var bActual = etran.TrExpr(actual);
+        CheckSubrange(actual.tok, bActual, p.Type, builder);
+        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, bActual, cce.NonNull(actual.Type), s.Method.Ins[i].Type));
         builder.Add(cmd);
         ins.Add(lhs);
       }
@@ -3611,7 +3640,12 @@ namespace Microsoft.Dafny {
         }
       }
 
-      if (type is BoolType || type is IntType) {
+      if (type is NatType) {
+        // nat:
+        // 0 <= x
+        return Bpl.Expr.Le(Bpl.Expr.Literal(0), x);
+
+      } else  if (type is BoolType || type is IntType) {
         // nothing todo
       
       } else if (type is SetType) {
@@ -3684,7 +3718,7 @@ namespace Microsoft.Dafny {
 
       if (lhs is IdentifierExpr) {
         var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?
-        TrAssignmentRhs(tok, bLhs, lhs.Type, rhs, builder, locals, etran);
+        TrAssignmentRhs(tok, bLhs, lhs.Type, rhs, lhs.Type, builder, locals, etran);
 
       } else if (lhs is FieldSelectExpr) {
         var fse = (FieldSelectExpr)lhs;
@@ -3693,7 +3727,7 @@ namespace Microsoft.Dafny {
         // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj]);
         builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
 
-        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, fse.Field.Type, rhs, builder, locals, etran);
+        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, fse.Field.Type, rhs, lhs.Type, builder, locals, etran);
 
         var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?
         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs));
@@ -3711,7 +3745,7 @@ namespace Microsoft.Dafny {
           // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj,index]);
           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
 
-          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
 
           var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?
           Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));
@@ -3733,7 +3767,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
           builder.Add(Assert(tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));
           // compute the RHS
-          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+          Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
           // do the update:  call UpdateArrayRange(arr, low, high, rhs);
           builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
             new Bpl.ExprSeq(obj, low, high, bRhs),
@@ -3748,7 +3782,7 @@ namespace Microsoft.Dafny {
         var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhs, "$index", predef.FieldName(mse.tok, predef.BoxType), builder, locals);
         builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
 
-        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+        Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
 
         var h = (Bpl.IdentifierExpr)etran.HeapExpr;  // TODO: is this cast always justified?
         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));
@@ -3763,8 +3797,10 @@ namespace Microsoft.Dafny {
     /// <summary>
     /// Generates an assignment of the translation of "rhs" to "bLhs" and then return "bLhs".  If "bLhs" is
     /// passed in as "null", this method will create a new temporary Boogie variable to hold the result.
+    /// Before the assignment, the generated code will check that "rhs" obeys any subrange requirements
+    /// entailed by "checkSubrangeType".
     /// </summary>
-    Bpl.IdentifierExpr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bLhs, Type lhsType, AssignmentRhs rhs,
+    Bpl.IdentifierExpr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bLhs, Type lhsType, AssignmentRhs rhs, Type checkSubrangeType,
                                        Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
       Contract.Requires(tok != null);
       Contract.Requires(rhs != null);
@@ -3787,6 +3823,7 @@ namespace Microsoft.Dafny {
         TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true);
 
         Bpl.Expr bRhs = etran.TrExpr(e.Expr);
+        CheckSubrange(tok, bRhs, checkSubrangeType, builder);
         bRhs = etran.CondApplyBox(tok, bRhs, e.Expr.Type, lhsType);
 
         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
@@ -3807,7 +3844,7 @@ namespace Microsoft.Dafny {
         if (tRhs.ArrayDimensions != null) {
           int i = 0;
           foreach (Expression dim in tRhs.ArrayDimensions) {
-            CheckWellformed(dim, new WFOptions(), null, locals, builder, etran);
+            CheckWellformed(dim, new WFOptions(), locals, builder, etran);
             if (tRhs.ArrayDimensions.Count == 1) {
               builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(dim)),
                 tRhs.ArrayDimensions.Count == 1 ? "array size might be negative" : string.Format("array size (dimension {0}) might be negative", i)));
@@ -3857,6 +3894,29 @@ namespace Microsoft.Dafny {
       return bLhs;
     }
 
+    void CheckSubrange(IToken tok, Expr bRhs, Type tp, StmtListBuilder builder) {
+      Contract.Requires(tok != null);
+      Contract.Requires(bRhs != null);
+      Contract.Requires(tp != null);
+      Contract.Requires(builder != null);
+
+      var isNat = CheckSubrange_Expr(tok, bRhs, tp);
+      if (isNat != null) {
+        builder.Add(Assert(tok, isNat, "value assigned to a nat must be non-negative"));
+      }
+    }
+
+    Bpl.Expr CheckSubrange_Expr(IToken tok, Expr bRhs, Type tp) {
+      Contract.Requires(tok != null);
+      Contract.Requires(bRhs != null);
+      Contract.Requires(tp != null);
+
+      if (tp is NatType) {
+        return Bpl.Expr.Le(Bpl.Expr.Literal(0), bRhs);
+      }
+      return null;
+    }
+
     Bpl.AssumeCmd AssumeGoodHeap(IToken tok, ExpressionTranslator etran) {
       Contract.Requires(tok != null);
       Contract.Requires(etran != null);
@@ -4163,7 +4223,8 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < dtv.Arguments.Count; i++) {
             Expression arg = dtv.Arguments[i];
             Type t = dtv.Ctor.Formals[i].Type;
-            args.Add(CondApplyBox(expr.tok, TrExpr(arg), cce.NonNull(arg.Type), t));
+            var bArg = TrExpr(arg);
+            args.Add(CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));
           }
           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
           return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
-- 
cgit v1.2.3