Dafny: support for nested match expressions

8 files changed, 320 insertions, 115 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c4955a6a..0d815bf4 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -666,6 +666,9 @@ MatchExpression<out Expression/*!*/ e>
   .)

   "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); .)

@@ -686,10 +689,20 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
     }

   ")" ]

   "=>"

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

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

                                  parseVarScope.PopMarker(); .)

   .

 

+/* 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>

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 290609fc..d49c78c6 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -977,11 +977,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(31);

 		}

 		Expect(43);

-		Expression(out body);

+		MatchOrExpr(out body);

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

 		parseVarScope.PopMarker(); 

 	}

 

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

+		e = dummyExpr; 

+		if (la.kind == 30) {

+			Get();

+			MatchOrExpr(out e);

+			Expect(31);

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

+			MatchExpression(out e);

+		} else if (StartOf(9)) {

+			Expression(out e);

+		} else SynErr(118);

+	}

+

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

 		Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;

 		IToken bodyStart, bodyEnd;

@@ -995,7 +1008,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ss.Add(s); 

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

 			VarDeclStmts(ss);

-		} else SynErr(118);

+		} else SynErr(119);

 	}

 

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

@@ -1073,7 +1086,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			s = new ReturnStmt(x); 

 			break;

 		}

-		default: SynErr(119); break;

+		default: SynErr(120); break;

 		}

 	}

 

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

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

 				els = s; 

-			} else SynErr(120);

+			} else SynErr(121);

 		}

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

 	}

@@ -1354,7 +1367,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 51) {

 			HavocStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else SynErr(121);

+		} else SynErr(122);

 		Expect(8);

 		if (bodyAssign != null) {

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

@@ -1393,7 +1406,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out e);

 			ee = new List<Expression>(); ee.Add(e); 

-		} else SynErr(122);

+		} else SynErr(123);

 		if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); } 

 	}

 

@@ -1403,7 +1416,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			IdentOrFuncExpression(out e);

 		} else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {

 			ObjectExpression(out e);

-		} else SynErr(123);

+		} else SynErr(124);

 		while (la.kind == 49 || la.kind == 92) {

 			SelectOrCallSuffix(ref e);

 		}

@@ -1449,7 +1462,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(124);

+		} else SynErr(125);

 		Expect(31);

 	}

 

@@ -1492,7 +1505,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {

 			ObjectExpression(out e);

 			SelectOrCallSuffix(ref e);

-		} else SynErr(125);

+		} else SynErr(126);

 		while (la.kind == 49 || la.kind == 92) {

 			SelectOrCallSuffix(ref e);

 		}

@@ -1506,7 +1519,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(126);

+		} else SynErr(127);

 	}

 

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

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

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

 			Get();

-		} else SynErr(127);

+		} else SynErr(128);

 	}

 

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

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

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

 			Get();

-		} else SynErr(128);

+		} else SynErr(129);

 	}

 

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

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

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

 			Get();

-		} else SynErr(129);

+		} else SynErr(130);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(130);

+		} else SynErr(131);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(131); break;

+		default: SynErr(132); break;

 		}

 	}

 

@@ -1698,7 +1711,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 83) {

 			Get();

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

-		} else SynErr(132);

+		} else SynErr(133);

 	}

 

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

@@ -1717,7 +1730,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			SelectExpression(out e);

 		} else if (StartOf(16)) {

 			ConstAtomExpression(out e);

-		} else SynErr(133);

+		} else SynErr(134);

 	}

 

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

@@ -1731,7 +1744,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 85) {

 			Get();

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

-		} else SynErr(134);

+		} else SynErr(135);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(135);

+		} else SynErr(136);

 	}

 

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

@@ -1830,7 +1843,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(50);

 			break;

 		}

-		default: SynErr(136); break;

+		default: SynErr(137); break;

 		}

 	}

 

@@ -1885,9 +1898,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 				QuantifierGuts(out e);

 			} else if (StartOf(9)) {

 				Expression(out e);

-			} else SynErr(137);

+			} else SynErr(138);

 			Expect(31);

-		} else SynErr(138);

+		} else SynErr(139);

 	}

 

 	void SelectOrCallSuffix(ref Expression/*!*/ e) {

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

 						

 					}

-				} else SynErr(139);

+				} else SynErr(140);

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

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(140);

