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.

3 files changed, 147 insertions, 19 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index ecb76ae8..835871d9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5244,7 +5244,8 @@ namespace Microsoft.Dafny
       // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.

       Type type = new InferredTypeProxy();

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

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

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

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

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

       if (dtd != null) {

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

@@ -5283,6 +5284,14 @@ namespace Microsoft.Dafny
                 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;

+

+              // update the type of the boundvars in the MatchCaseToken

+              if (v.tok is MatchCaseToken) {

+                MatchCaseToken mt = (MatchCaseToken)v.tok;

+                foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {

+                  UnifyTypes(entry.Item2.Type, v.Type);

+                }

+              }

             }

             i++;

           }

@@ -5331,11 +5340,11 @@ namespace Microsoft.Dafny
      *    case (Suc(a), Suc(b)) => minus(a, b)

      * To:  

      *  match x

-     *    case Zero => match y

+     *    case Zero => match y (originalToken)

      *        case _ => zero

-     *    case Suc(_) => match y

+     *    case Suc(_) => match y (AutoGeneratedToken)

      *        case Zero => x

-     *    case Suc(a) => match y

+     *    case Suc(a) => match y (AutoGeneratedToken)

       *        case (b) => minus(a,b)

      */    

     void DesugarMatchStmtWithTupleExpression(MatchStmt me) {

@@ -5347,6 +5356,9 @@ namespace Microsoft.Dafny
         } else {

           Expression source = e.Arguments[0];

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

+          // only keep the token for the first appearance, use autogenerated for the rest, otherwise more than one hovertext

+          // will show up in the IDE.

+          bool keepOrigToken = true; 

           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");

@@ -5362,9 +5374,10 @@ namespace Microsoft.Dafny
               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);

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

               }

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

+              keepOrigToken = false;

             }

           }

           me.UpdateSource(source);

@@ -5373,7 +5386,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    List<Statement> CreateMatchCaseStmtBody(Boogie.IToken tok, Expression source, CasePattern cp, List<Statement> body) {

+    List<Statement> CreateMatchCaseStmtBody(Boogie.IToken tok, Expression source, CasePattern cp, List<Statement> body, bool keepToken) {

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

       List<CasePattern> patterns;

       if (cp.Var != null) {

@@ -5387,6 +5400,10 @@ namespace Microsoft.Dafny
         patterns = cp.Arguments;

       }

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

+      if (!keepToken) {

+        AutoGeneratedTokenCloner cloner = new AutoGeneratedTokenCloner();

+        source = cloner.CloneExpr(source);

+      }

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

       // endTok??

       list.Add(new MatchStmt(tok, tok, source, cases, false));

@@ -5522,7 +5539,7 @@ namespace Microsoft.Dafny
       //    case Cons(y, #mc#) => match #mc#

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

 

-      Expression source = new NameSegment(pat.tok, v.Name, null);

+      Expression source = new NameSegment(new AutoGeneratedToken(pat.tok), v.Name, null);

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

       cases.Add(new MatchCaseStmt(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));

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

@@ -5547,6 +5564,27 @@ namespace Microsoft.Dafny
             foreach (MatchCaseStmt c in current.Cases) {

               old.Cases.Add(c);

             }

+            // add the token from mc to old_mc so the identifiers will show correctly in the IDE

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

+            Contract.Assert(old_mc.Arguments.Count == mc.Arguments.Count);

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

+              var bv = old_mc.Arguments[i];

+              MatchCaseToken mcToken;

+              if (!(bv.tok is MatchCaseToken)) {

+                // create a MatchCaseToken

+                mcToken = new MatchCaseToken(bv.tok);

+                // clone the bv but with the MatchCaseToken

+                var bvNew = new BoundVar(mcToken, bv.Name, bv.Type);

+                bvNew.IsGhost = bv.IsGhost;

+                arguments.Add(bvNew);

+              } else {

+                mcToken = (MatchCaseToken)bv.tok;

+                arguments.Add(bv);

+              }

+              mcToken.AddVar(bv.tok, bv, true);

+              mcToken.AddVar(mc.Arguments[i].tok, mc.Arguments[i], true);

+            }

+            old_mc.Arguments = arguments;

             thingsChanged = true;

           }

         } else {

@@ -5596,7 +5634,9 @@ namespace Microsoft.Dafny
             // 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);

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

+            ((MatchCaseToken)bv.tok).AddVar(bv1.tok, bv1, true);

+            ((MatchCaseToken)bv.tok).AddVar(bv2.tok, bv2, true);

             SubstituteMatchCaseBoundVar(one, bv1, bv);

             SubstituteMatchCaseBoundVar(other, bv2, bv);

           }

