Dafny: implemented a more precise scheme for allowing use of a function's rep axiom

8 files changed, 167 insertions, 122 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 58f0e8eb..a1408024 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -472,9 +472,15 @@ namespace Microsoft.Dafny {
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       

       // axiom

-      //   mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))

+      //   mh < ModuleContextHeight ||

+      //   (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))

       //   ==>

-      //   (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==>

+      //   (forall $Heap, formals ::

+      //       { f(args) }

+      //       $IsHeap($Heap) && this != null &&

+      //       (((mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && Pre($Heap,args)) ||

+      //        f#canCall(args))

+      //       ==>

       //       f(args) == body && ens);

       //

       // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then

@@ -533,14 +539,14 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))

-      ModuleDecl m = f.EnclosingClass.Module;

+      // mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))

+      ModuleDecl mod = f.EnclosingClass.Module;

       Bpl.Expr activate = Bpl.Expr.Or(

-        Bpl.Expr.Lt(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

+        Bpl.Expr.Lt(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

         Bpl.Expr.And(

-          Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

+          Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

           Bpl.Expr.Or(

-            Bpl.Expr.Lt(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

+            Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

             etran.InMethodContext())));

       

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

@@ -554,12 +560,26 @@ namespace Microsoft.Dafny {
         Contract.Assert(r != null);

         substMap.Add(specializationFormal, r);

       }

-      Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

-      Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);

+      Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType));

+      Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

 

+      Bpl.Expr pre = Bpl.Expr.True;

       foreach (Expression req in f.Req) {

-        ante = Bpl.Expr.And(ante, etran.TrExpr(Substitute(req, null, substMap)));

+        pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));

       }

+      // useViaPre: (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && Pre

+      Bpl.Expr useViaPre =

+        Bpl.Expr.And(

+          Bpl.Expr.Or(Bpl.Expr.Or(

+            Bpl.Expr.Neq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

+            Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),

+            etran.InMethodContext()),

+          pre);

+      // useViaCanCall: f#canCall(args)

+      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+      Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);

+      ante = Bpl.Expr.And(ante, Bpl.Expr.Or(useViaPre, useViaCanCall));

+

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

       Bpl.Expr meat = null;

@@ -1086,7 +1106,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void AddWellformednessCheck(Function f){

+    void AddWellformednessCheck(Function f) {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(f.EnclosingClass != null);

@@ -1109,11 +1129,11 @@ namespace Microsoft.Dafny {
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

       // the procedure itself

       Bpl.RequiresSeq req = new Bpl.RequiresSeq();

-      // free requires mh < ModuleContextHeight || (mh == ModuleContextHeight && fh < FunctionContextHeight);

-      ModuleDecl m = f.EnclosingClass.Module;

+      // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;

+      ModuleDecl mod = f.EnclosingClass.Module;

       Bpl.Expr context = Bpl.Expr.And(

-        Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

-        Bpl.Expr.Eq(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));

+        Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

+        Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));

       req.Add(Requires(f.tok, true, context, null, null));

       Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

         req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

@@ -1499,6 +1519,12 @@ namespace Microsoft.Dafny {
               CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder, contextDecrInferred);

             }

           }

+

+          // all is okay, so allow this function application access to the function's axiom

+          Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+          ExprSeq args = etran.FunctionInvocationArguments(e);

+          Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

+          builder.Add(new Bpl.AssumeCmd(expr.tok, canCallFuncAppl));

         }

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

@@ -1838,6 +1864,10 @@ namespace Microsoft.Dafny {
         Bpl.Function limitedF = new Bpl.Function(f.tok, f.FullName + "#limited", args, res);

         sink.TopLevelDeclarations.Add(limitedF);

       }

+

+      res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

+      Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);

+      sink.TopLevelDeclarations.Add(canCallF);

     }

     

     /// <summary>

@@ -3351,7 +3381,7 @@ namespace Microsoft.Dafny {
 

       return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));

     }

-    

+

     // ----- Expression ---------------------------------------------------------------------------

     

     internal class ExpressionTranslator {

@@ -3585,16 +3615,7 @@ namespace Microsoft.Dafny {
             }

           }

           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType(cce.NonNull(e.Type)));

-          Bpl.ExprSeq args = new Bpl.ExprSeq();

-          args.Add(HeapExpr);

-          if (!e.Function.IsStatic) {

-            args.Add(TrExpr(e.Receiver));

-          }

-          for (int i = 0; i < e.Args.Count; i++) {

-            Expression ee = e.Args[i];

-            Type t = e.Function.Formals[i].Type;

-            args.Add(CondApplyBox(expr.tok, TrExpr(ee), cce.NonNull(ee.Type), t));

-          }

+          Bpl.ExprSeq args = FunctionInvocationArguments(e);

           Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);

           return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);

         

