Merge

7 files changed, 489 insertions, 449 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 82604794..0fbeb9d6 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -211,7 +211,7 @@ namespace Microsoft.Dafny {
 

         Indent(ind);

         wr.Write("public {0}(", DtCtorName(ctor));

-        WriteFormals(ctor.Formals);

+        WriteFormals("", ctor.Formals);

         wr.WriteLine(") {");

         i = 0;

         foreach (Formal arg in ctor.Formals) {

@@ -297,11 +297,11 @@ namespace Microsoft.Dafny {
       wr.WriteLine("}");

     }

     

-    void WriteFormals(List<Formal/*!*/>/*!*/ formals)

+    void WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)

     {

+      Contract.Requires(sep != null);

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

       int i = 0;

-      string sep = "";

       foreach (Formal arg in formals) {

         if (!arg.IsGhost) {

           string name = FormalName(arg, i);

@@ -349,47 +349,9 @@ namespace Microsoft.Dafny {
               wr.Write("<{0}>", TypeParameters(f.TypeArgs));

             }

             wr.Write("(");

-            WriteFormals(f.Formals);

+            WriteFormals("", f.Formals);

             wr.WriteLine(") {");

-            if (f.Body is MatchExpr) {

-              MatchExpr me = (MatchExpr)f.Body;

-              // Type source = e;

-              // if (source._D is Dt_Ctor0) {

-              //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

-              //   ...

-              //   return Body0;

-              // } else if (...) {

-              //   ...

-              // } else if (true) {

-              //   ...

-              // }

-

-              string source = "_source" + tmpVarCount;

-              tmpVarCount++;

-              Indent(indent);

-              wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);

-              TrExpr(me.Source);

-              wr.WriteLine(";");

-

-              int i = 0;

-              foreach (MatchCaseExpr mc in me.Cases) {

-                MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);

-                

-                Indent(indent + 2*IndentAmount);

-                wr.Write("return ");

-                TrExpr(mc.Body);

-                wr.WriteLine(";");

-                i++;

-              }

-

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

-

-            } else {

-              Indent(indent + IndentAmount);

-              wr.Write("return ");

-              TrExpr(f.Body);

-              wr.WriteLine(";");

-            }

+            CompileReturnBody(f.Body, indent);

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

           }

           

@@ -402,11 +364,8 @@ namespace Microsoft.Dafny {
               wr.Write("<{0}>", TypeParameters(m.TypeArgs));

             }

             wr.Write("(");

-            WriteFormals(m.Ins);

-            if (m.Ins.Count != 0 && m.Outs.Count != 0) {

-              wr.Write(", ");

-            }

-            WriteFormals(m.Outs);

+            WriteFormals("", m.Ins);

+            WriteFormals(", ", m.Outs);

             wr.WriteLine(")");

             Indent(indent);  wr.WriteLine("{");

             foreach (Formal p in m.Outs) {

@@ -453,7 +412,51 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

+    void CompileReturnBody(Expression body, int indent) {

+      body = body.Resolved;

+      if (body is MatchExpr) {

+        MatchExpr me = (MatchExpr)body;

+        // Type source = e;

+        // if (source._D is Dt_Ctor0) {

+        //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

+        //   ...

+        //   return Body0;

+        // } else if (...) {

+        //   ...

+        // } else if (true) {

+        //   ...

+        // }

+

+        string source = "_source" + tmpVarCount;

+        tmpVarCount++;

+        Indent(indent);

+        wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);

+        TrExpr(me.Source);

+        wr.WriteLine(";");

+

+        if (me.Cases.Count == 0) {

+          // the verifier would have proved we never get here; still, we need some code that will compile

+          Indent(indent);

+          wr.WriteLine("throw new System.Exception();");

+        } else {

+          int i = 0;

+          foreach (MatchCaseExpr mc in me.Cases) {

+            MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);

+            CompileReturnBody(mc.Body, indent + IndentAmount);

+            i++;

+          }

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

+        }

+

+      } else {

+        Indent(indent + IndentAmount);

+        wr.Write("return ");

+        TrExpr(body);

+        wr.WriteLine(";");

+      }

+    }

