Allow MatchExpr and MatchStmt to have nested patterns. Such as

function last<T>(xs: List<T>): T
  requires xs != Nil
{
  match xs
  case Cons(y, Nil) => y
  case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
  match (x, y)
  case (Zero, _) => Zero
  case (Suc(_), Zero) => x
  case (Suc(a), Suc(b)) => minus(a, b)
}

1 files changed, 30 insertions, 30 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index bf42c71a..0259f12c 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -901,17 +901,7 @@ namespace Microsoft.Dafny {
           wr.WriteLine();

           Indent(caseInd);

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

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

-            string sep = "(";

-            foreach (BoundVar bv in mc.Arguments) {

-              wr.Write("{0}{1}", sep, bv.DisplayName);

-              if (bv.Type is NonProxyType) {

-                wr.Write(": {0}", bv.Type);

-              }

-              sep = ", ";

-            }

-            wr.Write(")");

-          }

+          PrintMatchCaseArgument(mc);

           wr.Write(" =>");

           foreach (Statement bs in mc.Body) {

             wr.WriteLine();

@@ -1199,17 +1189,7 @@ namespace Microsoft.Dafny {
           bool isLastCase = i == e.Cases.Count - 1;

           Indent(ind);

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

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

-            string sep = "(";

-            foreach (BoundVar bv in mc.Arguments) {

-              wr.Write("{0}{1}", sep, bv.DisplayName);

-              if (bv.Type is NonProxyType) {

-                wr.Write(": {0}", bv.Type);

-              }

-              sep = ", ";

-            }

-            wr.Write(")");

-          }

+          PrintMatchCaseArgument(mc);          

           wr.WriteLine(" =>");

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

           i++;

@@ -1246,6 +1226,33 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public void PrintMatchCaseArgument(MatchCase mc) {

+      if (mc.Arguments != null) {

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

+          string sep = "(";

+          foreach (BoundVar bv in mc.Arguments) {

+            wr.Write("{0}{1}", sep, bv.DisplayName);

+            if (bv.Type is NonProxyType) {

+              wr.Write(": {0}", bv.Type);

+            }

+            sep = ", ";

+          }

+          wr.Write(")");

+        }

+      } else {

+        Contract.Assert(mc.CasePatterns != null);

+        if (mc.CasePatterns.Count != 0) {

+          string sep = "(";

+          foreach (var cp in mc.CasePatterns) {

+            wr.Write(sep);

+            PrintCasePattern(cp);

+            sep = ", ";

+          }

+          wr.Write(")");

+        }

+      }

+    }

+

     public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {

       Contract.Requires(expr != null);

       PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1);

@@ -1859,14 +1866,7 @@ namespace Microsoft.Dafny {
         foreach (var mc in e.Cases) {

           bool isLastCase = i == e.Cases.Count - 1;

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

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

-            string sep = "(";

-            foreach (BoundVar bv in mc.Arguments) {

-              wr.Write("{0}{1}", sep, bv.DisplayName);

-              sep = ", ";

-            }

-            wr.Write(")");

-          }

+          PrintMatchCaseArgument(mc);

           wr.Write(" => ");

           PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);

           i++;