DafnyExtension: fixed more missing cases for hover texts

6 files changed, 100 insertions, 52 deletions

diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs
index 2f254135..b1b8828a 100644
--- a/Dafny/Cloner.cs
+++ b/Dafny/Cloner.cs
@@ -151,7 +151,7 @@ namespace Microsoft.Dafny
     }

 

     public FrameExpression CloneFrameExpr(FrameExpression frame) {

-      return new FrameExpression(CloneExpr(frame.E), frame.FieldName);

+      return new FrameExpression(Tok(frame.tok), CloneExpr(frame.E), frame.FieldName);

     }

     public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {

       if (aa.E != null) {

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index d8d95079..1629fe51 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -18,7 +18,7 @@ static ModuleDecl theModule;
 static BuiltIns theBuiltIns;

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

 static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);

-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

+static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

 static int anonymousIds = 0;

@@ -703,19 +703,24 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
    * any use of the function.  Nevertheless, as an experimental feature, the

    * language allows it (and it is sound).

    */

-  ( "*"                        (. fe = new FrameExpression(new WildcardExpr(t), null); .)

+  ( "*"                        (. fe = new FrameExpression(t, new WildcardExpr(t), null); .)

   | FrameExpression<out fe>

   )

   .

 FrameExpression<out FrameExpression/*!*/ fe>

-= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; fe = null; .)

- (( Expression<out e>

-    [ "`" Ident<out id>        (. fieldName = id.val; .)

+= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);

+     Expression/*!*/ e;

+     IToken/*!*/ id;

+     string fieldName = null;  IToken feTok = null;

+     fe = null;

+  .)

+ (( Expression<out e>          (. feTok = e.tok; .)

+    [ "`" Ident<out id>        (. fieldName = id.val;  feTok = id; .)

     ]

-                               (. fe = new FrameExpression(e, fieldName); .)

+                               (. fe = new FrameExpression(feTok, e, fieldName); .)

   ) |

   (  "`" Ident<out id>         (. fieldName = id.val; .)

-                               (. fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); .)

+                               (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .)

   ))

   .

 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index f342ecca..66ad49e9 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -2075,6 +2075,14 @@ namespace Microsoft.Dafny {
         AssumeToken = assumeToken;

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Expr;

+        foreach (var lhs in Lhss) {

+          yield return lhs;

+        }

+      }

+    }

   }

 

   public class UpdateStmt : ConcreteUpdateStatement

@@ -2401,6 +2409,23 @@ namespace Microsoft.Dafny {
       this.Decreases = decreases;

       this.Mod = mod;

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var mfe in Invariants) {

+          yield return mfe.E;

+        }

+        if (Decreases.Expressions != null) {

+          foreach (var e in Decreases.Expressions) {

+            yield return e;

+          }

+        }

+        if (Mod.Expressions != null) {

+          foreach (var fe in Mod.Expressions) {

+            yield return fe.E;

+          }

+        }

+      }

+    }

   }

 

   public class WhileStmt : LoopStmt

@@ -2432,6 +2457,9 @@ namespace Microsoft.Dafny {
         if (Guard != null) {

           yield return Guard;

         }

+        foreach (var e in base.SubExpressions) {

+          yield return e;

+        }

       }

     }

   }

@@ -2480,6 +2508,9 @@ namespace Microsoft.Dafny {
         foreach (var alt in Alternatives) {

           yield return alt.Guard;

         }

+        foreach (var e in base.SubExpressions) {

+          yield return e;

+        }

       }

     }

   }

@@ -3962,6 +3993,7 @@ namespace Microsoft.Dafny {
 

 

   public class FrameExpression {

+    public readonly IToken tok;

     public readonly Expression E;  // may be a WildcardExpr

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -3972,10 +4004,15 @@ namespace Microsoft.Dafny {
     public readonly string FieldName;

     public Field Field;  // filled in during resolution (but is null if FieldName is)

 

-    public FrameExpression(Expression e, string fieldName) {

+    /// <summary>

+    /// If a "fieldName" is given, then "tok" denotes its source location.  Otherwise, "tok"

+    /// denotes the source location of "e".

+    /// </summary>

+    public FrameExpression(IToken tok, Expression e, string fieldName) {

+      Contract.Requires(tok != null);

       Contract.Requires(e != null);

       Contract.Requires(!(e is WildcardExpr) || fieldName == null);

-

+      this.tok = tok;

       E = e;

       FieldName = fieldName;

     }

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index a81b256e..2f49f689 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -38,7 +38,7 @@ static ModuleDecl theModule;
 static BuiltIns theBuiltIns;

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

 static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);

-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

+static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

 static int anonymousIds = 0;

@@ -979,20 +979,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void FrameExpression(out FrameExpression/*!*/ fe) {

-		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; fe = null; 

+		Contract.Ensures(Contract.ValueAtReturn(out fe) != null);

+		Expression/*!*/ e;

+		IToken/*!*/ id;

+		string fieldName = null;  IToken feTok = null;

+		fe = null;

+		

 		if (StartOf(10)) {

 			Expression(out e);

+			feTok = e.tok; 

 			if (la.kind == 53) {

 				Get();

 				Ident(out id);

-				fieldName = id.val; 

+				fieldName = id.val;  feTok = id; 

 			}

-			fe = new FrameExpression(e, fieldName); 

+			fe = new FrameExpression(feTok, e, fieldName); 

 		} else if (la.kind == 53) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

-			fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); 

+			fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); 

 		} else SynErr(139);

 	}

 

