Dafny: added Statement.SubExpressions getter

DafnyExtension: added hover text for identifiers

5 files changed, 406 insertions, 7 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
index 7e64dd1d..09835ac9 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs
@@ -50,7 +50,7 @@ namespace DafnyLanguage
       _typeMap[DafnyTokenKinds.String] = standards.StringLiteral;

       _typeMap[DafnyTokenKinds.Comment] = standards.Comment;

       _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;

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

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

     }

 

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

@@ -82,16 +82,16 @@ namespace DafnyLanguage
   /// Defines an editor format for user-defined type.

   /// </summary>

   [Export(typeof(EditorFormatDefinition))]

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

-  [Name("Dafny user type")]

+  [ClassificationType(ClassificationTypeNames = "Dafny identifier")]

+  [Name("Dafny identifier")]

   [UserVisible(true)]

   //set the priority to be after the default classifiers

   [Order(Before = Priority.Default)]

   internal sealed class DafnyTypeFormat : ClassificationFormatDefinition

   {

     public DafnyTypeFormat() {

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

-      this.ForegroundColor = Colors.Coral;

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

+      this.ForegroundColor = Colors.CornflowerBlue;

     }

   }

 

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

     /// </summary>

     [Export(typeof(ClassificationTypeDefinition))]

-    [Name("Dafny user type")]

+    [Name("Dafny identifier")]

     internal static ClassificationTypeDefinition UserType = null;

   }

 }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index cfa7a070..66370dec 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -128,6 +128,8 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

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

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

     <Compile Include="ProgressMargin.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs
new file mode 100644
index 00000000..de0721ec
--- /dev/null
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs
@@ -0,0 +1,134 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Windows.Input;

+using Microsoft.VisualStudio.Language.Intellisense;

+using System.Collections.ObjectModel;

+using Microsoft.VisualStudio.Text;

+using Microsoft.VisualStudio.Text.Editor;

+using Microsoft.VisualStudio.Text.Tagging;

+using System.ComponentModel.Composition;

+using Microsoft.VisualStudio.Utilities;

+using System.Diagnostics.Contracts;

+

+

+namespace DafnyLanguage

+{

+  [Export(typeof(IQuickInfoSourceProvider))]

+  [ContentType("dafny")]

+  [Name("Dafny QuickInfo")]

+  class OokQuickInfoSourceProvider : IQuickInfoSourceProvider

+  {

+    [Import]

+    IBufferTagAggregatorFactoryService aggService = null;

+

+    public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) {

+      return new OokQuickInfoSource(textBuffer, aggService.CreateTagAggregator<DafnyTokenTag>(textBuffer));

+    }

+  }

+

+  class OokQuickInfoSource : IQuickInfoSource

+  {

+    private ITagAggregator<DafnyTokenTag> _aggregator;

+    private ITextBuffer _buffer;

+    private bool _disposed = false;

+

+

+    public OokQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {

+      _aggregator = aggregator;

+      _buffer = buffer;

+    }

+

+    public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan) {

+      applicableToSpan = null;

+

+      if (_disposed)

+        throw new ObjectDisposedException("TestQuickInfoSource");

+

+      var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot);

+

+      if (triggerPoint == null)

+        return;

+

+      foreach (IMappingTagSpan<DafnyTokenTag> curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) {

+        var s = curTag.Tag.HoverText;

+        if (s != null) {

+          var tagSpan = curTag.Span.GetSpans(_buffer).First();

+          applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive);

+          quickInfoContent.Add(s);

+        }

+      }

+    }

+

+    public void Dispose() {

+      _disposed = true;

+    }

+  }

+  // --------------------------------- QuickInfo controller ------------------------------------------

+

+  [Export(typeof(IIntellisenseControllerProvider))]

+  [Name("Dafny QuickInfo controller")]

+  [ContentType("dafny")]

+  class DafnyQuickInfoControllerProvider : IIntellisenseControllerProvider

