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

trying to substitute the nested CasePattern with the BoundVar.

1 files changed, 13 insertions, 9 deletions

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;

         }

       }