summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-07-15 17:43:38 -0700
committerGravatar wuestholz <unknown>2013-07-15 17:43:38 -0700
commit5e7d25359f1bd5425d5400019bfe08bcc87fb30f (patch)
treed5cf6b55f289518245115cfae103e6c79c7a7906 /Source/DafnyExtension
parent238e4c37734fa8d8baf1740cbe0fc145dd675bf8 (diff)
DafnyExtension: Added support for collecting additional information during resolution and displaying it.
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/ClassificationTagger.cs1
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs22
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs26
-rw-r--r--Source/DafnyExtension/TokenTagger.cs3
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