@@ -3811,6 +3832,23 @@ namespace Microsoft.Dafny {
         }

       }

 

+      public ExprSeq FunctionInvocationArguments(FunctionCallExpr e) {

+        Contract.Requires(e != null);

+        Contract.Ensures(Contract.Result<ExprSeq>() != null);

+

+        Bpl.ExprSeq args = new Bpl.ExprSeq();

+        args.Add(HeapExpr);

+        if (!e.Function.IsStatic) {

+          args.Add(TrExpr(e.Receiver));

+        }

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

+          Expression ee = e.Args[i];

+          Type t = e.Function.Formals[i].Type;

+          args.Add(CondApplyBox(e.tok, TrExpr(ee), cce.NonNull(ee.Type), t));

+        }

+        return args;

+      }

+

       public Bpl.Expr GetArrayIndexFieldName(IToken tok, List<Expression> indices) {

         Bpl.Expr fieldName = null;

         foreach (Expression idx in indices) {

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 5b51b3e4..d737a8cd 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -53,7 +53,7 @@ Dafny program verifier finished with 17 verified, 0 errors
 

 -------------------- TerminationDemos.dfy --------------------

 

-Dafny program verifier finished with 10 verified, 0 errors

+Dafny program verifier finished with 11 verified, 0 errors

 

 -------------------- Substitution.dfy --------------------

 

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 76925e8e..01a7c7bd 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -30,7 +30,7 @@ class Ackermann {
     else

       F(m - 1, F(m, n - 1))

   }

-/*

+

   function G(m: int, n: int): int

     requires 0 <= m && 0 <= n;

     ensures 0 <= G(m, n);

@@ -42,7 +42,6 @@ class Ackermann {
     else

       G(m - 1, G(m, n - 1))

   }

-*/

 }

 

 // -----------------------------------

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
index 98bb7033..7e64dd1d 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
@@ -22,9 +22,12 @@ namespace DafnyLanguage
     [Import]

     internal IClassificationTypeRegistryService ClassificationTypeRegistry = null;

 

+    [Import]

+    internal Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService Standards = null;

+

     public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

       ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);

-      return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry) as ITagger<T>;

+      return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger<T>;

     }

   }

 

@@ -36,15 +39,18 @@ namespace DafnyLanguage
 

     internal DafnyClassifier(ITextBuffer buffer,

                              ITagAggregator<DafnyTokenTag> tagAggregator,

-                             IClassificationTypeRegistryService typeService) {

+                             IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) {

       _buffer = buffer;

       _aggregator = tagAggregator;

       _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);

+      // use built-in classification types:

       _typeMap = new Dictionary<DafnyTokenKinds, IClassificationType>();

-      _typeMap[DafnyTokenKinds.Keyword] = typeService.GetClassificationType("keyword");  // use the built-in "keyword" classification type

-      _typeMap[DafnyTokenKinds.Number] = typeService.GetClassificationType("number");  // use the built-in "number" classification type

-      _typeMap[DafnyTokenKinds.String] = typeService.GetClassificationType("string");  // use the built-in "string" classification type

-      _typeMap[DafnyTokenKinds.Comment] = typeService.GetClassificationType("comment");  // use the built-in "comment" classification type

+      _typeMap[DafnyTokenKinds.Keyword] = standards.Keyword;

+      _typeMap[DafnyTokenKinds.Number] = standards.NumberLiteral;

+      _typeMap[DafnyTokenKinds.String] = standards.StringLiteral;

+      _typeMap[DafnyTokenKinds.Comment] = standards.Comment;

+      _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;

+      _typeMap[DafnyTokenKinds.TypeIdentifier] = typeService.GetClassificationType("Dafny user type");

     }

 

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

@@ -72,47 +78,20 @@ namespace DafnyLanguage
     }

   }

 

-#if false  // the commented-out code here shows show to define new classifier types; however, the Dafny mode just uses the built-in "keyword" and "number" classifier types

-  /// <summary>

-  /// Defines an editor format for the keyword type.

-  /// </summary>

-  [Export(typeof(EditorFormatDefinition))]

-  [ClassificationType(ClassificationTypeNames = "Dafny-keyword")]

-  [Name("Dafny-keyword")]

-  //this should be visible to the end user

-  [UserVisible(false)]

-  //set the priority to be after the default classifiers

-  [Order(Before = Priority.Default)]

-  internal sealed class Keyword : ClassificationFormatDefinition

-  {

-    /// <summary>

-    /// Defines the visual format for the "ordinary" classification type

-    /// </summary>

-    public Keyword() {

-      this.DisplayName = "Dafny keyword"; //human readable version of the name

-      this.ForegroundColor = Colors.BlueViolet;

-    }

-  }

