Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when

trying to substitute the nested CasePattern with the BoundVar.

4 files changed, 49 insertions, 26 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index eff7d97d..52845c3f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5950,13 +5950,9 @@ namespace Microsoft.Dafny
       }

 

       // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.

-      Type type = new InferredTypeProxy();

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

-      MatchCaseToken mcToken = new MatchCaseToken(s.Tok);

-      BoundVar bv = new BoundVar(mcToken, name, type);

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

+      List<Tuple<CasePattern, BoundVar>> patternSubst = new List<Tuple<CasePattern, BoundVar>>(); 

       if (dtd != null) {

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

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

       }

 

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

@@ -6008,7 +6004,7 @@ namespace Microsoft.Dafny
         // substitute body to replace the case pat with v. This needs to happen

         // after the body is resolved so we can scope the bv correctly.

         if (patternSubst.Count > 0) {

-          MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv);

+          MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst);

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

           foreach (Statement ss in mc.Body) {

             Statement clone = cloner.CloneStmt(ss);

@@ -6125,7 +6121,7 @@ namespace Microsoft.Dafny
      *       case Nil => y

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

      */

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

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

       Contract.Assert(dtd != null);

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

       if (ctors == null) {

@@ -6133,6 +6129,8 @@ namespace Microsoft.Dafny
         return;

       }

 

+      Type type = new InferredTypeProxy();

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

       foreach (MatchCaseStmt mc in s.Cases) {

         if (mc.Arguments != null) {

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

@@ -6140,6 +6138,7 @@ namespace Microsoft.Dafny
           return;

         }

 

+        BoundVar sourceVar = new BoundVar(new MatchCaseToken(s.Tok), name, type);

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

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

         Contract.Assert(ctors != null);

@@ -6157,7 +6156,7 @@ namespace Microsoft.Dafny
               arguments.Add(v);

             } else {

               DesugarMatchCasePattern(mc, pat, sourceVar);

-              patterns.Add(pat);

+              patterns.Add(new Tuple<CasePattern, BoundVar>(pat, sourceVar));

               arguments.Add(sourceVar);

             }

           }

@@ -8249,12 +8248,9 @@ namespace Microsoft.Dafny
       }

 

       // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.

-      Type type = new InferredTypeProxy();

-      string name = FreshTempVarName("_mc#", opts.codeContext);

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

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

+      List<Tuple<CasePattern, BoundVar>> patternSubst = new List<Tuple<CasePattern, BoundVar>>(); 

       if (dtd != null) {

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

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

       }

 

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

@@ -8306,7 +8302,7 @@ namespace Microsoft.Dafny
         // substitute body to replace the case pat with v. This needs to happen

         // after the body is resolved so we can scope the bv correctly.

         if (patternSubst.Count > 0) {

-          MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv);

+          MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst);

           mc.UpdateBody(cloner.CloneExpr(mc.Body));

           // resolve it again since we just cloned it.

           ResolveExpression(mc.Body, opts);

@@ -8408,7 +8404,7 @@ namespace Microsoft.Dafny
      *       case Nil => y

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

      * */

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

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

       Contract.Assert(dtd != null);

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

       if (ctors == null) {

@@ -8416,6 +8412,8 @@ namespace Microsoft.Dafny
         return;

       }

 

+      Type type = new InferredTypeProxy();

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

       foreach (MatchCaseExpr mc in me.Cases) {

         if (mc.Arguments != null) {

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

@@ -8423,6 +8421,7 @@ namespace Microsoft.Dafny
           return;

         }

 

+        BoundVar sourceVar = new BoundVar(new MatchCaseToken(me.tok), name, type);

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

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

         Contract.Assert(ctors != null);

@@ -8439,7 +8438,7 @@ namespace Microsoft.Dafny
               arguments.Add(v);

             } else {

               DesugarMatchCasePattern(mc, pat, sourceVar);

-              patterns.Add(pat);

+              patterns.Add(new Tuple<CasePattern, BoundVar>(pat, sourceVar));

               arguments.Add(sourceVar);

             }

           }

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 9a898cbe..13b16066 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -1429,16 +1429,16 @@ namespace Microsoft.Dafny
 

   class MatchCaseExprSubstituteCloner : Cloner

   {

-    private List<CasePattern> patternSubst;

+    private List<Tuple<CasePattern, BoundVar>> 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) {

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

       this.patternSubst = subst;

       this.oldvar = null;

-      this.var = var;

+      this.var = null;

     }

 

     public MatchCaseExprSubstituteCloner(BoundVar oldvar, BoundVar var) {

@@ -1471,21 +1471,23 @@ namespace Microsoft.Dafny
     public override Expression CloneApplySuffix(ApplySuffix e) {

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

       CasePattern cp = null;

-      if (FindMatchingPattern(e, out cp)) {

-        if (this.var.tok is MatchCaseToken) {

+      BoundVar bv = null;

+      if (FindMatchingPattern(e, out cp, out bv)) {

+        if (bv.tok is MatchCaseToken) {

           Contract.Assert(e.Args.Count == cp.Arguments.Count);

           for (int i = 0; i < e.Args.Count; i++) {

-            ((MatchCaseToken)this.var.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false);

+            ((MatchCaseToken)bv.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false);

           }

         }

-        return new NameSegment(new AutoGeneratedToken(e.tok), this.var.Name, null);

+        return new NameSegment(new AutoGeneratedToken(e.tok), bv.Name, null);

       } else {

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

       }

     }

 

-    private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern) {

+    private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern, out BoundVar bv) {

       pattern = null;

+      bv = null;

       if (patternSubst == null) {

         return false;

       }

@@ -1494,7 +1496,8 @@ namespace Microsoft.Dafny
         return false;

       }

       string applyName = ((NameSegment)lhs).Name;

-      foreach (CasePattern cp in patternSubst) {

+      foreach (Tuple<CasePattern, BoundVar> pair in patternSubst) {

+        CasePattern cp = pair.Item1;

         string ctorName = cp.Id;

         if (!(applyName.Equals(ctorName)) || (e.Args.Count != cp.Arguments.Count)) {

           continue;

@@ -1514,6 +1517,7 @@ namespace Microsoft.Dafny
         }

         if (found) {

           pattern = cp;

+          bv = pair.Item2;

           return true;

         }

       }

diff --git a/Test/dafny4/Bug111.dfy b/Test/dafny4/Bug111.dfy
new file mode 100644
index 00000000..730d44d3
--- /dev/null
+++ b/Test/dafny4/Bug111.dfy
@@ -0,0 +1,18 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

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

+

+datatype A = A(i:int)

+datatype B = B1(a1:A) | B2(a2:A)

+

+function f(b:B):int

+{

+  match b

+  {

+    case B1(A(i)) => i

+    case B2(A(j)) => j

+  }

+}

+

+

+

+

diff --git a/Test/dafny4/Bug111.dfy.expect b/Test/dafny4/Bug111.dfy.expect
new file mode 100644
index 00000000..c0c48e2b
--- /dev/null
+++ b/Test/dafny4/Bug111.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 1 verified, 0 errors