+			} else SynErr(141);

 			if (multipleIndices != null) {

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

 			} else {

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

 			

 			Expect(50);

-		} else SynErr(141);

+		} else SynErr(142);

 	}

 

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

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

 			Exists();

 			x = t; 

-		} else SynErr(142);

+		} else SynErr(143);

 		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

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

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

 			Get();

-		} else SynErr(143);

+		} else SynErr(144);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(144);

+		} else SynErr(145);

 	}

 

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

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

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(145);

+		} else SynErr(146);

 		Expect(8);

 	}

 

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

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

 			Get();

-		} else SynErr(146);

+		} else SynErr(147);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2234,35 +2247,36 @@ public class Errors {
 			case 115: s = "invalid FunctionBody"; break;

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

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

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

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

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

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

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

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

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

-			case 125: s = "invalid CallStmtSubExpr"; 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 ConstAtomExpression"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 			case 138: s = "invalid ObjectExpression"; break;

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

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

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

 			case 141: s = "invalid SelectOrCallSuffix"; 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;

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

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

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

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

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

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

 

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

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 0b93a1dc..6b97b471 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -239,7 +239,7 @@ namespace Microsoft.Dafny {
       if (f.Body != null) {

         Indent(indent);

         wr.WriteLine("{");

-        PrintExtendedExpr(f.Body, ind);

+        PrintExtendedExpr(f.Body, ind, true, false);

         Indent(indent);

         wr.WriteLine("}");

       }

@@ -560,7 +560,9 @@ namespace Microsoft.Dafny {
           }

           wr.WriteLine(" =>");

           foreach (Statement bs in mc.Body) {

+            Indent(caseInd + IndentAmount);

             PrintStatement(bs, caseInd + IndentAmount);

+            wr.WriteLine();

           }

         }

         Indent(indent);

@@ -604,7 +606,7 @@ namespace Microsoft.Dafny {
     

     // ----------------------------- PrintExpression -----------------------------

 

-    public void PrintExtendedExpr(Expression expr, int indent) {

+    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

       Contract.Requires(expr != null);

       Indent(indent);

       if (expr is ITEExpr) {

@@ -613,7 +615,7 @@ namespace Microsoft.Dafny {
           wr.Write("if ");

           PrintExpression(ite.Test);

           wr.WriteLine(" then");

-          PrintExtendedExpr(ite.Thn, indent + IndentAmount);

+          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);

           expr = ite.Els;

           if (expr is ITEExpr) {

             Indent(indent);  wr.Write("else ");

@@ -621,7 +623,7 @@ namespace Microsoft.Dafny {
             Indent(indent);  wr.WriteLine("else");

             Indent(indent + IndentAmount);

             PrintExpression(expr);

-            wr.WriteLine();

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

             return;

           }

         }

@@ -629,7 +631,10 @@ namespace Microsoft.Dafny {
         MatchExpr me = (MatchExpr)expr;

         wr.Write("match ");

         PrintExpression(me.Source);

+        wr.WriteLine();

+        int i = 0;

         foreach (MatchCaseExpr mc in me.Cases) {

+          bool isLastCase = i == me.Cases.Count - 1;

           Indent(indent);

           wr.Write("case {0}", mc.Id);

           if (mc.Arguments.Count != 0) {

@@ -640,12 +645,18 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          wr.WriteLine(" =>");

-          PrintExtendedExpr(mc.Body, indent + IndentAmount);

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

+          if (parensNeeded) {

+            wr.WriteLine(" => (");

+          } else {

+            wr.WriteLine(" =>");

+          }

+          PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen));

+          i++;

         }

       } else {

         PrintExpression(expr, indent);

-        wr.WriteLine();

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

       }

     }

     

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1e27c4db..57fe4f77 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -624,7 +624,8 @@ namespace Microsoft.Dafny {
         // any type is fine

       }

       if (f.Body != null) {

-        ResolveExpression(f.Body, false, f.IsGhost);

+        List<IVariable> matchVarContext = new List<IVariable>(f.Formals);

+        ResolveExpression(f.Body, false, f.IsGhost, matchVarContext);

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

         if (!UnifyTypes(f.Body.Type, f.ResultType)) {

           Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);

@@ -1713,7 +1714,11 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// "twoState" implies that "old" and "fresh" expressions are allowed

     /// </summary>

-    void ResolveExpression(Expression expr, bool twoState, bool specContext){

+    void ResolveExpression(Expression expr, bool twoState, bool specContext) {

+      ResolveExpression(expr, twoState, specContext, null);

+    }

+

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

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

@@ -2207,6 +2212,7 @@ namespace Microsoft.Dafny {
           dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);

         }

         Dictionary<string,DatatypeCtor> ctors;

+        IVariable goodMatchVariable = null;

         if (dtd == null) {

           Error(me.Source, "the type of the match source expression must be a datatype");

           ctors = null;

@@ -2216,8 +2222,12 @@ namespace Microsoft.Dafny {
           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

           

           IdentifierExpr ie = me.Source as IdentifierExpr;

-          if (ie == null || !(ie.Var is Formal)) {

-            Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function");

+          if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {

+            Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");

+          } else if (!matchVarContext.Contains(ie.Var)) {

+            Error(me.Source.tok, "match source expression '{0}' has already been used as a match source expression in this context", ie.Var.Name);

+          } else {

+            goodMatchVariable = ie.Var;

           }

           

           // build the type-parameter substitution map for this use of the datatype

@@ -2270,7 +2280,12 @@ namespace Microsoft.Dafny {
             }

             i++;

           }

-          ResolveExpression(mc.Body, twoState, specContext);

+          List<IVariable> innerMatchVarContext = new List<IVariable>(matchVarContext);

+          if (goodMatchVariable != null) {

+            innerMatchVarContext.Remove(goodMatchVariable);  // this variable is no longer available for matching

+          }

+          innerMatchVarContext.AddRange(mc.Arguments);

+          ResolveExpression(mc.Body, twoState, specContext, innerMatchVarContext);

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

           if (!UnifyTypes(expr.Type, mc.Body.Type)) {

             Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 08800623..c3eec272 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -445,17 +445,11 @@ namespace Microsoft.Dafny {
           Function f = (Function)member;

           AddFunction(f);

           if (f.Body is MatchExpr) {

-            MatchExpr me = (MatchExpr)f.Body;

-            Formal formal = (Formal)((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks

-            foreach (MatchCaseExpr mc in me.Cases) {

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

-              Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), formal, mc.Ctor, mc.Arguments);

-              sink.TopLevelDeclarations.Add(ax);

-            }

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

+            AddFunctionAxiomCase(f, (MatchExpr)f.Body, null);

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

             sink.TopLevelDeclarations.Add(axPost);

           } else {

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

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

             sink.TopLevelDeclarations.Add(ax);

           }

           if (f.IsRecursive && !f.IsUnlimited) {

@@ -492,16 +486,81 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens,

-                                 Formal specializationFormal,

-                                 DatatypeCtor ctor, List<BoundVar/*!*/> specializationReplacementFormals){

+    void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev) {

+      Contract.Requires(f != null);

+      Contract.Requires(me != null);

+      IVariable formal = ((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks

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

+        } else {

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

+          sink.TopLevelDeclarations.Add(ax);

+        }

+      }

+    }

+

+    class Specialization

+    {

+      public readonly List<Formal/*!*/> Formals;

+      public readonly List<Expression/*!*/> ReplacementExprs;

+      public readonly List<BoundVar/*!*/> ReplacementFormals;

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(cce.NonNullElements(Formals));

+        Contract.Invariant(cce.NonNullElements(ReplacementExprs));

+        Contract.Invariant(Formals.Count == ReplacementExprs.Count);

+        Contract.Invariant(cce.NonNullElements(ReplacementFormals));

+      }

+

+      public Specialization(IVariable formal, MatchCase mc, Specialization prev) {

+        Contract.Requires(formal is Formal || formal is BoundVar);

+        Contract.Requires(mc != null);

+        Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal));

+

+        List<Expression> rArgs = new List<Expression>();

+        foreach (BoundVar p in mc.Arguments) {

+          IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+          ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

+          rArgs.Add(ie);

+        }

+        // create and resolve datatype value

+        var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);

+        r.Ctor = mc.Ctor;

+        r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);

+

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

+        substMap.Add(formal, r);

+

+        // Fill in the fields

+        Formals = new List<Formal>();

+        ReplacementExprs = new List<Expression>();

+        ReplacementFormals = new List<BoundVar>();

+        if (prev != null) {

+          Formals.AddRange(prev.Formals);

+          foreach (var e in prev.ReplacementExprs) {

+            ReplacementExprs.Add(Substitute(e, null, substMap));

+          }

+          foreach (var rf in prev.ReplacementFormals) {

+            if (rf != formal) {

+              ReplacementFormals.Add(rf);

+            }

+          }

+        }

+        if (formal is Formal) {

+          Formals.Add((Formal)formal);

+          ReplacementExprs.Add(r);

+        }

+        ReplacementFormals.AddRange(mc.Arguments);

+      }

+    }

+

+    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization) {

       Contract.Requires(f != null);

-      Contract.Requires(specializationFormal == null || body != null);

       Contract.Requires(ens != null);

-      Contract.Requires(cce.NonNullElements(specializationReplacementFormals));

       Contract.Requires(predef != null);

-      Contract.Requires((specializationFormal == null) == (ctor == null));

-      Contract.Requires((specializationFormal == null) == (specializationReplacementFormals == null));

       Contract.Requires(f.EnclosingClass != null);

  

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

@@ -523,12 +582,12 @@ namespace Microsoft.Dafny {
       //       f(args)-has-the-expected-type);

       //

       // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then

-      // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by

-      // "specializationReplacementFormals".

+      // "specialization.Formals" (which are expected to be among the formals of "f") are excluded and replaced by

+      // "specialization.ReplacementFormals".

       // The list "args" is the list of formals of function "f"; except, if a specialization is provided, then

-      // "specializationFormal" is replaced by the expression "ctor(specializationReplacementFormals)".

-      // If a specialization is provided, occurrences of "specializationFormal" in "body", "f.Req", and "f.Ens"

-      // are also replaced by that expression.

+      // each of the "specialization.Formals" is replaced by the corresponding expression in "specialization.ReplacementExprs".

+      // If a specialization is provided, occurrences of "specialization.Formals" in "body", "f.Req", and "f.Ens"

+      // are also replaced by those corresponding expressions.

       //

       // The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.

       //

@@ -562,25 +621,18 @@ namespace Microsoft.Dafny {
           etran.GoodRef(f.tok, bvThisIdExpr, thisType));

         ante = Bpl.Expr.And(ante, wh);

       }

-      DatatypeValue r = null;

-      if (specializationReplacementFormals != null) {

-        Contract.Assert(ctor != null);  // follows from if guard and the precondition

-        List<Expression> rArgs = new List<Expression>();

-        foreach (BoundVar p in specializationReplacementFormals) {

+      if (specialization != null) {

+        foreach (BoundVar p in specialization.ReplacementFormals) {

           bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

           formals.Add(bv);

-          IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

-          ie.Var = p;  ie.Type = ie.Var.Type;  // resolve it here

-          rArgs.Add(ie);

           // add well-typedness conjunct to antecedent

           Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, bv), p.Type, etran);

           if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

         }

-        r = new DatatypeValue(f.tok, cce.NonNull(ctor.EnclosingDatatype).Name, ctor.Name, rArgs);

-        r.Ctor = ctor;  r.Type = new UserDefinedType(f.tok, ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);  // resolve it here

       }

       foreach (Formal p in f.Formals) {

-        if (p != specializationFormal) {

+        int i = specialization == null ? -1 : specialization.Formals.FindIndex(val => val == p);

+        if (i == -1) {

           bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

           formals.Add(bv);

           Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);

@@ -589,8 +641,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);

           if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

         } else {

-          Contract.Assert(r != null);  // it is set above

-          args.Add(etran.TrExpr(r));

+          args.Add(etran.TrExpr(specialization.ReplacementExprs[i]));

           // note, well-typedness conjuncts for the replacement formals has already been done above

         }

       }

@@ -606,9 +657,11 @@ namespace Microsoft.Dafny {
             etran.InMethodContext())));

       

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

