Fix various bugs in nested match patterns listed in issue #83

5 files changed, 414 insertions, 166 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 9b7bb12e..f13aa2f4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -294,8 +294,7 @@ namespace Microsoft.Dafny
         return new MapDisplayExpr(Tok(expr.tok), e.Finite, pp);

 

       } else if (expr is NameSegment) {

-        var e = (NameSegment)expr;

-        return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));

+        return CloneNameSegment(expr);

       } else if (expr is ExprDotName) {

         var e = (ExprDotName)expr;

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

@@ -449,6 +448,11 @@ namespace Microsoft.Dafny
       }

     }

 

+    public virtual NameSegment CloneNameSegment(Expression expr) {

+      var e = (NameSegment)expr;

+      return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));

+    }

+

     public virtual AssignmentRhs CloneRHS(AssignmentRhs rhs) {

       AssignmentRhs c;

       if (rhs is ExprRhs) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5f01f913..210e6f3d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5246,7 +5246,9 @@ namespace Microsoft.Dafny
       string name = FreshTempVarName("_mc#", codeContext);

       BoundVar bv = new BoundVar(s.Tok, name, type);

       List<CasePattern> patternSubst = new List<CasePattern>();

-      DesugarMatchCaseStmt(s, dtd, bv, patternSubst);

+      if (dtd != null) {

+        DesugarMatchCaseStmt(s, dtd, bv, patternSubst, codeContext);

+      }

 

       ISet<string> memberNamesUsed = new HashSet<string>();

       foreach (MatchCaseStmt mc in s.Cases) {

@@ -5270,20 +5272,20 @@ namespace Microsoft.Dafny
         }

         scope.PushMarker();

         int i = 0;

-        foreach (BoundVar v in mc.Arguments) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate parameter name: {0}", v.Name);

-          }

-          ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

-          if (ctor != null && i < ctor.Formals.Count) {

-            Formal formal = ctor.Formals[i];

-            Type st = SubstType(formal.Type, subst);

-            if (!UnifyTypes(v.Type, st)) {

-              Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);

+        if (mc.Arguments != null) {

+          foreach (BoundVar v in mc.Arguments) {

+            scope.Push(v.Name, v);

+            ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

+            if (ctor != null && i < ctor.Formals.Count) {

+              Formal formal = ctor.Formals[i];

+              Type st = SubstType(formal.Type, subst);

+              if (!UnifyTypes(v.Type, st)) {

+                Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);

+              }

+              v.IsGhost = formal.IsGhost;

             }

-            v.IsGhost = formal.IsGhost;

+            i++;

           }

-          i++;

         }

         foreach (Statement ss in mc.Body) {

           ResolveStatement(ss, bodyIsSpecOnly, codeContext);

@@ -5340,29 +5342,34 @@ namespace Microsoft.Dafny
       // (x, y) is treated as a 2-tuple constructor

       if (me.Source is DatatypeValue) {

         var e = (DatatypeValue)me.Source;

-        Contract.Assert(e.Arguments.Count >= 1);

-        Expression source = e.Arguments[0];

-        List<MatchCaseStmt> cases = new List<MatchCaseStmt>();

-        foreach (MatchCaseStmt mc in me.Cases) {

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

-          Contract.Assert(mc.CasePatterns.Count == e.Arguments.Count);

-          CasePattern cp = mc.CasePatterns[0];

-          List<CasePattern> patterns;

-          if (cp.Arguments != null) {

-            patterns = cp.Arguments;

-          } else {

-            patterns = new List<CasePattern>();

-          }

+        if (e.Arguments.Count < 1) {

+          Error(me.Tok, "match source tuple needs at least 1 argument");

+        } else {

+          Expression source = e.Arguments[0];

+          List<MatchCaseStmt> cases = new List<MatchCaseStmt>();

+          foreach (MatchCaseStmt mc in me.Cases) {

+            if (mc.CasePatterns == null || mc.CasePatterns.Count != e.Arguments.Count) {

+              Error(mc.tok, "case arguments count does not match source arguments count");

+            } else {

+              CasePattern cp = mc.CasePatterns[0];

+              List<CasePattern> patterns;

+              if (cp.Arguments != null) {

+                patterns = cp.Arguments;

+              } else {

+                patterns = new List<CasePattern>();

+              }

 

-          List<Statement> body = mc.Body;

-          for (int i = e.Arguments.Count; 1 <= --i; ) {

-            // others go into the body

-            body = CreateMatchCaseStmtBody(mc.tok, e.Arguments[i], mc.CasePatterns[i], body);

+              List<Statement> body = mc.Body;

+              for (int i = e.Arguments.Count; 1 <= --i; ) {

+                // others go into the body

+                body = CreateMatchCaseStmtBody(me.Tok, e.Arguments[i], mc.CasePatterns[i], body);

+              }

+              cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));

+            }

           }

-          cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));

+          me.UpdateSource(source);

+          me.UpdateCases(cases);

         }