+

     // ----- Type ---------------------------------------------------------------------------------

     

     readonly string DafnySetClass = "Dafny.Set";

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 11a2dfed..91028093 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -328,12 +328,12 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   .

 

 

-GIdentType<bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

-/* isGhost always returns as false if allowGhost is false */

+GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

+/* isGhost always returns as false if allowGhostKeyword is false */

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

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

      isGhost = false; .)

-  [ "ghost"                    (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)

+  [ "ghost"                    (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)

   ]

   IdentType<out id, out ty>

   .

@@ -430,7 +430,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   [ GenericParameters<typeArgs> ]

   Formals<true, !mmod.IsGhost, ins>

   [ "returns"

-    Formals<false, true, outs>

+    Formals<false, !mmod.IsGhost, outs>

   ]

 

   ( ";" { MethodSpec<req, mod, ens, dec> }

@@ -464,12 +464,12 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   )

   .

 

-Formals<.bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals.> 

+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> 

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

   "("

   [

-    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

-    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

+    GIdentType<allowGhostKeyword, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

+    { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

     }

   ]

   ")"

@@ -635,52 +635,10 @@ FrameExpression<out FrameExpression/*!*/ fe>
 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

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

   "{"                         (. bodyStart = t; .)

-  ( MatchExpression<out e>

-  | Expression<out e>

-  )

+  Expression<out e>

   "}"                         (. bodyEnd = t; .)

   .

   

-MatchExpression<out Expression/*!*/ e>

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

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

-  .)

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

-  Expression<out e>

-  /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,

-     but it's okay, because we want this closer match expression to bind as much as possible--use

-     parens around it to limit its scope. */

-  { CaseExpression<out c>     (. cases.Add(c); .)

-  }

-  (. e = new MatchExpr(x, e, cases); .)

-  .

-

-CaseExpression<out MatchCaseExpr/*!*/ c>

-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

-     List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

-     Expression/*!*/ body;

-  .)

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

-  Ident<out id>

-  [ "("

-    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

-    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

-    }

-  ")" ]

-  "=>"

-  MatchOrExpr<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

-  .

-

-/* Note, '(' is start of more than one alternative in MatchOrExpr, but the first intentionally hides

-   the third alternative in this regard, in order to also allow match expressions to be parenthesized. */

-MatchOrExpr<out Expression/*!*/ e>

-= (. e = dummyExpr; .)

-  ( "(" MatchOrExpr<out e> ")"

-  | MatchExpression<out e>

-  | Expression<out e>

-  )

-  .

-

 /*------------------------------------------------------------------------*/

 

 BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>

@@ -1190,6 +1148,7 @@ UnaryExpression<out Expression/*!*/ e>
   | EndlessExpression<out e>     /* these have no further suffix */

   | DottedIdentifiersAndFunction<out e>

     { Suffix<ref e> }

+  | DisplayExpr<out e>

   | ConstAtomExpression<out e>

     { Suffix<ref e> }

   )

@@ -1214,7 +1173,7 @@ NegOp = "!" | '\u00ac'.
  */

 ConstAtomExpression<out Expression/*!*/ e>

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

-     IToken/*!*/ x;  BigInteger n;  List<Expression/*!*/>/*!*/ elements;

+     IToken/*!*/ x;  BigInteger n;

      e = dummyExpr;

   .)

   ( "false"                                    (. e = new LiteralExpr(t, false); .)

@@ -1231,15 +1190,23 @@ ConstAtomExpression<out Expression/*!*/ e>
   | "|"                                        (. x = t; .)

       Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

-  | "{"                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

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

+      Expression<out e>                        (. e = new ParensExpression(x, e); .)

+    ")"

+  )

+  .

+

+DisplayExpr<out Expression e>

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

+     IToken/*!*/ x;  List<Expression/*!*/>/*!*/ elements;

+     e = dummyExpr;

+  .)

+  ( "{"                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

       [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements); .)

     "}"

   | "["                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

       [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)

     "]"

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

-      Expression<out e>                        (. e = new ParensExpression(x, e); .)

-    ")"

   )

   .

 

@@ -1252,11 +1219,41 @@ EndlessExpression<out Expression e>
     Expression<out e>

     "then" Expression<out e0>

     "else" Expression<out e1>                  (. e = new ITEExpr(x, e, e0, e1); .)