-      if (specializationFormal != null) {

-        Contract.Assert(r != null);

-        substMap.Add(specializationFormal, r);

+      if (specialization != null) {

+        Contract.Assert(specialization.Formals.Count == specialization.ReplacementExprs.Count);

+        for (int i = 0; i < specialization.Formals.Count; i++) {

+          substMap.Add(specialization.Formals[i], specialization.ReplacementExprs[i]);

+        }

       }

       Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType));

       Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

@@ -649,8 +702,12 @@ namespace Microsoft.Dafny {
       if (whr != null) { meat = Bpl.Expr.And(meat, whr); }

       Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));

       string comment = "definition axiom for " + f.FullName;

-      if (specializationFormal != null) {

-        comment = string.Format("{0}, specialized for '{1}'", comment, specializationFormal.Name);

+      if (specialization != null) {

+        string sep = "{0}, specialized for '{1}'";

+        foreach (var formal in specialization.Formals) {

+          comment = string.Format(sep, comment, formal.Name);

+          sep = "{0}, '{1}'";

+        }

       }

       return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);

     }

@@ -1831,11 +1888,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, null, locals, b, etran);

-          if (result != null) {

-            b.Add(new Bpl.AssumeCmd(mc.tok, Bpl.Expr.Eq(result, etran.TrExpr(mc.Body))));

-            b.Add(new Bpl.AssumeCmd(mc.tok, CanCallAssumption(mc.Body, etran)));

-          }