-

   /// <summary>

-  /// Defines an editor format for the OrdinaryClassification type that has a purple background

-  /// and is underlined.

+  /// Defines an editor format for user-defined type.

   /// </summary>

   [Export(typeof(EditorFormatDefinition))]

-  [ClassificationType(ClassificationTypeNames = "Dafny-number")]

-  [Name("Dafny-number")]

-  //this should be visible to the end user

-  [UserVisible(false)]

+  [ClassificationType(ClassificationTypeNames = "Dafny user type")]

+  [Name("Dafny user type")]

+  [UserVisible(true)]

   //set the priority to be after the default classifiers

   [Order(Before = Priority.Default)]

-  internal sealed class Number : ClassificationFormatDefinition

+  internal sealed class DafnyTypeFormat : ClassificationFormatDefinition

   {

-    /// <summary>

-    /// Defines the visual format for the "ordinary" classification type

-    /// </summary>

-    public Number() {

-      this.DisplayName = "Dafny numeric literal"; //human readable version of the name

-      this.ForegroundColor = Colors.Orange;

+    public DafnyTypeFormat() {

+      this.DisplayName = "Dafny user type"; //human readable version of the name

+      this.ForegroundColor = Colors.Coral;

     }

   }

 

@@ -122,15 +101,7 @@ namespace DafnyLanguage
     /// Defines the "ordinary" classification type.

     /// </summary>

     [Export(typeof(ClassificationTypeDefinition))]

-    [Name("Dafny-keyword")]

-    internal static ClassificationTypeDefinition Keyword = null;

-

-    /// <summary>

-    /// Defines the "ordinary" classification type.

-    /// </summary>

-    [Export(typeof(ClassificationTypeDefinition))]

-    [Name("Dafny-number")]

-    internal static ClassificationTypeDefinition Number = null;

+    [Name("Dafny user type")]

+    internal static ClassificationTypeDefinition UserType = null;

   }

-#endif

 }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index dedb141e..55f2ee34 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -130,6 +130,8 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

+    <Compile Include="Visitor.cs" />

+    <Compile Include="IdentifierTagger.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

     <Compile Include="DafnyDriver.cs" />

@@ -143,6 +145,7 @@
     <Compile Include="Properties\AssemblyInfo.cs" />

   </ItemGroup>

   <ItemGroup>

+    <None Include="app.config" />

     <None Include="source.extension.vsixmanifest">

       <SubType>Designer</SubType>

     </None>

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index acd357b1..390ed01f 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -40,12 +40,14 @@ namespace DafnyLanguage
   }

 

   /// <summary>

-  /// Translate PkgDefTokenTags into ErrorTags and Error List items

+  /// Translate DafnyResolverTag's into IOutliningRegionTag's

   /// </summary>

   internal sealed class OutliningTagger : ITagger<IOutliningRegionTag>

   {

     ITextBuffer _buffer;

     ITagAggregator<DafnyResolverTag> _aggregator;

+    Dafny.Program _program;

+    List<ORegion> _regions = new List<ORegion>();

 

     internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {

       _buffer = buffer;

@@ -59,51 +61,22 @@ namespace DafnyLanguage
     public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

       if (spans.Count == 0) yield break;

       var snapshot = spans[0].Snapshot;

-      foreach (var tagSpan in this._aggregator.GetTags(spans)) {

-        DafnyResolverTag t = tagSpan.Tag;

-        DafnySuccessResolverTag st = t as DafnySuccessResolverTag;

-        if (st != null) {

-          foreach (Dafny.ModuleDecl module in st.Program.Modules) {

-            if (!module.IsDefaultModule) {

-              yield return GetOutliningRegionTag(snapshot, module, "module");

-            }

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

-              if (d is Dafny.DatatypeDecl) {

-                yield return GetOutliningRegionTag(snapshot, d, "datatype");

-              } else {

-                Dafny.ClassDecl cl = (Dafny.ClassDecl)d;

-                if (!cl.IsDefaultClass) {

-                  yield return GetOutliningRegionTag(snapshot, cl, "class");

-                }

-                // do the class members (in particular, functions and methods)

-                foreach (Dafny.MemberDecl m in cl.Members) {

-                  if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {

-                    yield return GetOutliningRegionTag(snapshot, m, "function");

-                  } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

-                    yield return GetOutliningRegionTag(snapshot, m, "method");

-                  }

-                }

-              }

-            }

-          }

-        }

+      foreach (var r in _regions) {

+        yield return new TagSpan<OutliningRegionTag>(

+          new SnapshotSpan(snapshot, r.Start, r.Length),

+          new OutliningRegionTag(false, false, "...", r.HoverText));

       }

     }

 