-        me.UpdateSource(source);

-        me.UpdateCases(cases);

       }

     }

 

@@ -5398,9 +5405,14 @@ namespace Microsoft.Dafny
      *       case Nil => y

      *       case Cons(z, zs) => last(ys)

      */

-    void DesugarMatchCaseStmt(MatchStmt s, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns) {

+    void DesugarMatchCaseStmt(MatchStmt s, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns, ICodeContext codeContext) {

       Contract.Assert(dtd != null);

       Dictionary<string, DatatypeCtor> ctors = datatypeCtors[dtd];

+      if (ctors == null) {

+        // there is no constructor, no need to desugar

+        return;

+      }

+

       foreach (MatchCaseStmt mc in s.Cases) {

         if (mc.Arguments != null) {

           // already desugared. This happens during the second pass resolver after cloning.

@@ -5410,46 +5422,31 @@ namespace Microsoft.Dafny
 

         Contract.Assert(mc.Arguments == null);

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

+        Contract.Assert(ctors != null);

         DatatypeCtor ctor = null;

-        if (ctors != null) {

-          if (!ctors.TryGetValue(mc.Id, out ctor)) {

-            Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);

-          } else {

-            Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

-            mc.Ctor = ctor;

-            if (ctor.Formals.Count != mc.CasePatterns.Count) {

-              Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);

-            }

-          }

-        }

-        scope.PushMarker();

-        List<BoundVar> arguments = new List<BoundVar>();

-        foreach (CasePattern pat in mc.CasePatterns) {

-          // Find the constructor in the given datatype

-          // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible

-          ctor = null;

-          if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy && dtd != null)) {

-            if (datatypeCtors[dtd].TryGetValue(pat.Id, out ctor)) {

-              pat.Ctor = ctor;

-              pat.Var = null;

-            }

-          }

-          if (pat.Var != null) {

-            BoundVar v = pat.Var;

-            arguments.Add(v);

-            if (!scope.Push(v.Name, v)) {

-              Error(v, "Duplicate name: {0}", v.Name);

+

+        if (ctors.TryGetValue(mc.Id, out ctor)) {

+          scope.PushMarker();

+          foreach (CasePattern pat in mc.CasePatterns) {

+            FindDuplicateIdentifier(pat, ctors, true);

+          }

+          List<BoundVar> arguments = new List<BoundVar>();

+          foreach (CasePattern pat in mc.CasePatterns) {

+            if (pat.Var != null) {

+              BoundVar v = pat.Var;

+              arguments.Add(v);

+            } else {

+              DesugarMatchCasePattern(mc, pat, sourceVar);

+              patterns.Add(pat);

+              arguments.Add(sourceVar);

             }

-          } else {

-            DesugarMatchCasePattern(mc, pat, sourceVar);

-            patterns.Add(pat);

-            arguments.Add(sourceVar);

           }

+          mc.Arguments = arguments;

+          mc.CasePatterns = null;

+          scope.PopMarker();

         }

-        mc.Arguments = arguments;

-        mc.CasePatterns = null;

-        scope.PopMarker();

       }

+      

 

       List<MatchCaseStmt> newCases = new List<MatchCaseStmt>();

 

@@ -5473,13 +5470,13 @@ namespace Microsoft.Dafny
         if (CaseExprHasWildCard(mc)) {

           mcWithWildCard.Add(mc);

         } else {

-          thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap);

+          thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap, codeContext);

         }

       }

 

       foreach (MatchCaseStmt mc in mcWithWildCard) {

         // now process with cases with wildcard

-        thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap);