+  | MatchExpression<out e>

   | QuantifierGuts<out e>

   | ComprehensionExpr<out e>

   )

   .

 

+MatchExpression<out Expression/*!*/ e>

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

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

+  .)

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

+  Expression<out e>

+  /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,

+     but it's okay, because we want this closer match expression to bind as much as possible--use

+     parens around it to limit its scope. */

+  { CaseExpression<out c>     (. cases.Add(c); .)

+  }

+  (. e = new MatchExpr(x, e, cases); .)

+  .

+

+CaseExpression<out MatchCaseExpr/*!*/ c>

+= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

+     List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

+     Expression/*!*/ body;

+  .)

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

+  Ident<out id>

+  [ "("

+    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

+    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

+    }

+  ")" ]

+  "=>"

+  Expression<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

+  .

 

 /*------------------------------------------------------------------------*/

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 840344bd..100e34e1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-

+	

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

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

 	}

 

@@ -160,15 +160,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 {

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

 	}

 

-

+	

 	void Dafny() {

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

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

@@ -511,7 +511,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Formals(true, !mmod.IsGhost, ins);

 		if (la.kind == 26) {

 			Get();

-			Formals(false, true, outs);

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

 		}

 		if (la.kind == 17) {

 			Get();

@@ -604,13 +604,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		EquivExpression(out e);

 	}

 

-	void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

+	void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

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

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

 		isGhost = false; 

 		if (la.kind == 11) {

 			Get();

-			if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

+			if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

 		}

 		IdentType(out id, out ty);

 	}

@@ -723,15 +723,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

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

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

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

 		Expect(32);

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

-			GIdentType(allowGhosts, out id, out ty, out isGhost);

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

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

 			while (la.kind == 19) {

 				Get();

-				GIdentType(allowGhosts, out id, out ty, out isGhost);

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

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

 			}

 		}

@@ -894,11 +894,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 

 		Expect(7);

 		bodyStart = t; 

-		if (la.kind == 44) {

-			MatchExpression(out e);

-		} else if (StartOf(8)) {

-			Expression(out e);

-		} else SynErr(114);

+		Expression(out e);

 		Expect(8);

 		bodyEnd = t; 

 	}

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

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(115);

+		} else SynErr(114);

 	}

 

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

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

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(116);

-	}

-

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

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

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

-		

-		Expect(44);

-		x = t; 

-		Expression(out e);

-		while (la.kind == 45) {

-			CaseExpression(out c);

-			cases.Add(c); 

-		}

-		e = new MatchExpr(x, e, cases); 

-	}

-

-	void CaseExpression(out MatchCaseExpr/*!*/ c) {

-		Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

-		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

-		Expression/*!*/ body;

-		

-		Expect(45);

-		x = t; 

-		Ident(out id);

-		if (la.kind == 32) {

-			Get();

-			Ident(out arg);

-			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

-			while (la.kind == 19) {

-				Get();

-				Ident(out arg);

-				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

-			}

-			Expect(33);

-		}

-		Expect(46);

-		MatchOrExpr(out body);

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

-	}

-

-	void MatchOrExpr(out Expression/*!*/ e) {

-		e = dummyExpr; 

-		if (la.kind == 32) {

-			Get();

-			MatchOrExpr(out e);

-			Expect(33);

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

-			MatchExpression(out e);

-		} else if (StartOf(8)) {

-			Expression(out e);

-		} else SynErr(117);

+		} else SynErr(115);

 	}

 

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

