Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss to VarDeclStmt.Locals

10 files changed, 61 insertions, 64 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 385bfd78..8ac0b3a8 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -484,7 +484,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

-        var lhss = s.Lhss.ConvertAll(c => new VarDecl(Tok(c.Tok), Tok(c.EndTok), c.Name, CloneType(c.OptionalType), c.IsGhost));

+        var lhss = s.Locals.ConvertAll(c => new LocalVariable(Tok(c.Tok), Tok(c.EndTok), c.Name, CloneType(c.OptionalType), c.IsGhost));

         r = new VarDeclStmt(Tok(s.Tok), Tok(s.EndTok), lhss, (ConcreteUpdateStatement)CloneStmt(s.Update));

 

       } else {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 97c21a89..77bbd6bf 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1556,8 +1556,8 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

-        foreach (var lhs in s.Lhss) {

-          TrVarDecl(lhs, true, indent);

+        foreach (var local in s.Locals) {

+          TrLocalVar(local, true, indent);

         }

         if (s.Update != null) {

           TrStmt(s.Update, indent);

@@ -1841,7 +1841,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrVarDecl(VarDecl s, bool alwaysInitialize, int indent) {

+    void TrLocalVar(LocalVariable s, bool alwaysInitialize, int indent) {

       Contract.Requires(s != null);

       if (s.IsGhost) {

         // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 563c1d6c..f281d9fc 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -425,13 +425,13 @@ IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
   ":"

   Type<out ty>

   .

-LocalIdentTypeOptional<out VarDecl var, bool isGhost>

+LocalIdentTypeOptional<out LocalVariable var, bool isGhost>

 = (. IToken id;  Type ty;  Type optType = null;

   .)

   WildIdent<out id, true>

   [ ":" Type<out ty>             (. optType = ty; .)

   ]

-  (. var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)

+  (. var = new LocalVariable(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)

   .

 IdentTypeOptional<out BoundVar var>

 = (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);

@@ -1143,9 +1143,9 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
   .

 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

-     VarDecl/*!*/ d;

+     LocalVariable d;

      AssignmentRhs r;  IdentifierExpr lhs0;

-     List<VarDecl> lhss = new List<VarDecl>();

+     List<LocalVariable> lhss = new List<LocalVariable>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

      IToken suchThatAssume = null;

      Expression suchThat = null;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 47059763..cca4e56c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1514,7 +1514,7 @@ namespace Microsoft.Dafny {
     public Constructor Member_Init;  // created during registration phase of resolution; its specification is filled in during resolution

     public Predicate Member_Valid;  // created during registration phase of resolution; its specification is filled in during resolution

     public Method Member_MoveNext;  // created during registration phase of resolution; its specification is filled in during resolution

-    public readonly VarDecl YieldCountVariable;

+    public readonly LocalVariable YieldCountVariable;

     public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

                         List<Formal> ins, List<Formal> outs,

                         Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,

@@ -1554,7 +1554,7 @@ namespace Microsoft.Dafny {
       OutsHistoryFields = new List<Field>();

       DecreasesFields = new List<Field>();

 

-      YieldCountVariable = new VarDecl(tok, tok, "_yieldCount", new EverIncreasingType(), true);

+      YieldCountVariable = new LocalVariable(tok, tok, "_yieldCount", new EverIncreasingType(), true);

       YieldCountVariable.type = YieldCountVariable.OptionalType;  // resolve YieldCountVariable here

     }

 

@@ -1852,7 +1852,7 @@ namespace Microsoft.Dafny {
       }

     }

     public string DisplayName {

-      get { return VarDecl.DisplayNameHelper(this); }

+      get { return LocalVariable.DisplayNameHelper(this); }

     }

     private string uniqueName;

     public string UniqueName {

@@ -2832,21 +2832,21 @@ namespace Microsoft.Dafny {
 

   public class VarDeclStmt : Statement

   {

-    public readonly List<VarDecl> Lhss;

+    public readonly List<LocalVariable> Locals;

     public readonly ConcreteUpdateStatement Update;

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(Lhss));

+      Contract.Invariant(cce.NonNullElements(Locals));

     }

 

-    public VarDeclStmt(IToken tok, IToken endTok, List<VarDecl> lhss, ConcreteUpdateStatement update)

+    public VarDeclStmt(IToken tok, IToken endTok, List<LocalVariable> locals, ConcreteUpdateStatement update)

       : base(tok, endTok)

     {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

-      Contract.Requires(lhss != null);

+      Contract.Requires(locals != null);

 

-      Lhss = lhss;

+      Locals = locals;

       Update = update;

     }

 

@@ -3006,7 +3006,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class VarDecl : /*Statement,*/ IVariable {

+  public class LocalVariable : IVariable {

     public readonly IToken Tok;

     public readonly IToken EndTok;  // typically a terminating semi-colon or end-curly-brace

     readonly string name;

@@ -3018,7 +3018,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(OptionalType != null);

     }

 

-    public VarDecl(IToken tok, IToken endTok, string name, Type type, bool isGhost) {

+    public LocalVariable(IToken tok, IToken endTok, string name, Type type, bool isGhost) {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

       Contract.Requires(name != null);

@@ -3101,7 +3101,7 @@ namespace Microsoft.Dafny {
       }

     }

     /// <summary>

-    /// This method retrospectively makes the VarDecl a ghost.  It is to be used only during resolution.

+    /// This method retrospectively makes the LocalVariable a ghost.  It is to be used only during resolution.

     /// </summary>

     public void MakeGhost() {

       this.IsGhost = true;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a52d840c..b8800af7 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1058,7 +1058,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		TypeAndToken(out tok, out ty);

 	}

 

-	void LocalIdentTypeOptional(out VarDecl var, bool isGhost) {

+	void LocalIdentTypeOptional(out LocalVariable var, bool isGhost) {

 		IToken id;  Type ty;  Type optType = null;

 		

 		WildIdent(out id, true);

@@ -1067,7 +1067,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 			Type(out ty);

 			optType = ty; 

 		}

-		var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); 

+		var = new LocalVariable(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); 

 	}

 

 	void IdentTypeOptional(out BoundVar var) {

@@ -1779,9 +1779,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void VarDeclStatement(out Statement/*!*/ s) {

 		IToken x = null, assignTok = null;  bool isGhost = false;

-		VarDecl/*!*/ d;

+		LocalVariable d;

 		AssignmentRhs r;  IdentifierExpr lhs0;

-		List<VarDecl> lhss = new List<VarDecl>();

+		List<LocalVariable> lhss = new List<LocalVariable>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

 		IToken suchThatAssume = null;

 		Expression suchThat = null;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index b370b507..c4e8d7db 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -807,18 +807,18 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

-        if (s.Lhss.Exists(v => v.IsGhost)) {

+        if (s.Locals.Exists(v => v.IsGhost)) {

           wr.Write("ghost ");

         }

         wr.Write("var");

         string sep = "";

-        foreach (var lhs in s.Lhss) {

+        foreach (var local in s.Locals) {

           wr.Write(sep);

-          if (lhs.Attributes != null) {

-            PrintAttributes(lhs.Attributes);

+          if (local.Attributes != null) {

+            PrintAttributes(local.Attributes);

           }

-          wr.Write(" {0}", lhs.DisplayName);

-          PrintType(": ", lhs.OptionalType);

+          wr.Write(" {0}", local.DisplayName);

+          PrintType(": ", local.OptionalType);

           sep = ",";

         }

         if (s.Update != null) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 75dbaad3..7333f950 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1040,7 +1040,7 @@ namespace Microsoft.Dafny
             Expression addedAssert = null;

             if (oldS is VarDeclStmt) {

               var cOld = (VarDeclStmt)oldS;

-              if (VarDeclAgree(cOld.Lhss, cNew.Lhss)) {

+              if (LocalVarsAgree(cOld.Locals, cNew.Locals)) {

                 var update = cNew.Update as UpdateStmt;

                 if (update != null && update.Rhss.TrueForAll(rhs => !rhs.CanAffectPreviouslyKnownExpressions)) {

                   // Note, we allow switching between ghost and non-ghost, since that seems unproblematic.

@@ -1202,7 +1202,7 @@ namespace Microsoft.Dafny
       }

       return true;

     }

-    private bool VarDeclAgree(List<VarDecl> old, List<VarDecl> nw) {

+    private bool LocalVarsAgree(List<LocalVariable> old, List<LocalVariable> nw) {

       if (old.Count != nw.Count)

         return false;

       for (int i = 0; i < old.Count; i++) {

@@ -1249,7 +1249,7 @@ namespace Microsoft.Dafny
         return oth != null && oth.Guard == null;

       } else if (nxt is VarDeclStmt) {

         var oth = other as VarDeclStmt;

-        return oth != null && VarDeclAgree(((VarDeclStmt)nxt).Lhss, oth.Lhss);

+        return oth != null && LocalVarsAgree(((VarDeclStmt)nxt).Locals, oth.Locals);

       } else if (nxt is BlockStmt) {

         var b = (BlockStmt)nxt;

         if (b.Labels != null) {

@@ -1397,8 +1397,8 @@ namespace Microsoft.Dafny
         var l = lhs.Resolved;

         if (l is IdentifierExpr) {

           var ident = (IdentifierExpr)l;

-          Contract.Assert(ident.Var is VarDecl || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)

-          if ((ident.Var is VarDecl && RefinementToken.IsInherited(((VarDecl)ident.Var).Tok, m)) || ident.Var is Formal) {

+          Contract.Assert(ident.Var is LocalVariable || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)

+          if ((ident.Var is LocalVariable && RefinementToken.IsInherited(((LocalVariable)ident.Var).Tok, m)) || ident.Var is Formal) {

             // for some reason, formals are not considered to be inherited.

             reporter.Error(l.tok, "cannot assign to variable defined previously");

             return false;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c551e91f..4fea4f83 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1873,8 +1873,8 @@ namespace Microsoft.Dafny
       protected override void VisitOneStmt(Statement stmt) {

         if (stmt is VarDeclStmt) {

           var s = (VarDeclStmt)stmt;

-          foreach (var lhs in s.Lhss) {

-            CheckTypeIsDetermined(lhs.Tok, lhs.Type, "local variable");

+          foreach (var local in s.Locals) {

+            CheckTypeIsDetermined(local.Tok, local.Type, "local variable");

           }

         } else if (stmt is ForallStmt) {

           var s = (ForallStmt)stmt;

@@ -4058,23 +4058,23 @@ namespace Microsoft.Dafny
         ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

-        foreach (var v in s.Lhss) {

-          ResolveType(v.Tok, v.OptionalType, ResolveTypeOption.InferTypeProxies, null);

-          v.type = v.OptionalType;

+        foreach (var local in s.Locals) {

+          ResolveType(local.Tok, local.OptionalType, ResolveTypeOption.InferTypeProxies, null);

+          local.type = local.OptionalType;

           // now that the declaration has been processed, add the name to the scope

-          if (!scope.Push(v.Name, v)) {

-            Error(v.Tok, "Duplicate local-variable name: {0}", v.Name);

+          if (!scope.Push(local.Name, local)) {

+            Error(local.Tok, "Duplicate local-variable name: {0}", local.Name);

           }

           if (specContextOnly) {

             // a local variable in a specification-only context might as well be ghost

-            v.IsGhost = true;

+            local.IsGhost = true;

           }

         }

         if (s.Update != null) {

           ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

         }

         if (!s.IsGhost) {

-          s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Lhss.All(v => v.IsGhost);

+          s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);

         }

 

       } else if (stmt is AssignStmt) {

@@ -4929,9 +4929,9 @@ namespace Microsoft.Dafny
               if (resolvedLhs is IdentifierExpr) {

                 var ll = (IdentifierExpr)resolvedLhs;

                 if (!ll.Var.IsGhost) {

-                  if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {

+                  if (ll is AutoGhostIdentifierExpr && ll.Var is LocalVariable) {

                     // the variable was actually declared in this statement, so auto-declare it as ghost

-                    ((VarDecl)ll.Var).MakeGhost();

+                    ((LocalVariable)ll.Var).MakeGhost();

                   } else {

                     Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

                   }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0fee723a..70e7644f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2132,7 +2132,7 @@ namespace Microsoft.Dafny {
 

     ModuleDefinition currentModule = null;  // the name of the module whose members are currently being translated

     ICallable codeContext = null;  // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness

-    LocalVariable yieldCountVariable = null;  // non-null when an iterator body is being translated

+    Bpl.LocalVariable yieldCountVariable = null;  // non-null when an iterator body is being translated

     bool assertAsAssume = false; // generate assume statements instead of assert statements

     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

@@ -3574,7 +3574,7 @@ namespace Microsoft.Dafny {
         Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

         for (int i = 0; i < e.Function.Formals.Count; i++) {

           Formal p = e.Function.Formals[i];

-          VarDecl local = new VarDecl(p.tok, p.tok, p.Name, p.Type, p.IsGhost);

+          LocalVariable local = new LocalVariable(p.tok, p.tok, p.Name, p.Type, p.IsGhost);

           local.type = local.OptionalType;  // resolve local here

           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration));

           ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -4354,7 +4354,7 @@ namespace Microsoft.Dafny {
       var substMap = new Dictionary<IVariable, Expression>();

       for (int i = 0; i < method.Ins.Count; i++) {

         var p = method.Ins[i];

-        var local = new VarDecl(p.tok, p.tok, p.Name + "#", p.Type, p.IsGhost);

+        var local = new LocalVariable(p.tok, p.tok, p.Name + "#", p.Type, p.IsGhost);

         local.type = local.OptionalType;  // resolve local here

         var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(methodCheck.Refining));

         ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -5409,11 +5409,11 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

-        foreach (var lhs in s.Lhss) {

-          Bpl.Type varType = TrType(lhs.Type);

-          Bpl.Expr wh = GetWhereClause(lhs.Tok, new Bpl.IdentifierExpr(lhs.Tok, lhs.AssignUniqueName(currentDeclaration), varType), lhs.Type, etran);

-          Bpl.LocalVariable var = new Bpl.LocalVariable(lhs.Tok, new Bpl.TypedIdent(lhs.Tok, lhs.AssignUniqueName(currentDeclaration), varType, wh));

-          var.Attributes = etran.TrAttributes(lhs.Attributes, null); ;

+        foreach (var local in s.Locals) {

+          Bpl.Type varType = TrType(local.Type);

+          Bpl.Expr wh = GetWhereClause(local.Tok, new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration), varType), local.Type, etran);

+          Bpl.LocalVariable var = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration), varType, wh));

+          var.Attributes = etran.TrAttributes(local.Attributes, null); ;

           locals.Add(var);

         }

         if (s.Update != null) {

@@ -6362,7 +6362,7 @@ namespace Microsoft.Dafny {
       var substMap = new Dictionary<IVariable, Expression>();

       for (int i = 0; i < callee.Ins.Count; i++) {

         var formal = callee.Ins[i];

-        var local = new VarDecl(formal.tok, formal.tok, formal.Name + "#", formal.Type, formal.IsGhost);

+        var local = new LocalVariable(formal.tok, formal.tok, formal.Name + "#", formal.Type, formal.IsGhost);

         local.type = local.OptionalType;  // resolve local here

         var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration));

         ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -6462,7 +6462,7 @@ namespace Microsoft.Dafny {
 

       var substMap = new Dictionary<IVariable, Expression>();

       foreach (BoundVar bv in boundVars) {

-        VarDecl local = new VarDecl(bv.tok, bv.tok, bv.Name, bv.Type, bv.IsGhost);

+        LocalVariable local = new LocalVariable(bv.tok, bv.tok, bv.Name, bv.Type, bv.IsGhost);

         local.type = local.OptionalType;  // resolve local here

         IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration));

         ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -8622,7 +8622,7 @@ namespace Microsoft.Dafny {
           var substMap = new Dictionary<IVariable, Expression>();

           var argIndex = 0;

           foreach (var bv in mc.Arguments) {

-            if (!VarDecl.HasWildcardName(bv)) {

+            if (!LocalVariable.HasWildcardName(bv)) {

               var dtor = mc.Ctor.Destructors[argIndex];

               var dv = new FieldSelectExpr(bv.tok, e.Source, dtor.Name);

               dv.Field = dtor;  // resolve here

@@ -10889,7 +10889,7 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is VarDeclStmt) {

           var s = (VarDeclStmt)stmt;

-          var lhss = s.Lhss.ConvertAll(c => new VarDecl(c.Tok, c.EndTok, c.Name, c.OptionalType == null ? null : Resolver.SubstType(c.OptionalType, typeMap), c.IsGhost));

+          var lhss = s.Locals.ConvertAll(c => new LocalVariable(c.Tok, c.EndTok, c.Name, c.OptionalType == null ? null : Resolver.SubstType(c.OptionalType, typeMap), c.IsGhost));

           var rr = new VarDeclStmt(s.Tok, s.EndTok, lhss, (ConcreteUpdateStatement)SubstStmt(s.Update));

           r = rr;

         } else {

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 962dec3c..4cf752fb 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -278,8 +278,8 @@ namespace DafnyLanguage
       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) {

-          IdRegion.Add(regions, lhs.Tok, lhs, true, module);

+        foreach (var local in s.Locals) {

+          IdRegion.Add(regions, local.Tok, local, true, module);

         }

         if (s.Update == null) {

           // the VarDeclStmt has no associated assignment

@@ -296,9 +296,6 @@ namespace DafnyLanguage
         }

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

         return;

-      } else  if (stmt is VarDecl) {

-        var s = (VarDecl)stmt;

-        IdRegion.Add(regions, s.Tok, s, true, module);

       } else if (stmt is ForallStmt) {

         var s = (ForallStmt)stmt;

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

@@ -385,7 +382,7 @@ namespace DafnyLanguage
         Length = v.DisplayName.Length;

         if (kind == null) {

           // use default

-          if (v is VarDecl) {

+          if (v is LocalVariable) {

             kind = "local variable";

           } else if (v is BoundVar) {

             kind = "bound variable";

@@ -399,7 +396,7 @@ namespace DafnyLanguage
         }

         Variable = v;

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

-        Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;

+        Kind = !isDefinition ? OccurrenceKind.Use : LocalVariable.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;

       }

       private IdRegion(Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(tok != null);