@@ -7708,7 +7748,7 @@ 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(me.tok, name, type);

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

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

       if (dtd != null) {

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

@@ -7748,6 +7788,14 @@ namespace Microsoft.Dafny
                 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;

+

+              // update the type of the boundvars in the MatchCaseToken

+              if (v.tok is MatchCaseToken) {

+                MatchCaseToken mt = (MatchCaseToken)v.tok;

+                foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {

+                  UnifyTypes(entry.Item2.Type, v.Type);

+                }

+              }

             }

             i++;

           }

@@ -7945,7 +7993,7 @@ namespace Microsoft.Dafny
       //    case Cons(y, #mc#) => match #mc#

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

 

-      Expression source = new NameSegment(pat.tok, v.Name, null);

+      Expression source = new NameSegment(new AutoGeneratedToken(pat.tok), v.Name, null);

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

       cases.Add(new MatchCaseExpr(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));

       MatchExpr e = new MatchExpr(pat.tok, source, cases, false);

@@ -7975,6 +8023,27 @@ namespace Microsoft.Dafny
           foreach (MatchCaseExpr c in current.Cases) {

             old.Cases.Add(c);

           }

+          // add the token from mc to old_mc so the identifiers will show correctly in the IDE

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

+          Contract.Assert(old_mc.Arguments.Count == mc.Arguments.Count);

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

+            var bv = old_mc.Arguments[i];

+            MatchCaseToken mcToken;

+            if (!(bv.tok is MatchCaseToken)) {

+              // create a MatchCaseToken

+              mcToken = new MatchCaseToken(bv.tok);

+              // clone the bv but with the MatchCaseToken

+              var bvNew = new BoundVar(mcToken, bv.Name, bv.Type);

+              bvNew.IsGhost = bv.IsGhost;

+              arguments.Add(bvNew);

+            } else {

+              mcToken = (MatchCaseToken)bv.tok;

+              arguments.Add(bv);

+            }

+            mcToken.AddVar(bv.tok, bv, true);

+            mcToken.AddVar(mc.Arguments[i].tok, mc.Arguments[i], true);

+          }

+          old_mc.Arguments = arguments;

           thingsChanged = true;

         } else {

           // duplicate cases, do nothing for now. The error will be reported during resolving

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

     }

 

+

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

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

       // into BoundVars.

@@ -8018,7 +8088,11 @@ namespace Microsoft.Dafny
             // 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);

+            MatchCaseToken mcToken = new MatchCaseToken(one.tok);

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

+            mcToken.AddVar(bv1.tok, bv1, true);

+            mcToken.AddVar(bv2.tok, bv2, true);

+            // substitute the appeareance of old bv with the new bv in the match case

             SubstituteMatchCaseBoundVar(one, bv1, bv);

             SubstituteMatchCaseBoundVar(other, bv2, bv);

           }

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);

+    }

+  }

 }

 

 

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 086ac8e4..262dddcd 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -270,7 +270,17 @@ namespace DafnyLanguage
       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         foreach (var kase in e.Cases) {

-          kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));

+          kase.Arguments.ForEach(bv => {

+            IdRegion.Add(regions, bv.tok, bv, true, module);

+            // if the arguments is an encapsulation of different boundvars from nested match cases,

+            // add the boundvars so that they can show up in the IDE correctly

+            if (bv.tok is MatchCaseToken) {

+              MatchCaseToken mt = (MatchCaseToken)bv.tok;

+              foreach(Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {

+                IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);

+              }

+            }

+          });

         }

       } else if (expr is ChainingExpression) {

         var e = (ChainingExpression)expr;

@@ -313,7 +323,17 @@ namespace DafnyLanguage
       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         foreach (var kase in s.Cases) {

-          kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));

+          kase.Arguments.ForEach(bv => {

+            IdRegion.Add(regions, bv.tok, bv, true, module);

+            // if the arguments is an encapsulation of different boundvars from nested match cases,

+            // add the boundvars so that they can show up in the IDE correctly

+            if (bv.tok is MatchCaseToken) {

+              MatchCaseToken mt = (MatchCaseToken)bv.tok;

+              foreach (Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {

+                IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);

+              }

+            }              

+          });

         }

       } else if (stmt is LoopStmt) {

         var s = (LoopStmt)stmt;