@@ -1129,7 +1135,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

 		if (la.kind == 52) {

 			Get();

-			fe = new FrameExpression(new WildcardExpr(t), null); 

+			fe = new FrameExpression(t, new WildcardExpr(t), null); 

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

 		} else SynErr(147);

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index bf6dce17..c281aa4e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -742,13 +742,13 @@ namespace Microsoft.Dafny
       return new Specification<FrameExpression>(ee, null);

     }

     FrameExpression CloneFrameExpr(FrameExpression frame) {

-      return new FrameExpression(CloneExpr(frame.E), frame.FieldName);

+      return new FrameExpression(frame.tok, CloneExpr(frame.E), frame.FieldName);

     }

     MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {

       return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);

     }

     BoundVar CloneBoundVar(BoundVar bv) {

-      return new BoundVar((bv.tok), bv.Name, CloneType(bv.Type));

+      return new BoundVar(bv.tok, bv.Name, CloneType(bv.Type));

     }

     Expression CloneExpr(Expression expr) {

       if (expr == null) {

@@ -756,37 +756,37 @@ namespace Microsoft.Dafny
       } else if (expr is LiteralExpr) {

         var e = (LiteralExpr)expr;

         if (e.Value == null) {

-          return new LiteralExpr((e.tok));

+          return new LiteralExpr(e.tok);

         } else if (e.Value is bool) {

-          return new LiteralExpr((e.tok), (bool)e.Value);

+          return new LiteralExpr(e.tok, (bool)e.Value);

         } else {

-          return new LiteralExpr((e.tok), (BigInteger)e.Value);

+          return new LiteralExpr(e.tok, (BigInteger)e.Value);

         }

 

       } else if (expr is ThisExpr) {

         if (expr is ImplicitThisExpr) {

-          return new ImplicitThisExpr((expr.tok));

+          return new ImplicitThisExpr(expr.tok);

         } else {

-          return new ThisExpr((expr.tok));

+          return new ThisExpr(expr.tok);

         }

 

       } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-        return new IdentifierExpr((e.tok), e.Name);

+        return new IdentifierExpr(e.tok, e.Name);

 

       } else if (expr is DatatypeValue) {

         var e = (DatatypeValue)expr;

-        return new DatatypeValue((e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));

+        return new DatatypeValue(e.tok, e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));

 

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         if (expr is SetDisplayExpr) {

-          return new SetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));

+          return new SetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

         } else if (expr is MultiSetDisplayExpr) {

-          return new MultiSetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));

+          return new MultiSetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

         } else {

           Contract.Assert(expr is SeqDisplayExpr);

-          return new SeqDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));

+          return new SeqDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

         }

 

       } else if (expr is MapDisplayExpr) {

@@ -795,50 +795,50 @@ namespace Microsoft.Dafny
         foreach (ExpressionPair p in e.Elements) {

           pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));

         }

-        return new MapDisplayExpr((expr.tok), pp);