@@ -988,55 +933,85 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		if (la.kind == 7) {

+		switch (la.kind) {

+		case 7: {

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

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

+			break;

+		}

+		case 63: {

 			AssertStmt(out s);

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

+			break;

+		}

+		case 64: {

 			AssumeStmt(out s);

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

+			break;

+		}

+		case 65: {

 			PrintStmt(out s);

-		} else if (StartOf(11)) {

+			break;

+		}

+		case 1: case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {

 			UpdateStmt(out s);

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

+			break;

+		}

+		case 53: {

 			HavocStmt(out s);

-		} else if (la.kind == 11 || la.kind == 18) {

+			break;

+		}

+		case 11: case 18: {

 			VarDeclStatement(out s);

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

+			break;

+		}

+		case 54: {

 			IfStmt(out s);

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

+			break;

+		}

+		case 58: {

 			WhileStmt(out s);

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

+			break;

+		}

+		case 60: {

 			MatchStmt(out s);

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

+			break;

+		}

+		case 61: {

 			ForeachStmt(out s);

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

+			break;

+		}

+		case 44: {

 			Get();

 			x = t; 

 			Ident(out id);

 			Expect(22);

 			OneStmt(out s);

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

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

+			break;

+		}

+		case 45: {

 			Get();

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

 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

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

-				while (la.kind == 48) {

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

+				while (la.kind == 45) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(118);

+			} else SynErr(116);

 			Expect(17);

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

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

+			break;

+		}

+		case 46: {

 			Get();

 			x = t; 

 			Expect(17);

 			s = new ReturnStmt(x); 

-		} else SynErr(119);

+			break;

+		}

+		default: SynErr(117); break;

+		}

 	}

 

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

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

 			Get();

 			rhss.Add(new ExprRhs(e)); 

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

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

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 19) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			Expect(50);

+			Expect(47);

 			x = t; 

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

@@ -1106,13 +1081,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 22) {

 			Get();

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

-		} else SynErr(120);

+		} else SynErr(118);

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

 	}

 

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

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

-		Expect(56);

+		Expect(53);

 		x = t; 

 		Lhs(out lhs);

 		Expect(17);

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

 			lhss.Add(d); 

 		}

-		if (la.kind == 50) {

+		if (la.kind == 47) {

 			Get();

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

 			Rhs(out r, lhs0);

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

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(57);

+		Expect(54);

 		x = t; 

 		if (la.kind == 32) {

 			Guard(out guard);

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

-			if (la.kind == 58) {

+			if (la.kind == 55) {

 				Get();

-				if (la.kind == 57) {

+				if (la.kind == 54) {

 					IfStmt(out s);

 					els = s; 

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

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

 					els = s; 

-				} else SynErr(121);

+				} else SynErr(119);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(122);

+		} else SynErr(120);

 	}

 

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

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

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(59);

+		Expect(58);

 		x = t; 

 		if (la.kind == 32) {

 			Guard(out guard);

@@ -1215,22 +1190,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases);

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

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

-		} else if (StartOf(12)) {

+		} else if (StartOf(11)) {

 			LoopSpec(out invariants, out decreases);

 			AlternativeBlock(out alternatives);

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

-		} else SynErr(123);

+		} else SynErr(121);

 	}

 

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

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

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

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

-		Expect(44);

+		Expect(60);

 		x = t; 

 		Expression(out e);

 		Expect(7);

-		while (la.kind == 45) {

+		while (la.kind == 56) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1275,13 +1250,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			}

 		}

-		if (StartOf(11)) {

+		if (StartOf(12)) {

 			UpdateStmt(out s);

 			bodyAssign = s; 

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

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

 			HavocStmt(out s);

 			bodyAssign = s; 

-		} else SynErr(124);

+		} else SynErr(122);

 		Expect(8);

 		if (bodyAssign != null) {

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

@@ -1296,16 +1271,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

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

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(13)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

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

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

-		} else SynErr(125);

