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, 32 insertions, 5 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 9f83bf09..f729d411 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -300,9 +300,8 @@ namespace Microsoft.Dafny
         var e = (ExprDotName)expr;

         return new ExprDotName(Tok(e.tok), CloneExpr(e.Lhs), e.SuffixName, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));

       } else if (expr is ApplySuffix) {

-        var e = (ApplySuffix)expr;

-        return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));

-

+        var e = (ApplySuffix) expr;

+        return CloneApplySuffix(e);

       } else if (expr is MemberSelectExpr) {

         var e = (MemberSelectExpr)expr;

         return new MemberSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.MemberName);

@@ -411,7 +410,7 @@ namespace Microsoft.Dafny
       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),

-          e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces);

+          e.Cases.ConvertAll(CloneMatchCaseExpr), e.UsesOptionalBraces);

 

       } else if (expr is NegationExpression) {

         var e = (NegationExpression)expr;

@@ -422,6 +421,22 @@ namespace Microsoft.Dafny
       }

     }

 

+    public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) {

+      Contract.Requires(c != null);

+      if (c.Arguments != null) {

+        Contract.Assert(c.CasePatterns == null);

+        return new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body));

+      } else {

+        Contract.Assert(c.Arguments == null);

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

+        return new MatchCaseExpr(Tok(c.tok), c.Id, c.CasePatterns.ConvertAll(CloneCasePattern), CloneExpr(c.Body));

+      }

+    }

+

+    public virtual Expression CloneApplySuffix(ApplySuffix e) {

+        return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));

+    }

+

     public virtual CasePattern CloneCasePattern(CasePattern pat) {

       Contract.Requires(pat != null);

       if (pat.Var != null) {

@@ -530,7 +545,7 @@ namespace Microsoft.Dafny
       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),

-          s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))), s.UsesOptionalBraces);

+          s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);

 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

@@ -562,6 +577,18 @@ namespace Microsoft.Dafny
       return r;

     }

 

+    public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) {

+      Contract.Requires(c != null);

+      if (c.Arguments != null) {

+        Contract.Assert(c.CasePatterns == null);

+        return new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt));

+      } else {

+        Contract.Assert(c.Arguments == null);

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

+        return new MatchCaseStmt(Tok(c.tok), c.Id, c.CasePatterns.ConvertAll(CloneCasePattern), c.Body.ConvertAll(CloneStmt));

+      }

+    }

+

     public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) {

       if (op is CalcStmt.BinaryCalcOp) {

         return new CalcStmt.BinaryCalcOp(((CalcStmt.BinaryCalcOp) op).Op);