Merge my autoTriggers work into the master branch

This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.

1 files changed, 40 insertions, 6 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 480b3f61..d6f54aa7 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

 {

@@ -1169,10 +1170,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));

       }

@@ -1183,7 +1184,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));

       }

@@ -1191,14 +1192,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;

       }

@@ -1226,12 +1235,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);

+    }

+  }

 }