+        thingsChanged |= CombineMatchCaseStmt(mc, newCases, caseMap, codeContext);

       }

 

       if (thingsChanged) {

@@ -5487,6 +5484,37 @@ namespace Microsoft.Dafny
       }

     }

 

+    void FindDuplicateIdentifier(CasePattern pat, Dictionary<string, DatatypeCtor> ctors, bool topLevel) {

+      Contract.Assert(ctors != null);

+      DatatypeCtor ctor = null;

+      // Find the constructor in the given datatype

+      // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible

+      if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy)) {

+        if (ctors.TryGetValue(pat.Id, out ctor)) {

+          pat.Ctor = ctor;

+          pat.Var = null;

+        }

+      }

+      if (pat.Var != null) {

+        BoundVar v = pat.Var;

+        if (topLevel) {

+          if (!scope.Push(v.Name, v)) {

+            Error(v, "Duplicate parameter name: {0}", v.Name);

+          }

+        } else {

+          if (scope.Find(v.Name) != null) {

+            Error(v, "Duplicate parameter name: {0}", v.Name);

+          }

+        }

+      } else {

+        if (pat.Arguments != null) {

+          foreach (CasePattern cp in pat.Arguments) {

+            FindDuplicateIdentifier(cp, ctors, false);

+          }

+        }

+      }

+    }

+

     void DesugarMatchCasePattern(MatchCaseStmt mc, CasePattern pat, BoundVar v) {

       // convert 

       //    case Cons(y, Cons(z, zs)) => body

@@ -5503,7 +5531,7 @@ namespace Microsoft.Dafny
       mc.UpdateBody(list);

     }

 

