DafnyExtension: fixed more missing cases for hover texts

7 files changed, 176 insertions, 93 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 2f254135..b1b8828a 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/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/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d8d95079..1629fe51 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/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/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f342ecca..66ad49e9 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/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/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a81b256e..2f49f689 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bf6dce17..c281aa4e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/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/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4dea968e..d88830a7 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/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;

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index bec65954..77a1fcf8 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -20,7 +20,7 @@ using Microsoft.VisualStudio.Text.Projection;
 using Microsoft.VisualStudio.Utilities;

 using System.Diagnostics.Contracts;

 using Bpl = Microsoft.Boogie;

-using Dafny = Microsoft.Dafny;

+using Microsoft.Dafny;

 

 namespace DafnyLanguage

 {

@@ -47,7 +47,7 @@ namespace DafnyLanguage
   {

     ITextBuffer _buffer;

     ITextSnapshot _snapshot;  // the most recent snapshot of _buffer that we have been informed about

-    Dafny.Program _program;  // the program parsed from _snapshot

+    Microsoft.Dafny.Program _program;  // the program parsed from _snapshot

     List<IdRegion> _regions = new List<IdRegion>();  // the regions generated from _program

     ITagAggregator<DafnyResolverTag> _aggregator;

 

@@ -104,7 +104,7 @@ namespace DafnyLanguage
       }

     }

 

-    bool ComputeIdentifierRegions(Dafny.Program program, ITextSnapshot snapshot) {

+    bool ComputeIdentifierRegions(Microsoft.Dafny.Program program, ITextSnapshot snapshot) {

       Contract.Requires(snapshot != null);

 

       if (program == _program)

@@ -113,12 +113,12 @@ namespace DafnyLanguage
       List<IdRegion> newRegions = new List<IdRegion>();

 

       foreach (var module in program.Modules) {

-        foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {

-          if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {

+        foreach (var d in module.TopLevelDecls) {

+          if (!HasBodyTokens(d) && !(d is ClassDecl)) {

             continue;

           }

-          if (d is Dafny.DatatypeDecl) {

-            var dt = (Dafny.DatatypeDecl)d;

+          if (d is DatatypeDecl) {

+            var dt = (DatatypeDecl)d;

             foreach (var ctor in dt.Ctors) {

               foreach (var dtor in ctor.Destructors) {

                 if (dtor != null) {

@@ -126,26 +126,26 @@ namespace DafnyLanguage
                 }

               }

             }

-          } else if (d is Dafny.ClassDecl) {

-            var cl = (Dafny.ClassDecl)d;

+          } else if (d is ClassDecl) {

+            var cl = (ClassDecl)d;

             foreach (var member in cl.Members) {

               if (!HasBodyTokens(member)) {

                 continue;

               }

-              if (member is Dafny.Function) {

-                var f = (Dafny.Function)member;

+              if (member is Function) {

+                var f = (Function)member;

                 foreach (var p in f.Formals) {

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

                 }

                 f.Req.ForEach(e => ExprRegions(e, newRegions));

-                f.Reads.ForEach(e => ExprRegions(e.E, newRegions));

+                f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true));

                 f.Ens.ForEach(e => ExprRegions(e, newRegions));

                 f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));

                 if (f.Body != null) {

                   ExprRegions(f.Body, newRegions);

                 }

-              } else if (member is Dafny.Method) {

-                var m = (Dafny.Method)member;

+              } else if (member is Method) {

+                var m = (Method)member;

                 foreach (var p in m.Ins) {

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

                 }

@@ -153,14 +153,14 @@ namespace DafnyLanguage
                   newRegions.Add(new IdRegion(p.tok, p, true));

                 }

                 m.Req.ForEach(e => ExprRegions(e.E, newRegions));

-                m.Mod.Expressions.ForEach(e => ExprRegions(e.E, newRegions));

+                m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true));

                 m.Ens.ForEach(e => ExprRegions(e.E, newRegions));

                 m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));

                 if (m.Body != null) {

                   StatementRegions(m.Body, newRegions);

                 }

-              } else if (member is Dafny.Field) {

-                var fld = (Dafny.Field)member;

+              } else if (member is Field) {

+                var fld = (Field)member;

                 newRegions.Add(new IdRegion(fld.tok, fld, "field", true));

               }

             }

@@ -173,27 +173,38 @@ namespace DafnyLanguage
       return true;

     }

 

-    static void ExprRegions(Dafny.Expression expr, List<IdRegion> regions) {

+    static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions) {

+      Contract.Requires(fe != null);

+      Contract.Requires(regions != null);

+      if (descendIntoExpressions) {

+        ExprRegions(fe.E, regions);

+      }

+      if (fe.Field != null) {

+        regions.Add(new IdRegion(fe.tok, fe.Field, "field", false));

+      }

+    }

+