+		} else SynErr(123);

 	}

 

 	void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {

@@ -1316,16 +1291,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> args;

 		r = null;  // to please compiler

 		

-		if (la.kind == 51) {

+		if (la.kind == 48) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

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

-				if (la.kind == 52) {

+			if (la.kind == 49 || la.kind == 51) {

+				if (la.kind == 49) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(53);

+					Expect(50);

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

 					

 				} else {

@@ -1347,7 +1322,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(126);

+		} else SynErr(124);

 	}

 

 	void Guard(out Expression e) {

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(127);

+		} else SynErr(125);

 		Expect(33);

 	}

 

@@ -1378,11 +1353,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Statement> body;

 		

 		Expect(7);

-		while (la.kind == 45) {

+		while (la.kind == 56) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(46);

+			Expect(57);

 			body = new List<Statement>(); 

 			while (StartOf(9)) {

 				Stmt(body);

@@ -1397,14 +1372,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 		invariants = new List<MaybeFreeExpression/*!*/>();

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

 		

-		while (la.kind == 28 || la.kind == 31 || la.kind == 60) {

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

+		while (la.kind == 28 || la.kind == 31 || la.kind == 59) {

+			if (la.kind == 28 || la.kind == 59) {

 				isFree = false; 

 				if (la.kind == 28) {

 					Get();

 					isFree = true; 

 				}

-				Expect(60);

+				Expect(59);

 				Expression(out e);

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

 				Expect(17);

@@ -1428,7 +1403,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

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

 		

-		Expect(45);

+		Expect(56);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 32) {

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

 			Expect(33);

 		}

-		Expect(46);

+		Expect(57);

 		while (StartOf(9)) {

 			Stmt(body);

 		}

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

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(128);

+		} else SynErr(126);

 	}

 

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

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

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

 			Get();

-		} else SynErr(129);

+		} else SynErr(127);

 	}

 

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

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

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

 			Get();

-		} else SynErr(130);

+		} else SynErr(128);

 	}

 

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

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

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

 			Get();

-		} else SynErr(131);

+		} else SynErr(129);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(132);

+		} else SynErr(130);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(133); break;

+		default: SynErr(131); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(134);

+		} else SynErr(132);

 	}

 

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

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

-		if (la.kind == 84) {

+		switch (la.kind) {

+		case 84: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

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

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

+			break;

+		}

+		case 87: case 88: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

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

-		} else if (StartOf(16)) {

+			break;

+		}

+		case 37: case 54: case 60: case 98: case 99: case 100: case 101: {

 			EndlessExpression(out e);

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

+			break;

+		}

+		case 1: {

 			DottedIdentifiersAndFunction(out e);

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

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(13)) {

+			break;

+		}

+		case 7: case 49: {

+			DisplayExpr(out e);

+			break;

+		}

+		case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {

 			ConstAtomExpression(out e);

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

+			while (la.kind == 49 || la.kind == 51) {

 				Suffix(ref e);

 			}

-		} else SynErr(135);

+			break;

+		}

+		default: SynErr(133); break;

+		}

 	}

 

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

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

 			Get();

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

-		} else SynErr(136);

+		} else SynErr(134);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(137);

+		} else SynErr(135);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1771,20 +1762,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression e0, e1;

 		e = dummyExpr;

 		

-		if (la.kind == 57) {

+		if (la.kind == 54) {

 			Get();

 			x = t; 

 			Expression(out e);

 			Expect(96);

 			Expression(out e0);

-			Expect(58);

+			Expect(55);

 			Expression(out e1);

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

-		} else if (StartOf(17)) {

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

+			MatchExpression(out e);

+		} else if (StartOf(16)) {

 			QuantifierGuts(out e);

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

 			ComprehensionExpr(out e);

-		} else SynErr(138);

+		} else SynErr(136);

 	}

 

 	void DottedIdentifiersAndFunction(out Expression e) {

@@ -1794,7 +1787,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 54) {

+		while (la.kind == 51) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

@@ -1816,7 +1809,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 54) {

+		if (la.kind == 51) {

 			Get();

 			Ident(out id);

 			if (la.kind == 32) {

@@ -1829,7 +1822,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				e = new FunctionCallExpr(id, id.val, e, args); 

 			}

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

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

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

 			Get();

 			x = t; 

 			if (StartOf(8)) {

@@ -1842,11 +1835,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

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

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

 					while (la.kind == 19) {

 						Get();

 						Expression(out ee);

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

 						

 					}

-				} else SynErr(139);

+				} else SynErr(137);

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

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(140);

+			} else SynErr(138);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

@@ -1885,13 +1878,37 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  }

 			}

 			

-			Expect(53);

-		} else SynErr(141);

+			Expect(50);

+		} else SynErr(139);

+	}

+

