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

6 files changed, 69 insertions, 5 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e1305ae3..1d041ded 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -25,7 +25,9 @@ namespace Microsoft.Dafny {
                                                      // purposes of translation and compilation.

     public List<ModuleDefinition> CompileModules; // filled in during resolution.

                                                   // Contains the definitions to be used for compilation.

-                                    

+

+    List<AdditionalInformation> _additionalInformation = new List<AdditionalInformation>();

+    public List<AdditionalInformation> AdditionalInformation { get { return _additionalInformation; } }

     public readonly ModuleDecl DefaultModule;

     public readonly ModuleDefinition DefaultModuleDef;

     public readonly BuiltIns BuiltIns;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6cf687f0..c4f784f1 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -62,6 +62,13 @@ namespace Microsoft.Dafny
     }

   }

 

+  public struct AdditionalInformation

+  {

+    public IToken Token;

+    public string Text;

+    public int Length;

+  }

+

   public class Resolver : ResolutionErrorReporter

   {

     readonly BuiltIns builtIns;

@@ -70,6 +77,16 @@ namespace Microsoft.Dafny
     //Dictionary<string, ModuleDecl> importedNames; // the imported modules, as a map.

     ModuleSignature moduleInfo = null;

 

+    public Action<AdditionalInformation> AdditionalInformationReporter;

+

+    internal void ReportAddionalInformation(IToken token, string text, int length)

+    {

+      if (AdditionalInformationReporter != null)

+      {

+        AdditionalInformationReporter(new AdditionalInformation { Token = token, Text = text, Length = length });

+      }

+    }

+

     class AmbiguousTopLevelDecl : TopLevelDecl  // only used with "classes"

     {

       readonly TopLevelDecl A;

@@ -1532,6 +1549,7 @@ namespace Microsoft.Dafny
               var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);

               if (status != TailRecursionStatus.NotTailRecursive) {

                 m.IsTailRecursive = true;

+                ReportAddionalInformation(m.tok, "is tail recursive", m.Name.Length);

               }

             }

           }

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