Fix identifiers in nested match patterns not showing in the IDE bug. Remember

BoundVars that are combined in rewriting of the nested match patterns so they
show up in the IDE correctly.

1 files changed, 40 insertions, 6 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 1dd985cb..9eb6bac2 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using Bpl = Microsoft.Boogie;

+using IToken = Microsoft.Boogie.IToken;

 

 namespace Microsoft.Dafny

 {

@@ -1140,10 +1141,10 @@ namespace Microsoft.Dafny
     }

 

     public override BoundVar CloneBoundVar(BoundVar bv) {

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

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

       BoundVar bvNew;

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

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

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

       } else {

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

       }

@@ -1154,7 +1155,7 @@ namespace Microsoft.Dafny
     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));

+        return new NameSegment(new AutoGeneratedToken(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));

       }

@@ -1162,14 +1163,22 @@ namespace Microsoft.Dafny
 

     public override Expression CloneApplySuffix(ApplySuffix e) {

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

-      if (FindMatchingPattern(e)) {

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

+      CasePattern cp = null;

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

+        if (this.var.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);

+          }

+        }

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

       } else {

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

       }

     }

 

-    private bool FindMatchingPattern(ApplySuffix e) {

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

+      pattern = null;

       if (patternSubst == null) {

         return false;

       }

@@ -1197,12 +1206,37 @@ namespace Microsoft.Dafny
           }

         }

         if (found) {

+          pattern = cp;

           return true;

         }

       }

       return false;

     }

   }

+

+  // MatchCaseToken is used to record BoundVars that are consolidated due to rewrite of

+  // nested match patterns. We want to record the original BoundVars that are consolidated

+  // so that they will show up in the IDE correctly.

+  public class MatchCaseToken : AutoGeneratedToken

+  {

+    public readonly List<Tuple<IToken, BoundVar, bool>> varList;

+    public MatchCaseToken(IToken tok)

+      : base(tok) {

+      varList = new List<Tuple<IToken, BoundVar, bool>>();

+    }

+

+    public void AddVar(IToken tok, BoundVar var, bool isDefinition) {

+      varList.Add(new Tuple<IToken, BoundVar, bool>(tok, var, isDefinition));

+    }

+  }

+

+  // A cloner that replace the original token with AutoGeneratedToken.

+  class AutoGeneratedTokenCloner : Cloner

+  {

+    public override IToken Tok(IToken tok) {

+      return new AutoGeneratedToken(tok);

+    }

+  }

 }