+	void DisplayExpr(out Expression e) {

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

+		IToken/*!*/ x;  List<Expression/*!*/>/*!*/ elements;

+		e = dummyExpr;

+		

+		if (la.kind == 7) {

+			Get();

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

+			if (StartOf(8)) {

+				Expressions(elements);

+			}

+			e = new SetDisplayExpr(x, elements); 

+			Expect(8);

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

+			Get();

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

+			if (StartOf(8)) {

+				Expressions(elements);

+			}

+			e = new SeqDisplayExpr(x, elements); 

+			Expect(50);

+		} else SynErr(140);

 	}

 

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

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

-		IToken/*!*/ x;  BigInteger n;  List<Expression/*!*/>/*!*/ elements;

+		IToken/*!*/ x;  BigInteger n;

 		e = dummyExpr;

 		

 		switch (la.kind) {

@@ -1955,26 +1972,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(16);

 			break;

 		}

-		case 7: {

-			Get();

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

-			if (StartOf(8)) {

-				Expressions(elements);

-			}

-			e = new SetDisplayExpr(x, elements); 

-			Expect(8);

-			break;

-		}

-		case 52: {

-			Get();

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

-			if (StartOf(8)) {

-				Expressions(elements);

-			}

-			e = new SeqDisplayExpr(x, elements); 

-			Expect(53);

-			break;

-		}

 		case 32: {

 			Get();

 			x = t; 

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

 			break;

 		}

-		default: SynErr(142); break;

+		default: SynErr(141); break;

 		}

 	}

 

@@ -1998,6 +1995,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 	}

 

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

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

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

+		

+		Expect(60);

+		x = t; 

+		Expression(out e);

+		while (la.kind == 56) {

+			CaseExpression(out c);

+			cases.Add(c); 

+		}

+		e = new MatchExpr(x, e, cases); 

+	}

+

 	void QuantifierGuts(out Expression/*!*/ q) {

 		Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;

 		bool univ = false;

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

 			Exists();

 			x = t; 

-		} else SynErr(143);

+		} else SynErr(142);

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

 		while (la.kind == 19) {

@@ -2067,12 +2078,36 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 	}

 

+	void CaseExpression(out MatchCaseExpr/*!*/ c) {

+		Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

+		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

+		Expression/*!*/ body;

+		

+		Expect(56);

+		x = t; 

+		Ident(out id);

+		if (la.kind == 32) {

+			Get();

+			Ident(out arg);

+			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

+			while (la.kind == 19) {

+				Get();

+				Ident(out arg);

+				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

+			}

+			Expect(33);

+		}

+		Expect(57);

+		Expression(out body);

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

+	}

+

 	void Forall() {

 		if (la.kind == 98) {

 			Get();

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

 			Get();

-		} else SynErr(144);

+		} else SynErr(143);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(145);

+		} else SynErr(144);

 	}

 

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

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

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(146);

+		} else SynErr(145);

 		Expect(8);

 	}

 

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

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

 			Get();

-		} else SynErr(147);

+		} else SynErr(146);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2113,7 +2148,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(22);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(18)) {

+		if (StartOf(17)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 19) {

@@ -2129,13 +2164,13 @@ 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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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},

@@ -2145,17 +2180,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 } // end Parser

@@ -2164,20 +2198,18 @@ 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;