+          CheckWellformed(mc.Body, options, result, locals, b, etran);

           ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);

           els = null;

         }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 018a29e2..9501d26d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -408,7 +408,9 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela
 Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

 Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)

 Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts

-8 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context

+Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context

+10 resolution/type errors detected in Modules0.dfy

 

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

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

@@ -585,7 +587,7 @@ Execution trace:
     (0,0): anon24_Else

     (0,0): anon25_Then

 

-Dafny program verifier finished with 11 verified, 1 error

+Dafny program verifier finished with 17 verified, 1 error

 

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

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

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index a7ac03d9..998b20bc 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -93,3 +93,47 @@ method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode
       }

   }

 }

+

+class NestedMatchExpr {

+  function Cadr<T>(a: List<T>, default: T): T

+  {

+    match a

+    case Nil => default

+    case Cons(x,t) =>

+      match t

+      case Nil => default

+      case Cons(y,tail) => y

+  }

+  // CadrAlt is the same as Cadr, but it writes its two outer cases in the opposite order

+  function CadrAlt<T>(a: List<T>, default: T): T

+  {

+    match a

+    case Cons(x,t) => (

+      match t

+      case Nil => default

+      case Cons(y,tail) => y)

+    case Nil => default

+  }

+  method TestNesting0()

+  {

+    var x := 5;

+    var list := #List.Cons(3, #List.Cons(6, #List.Nil));

+    assert Cadr(list, x) == 6;

+    match (list) {

+      case Nil => assert false;

+      case Cons(h,t) => assert Cadr(t, x) == 5;

+    }

+  }

+  method TestNesting1(a: List<NestedMatchExpr>)

+    ensures Cadr(a, this) == CadrAlt(a, this);

+  {

+    match (a) {

+      case Nil =>

+      case Cons(x,t) =>

+        match (t) {

+          case Nil =>

+          case Cons(y,tail) =>

+        }

+    }

+  }

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 3e8d1e25..adce71a8 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -120,3 +120,56 @@ class Ghosty {
   method Callee(a: int, ghost b: int) { }

   ghost method Theorem(a: int) { }

 }

+

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

+

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

+

+function NestedMatch0(tree: Tree): int

+{

+  match tree

+  case Nil => 0

+  case Cons(h,l,r) =>

+    match tree  // error: cannot match on "tree" again

+    case Nil => 0

+    case Cons(hh,ll,rr) => hh

+}

+

+function NestedMatch1(tree: Tree): int

+{

+  match tree

+  case Nil => 0

+  case Cons(h,l,r) =>

+    match l

+    case Nil => 0

+    case Cons(h0,l0,r0) =>

+      match r

+      case Nil => 0

+      case Cons(h1,l1,r1) => h + h0 + h1

+}

+

+function NestedMatch2(tree: Tree): int

+{

+  match tree

+  case Nil => 0

+  case Cons(h,l,r) =>

+    match l

+    case Nil => 0

+    case Cons(h,l0,tree) =>  // fine to declare another "h" and "tree" here

+      match r

+      case Nil => 0

+      case Cons(h1,l1,r1) => h + h1

+}

+

+function NestedMatch3(tree: Tree): int

+{

+  match tree

+  case Nil => 0

+  case Cons(h,l,r) =>

+    match l

+    case Nil => 0

+    case Cons(h0,l0,r0) =>

+      match l  // error: cannot match on "l" again

+      case Nil => 0

+      case Cons(h1,l1,r1) => h + h0 + h1

+}