-    bool CombineMatchCaseStmt(MatchCaseStmt mc, List<MatchCaseStmt> newCases, Dictionary<string, MatchCaseStmt> caseMap) {

+    bool CombineMatchCaseStmt(MatchCaseStmt mc, List<MatchCaseStmt> newCases, Dictionary<string, MatchCaseStmt> caseMap, ICodeContext codeContext) {

       bool thingsChanged = false;

       MatchCaseStmt old_mc;

       if (caseMap.TryGetValue(mc.Id, out old_mc)) {

@@ -5513,9 +5541,9 @@ namespace Microsoft.Dafny
         if ((oldBody.Count == 1) && (oldBody[0] is MatchStmt)

             && (body.Count == 1) && (body[0] is MatchStmt)) {

           // both only have on statement and the statement is MatchStmt

-          MatchStmt old = (MatchStmt) oldBody[0];

-          MatchStmt current = (MatchStmt) body[0];

-          if (SameMatchCase(old_mc, mc)) {

+          if (SameMatchCaseStmt(old_mc, mc, codeContext)) {

+            MatchStmt old = (MatchStmt)old_mc.Body[0];

+            MatchStmt current = (MatchStmt)mc.Body[0];

             foreach (MatchCaseStmt c in current.Cases) {

               old.Cases.Add(c);

             }

@@ -5532,7 +5560,7 @@ namespace Microsoft.Dafny
       return thingsChanged;

     }

 

-    bool SameMatchCase(MatchCaseStmt one, MatchCaseStmt other) {

+    bool SameMatchCaseStmt(MatchCaseStmt one, MatchCaseStmt other, ICodeContext codeContext) {

       // this method is called after all the CasePattern in the match cases are converted

       // into BoundVars.

       Contract.Assert(one.CasePatterns == null && one.Arguments != null);

@@ -5562,14 +5590,43 @@ namespace Microsoft.Dafny
       for (int i = 0; i < one.Arguments.Count; i++) {

         BoundVar bv1 = one.Arguments[i];

         BoundVar bv2 = other.Arguments[i];

-        if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2) &&

-            !bv1.Name.Equals(bv2.Name)) {

-          return false;

+        if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2)) {

+          if (!bv1.Name.Equals(bv2.Name)) {

+            // need to substitute bv2 with bv1 in the matchstmt body

+            // what if match body already has the bv?? need to make a new bv

+            Type type = new InferredTypeProxy();

+            string name = FreshTempVarName("_mc#", codeContext);

+            BoundVar bv = new BoundVar(one.tok, name, type);

+            SubstituteMatchCaseBoundVar(one, bv1, bv);

+            SubstituteMatchCaseBoundVar(other, bv2, bv);

+          }

         }

       }

       return true;

     }

 

+    void SubstituteMatchCaseBoundVar(MatchCaseStmt mc, BoundVar oldBv, BoundVar newBv) {

+      List<BoundVar> arguments = new List<BoundVar>();

+      for (int i = 0; i < mc.Arguments.Count; i++) {

+        BoundVar bv = mc.Arguments[i];

+        if (bv == oldBv) {

+          arguments.Add(newBv);

+        } else {

+          arguments.Add(bv);

+        }

+      }

+      mc.Arguments = arguments;

+

+      // substitue the oldBv with newBv in the body

+      MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(oldBv, newBv);

+      List<Statement> list = new List<Statement>();

+      foreach (Statement ss in mc.Body) {

+        Statement clone = cloner.CloneStmt(ss);

+        list.Add(clone);

+      }

+      mc.UpdateBody(list);

+    }

+

     void FillInDefaultLoopDecreases(LoopStmt loopStmt, Expression guard, List<Expression> theDecreases, ICallable enclosingMethod) {

       Contract.Requires(loopStmt != null);

       Contract.Requires(theDecreases != null);

@@ -7653,7 +7710,9 @@ namespace Microsoft.Dafny
       string name = FreshTempVarName("_mc#", opts.codeContext);

       BoundVar bv = new BoundVar(me.tok, name, type);

       List<CasePattern> patternSubst = new List<CasePattern>();

-      DesugarMatchCaseExpr(me, dtd, bv, patternSubst);

+      if (dtd != null) {

+        DesugarMatchCaseExpr(me, dtd, bv, patternSubst, opts.codeContext);

+      }

 

       ISet<string> memberNamesUsed = new HashSet<string>();

       expr.Type = new InferredTypeProxy();

@@ -7678,20 +7737,20 @@ namespace Microsoft.Dafny
         }

         scope.PushMarker();

         int i = 0;

-        foreach (BoundVar v in mc.Arguments) {

-          if (!scope.Push(v.Name, v)) {

-            Error(v, "Duplicate parameter name: {0}", v.Name);

-          }

-          ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

-          if (ctor != null && i < ctor.Formals.Count) {

-            Formal formal = ctor.Formals[i];

-            Type st = SubstType(formal.Type, subst);

-            if (!UnifyTypes(v.Type, st)) {

-              Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);

+        if (mc.Arguments != null) {

+          foreach (BoundVar v in mc.Arguments) {

+            scope.Push(v.Name, v);

+            ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);

+            if (ctor != null && i < ctor.Formals.Count) {

+              Formal formal = ctor.Formals[i];

+              Type st = SubstType(formal.Type, subst);

+              if (!UnifyTypes(v.Type, st)) {

+                Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);

+              }

+              v.IsGhost = formal.IsGhost;

             }

-            v.IsGhost = formal.IsGhost;

+            i++;

           }

-          i++;

         }

         ResolveExpression(mc.Body, opts);

         // substitute body to replace the case pat with v. This needs to happen

@@ -7742,29 +7801,34 @@ namespace Microsoft.Dafny
       // (x, y) is treated as a 2-tuple constructor

       if (me.Source is DatatypeValue) {

         var e = (DatatypeValue)me.Source;

-        Contract.Assert(e.Arguments.Count >= 1);

-        Expression source = e.Arguments[0];

-        List<MatchCaseExpr> cases = new List<MatchCaseExpr>();

-        foreach (MatchCaseExpr mc in me.Cases) {

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

-          Contract.Assert(mc.CasePatterns.Count == e.Arguments.Count);

-          CasePattern cp = mc.CasePatterns[0];

-          List<CasePattern> patterns;

-          if (cp.Arguments != null) {

-            patterns = cp.Arguments;

-          } else {

-            patterns = new List<CasePattern>();

-          }

+        if (e.Arguments.Count < 1) {

+          Error(me.tok, "match source tuple needs at least 1 argument");

+        } else {

+          Expression source = e.Arguments[0];

+          List<MatchCaseExpr> cases = new List<MatchCaseExpr>();

+          foreach (MatchCaseExpr mc in me.Cases) {

+            if (mc.CasePatterns == null || mc.CasePatterns.Count != e.Arguments.Count) {

+              Error(mc.tok, "case arguments count does not match source arguments count");

+            } else {

+              CasePattern cp = mc.CasePatterns[0];

+              List<CasePattern> patterns;

+              if (cp.Arguments != null) {

+                patterns = cp.Arguments;

+              } else {

+                patterns = new List<CasePattern>();

+              }

 

-          Expression body = mc.Body;

-          for (int i = e.Arguments.Count; 1 <= --i; ) {

-            // others go into the body

-            body = CreateMatchCaseExprBody(mc.tok, e.Arguments[i], mc.CasePatterns[i], body);

+              Expression body = mc.Body;

+              for (int i = e.Arguments.Count; 1 <= --i; ) {

+                // others go into the body

+                body = CreateMatchCaseExprBody(me.tok, e.Arguments[i], mc.CasePatterns[i], body);

+              }

+              cases.Add(new MatchCaseExpr(cp.tok, cp.Id, patterns, body));

+            }

           }

-          cases.Add(new MatchCaseExpr(cp.tok, cp.Id, patterns, body));

+          me.UpdateSource(source);

+          me.UpdateCases(cases);

         }

-        me.UpdateSource(source);

-        me.UpdateCases(cases);

       }

     }

 

@@ -7796,9 +7860,14 @@ namespace Microsoft.Dafny
      *       case Nil => y

      *       case Cons(z, zs) => last(ys)

      * */

-    void DesugarMatchCaseExpr(MatchExpr me, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns) {

+    void DesugarMatchCaseExpr(MatchExpr me, DatatypeDecl dtd, BoundVar sourceVar, List<CasePattern> patterns, ICodeContext codeContext) {

       Contract.Assert(dtd != null);

       Dictionary<string, DatatypeCtor> ctors = datatypeCtors[dtd];

+      if (ctors == null) {

+        // no constructors, there is no need to desugar

+        return;

+      }

+

       foreach (MatchCaseExpr mc in me.Cases) {

         if (mc.Arguments != null) {

           // already desugared. This happens during the second pass resolver after cloning.

@@ -7808,47 +7877,30 @@ namespace Microsoft.Dafny
 

         Contract.Assert(mc.Arguments == null);

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

+        Contract.Assert(ctors != null);

         DatatypeCtor ctor = null;

-        if (ctors != null) {

-          if (!ctors.TryGetValue(mc.Id, out ctor)) {

-            Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);

-          } else {

-            Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

-            mc.Ctor = ctor;

-            if (ctor.Formals.Count != mc.CasePatterns.Count) {

-              Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.CasePatterns.Count, ctor.Formals.Count);

-            }

-          }

-        }

-        scope.PushMarker();

-        List<BoundVar> arguments = new List<BoundVar>();

-        foreach (CasePattern pat in mc.CasePatterns) {

-          // Find the constructor in the given datatype

-          // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible

-          ctor = null;

-          if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy && dtd != null)) {

-            if (datatypeCtors[dtd].TryGetValue(pat.Id, out ctor)) {

-              pat.Ctor = ctor;

-              pat.Var = null;

-            }

-          }

-          if (pat.Var != null) {

-            BoundVar v = pat.Var;

-            arguments.Add(v);

-            if (!scope.Push(v.Name, v)) {

-              Error(v, "Duplicate name: {0}", v.Name);

+        if (ctors.TryGetValue(mc.Id, out ctor)) {

+          scope.PushMarker();

+          foreach (CasePattern pat in mc.CasePatterns) {

+            FindDuplicateIdentifier(pat, ctors, true);

+          }

+          List<BoundVar> arguments = new List<BoundVar>();

+          foreach (CasePattern pat in mc.CasePatterns) {

+            if (pat.Var != null) {

+              BoundVar v = pat.Var;

+              arguments.Add(v);

+            } else {

+              DesugarMatchCasePattern(mc, pat, sourceVar);

+              patterns.Add(pat);

+              arguments.Add(sourceVar);

             }

-          } else {

-            DesugarMatchCasePattern(mc, pat, sourceVar);

-            patterns.Add(pat);

-            arguments.Add(sourceVar);

           }

+          mc.Arguments = arguments;

+          mc.CasePatterns = null;

+          scope.PopMarker();

         }

-

-        mc.Arguments = arguments;

-        mc.CasePatterns = null;

-        scope.PopMarker();

       }

+      

 

       List<MatchCaseExpr> newCases = new List<MatchCaseExpr>();

       

@@ -7872,13 +7924,13 @@ namespace Microsoft.Dafny
         if (CaseExprHasWildCard(mc)) {

           mcWithWildCard.Add(mc);

         } else {

-          thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap);

+          thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap, codeContext);

         }

       }

 

       foreach (MatchCaseExpr mc in mcWithWildCard) {

         // now process with cases with wildcard

-        thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap);

+        thingsChanged |= CombineMatchCaseExpr(mc, newCases, caseMap, codeContext);

       }      

 

       if (thingsChanged) {

@@ -7902,24 +7954,24 @@ namespace Microsoft.Dafny
 

 

     bool CaseExprHasWildCard(MatchCase mc) {

-      foreach (BoundVar bv in mc.Arguments) {

-        if (LocalVariable.HasWildcardName(bv)) {

-          return true;

+      if (mc.Arguments != null) {

+        foreach (BoundVar bv in mc.Arguments) {

+          if (LocalVariable.HasWildcardName(bv)) {

+            return true;

+          }

         }

       }

       return false;

     }

 

-    bool CombineMatchCaseExpr(MatchCaseExpr mc, List<MatchCaseExpr> newCases, Dictionary<string, MatchCaseExpr> caseMap) {

+    bool CombineMatchCaseExpr(MatchCaseExpr mc, List<MatchCaseExpr> newCases, Dictionary<string, MatchCaseExpr> caseMap, ICodeContext codeContext) {

       bool thingsChanged = false;

       MatchCaseExpr old_mc;

       if (caseMap.TryGetValue(mc.Id, out old_mc)) {

         // already has a case with the same ctor, try to consolidate the body.

-        Expression oldBody = old_mc.Body;

-        Expression body = mc.Body;

-        if (SameMatchCase(old_mc, mc)) {

-          MatchExpr old = (MatchExpr)oldBody;

-          MatchExpr current = (MatchExpr)body;

+        if (SameMatchCaseExpr(old_mc, mc, codeContext)) {

+          MatchExpr old = (MatchExpr)old_mc.Body;

+          MatchExpr current = (MatchExpr)mc.Body;

           foreach (MatchCaseExpr c in current.Cases) {

             old.Cases.Add(c);

           }

@@ -7935,7 +7987,7 @@ namespace Microsoft.Dafny
       return thingsChanged;

     }

 

-    bool SameMatchCase(MatchCaseExpr one, MatchCaseExpr other) {

+    bool SameMatchCaseExpr(MatchCaseExpr one, MatchCaseExpr other, ICodeContext codeContext) {

       // this method is called after all the CasePattern in the match cases are converted

       // into BoundVars.

       Contract.Assert(one.CasePatterns == null && one.Arguments != null);

@@ -7960,14 +8012,39 @@ namespace Microsoft.Dafny
       for (int i = 0; i < one.Arguments.Count; i++) {

         BoundVar bv1 = one.Arguments[i];

         BoundVar bv2 = other.Arguments[i];

-        if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2) &&

-            !bv1.Name.Equals(bv2.Name)) {

-          return false;

+        if (!LocalVariable.HasWildcardName(bv1) && !LocalVariable.HasWildcardName(bv2)) {

+          if (!bv1.Name.Equals(bv2.Name)) {

+            // need to substitute bv2 with bv1 in the matchstmt body

+            // what if match body already has the bv?? need to make a new bv

+            Type type = new InferredTypeProxy();

+            string name = FreshTempVarName("_mc#", codeContext);

+            BoundVar bv = new BoundVar(one.tok, name, type);

+            SubstituteMatchCaseBoundVar(one, bv1, bv);

+            SubstituteMatchCaseBoundVar(other, bv2, bv);

+          }

         }

       }

       return true;

     }

 

+    void SubstituteMatchCaseBoundVar(MatchCaseExpr mc, BoundVar oldBv, BoundVar newBv) {

+      List<BoundVar> arguments = new List<BoundVar>();

+      for (int i = 0; i < mc.Arguments.Count; i++) {

+        BoundVar bv = mc.Arguments[i];

+        if (bv == oldBv) {

+          arguments.Add(newBv);

+        } else {

+          arguments.Add(bv);

+        }

+      }

+      mc.Arguments = arguments;

+

+      // substitue the oldBv with newBv in the body

+      MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(oldBv, newBv);

+      Expression clone = cloner.CloneExpr(mc.Body);

+      mc.UpdateBody(clone);

+    }

+

     void ResolveCasePattern(CasePattern pat, Type sourceType, ICodeContext context) {

       Contract.Requires(pat != null);

       Contract.Requires(sourceType != null);

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4e66915d..1dd985cb 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -1122,15 +1122,44 @@ namespace Microsoft.Dafny
   class MatchCaseExprSubstituteCloner : Cloner

   {

     private List<CasePattern> patternSubst;

+    private BoundVar oldvar;

     private BoundVar var;

 

     // the cloner is called after resolving the body of matchexpr, trying

     // to replace casepattern in the body that has been replaced by bv

     public MatchCaseExprSubstituteCloner(List<CasePattern> subst, BoundVar var) {

       this.patternSubst = subst;

+      this.oldvar = null;

       this.var = var;

     }

 

+    public MatchCaseExprSubstituteCloner(BoundVar oldvar, BoundVar var) {

+      this.patternSubst = null;

+      this.oldvar = oldvar;

+      this.var = var;

+    }

+

+    public override BoundVar CloneBoundVar(BoundVar bv) {

+      // replace bv with this.var is bv == oldvar

+      BoundVar bvNew;

+      if (oldvar != null && bv.Name.Equals(oldvar.Name)) {

+        bvNew = new BoundVar(Tok(bv.tok), oldvar.Name, CloneType(bv.Type));

+      } else {

+        bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));

+      }

+      bvNew.IsGhost = bv.IsGhost;

+      return bvNew;

+    }

+

+    public override NameSegment CloneNameSegment(Expression expr) {

+      var e = (NameSegment)expr;

+      if (oldvar != null && e.Name.Equals(oldvar.Name)) {

+        return new NameSegment(Tok(e.tok), var.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));

+      } else {

+        return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));

+      }

+    }

+

     public override Expression CloneApplySuffix(ApplySuffix e) {

       // if the ApplySuffix matches the CasePattern, then replace it with the BoundVar.

       if (FindMatchingPattern(e)) {

@@ -1141,6 +1170,9 @@ namespace Microsoft.Dafny
     }

 

     private bool FindMatchingPattern(ApplySuffix e) {

+      if (patternSubst == null) {

+        return false;

+      }

       Expression lhs = e.Lhs;

       if (!(lhs is NameSegment)) {

         return false;

@@ -1160,6 +1192,8 @@ namespace Microsoft.Dafny
             if (bv1 != arg2.Var) {

               found = false;

             }

+          } else {

+            found = false;

           }

         }

         if (found) {

diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy
new file mode 100644
index 00000000..ef597936
--- /dev/null
+++ b/Test/dafny0/NestedPatterns.dfy
@@ -0,0 +1,124 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype List<T> = Nil | Cons(head: T, tail: List<T>)

+    

+method MethodA<T>(xs: List<T>) returns (ys: List<T>)

+{

+  match xs

+  case Nil =>

+    ys := Nil;

+  case Cons(h, Nil) =>

+    ys := Nil;

+  case Cons(h, Cons(h', tt)) => 

+    ys := tt;

+}

+    

+method MethodB<T>(xs: List<T>)

+{

+  match xs

+  case Nil =>

+  case Cons(h, Nil) =>

+    var x := 12;

+    var xxs := Cons(Nil, Nil);

+  case Cons(h, Cons(h', tt)) => 

+}

+    

+method MethodC<T>(xs: List<T>) returns (ys: List<T>)

+  requires xs.Cons? ==> !xs.tail.Cons?;

+{

+  match xs

+  case Nil =>

+    ys := Nil;

+  case Cons(h, Nil) =>

+    ys := Nil;

+}

+

+method MethodD<T>(xs: List<T>) returns (ys: List<T>)

+{

+  match xs

+  case Nil =>

+    ys := Nil;

+  case Cons(h, Nil) =>

+    var xxs: List<List<T>> := Cons(Nil, Nil);  // BUG: type inference is not doing the right thing on this lint

+  case Cons(h, Cons(h0, tt)) => 

+}

+

+method MethodE<T>(xs: List<T>) returns (ys: List<T>)

+{

+  var xxs: List<List<T>> := Cons(Nil, Nil);  // here it works! (but the same line in MethodD does not work)

+}

+

+method MethodF<T>(xs: List<T>) returns (ys: List<T>)

+  requires xs.Cons? ==> !xs.tail.Cons?;

+{

+  match xs

+  case Nil =>

+  case Cons(h, Nil) =>

+  case Cons(h0, Cons(h1, tt)) =>  // BUG: Dafny complains that Cons appears in more than one case; it seems to be due to the

+                                  // fact that the previous case uses identifier "h" as the first argument to Cons, whereas this

+                                  // line uses "h0"

+}

+

+method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>)

+{

+  match xs

+  case Nil =>

+    xxs := Cons(Nil, Nil);  // BUG: this causes there to be an "unresolved identifier: _mc#0" error; oddly enough, the error goes away if the third case is commented out

+  case Cons(h, t) =>

+  case Cons(h, Cons(ht, tt)) => 

+}

+

+method AssertionFailure(xs: List<T>)

+{

+  match xs

+  case (Nil) =>  // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)

+  case (Cons(h, t)) =>  // BUG: ditto

+}

+

+method DuplicateIdentifierInPattern0<T>(xs: List<T>)

+{

+  match xs

+  case Nil =>

+  case Cons(h, Nil) =>

+  case Cons(h, Cons(_, h)) =>  // BUG:  this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported

+}

+

+method DuplicateIdentifierInPattern1<T>(xs: List<T>)

+{

+  match xs

+  case Nil =>

+  case Cons(h, Nil) =>

+  case Cons(h, Cons(h, _)) =>  // BUG:  this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported

+}

+

+method DuplicateIdentifierInPattern2<T>(xs: List<T>)

+{

+  match xs

+  case Nil =>

+  case Cons(h, Nil) =>

+  case Cons(h, Cons(e, e)) =>  // BUG:  here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal

+}

+

+method Tuples0(xs: List<T>, ys: List<T>)

+{

+  match (xs, ys)

+  case (Nil, Nil) =>

+  case (Cons(a, b), Nil) =>

+  case (Nil, Cons(x, y)) =>

+  case (Cons(a, b), Cons(x, y)) =>  // BUG: here and in some other places above, not all identifiers are highlighted in the Dafny IDE; it looks like

+                                    // only the identifiers in the last constructors are

+}

+

+method Tuples1(xs: List<T>, ys: List<T>)

+{

+  match (xs, ys, 4)

+  case (Nil, Nil) =>  // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an

+                      // assertion failure "mc.CasePatterns.Count == e.Arguments.Count"

+}

+

+method Tuples2(xs: List<T>, ys: List<T>)

+{

+  match (xs, ys, ())

+  case (Nil, Nil, ()) =>  // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"

+}

diff --git a/Test/dafny0/NestedPatterns.dfy.expect b/Test/dafny0/NestedPatterns.dfy.expect
new file mode 100644
index 00000000..d83a7da1
--- /dev/null
+++ b/Test/dafny0/NestedPatterns.dfy.expect
@@ -0,0 +1,9 @@
+NestedPatterns.dfy(69,2): Error: member Cons appears in more than one case

+NestedPatterns.dfy(75,2): Error: member  does not exist in datatype List

+NestedPatterns.dfy(76,2): Error: member  does not exist in datatype List

+NestedPatterns.dfy(84,23): Error: Duplicate parameter name: h

+NestedPatterns.dfy(92,20): Error: Duplicate parameter name: h

+NestedPatterns.dfy(100,23): Error: Duplicate parameter name: e

+NestedPatterns.dfy(116,2): Error: case arguments count does not match source arguments count

+NestedPatterns.dfy(122,2): Error: match source tuple needs at least 1 argument

+8 resolution/type errors detected in NestedPatterns.dfy