-    TagSpan<OutliningRegionTag> GetOutliningRegionTag(ITextSnapshot snapshot, Dafny.Declaration decl, string kind) {

-      int startPosition = decl.BodyStartTok.pos + 1;  // skip the open-curly brace itself

-      int length = decl.BodyEndTok.pos - startPosition;

-      return new TagSpan<OutliningRegionTag>(

-        new SnapshotSpan(snapshot, startPosition, length),

-        new OutliningRegionTag(false, false, "...", string.Format("body of {0} {1}", kind, decl.Name)));

-    }

-

     // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

 

     void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {

       var r = sender as ResolverTagger;

       if (r != null && r._program != null) {

+        if (!ComputeOutliningRegions(r._program))

+          return;  // no new regions

+

         var chng = TagsChanged;

         if (chng != null) {

           NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);

@@ -114,5 +87,53 @@ namespace DafnyLanguage
         }

       }

     }

+

+    bool ComputeOutliningRegions(Dafny.Program program) {

+      if (program == _program)

+        return false;  // no new regions

+

+      List<ORegion> newRegions = new List<ORegion>();

+

+      foreach (Dafny.ModuleDecl module in program.Modules) {

+        if (!module.IsDefaultModule) {

+          newRegions.Add(new ORegion(module, "module"));

+        }

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

+          if (d is Dafny.DatatypeDecl) {

+            newRegions.Add(new ORegion(d, "datatype"));

+          } else {

+            Dafny.ClassDecl cl = (Dafny.ClassDecl)d;

+            if (!cl.IsDefaultClass) {

+              newRegions.Add(new ORegion(cl, "class"));

+            }

+            // do the class members (in particular, functions and methods)

+            foreach (Dafny.MemberDecl m in cl.Members) {

+              if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {

+                newRegions.Add(new ORegion(m, "function"));

+              } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

+                newRegions.Add(new ORegion(m, "method"));

+              }

+            }

+          }

+        }

+      }

+      _regions = newRegions;

+      _program = program;

+      return true;

+    }

+

+    class ORegion

+    {

+      public readonly int Start;

+      public readonly int Length;

+      public readonly string HoverText;

+      public ORegion(Dafny.Declaration decl, string kind) {

+        int startPosition = decl.BodyStartTok.pos + 1;  // skip the open-curly brace itself

+        int length = decl.BodyEndTok.pos - startPosition;

+        Start = startPosition;

+        Length = length;

+        HoverText = string.Format("body of {0} {1}", kind, decl.Name);

+      }

+    }

   }

 }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 9b0e5025..a9254621 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -7,7 +7,7 @@ using Microsoft.VisualStudio.Text.Classification;
 using Microsoft.VisualStudio.Text.Editor;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

-

+using Dafny = Microsoft.Dafny;

 

 namespace DafnyLanguage

 {

@@ -23,7 +23,8 @@ namespace DafnyLanguage
 

   public enum DafnyTokenKinds

   {

-    Keyword, Number, String, Comment

+    Keyword, Number, String, Comment,

+    TypeIdentifier, VariableIdentifier

   }

 

   public class DafnyTokenTag : ITag

@@ -34,6 +35,18 @@ namespace DafnyLanguage
       this.Kind = kind;

     }

   }

+  public class IdentifierDafnyTokenTag : DafnyTokenTag

+  {

+    public IdentifierDafnyTokenTag()

+      : base(DafnyTokenKinds.VariableIdentifier) {

+    }

+  }

+  public class TypeDafnyTokenTag : DafnyTokenTag

+  {

+    public TypeDafnyTokenTag()

+      : base(DafnyTokenKinds.TypeIdentifier) {

+    }

+  }

 

   internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>

   {

@@ -261,6 +274,7 @@ namespace DafnyLanguage
                 case "refines":

                 case "replaces":

                 case "requires":

+                case "result":

                 case "return":

                 case "returns":

                 case "seq":

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs b/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs
index 3677671a..03456c85 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs
@@ -13,7 +13,7 @@ using Microsoft.VisualStudio.Utilities;
 

 namespace DafnyLanguage

 {

-#if false

+#if LATER_MAYBE

   #region // (the current annoying) word highligher

   internal class HighlightWordTagger : ITagger<HighlightWordTag>

   {

@@ -60,8 +60,7 @@ namespace DafnyLanguage
       // If the new caret position is still within the current word (and on the same snapshot), we don't need to check it

       if (CurrentWord.HasValue

           && CurrentWord.Value.Snapshot == View.TextSnapshot

-          && point.Value >= CurrentWord.Value.Start

-          && point.Value <= CurrentWord.Value.End) {

+          && CurrentWord.Value.Start <= point.Value && point.Value <= CurrentWord.Value.End) {

         return;

       }