Mark auto-generated expressions (in "decreases" clauses) and don't use these when figuring out hover text.

4 files changed, 46 insertions, 5 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 38b611d3..4a69e495 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -330,6 +330,11 @@ namespace Microsoft.Dafny
         var e = (ITEExpr)expr;

         return new ITEExpr(Tok(e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));

 

+      } else if (expr is AutoGeneratedExpression) {

+        var e = (AutoGeneratedExpression)expr;

+        var a = CloneExpr(e.E);

+        return new AutoGeneratedExpression(Tok(e.tok), a);

+

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

         return CloneExpr(e.E);  // skip the parentheses in the clone

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 98273d86..d605b860 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5559,6 +5559,34 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// An AutoGeneratedExpression is simply a wrapper around an expression.  This expression tells the generation of hover text (in the Dafny IDE)

+  /// that the expression was no supplied directly in the program text and should therefore be ignored.  In other places, an AutoGeneratedExpression

+  /// is just a parenthesized expression, which means that it works just the like expression .E that it contains.

+  /// (Ironically, AutoGeneratedExpression, which is like the antithesis of concrete syntax, inherits from ConcreteSyntaxExpression, which perhaps

+  /// should rather have been called SemanticsNeutralExpressionWrapper.)

+  /// </summary>

+  public class AutoGeneratedExpression : ParensExpression

+  {

+    public AutoGeneratedExpression(IToken tok, Expression e)

+      : base(tok, e) {

+      Contract.Requires(tok != null);

+      Contract.Requires(e != null);

+    }

+

+    /// <summary>

+    /// This maker method takes a resolved expression "e" and wraps a resolved AutoGeneratedExpression

+    /// around it.

+    /// </summary>

+    public static AutoGeneratedExpression Create(Expression e) {

+      Contract.Requires(e != null);

+      var a = new AutoGeneratedExpression(e.tok, e);

+      a.type = e.Type;

+      a.ResolvedExpression = e;

+      return a;

+    }

+  }

+

   public class ChainingExpression : ConcreteSyntaxExpression

   {

     public readonly List<Expression> Operands;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9799b742..d05c04d4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -409,7 +409,7 @@ namespace Microsoft.Dafny
           if (fn.Reads.Count != 0) {

             // start the default lexicographic tuple with the reads clause

             var r = FrameToObjectSet(fn.Reads);

-            decr.Add(r);

+            decr.Add(AutoGeneratedExpression.Create(r));

           }

         }

 

@@ -419,7 +419,7 @@ namespace Microsoft.Dafny
           if (!(p is ImplicitFormal) && p.Type.IsOrdered) {

             var ie = new IdentifierExpr(p.tok, p.Name);

             ie.Var = p; ie.Type = p.Type;  // resolve it here

-            decr.Add(ie);

+            decr.Add(AutoGeneratedExpression.Create(ie));

           }

         }

 

@@ -1280,6 +1280,11 @@ namespace Microsoft.Dafny
         var e = (ITEExpr)expr;

         return new ITEExpr(e.tok, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));

 

+      } else if (expr is AutoGeneratedExpression) {

+        var e = (AutoGeneratedExpression)expr;

+        var a = CloneExpr(e.E);

+        return new AutoGeneratedExpression(e.tok, a);

+

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

         return CloneExpr(e.E);  // skip the parentheses in the clone

@@ -4495,7 +4500,7 @@ namespace Microsoft.Dafny
               // Make the following guess:  if prefix then guess else -1

               guess = Expression.CreateITE(prefix, guess, Expression.CreateIntLiteral(prefix.tok, -1));

             }

-            theDecreases.Add(guess);

+            theDecreases.Add(AutoGeneratedExpression.Create(guess));

             break;  // ignore any further conjuncts

           }

           if (prefix == null) {

@@ -4510,7 +4515,7 @@ namespace Microsoft.Dafny
         var ie = new IdentifierExpr(loopStmt.Tok, iter.YieldCountVariable.Name);

         ie.Var = iter.YieldCountVariable;  // resolve here

         ie.Type = iter.YieldCountVariable.Type;  // resolve here

-        theDecreases.Insert(0, ie);

+        theDecreases.Insert(0, AutoGeneratedExpression.Create(ie));

         loopStmt.InferredDecreases = true;

       }

       if (loopStmt.InferredDecreases) {

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index d459d7eb..f2961d63 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -237,7 +237,10 @@ namespace DafnyLanguage
     static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {

       Contract.Requires(expr != null);

       Contract.Requires(regions != null);

-      if (expr is IdentifierExpr) {

+      if (expr is AutoGeneratedExpression) {

+        // do nothing

+        return;

+      } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

         IdRegion.Add(regions, e.tok, e.Var, false, module);

       } else if (expr is FieldSelectExpr) {