+        return new MapDisplayExpr(expr.tok, pp);

       } else if (expr is ExprDotName) {

         var e = (ExprDotName)expr;

-        return new ExprDotName((e.tok), CloneExpr(e.Obj), e.SuffixName);

+        return new ExprDotName(e.tok, CloneExpr(e.Obj), e.SuffixName);

 

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

-        return new FieldSelectExpr((e.tok), CloneExpr(e.Obj), e.FieldName);

+        return new FieldSelectExpr(e.tok, CloneExpr(e.Obj), e.FieldName);

 

       } else if (expr is SeqSelectExpr) {

         var e = (SeqSelectExpr)expr;

-        return new SeqSelectExpr((e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));

+        return new SeqSelectExpr(e.tok, e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));

 

       } else if (expr is MultiSelectExpr) {

         var e = (MultiSelectExpr)expr;

-        return new MultiSelectExpr((e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));

+        return new MultiSelectExpr(e.tok, CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));

 

       } else if (expr is SeqUpdateExpr) {

         var e = (SeqUpdateExpr)expr;

-        return new SeqUpdateExpr((e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));

+        return new SeqUpdateExpr(e.tok, CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));

 

       } else if (expr is FunctionCallExpr) {

         var e = (FunctionCallExpr)expr;

-        return new FunctionCallExpr((e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr));

+        return new FunctionCallExpr(e.tok, e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr));

 

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

-        return new OldExpr((e.tok), CloneExpr(e.E));

+        return new OldExpr(e.tok, CloneExpr(e.E));

 

       } else if (expr is MultiSetFormingExpr) {

         var e = (MultiSetFormingExpr)expr;

-        return new MultiSetFormingExpr((e.tok), CloneExpr(e.E));

+        return new MultiSetFormingExpr(e.tok, CloneExpr(e.E));

 

       } else if (expr is FreshExpr) {

         var e = (FreshExpr)expr;

-        return new FreshExpr((e.tok), CloneExpr(e.E));

+        return new FreshExpr(e.tok, CloneExpr(e.E));

 

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

-        return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E));

+        return new UnaryExpr(e.tok, e.Op, CloneExpr(e.E));

 

       } else if (expr is BinaryExpr) {

         var e = (BinaryExpr)expr;

-        return new BinaryExpr((e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));

+        return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1));

 

       } else if (expr is ChainingExpression) {

         var e = (ChainingExpression)expr;

@@ -846,11 +846,11 @@ namespace Microsoft.Dafny
 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

-        return new LetExpr((e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));

+        return new LetExpr(e.tok, e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));

 

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

-        var tk = (e.tok);

+        var tk = e.tok;

         var bvs = e.BoundVars.ConvertAll(CloneBoundVar);

         var range = CloneExpr(e.Range);

         var term = CloneExpr(e.Term);

@@ -866,20 +866,20 @@ namespace Microsoft.Dafny
         }

 

       } else if (expr is WildcardExpr) {

-        return new WildcardExpr((expr.tok));

+        return new WildcardExpr(expr.tok);

 

       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         if (e is AssertExpr) {

-          return new AssertExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));

+          return new AssertExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body));

         } else {

           Contract.Assert(e is AssumeExpr);

-          return new AssumeExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));

+          return new AssumeExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body));

         }

 

       } else if (expr is ITEExpr) {

         var e = (ITEExpr)expr;

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

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

 

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

@@ -892,8 +892,8 @@ namespace Microsoft.Dafny
 

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

-        return new MatchExpr((e.tok), CloneExpr(e.Source),

-          e.Cases.ConvertAll(c => new MatchCaseExpr((c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));

+        return new MatchExpr(e.tok, CloneExpr(e.Source),

+          e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));

 

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

diff --git a/Dafny/Rewriter.cs b/Dafny/Rewriter.cs
index 4dea968e..d88830a7 100644
--- a/Dafny/Rewriter.cs
+++ b/Dafny/Rewriter.cs
@@ -87,13 +87,13 @@ namespace Microsoft.Dafny
         if (member is Function && member.Name == "Valid" && !member.IsStatic) {

           var valid = (Function)member;

           // reads this;

-          valid.Reads.Add(new FrameExpression(new ThisExpr(tok), null));

+          valid.Reads.Add(new FrameExpression(tok, new ThisExpr(tok), null));

           // reads Repr;

-          valid.Reads.Add(new FrameExpression(new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null));

+          valid.Reads.Add(new FrameExpression(tok, new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null));

         } else if (member is Constructor) {

           var ctor = (Constructor)member;

           // modifies this;

-          ctor.Mod.Expressions.Add(new FrameExpression(new ImplicitThisExpr(tok), null));

+          ctor.Mod.Expressions.Add(new FrameExpression(tok, new ImplicitThisExpr(tok), null));

           // ensures Valid();

           ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));

           // ensures fresh(Repr - {this});

@@ -230,7 +230,7 @@ namespace Microsoft.Dafny
           var m = (Method)member;

           if (Valid != null && !IsSimpleQueryMethod(m)) {

             // modifies Repr;

-            m.Mod.Expressions.Add(new FrameExpression(Repr, null));

+            m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));

             // ensures Valid();

             var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());

             valid.Function = Valid;