+    static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions) {

       Contract.Requires(expr != null);

       Contract.Requires(regions != null);

-      if (expr is Dafny.IdentifierExpr) {

-        var e = (Dafny.IdentifierExpr)expr;

+      if (expr is IdentifierExpr) {

+        var e = (IdentifierExpr)expr;

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

-      } else if (expr is Dafny.FieldSelectExpr) {

-        var e = (Dafny.FieldSelectExpr)expr;

+      } else if (expr is FieldSelectExpr) {

+        var e = (FieldSelectExpr)expr;

         regions.Add(new IdRegion(e.tok, e.Field, "field", false));

-      } else if (expr is Dafny.ComprehensionExpr) {

-        var e = (Dafny.ComprehensionExpr)expr;

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

         foreach (var bv in e.BoundVars) {

           regions.Add(new IdRegion(bv.tok, bv, true));

         }

-      } else if (expr is Dafny.MatchExpr) {

-        var e = (Dafny.MatchExpr)expr;

+      } else if (expr is MatchExpr) {

+        var e = (MatchExpr)expr;

         foreach (var kase in e.Cases) {

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

         }

-      } else if (expr is Dafny.ChainingExpression) {

-        var e = (Dafny.ChainingExpression)expr;

+      } else if (expr is ChainingExpression) {

+        var e = (ChainingExpression)expr;

         // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)

         e.Operands.ForEach(ee => ExprRegions(ee, regions));

         return;  // return here, so as to avoid doing the subexpressions below

@@ -203,20 +214,44 @@ namespace DafnyLanguage
       }

     }

 

-    static void StatementRegions(Dafny.Statement stmt, List<IdRegion> regions) {

+    static void StatementRegions(Statement stmt, List<IdRegion> regions) {

       Contract.Requires(stmt != null);

       Contract.Requires(regions != null);

-      if (stmt is Dafny.VarDecl) {

-        var s = (Dafny.VarDecl)stmt;

+      if (stmt is VarDeclStmt) {

+        var s = (VarDeclStmt)stmt;

+        // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)

+        foreach (var lhs in s.Lhss) {

+          regions.Add(new IdRegion(lhs.Tok, lhs, true));

+        }

+        if (s.Update is UpdateStmt) {

+          var upd = (UpdateStmt)s.Update;

+          foreach (var rhs in upd.Rhss) {

+            foreach (var ee in rhs.SubExpressions) {

+              ExprRegions(ee, regions);

+            }

+          }

+        } else {

+          var upd = (AssignSuchThatStmt)s.Update;

+          ExprRegions(upd.Expr, regions);

+        }

+        // we're done, so don't do the sub-statements/expressions again

+        return;

+      } else  if (stmt is VarDecl) {

+        var s = (VarDecl)stmt;

         regions.Add(new IdRegion(s.Tok, s, true));

-      } else if (stmt is Dafny.ParallelStmt) {

-        var s = (Dafny.ParallelStmt)stmt;

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

         s.BoundVars.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));

-      } else if (stmt is Dafny.MatchStmt) {

-        var s = (Dafny.MatchStmt)stmt;

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

         foreach (var kase in s.Cases) {

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

         }

+      } else if (stmt is LoopStmt) {

+        var s = (LoopStmt)stmt;

+        if (s.Mod.Expressions != null) {

+          s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false));

+        }

       }

       foreach (var ee in stmt.SubExpressions) {

         ExprRegions(ee, regions);

@@ -226,7 +261,7 @@ namespace DafnyLanguage
       }

     }

 

-    bool HasBodyTokens(Dafny.Declaration decl) {

+    bool HasBodyTokens(Declaration decl) {

       Contract.Requires(decl != null);

       return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;

     }

@@ -237,24 +272,24 @@ namespace DafnyLanguage
       public readonly int Length;

       public readonly string HoverText;

       public readonly bool IsDefinition;

-      public IdRegion(Bpl.IToken tok, Dafny.IVariable v, bool isDefinition) {

+      public IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

         Start = tok.pos;

         Length = v.Name.Length;

         string kind;

-        if (v is Dafny.VarDecl) {

+        if (v is VarDecl) {

           kind = "local variable";

-        } else if (v is Dafny.BoundVar) {

+        } else if (v is BoundVar) {

           kind = "bound variable";

         } else {

-          var formal = (Dafny.Formal)v;

+          var formal = (Formal)v;

           kind = formal.InParam ? "in-parameter" : "out-parameter";

         }

         HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.ToString(), v.IsGhost ? "ghost " : "", kind);

         IsDefinition = isDefinition;

       }

-      public IdRegion(Bpl.IToken tok, Dafny.Field decl, string kind, bool isDefinition) {

+      public IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) {

         Contract.Requires(tok != null);

         Contract.Requires(decl != null);

         Contract.Requires(kind != null);