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

5 files changed, 101 insertions, 93 deletions

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;

       }