diff options
Diffstat (limited to 'Source/DafnyExtension/IdentifierTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 167 |
1 files changed, 99 insertions, 68 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index 3bb8f01c..998a2d7f 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -15,7 +15,6 @@ using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Utilities;
using Bpl = Microsoft.Boogie;
-
namespace DafnyLanguage
{
@@ -136,9 +135,8 @@ 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 info in program.reporter.AllMessages[ErrorLevel.Info]) {
+ IdRegion.Add(newRegions, program, info.token, info.message, info.token.val.Length);
}
foreach (var module in program.Modules) {
@@ -151,73 +149,75 @@ namespace DafnyLanguage foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors) {
if (dtor.CorrespondingFormal.HasName) {
- IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);
+ IdRegion.Add(newRegions, program, dtor.tok, dtor, null, "destructor", true, module);
}
}
}
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
foreach (var p in iter.Ins) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
foreach (var p in iter.Outs) {
- IdRegion.Add(newRegions, p.tok, p, true, "yield-parameter", module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, "yield-parameter", module);
}
- iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, module));
+ iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, program, module));
if (!((ICallable)iter).InferredDecreases) {
- iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
}
if (iter.Body != null) {
- StatementRegions(iter.Body, newRegions, module);
+ StatementRegions(iter.Body, newRegions, program, module);
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
- if (member is Function) {
+ if (Attributes.Contains(member.Attributes, "auto_generated")) {
+ // do nothing
+ } else if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
- f.Req.ForEach(e => ExprRegions(e, newRegions, module));
- f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- f.Ens.ForEach(e => ExprRegions(e, newRegions, module));
- f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ f.Req.ForEach(e => ExprRegions(e, newRegions, program, module));
+ f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ f.Ens.ForEach(e => ExprRegions(e, newRegions, program, module));
+ f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
if (f.Body != null) {
- ExprRegions(f.Body, newRegions, module);
+ ExprRegions(f.Body, newRegions, program, module);
}
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
foreach (var p in m.Outs) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
- m.Req.ForEach(e => ExprRegions(e.E, newRegions, module));
- m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module));
- m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ m.Req.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ m.Ens.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
if (m.Body != null) {
- StatementRegions(m.Body, newRegions, module);
+ StatementRegions(m.Body, newRegions, program, module);
}
} else if (member is SpecialField) {
// do nothing
} else if (member is Field) {
var fld = (Field)member;
- IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
+ IdRegion.Add(newRegions, program, fld.tok, fld, null, "field", true, module);
}
}
} else if (d is NewtypeDecl) {
var dd = (NewtypeDecl)d;
if (dd.Var != null) {
- IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module);
- ExprRegions(dd.Constraint, newRegions, module);
+ IdRegion.Add(newRegions, program, dd.Var.tok, dd.Var, true, module);
+ ExprRegions(dd.Constraint, newRegions, program, module);
}
}
}
@@ -228,67 +228,80 @@ namespace DafnyLanguage return true;
}
- static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, ModuleDefinition module) {
+ static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(fe != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (descendIntoExpressions) {
- ExprRegions(fe.E, regions, module);
+ ExprRegions(fe.E, regions, prog, module);
}
if (fe.Field != null) {
Microsoft.Dafny.Type showType = null; // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)
- IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);
+ IdRegion.Add(regions, prog, fe.tok, fe.Field, showType, "field", false, module);
}
}
- static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {
+ static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(expr != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (expr is AutoGeneratedExpression) {
// do nothing
return;
} else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- IdRegion.Add(regions, e.tok, e.Var, false, module);
+ IdRegion.Add(regions, prog, e.tok, e.Var, false, module);
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
var field = e.Member as Field;
if (field != null) {
- IdRegion.Add(regions, e.tok, field, e.Type, "field", false, module);
+ IdRegion.Add(regions, prog, e.tok, field, e.Type, "field", false, module);
}
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var bv in e.BoundVars) {
- IdRegion.Add(regions, bv.tok, bv, true, module);
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
}
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
- IdRegion.Add(regions, bv.tok, bv, true, module);
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
foreach (var kase in e.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach(Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
// Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)
- e.Operands.ForEach(ee => ExprRegions(ee, regions, module));
+ e.Operands.ForEach(ee => ExprRegions(ee, regions, prog, module));
return; // return here, so as to avoid doing the subexpressions below
}
foreach (var ee in expr.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
}
- static void StatementRegions(Statement stmt, List<IdRegion> regions, ModuleDefinition module) {
+ static void StatementRegions(Statement stmt, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(stmt != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
// Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)
foreach (var local in s.Locals) {
- IdRegion.Add(regions, local.Tok, local, true, module);
+ IdRegion.Add(regions, prog, local.Tok, local, true, module);
}
if (s.Update == null) {
// the VarDeclStmt has no associated assignment
@@ -296,48 +309,58 @@ namespace DafnyLanguage var upd = (UpdateStmt)s.Update;
foreach (var rhs in upd.Rhss) {
foreach (var ee in rhs.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
}
} else {
var upd = (AssignSuchThatStmt)s.Update;
- ExprRegions(upd.Expr, regions, module);
+ ExprRegions(upd.Expr, regions, prog, module);
}
// we're done, so don't do the sub-statements/expressions again
return;
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, prog, bv.tok, bv, true, module));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach (Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;
if (s.Mod.Expressions != null) {
- s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));
+ s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, prog, module));
}
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
// skip the last line, which is just a duplicate anyway
for (int i = 0; i < s.Lines.Count - 1; i++) {
- ExprRegions(s.Lines[i], regions, module);
+ ExprRegions(s.Lines[i], regions, prog, module);
}
foreach (var ss in stmt.SubStatements) {
- StatementRegions(ss, regions, module);
+ StatementRegions(ss, regions, prog, module);
}
return;
}
foreach (var ee in stmt.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
foreach (var ss in stmt.SubStatements) {
- StatementRegions(ss, regions, module);
+ StatementRegions(ss, regions, prog, module);
}
}
- class IdRegion
+ class IdRegion : DafnyRegion
{
public readonly int Start;
public readonly int Length;
@@ -346,40 +369,39 @@ namespace DafnyLanguage public readonly OccurrenceKind Kind;
public readonly IVariable Variable;
- static bool SurfaceSyntaxToken(Bpl.IToken tok) {
- Contract.Requires(tok != null);
- return !(tok is TokenWrapper);
- }
-
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- Add(regions, tok, v, isDefinition, null, context);
+ Add(regions, prog, tok, v, isDefinition, null, context);
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, v, isDefinition, kind, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, string text, int length) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(text != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));
}
}
@@ -433,6 +455,15 @@ namespace DafnyLanguage }
}
+ public abstract class DafnyRegion
+ {
+ public static bool InMainFileAndUserDefined(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
+ Contract.Requires(prog != null);
+ Contract.Requires(tok != null);
+ return object.Equals(prog.FullName, tok.filename) && !(tok is AutoGeneratedToken);
+ }
+ }
+
#endregion
}
|