+  {

+    [Import]

+    internal IQuickInfoBroker QuickInfoBroker { get; set; }

+

+    public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList<ITextBuffer> subjectBuffers) {

+      return new DafnyQuickInfoController(textView, subjectBuffers, this);

+    }

+  }

+

+  class DafnyQuickInfoController : IIntellisenseController

+  {

+    private ITextView _textView;

+    private IList<ITextBuffer> _subjectBuffers;

+    private DafnyQuickInfoControllerProvider _componentContext;

+

+    private IQuickInfoSession _session;

+

+    internal DafnyQuickInfoController(ITextView textView, IList<ITextBuffer> subjectBuffers, DafnyQuickInfoControllerProvider componentContext) {

+      _textView = textView;

+      _subjectBuffers = subjectBuffers;

+      _componentContext = componentContext;

+

+      _textView.MouseHover += this.OnTextViewMouseHover;

+    }

+

+    public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) {

+    }

+

+    public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) {

+    }

+

+    public void Detach(ITextView textView) {

+      if (_textView == textView) {

+        _textView.MouseHover -= OnTextViewMouseHover;

+        _textView = null;

+      }

+    }

+

+    void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) {

+      SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position));

+

+      if (point != null) {

+        ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive);

+

+        // Find the broker for this buffer

+        if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) {

+          _session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true);

+          _session.Start();

+        }

+      }

+    }

+

+    SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) {

+      return _textView.BufferGraph.MapDownToFirstMatch(

+        topPosition,

+        PointTrackingMode.Positive,

+        snapshot => _subjectBuffers.Contains(snapshot.TextBuffer),

+        PositionAffinity.Predecessor);

+    }

+  }

+}

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
new file mode 100644
index 00000000..ab2bc790
--- /dev/null
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -0,0 +1,264 @@
+//***************************************************************************

+// Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

+// This code released under the terms of the 

+// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)

+//***************************************************************************

+using EnvDTE;

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.ComponentModel.Composition;

+using System.Windows.Threading;

+using Microsoft.VisualStudio.Shell;

+using Microsoft.VisualStudio.Shell.Interop;

+using Microsoft.VisualStudio.Text;

+using Microsoft.VisualStudio.Text.Classification;

+using Microsoft.VisualStudio.Text.Editor;

+using Microsoft.VisualStudio.Text.Tagging;

+using Microsoft.VisualStudio.Text.Projection;

+using Microsoft.VisualStudio.Utilities;

+using System.Diagnostics.Contracts;

+using Bpl = Microsoft.Boogie;

+using Dafny = Microsoft.Dafny;

+

+namespace DafnyLanguage

+{

+  [Export(typeof(ITaggerProvider))]

+  [ContentType("dafny")]

+  [TagType(typeof(DafnyTokenTag))]

+  internal sealed class IdentifierTaggerProvider : ITaggerProvider

+  {

+    [Import]

+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;

+

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

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

+      // create a single tagger for each buffer.

+      Func<ITagger<T>> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger<T>; };

+      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);

+    }

+  }

+

+  /// <summary>

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

+  /// </summary>

+  internal sealed class IdentifierTagger : ITagger<DafnyTokenTag>

+  {

+    ITextBuffer _buffer;

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

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

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

+    ITagAggregator<DafnyResolverTag> _aggregator;

+

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

+      _buffer = buffer;

+      _snapshot = _buffer.CurrentSnapshot;

+      _aggregator = tagAggregator;

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

+    }

+

+    /// <summary>

+    /// Find the Error tokens in the set of all tokens and create an ErrorTag for each

+    /// </summary>

+    public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

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

+      // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.)

+      // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans.

+      // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the

+      // first spand and the .End of the last span:

+      var startPoint = spans[0].Start;

+      var endPoint = spans[spans.Count - 1].End;

+

+      // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags.  We need to translate

+      // these back into the most recent snapshot that we've computed regions for, namely _snapshot.

+      var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive);

+      int start = entire.Start;

+      int end = entire.End;