@@ -2224,23 +2256,23 @@ public class Errors {
 			case 41: s = "\"reads\" expected"; break;

 			case 42: s = "\"*\" expected"; break;

 			case 43: s = "\"`\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 60: s = "\"invariant\" 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 = "\"case\" expected"; break;

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

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

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

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

 			case 61: s = "\"foreach\" expected"; break;

 			case 62: s = "\"in\" expected"; break;

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

@@ -2294,44 +2326,43 @@ public class Errors {
 			case 111: s = "invalid MethodSpec"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

-		return s;

+    return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2339,9 +2370,8 @@ 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/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5ee2f0c9..6a84a361 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -712,7 +712,7 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          bool parensNeeded = !isLastCase && mc.Body is MatchExpr;

+          bool parensNeeded = !isLastCase && mc.Body.Resolved is MatchExpr;

           if (parensNeeded) {

             wr.WriteLine(" => (");

           } else {

@@ -721,6 +721,8 @@ namespace Microsoft.Dafny {
           PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen));

           i++;

         }

+      } else if (expr is ParensExpression) {

+        PrintExtendedExpr((ParensExpression)expr, indent, isRightmost, endWithCloseParen);

       } else {

         PrintExpression(expr, indent);

         wr.WriteLine(endWithCloseParen ? ")" : "");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 96907777..b1bbe6c4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1993,6 +1993,10 @@ namespace Microsoft.Dafny {
       ResolveExpression(expr, twoState, null);

     }

 

+    /// <summary>

+    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression; 

+    /// if null, no "match" expression will be allowed.

+    /// </summary>

     void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

@@ -2009,7 +2013,7 @@ namespace Microsoft.Dafny {
 

       if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, twoState, matchVarContext);  // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression

         e.ResolvedExpression = e.E;

         e.Type = e.E.Type;

 

@@ -2464,6 +2468,10 @@ namespace Microsoft.Dafny {
       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

+        if (matchVarContext == null) {

+          Error(me, "'match' expressions are not supported in this context");

+          matchVarContext = new List<IVariable>();

+        }

         ResolveExpression(me.Source, twoState);

         Contract.Assert(me.Source.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 083c0c0c..d45bbbbe 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/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,17 +31,15 @@ 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;

@@ -53,12 +51,12 @@ public class Buffer {
 

 		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;

@@ -75,14 +73,14 @@ public class Buffer {
 	}

 

 	~Buffer() { Close(); }

-

+	

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-

+	

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;

 		return ch;

 	}

-

+	

 	public string/*!*/ GetString (int beg, int end) {

 	  Contract.Ensures(Contract.Result<string>() != null);

 		int len = 0;

@@ -141,7 +139,7 @@ public class Buffer {
 			}

 		}

 	}

-

+	

 	// 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.

@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 104;

 

 

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

-	}

-

+[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

@@ -239,13 +236,13 @@ public class Scanner {
 

 	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;

@@ -270,8 +267,8 @@ public class Scanner {
 		start[41] = 22; 

 		start[42] = 23; 

 		start[96] = 24; 

-		start[91] = 27; 

-		start[93] = 28; 

+		start[91] = 26; 

+		start[93] = 27; 

 		start[46] = 62; 

 		start[8660] = 31; 

 		start[8658] = 33; 

@@ -293,9 +290,9 @@ public class Scanner {
 		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;

@@ -305,14 +302,15 @@ public class Scanner {
 			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);

@@ -321,9 +319,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

+		

 		Init();

 	}

-

+	

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -344,11 +343,11 @@ public class Scanner {
 	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 +358,7 @@ public class Scanner {
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; }

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +366,9 @@ public class Scanner {
 //			// 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 +418,7 @@ public class Scanner {
 				return;

 			  }

 

-

+			

 		}

 

 	}

@@ -513,18 +512,18 @@ public class Scanner {
 			case "object": t.kind = 39; break;

 			case "function": t.kind = 40; break;

 			case "reads": t.kind = 41; break;

-			case "match": t.kind = 44; break;

-			case "case": t.kind = 45; break;

-			case "label": t.kind = 47; break;

-			case "break": t.kind = 48; break;

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

-			case "new": t.kind = 51; break;

-			case "choose": t.kind = 55; break;

-			case "havoc": t.kind = 56; break;

-			case "if": t.kind = 57; break;

-			case "else": t.kind = 58; break;

-			case "while": t.kind = 59; break;

-			case "invariant": t.kind = 60; 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 "case": t.kind = 56; break;

+			case "while": t.kind = 58; break;

+			case "invariant": t.kind = 59; break;

+			case "match": t.kind = 60; break;

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

 			case "in": t.kind = 62; break;

 			case "assert": t.kind = 63; break;

@@ -556,13 +555,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) {

-			Contract.Assert(start[ch] != null);

-			state = (int) start[ch];

-		}

+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

 		else { state = 0; }

 		tlen = 0; AddCh();

-

+		

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -657,13 +653,13 @@ public class Scanner {
 			case 24:

 				{t.kind = 43; break;}

 			case 25:

-				{t.kind = 46; break;}

+				{t.kind = 47; break;}

 			case 26:

-				{t.kind = 50; break;}

+				{t.kind = 49; break;}

 			case 27:

-				{t.kind = 52; break;}

+				{t.kind = 50; break;}

 			case 28:

-				{t.kind = 53; break;}

+				{t.kind = 57; break;}

 			case 29:

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

 				else {goto case 0;}

@@ -725,7 +721,7 @@ public class Scanner {
 				{t.kind = 103; break;}

 			case 57:

 				recEnd = pos; recKind = 15;

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

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

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

 				else {t.kind = 15; break;}

 			case 58:

@@ -734,7 +730,7 @@ public class Scanner {
 				else {t.kind = 16; break;}

 			case 59:

 				recEnd = pos; recKind = 22;

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

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

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

 				else {t.kind = 22; break;}

 			case 60:

@@ -746,9 +742,9 @@ public class Scanner {
 				if (ch == '=') {AddCh(); goto case 39;}

 				else {t.kind = 24; break;}

 			case 62:

-				recEnd = pos; recKind = 54;

+				recEnd = pos; recKind = 51;

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

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

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

 			case 63:

 				recEnd = pos; recKind = 87;

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

@@ -768,14 +764,14 @@ public class Scanner {
 		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);

@@ -796,7 +792,7 @@ public class Scanner {
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-

+	

 		return pt;

 	}

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 19272ef4..8752ffea 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -460,12 +460,13 @@ namespace Microsoft.Dafny {
             AddLimitedAxioms(f, 1);

           }

           for (int layerOffset = 0; layerOffset < 2; layerOffset++) {

-            if (f.Body is MatchExpr) {

-              AddFunctionAxiomCase(f, (MatchExpr)f.Body, null, layerOffset);

+            var body = f.Body == null ? null : f.Body.Resolved;

+            if (body is MatchExpr) {

+              AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);

               Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, layerOffset);

               sink.TopLevelDeclarations.Add(axPost);

             } else {

-              Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, layerOffset);

+              Bpl.Axiom ax = FunctionAxiom(f, body, f.Ens, null, layerOffset);

               sink.TopLevelDeclarations.Add(ax);

             }

             if (!f.IsRecursive || f.IsUnlimited) { break; }

@@ -510,10 +511,11 @@ namespace Microsoft.Dafny {
       foreach (MatchCaseExpr mc in me.Cases) {

         Contract.Assert(mc.Ctor != null);  // the field is filled in by resolution

         Specialization s = new Specialization(formal, mc, prev);

-        if (mc.Body is MatchExpr) {

-          AddFunctionAxiomCase(f, (MatchExpr)mc.Body, s, layerOffset);

+        var body = mc.Body.Resolved;

+        if (body is MatchExpr) {

+          AddFunctionAxiomCase(f, (MatchExpr)body, s, layerOffset);

         } else {

-          Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), s, layerOffset);

+          Bpl.Axiom ax = FunctionAxiom(f, body, new List<Expression>(), s, layerOffset);

           sink.TopLevelDeclarations.Add(ax);

         }

       }

@@ -2093,6 +2095,7 @@ namespace Microsoft.Dafny {
       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

         CheckWellformedWithResult(e.ResolvedExpression, options, result, resultType, locals, builder, etran);

+        result = null;

 

       } else {

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

@@ -3067,7 +3070,8 @@ namespace Microsoft.Dafny {
           Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);

           Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));

           // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences

-          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));

+          var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);

+          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));

         }

         oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);

         

@@ -5332,7 +5336,7 @@ namespace Microsoft.Dafny {
       } else if (expandFunctions && expr is FunctionCallExpr) {

         var fexp = (FunctionCallExpr)expr;

         Contract.Assert(fexp.Function != null);  // filled in during resolution

-        if (fexp.Function.Body != null && !(fexp.Function.Body is MatchExpr)) {

+        if (fexp.Function.Body != null && !(fexp.Function.Body.Resolved is MatchExpr)) {

           // inline this body

           Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

           Contract.Assert(fexp.Args.Count == fexp.Function.Formals.Count);

@@ -5533,7 +5537,7 @@ namespace Microsoft.Dafny {
       // consider automatically applying induction

       var inductionVariables = new List<BoundVar>();

       foreach (var n in e.BoundVars) {

-        if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

+        if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

           if (CommandLineOptions.Clo.Trace) {

             Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);

             new Printer(Console.Out).PrintExpression(e);