Added {:auto_generated} trigger, which indicates that a declaration was not explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.

2 files changed, 7 insertions, 6 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 962b07b9..4e66915d 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -496,6 +496,7 @@ namespace Microsoft.Dafny
 

             // Annotate the new function so we remember that we introduced it

             fWithBody.Attributes = new Attributes("opaque_full", new List<Expression>(), fWithBody.Attributes);

+            fWithBody.Attributes = new Attributes("auto_generated", new List<Expression>(), fWithBody.Attributes);

 

             // Create a lemma to allow the user to selectively reveal the function's body          

             // That is, given:

@@ -505,7 +506,7 @@ namespace Microsoft.Dafny
             //     ensures foo(x, y) < 10;

             //   { x + y }

             // We produce:

-            //   lemma {:axiom} reveal_foo()

+            //   lemma {:axiom} {:auto_generated} reveal_foo()

             //     ensures forall x:int, y:int {:trigger foo(x,y)} :: 0 <= x < 5 && 0 <= y < 5 ==> foo(x,y) == foo_FULL(x,y);

             Expression reqExpr = new LiteralExpr(f.tok, true);

             foreach (Expression req in f.Req) {

@@ -518,10 +519,7 @@ namespace Microsoft.Dafny
               typeVars.Add(cloner.CloneTypeParam(tp));

             }

 

-            List<BoundVar> boundVars = new List<BoundVar>();

-            foreach (Formal formal in f.Formals) {

-              boundVars.Add(new BoundVar(f.tok, formal.Name, cloner.CloneType(formal.Type)));

-            }

+            var boundVars = f.Formals.ConvertAll(formal => new BoundVar(formal.tok, formal.Name, cloner.CloneType(formal.Type)));

 

             // Build the implication connecting the function's requires to the connection with the revealed-body version

             Func<Function, Expression> func_builder = func =>

@@ -552,6 +550,7 @@ namespace Microsoft.Dafny
 

             // Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body

             Attributes lemma_attrs = new Attributes("axiom", new List<Expression>(), null);

+            lemma_attrs = new Attributes("auto_generated", new List<Expression>(), lemma_attrs);

 

             var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),

                                     new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 3bb8f01c..086ac8e4 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -179,7 +179,9 @@ namespace DafnyLanguage
           } else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             foreach (var member in cl.Members) {

-              if (member is Function) {

+              if (Attributes.Contains(member.Attributes, "auto_generated")) {

+                // do nothing

+              } else  if (member is Function) {

                 var f = (Function)member;

                 foreach (var p in f.Formals) {

                   IdRegion.Add(newRegions, p.tok, p, true, module);