DafnyExtension: Added support for collecting additional information during resolution and displaying it.

4 files changed, 48 insertions, 4 deletions

diff --git a/Source/DafnyExtension/ClassificationTagger.cs b/Source/DafnyExtension/ClassificationTagger.cs
index b3bafa11..5be982ed 100644
--- a/Source/DafnyExtension/ClassificationTagger.cs
+++ b/Source/DafnyExtension/ClassificationTagger.cs
@@ -59,6 +59,7 @@ namespace DafnyLanguage
       _typeMap[DafnyTokenKind.String] = standards.StringLiteral;

       _typeMap[DafnyTokenKind.Comment] = standards.Comment;

       _typeMap[DafnyTokenKind.VariableIdentifier] = standards.Identifier;

+      _typeMap[DafnyTokenKind.AdditionalInformation] = standards.Other;

       _typeMap[DafnyTokenKind.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");

 

       if (!DafnyMenuWasInitialized)

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index ade7c332..b4f44df0 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -1,8 +1,11 @@
-using System.Collections.Concurrent;

+using System;

+using System.Collections.Concurrent;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.IO;

+using System.Linq;

 using Microsoft.Boogie;

+using Microsoft.Dafny;

 using Microsoft.VisualStudio.Text;

 using Bpl = Microsoft.Boogie;

 using Dafny = Microsoft.Dafny;

@@ -98,11 +101,12 @@ namespace DafnyLanguage
         return false;

       Dafny.Program program = new Dafny.Program(_filename, module, builtIns);

 

-      Dafny.Resolver r = new VSResolver(program, this);

+      var r = new VSResolver(program, this);

       r.ResolveProgram(program);

       if (r.ErrorCount != 0)

         return false;

 

+      program.AdditionalInformation.AddRange(r.AdditionalInformation);

       _program = program;

       return true;  // success

     }

@@ -134,10 +138,24 @@ namespace DafnyLanguage
     class VSResolver : Dafny.Resolver

     {

       DafnyDriver dd;

+      Dictionary<IToken, HashSet<AdditionalInformation>> _additionalInformation = new Dictionary<IToken, HashSet<AdditionalInformation>>();

+      public List<AdditionalInformation> AdditionalInformation { get { return _additionalInformation.Values.SelectMany(i => i).ToList(); } }

+

       public VSResolver(Dafny.Program program, DafnyDriver dd)

         : base(program) {

         this.dd = dd;

+

+        AdditionalInformationReporter =

+          (addinfo)

+            =>

+            {

+              if (!_additionalInformation.ContainsKey(addinfo.Token)) {

+                _additionalInformation.Add(addinfo.Token, new HashSet<AdditionalInformation>());

+              }

+              _additionalInformation[addinfo.Token].Add(addinfo);

+            };

       }

+

       public override void Error(Bpl.IToken tok, string msg, params object[] args) {

         string s = string.Format(msg, args);

         dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 49c7bb01..e334271f 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -87,6 +87,8 @@ namespace DafnyLanguage
               kind = DafnyTokenKind.VariableIdentifierDefinition; break;

             case IdRegion.OccurrenceKind.WildDefinition:

               kind = DafnyTokenKind.Keyword; break;

+            case IdRegion.OccurrenceKind.AdditionalInformation:

+              kind = DafnyTokenKind.AdditionalInformation; break;

             default:

               Contract.Assert(false);  // unexpected OccurrenceKind

               goto case IdRegion.OccurrenceKind.Use;  // to please compiler

@@ -134,6 +136,11 @@ namespace DafnyLanguage
 

       List<IdRegion> newRegions = new List<IdRegion>();

 

+      foreach (var addInfo in program.AdditionalInformation)

+      {

+        IdRegion.Add(newRegions, addInfo.Token, addInfo.Text, addInfo.Length);

+      }

+

       foreach (var module in program.Modules) {

         if (module.IsFacade) {

           continue;

@@ -316,7 +323,7 @@ namespace DafnyLanguage
       public readonly int Start;

       public readonly int Length;

       public readonly string HoverText;

-      public enum OccurrenceKind { Use, Definition, WildDefinition }

+      public enum OccurrenceKind { Use, Definition, WildDefinition, AdditionalInformation }

       public readonly OccurrenceKind Kind;

 

       static bool SurfaceSyntaxToken(Bpl.IToken tok) {

@@ -348,6 +355,15 @@ namespace DafnyLanguage
         }

       }

 

+      public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {

+        Contract.Requires(regions != null);

+        Contract.Requires(tok != null);

+        Contract.Requires(text != null);

+        if (SurfaceSyntaxToken(tok)) {

+          regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

+        }

+      }

+

       private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

@@ -385,6 +401,14 @@ namespace DafnyLanguage
           decl.IsUserMutable || decl is DatatypeDestructor ? "" : decl.IsMutable ? " non-assignable " : "immutable ");

         Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition;

       }

+

+      private IdRegion(Bpl.IToken tok, OccurrenceKind occurrenceKind, string info, int length)

+      {

+        this.Start = tok.pos;

+        this.Length = length;

+        this.Kind = occurrenceKind;

+        this.HoverText = info;

+      }

     }

   }

 

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 4980bf0a..abe67751 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -30,7 +30,8 @@ namespace DafnyLanguage
   public enum DafnyTokenKind

   {

     Keyword, Number, String, Comment,

-    VariableIdentifier, VariableIdentifierDefinition

+    VariableIdentifier, VariableIdentifierDefinition,

+    AdditionalInformation

   }

 

   public class DafnyTokenTag : ITag