+      foreach (var r in _regions) {

+        if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {

+          yield return new TagSpan<DafnyTokenTag>(

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

+            new DafnyTokenTag(r.IsDefinition ? DafnyTokenKinds.VariableIdentifierDefinition : DafnyTokenKinds.VariableIdentifier, r.HoverText));

+        }

+      }

+    }

+

+    // 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 (!ComputeIdentifierRegions(r._program, r._snapshot))

+          return;  // no new regions

+

+        var chng = TagsChanged;

+        if (chng != null) {

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

+          if (spans.Count > 0) {

+            SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

+            chng(this, new SnapshotSpanEventArgs(span));

+          }

+        }

+      }

+    }

+

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

+      Contract.Requires(snapshot != null);

+

+      if (program == _program)

+        return false;  // no new regions

+

+      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)) {

+            continue;

+          }

+          if (d is Dafny.DatatypeDecl) {

+            var dt = (Dafny.DatatypeDecl)d;

+            foreach (var ctor in dt.Ctors) {

+              foreach (var dtor in ctor.Destructors) {

+                if (dtor != null) {

+                  newRegions.Add(new IdRegion(dtor.tok, dtor, "destructor", true));

+                }

+              }

+            }

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

+            var cl = (Dafny.ClassDecl)d;

+            foreach (var member in cl.Members) {

+              if (!HasBodyTokens(member)) {

+                continue;

+              }

+              if (member is Dafny.Function) {

+                var f = (Dafny.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.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;

+                foreach (var p in m.Ins) {

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

+                }

+                foreach (var p in m.Outs) {

+                  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.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;

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

+              }

+            }

+          }

+        }

+      }

+      _snapshot = snapshot;

+      _regions = newRegions;

+      _program = program;

+      return true;

+    }

+

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

+      Contract.Requires(expr != null);

+      Contract.Requires(regions != null);

+      if (expr is Dafny.IdentifierExpr) {

+        var e = (Dafny.IdentifierExpr)expr;

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

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

+        var e = (Dafny.FieldSelectExpr)expr;

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

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

+        var e = (Dafny.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;

+        foreach (var kase in e.Cases) {

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

+        }

+      }

+      foreach (var ee in expr.SubExpressions) {

+        ExprRegions(ee, regions);

+      }

+    }

+

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

+      Contract.Requires(stmt != null);

+      Contract.Requires(regions != null);

+      if (stmt is Dafny.VarDecl) {

+        var s = (Dafny.VarDecl)stmt;

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

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

+        var s = (Dafny.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;

+        foreach (var kase in s.Cases) {

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

+        }

+      }

+      foreach (var ee in stmt.SubExpressions) {

+        ExprRegions(ee, regions);

+      }

+      foreach (var ss in stmt.SubStatements) {

+        StatementRegions(ss, regions);

+      }

+    }

+

+    bool HasBodyTokens(Dafny.Declaration decl) {

+      Contract.Requires(decl != null);

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

+    }

+

+    class IdRegion

+    {

+      public readonly int Start;

+      public readonly int Length;

+      public readonly string HoverText;

+      public readonly bool IsDefinition;

+      public IdRegion(Bpl.IToken tok, Dafny.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) {

+          kind = "local variable";

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

+          kind = "bound variable";

+        } else {

+          var formal = (Dafny.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) {

+        Contract.Requires(tok != null);

+        Contract.Requires(decl != null);

+        Contract.Requires(kind != null);

+        Start = tok.pos;

+        Length = decl.Name.Length;

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

+        IsDefinition = isDefinition;

+      }

+    }

+  }

+

+}

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index 10bb36e1..2017cfaa 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -186,7 +186,6 @@ namespace DafnyLanguage
       _errorProvider.Tasks.Clear();

       foreach (var err in AllErrors()) {

         ErrorTask task = new ErrorTask() {

-          // CanDelete = true,

           Category = TaskCategory.BuildCompile,

           ErrorCategory = CategoryConversion(err.Category),

           Text = err.Message,