diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 47 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 86 |
2 files changed, 77 insertions, 56 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 722515ce..2d6d353c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -189,7 +189,7 @@ namespace Microsoft.Dafny { }
[Pure]
- public abstract string TypeName(ModuleDecl/*?*/ context);
+ public abstract string TypeName(ModuleDefinition/*?*/ context);
[Pure]
public override string ToString() {
return TypeName(null);
@@ -318,14 +318,14 @@ namespace Microsoft.Dafny { public class BoolType : BasicType {
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
return "bool";
}
}
public class IntType : BasicType {
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
return "int";
}
}
@@ -333,7 +333,7 @@ namespace Microsoft.Dafny { public class NatType : IntType
{
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
return "nat";
}
}
@@ -341,7 +341,7 @@ namespace Microsoft.Dafny { public class ObjectType : BasicType
{
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
return "object";
}
}
@@ -369,7 +369,7 @@ namespace Microsoft.Dafny { Contract.Requires(arg != null);
}
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "set<" + base.Arg.TypeName(context) + ">";
@@ -382,7 +382,7 @@ namespace Microsoft.Dafny { Contract.Requires(arg != null);
}
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "multiset<" + base.Arg.TypeName(context) + ">";
@@ -395,7 +395,7 @@ namespace Microsoft.Dafny { }
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
return "seq<" + base.Arg.TypeName(context) + ">";
@@ -412,7 +412,7 @@ namespace Microsoft.Dafny { get { return Arg; }
}
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Domain));
Contract.Assume(cce.IsPeerConsistent(Range));
@@ -538,10 +538,18 @@ namespace Microsoft.Dafny { }
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
-
- string s = Util.Comma(".", Path, i => i.val) + (Path.Count == 0 ? "" : ".") + Name; // TODO: use context
+ string s = "";
+ foreach (var t in Path) {
+ if (context != null && t == context.tok) {
+ // drop the prefix up to here
+ s = "";
+ } else {
+ s += t.val + ".";
+ }
+ }
+ s += Name;
if (TypeArgs.Count != 0) {
s += "<" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ">";
}
@@ -584,7 +592,7 @@ namespace Microsoft.Dafny { }
[Pure]
- public override string TypeName(ModuleDecl context) {
+ public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(T == null || cce.IsPeerConsistent(T));
@@ -977,6 +985,13 @@ namespace Microsoft.Dafny { return Module.Name + "." + Name;
}
}
+ public string FullNameInContext(ModuleDefinition context) {
+ if (Module == context) {
+ return Name;
+ } else {
+ return Module.Name + "." + Name;
+ }
+ }
public string FullCompileName {
get {
return Module.CompileName + "." + CompileName;
@@ -1154,6 +1169,12 @@ namespace Microsoft.Dafny { return EnclosingClass.FullName + "." + Name;
}
}
+ public string FullNameInContext(ModuleDefinition context) {
+ Contract.Requires(EnclosingClass != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ return EnclosingClass.FullNameInContext(context) + "." + Name;
+ }
public string FullCompileName {
get {
Contract.Requires(EnclosingClass != null);
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index bc35e33c..db91cd92 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -119,7 +119,7 @@ namespace DafnyLanguage foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors) {
if (dtor != null) {
- IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true);
+ IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true, module);
}
}
}
@@ -129,33 +129,33 @@ namespace DafnyLanguage if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
- IdRegion.Add(newRegions, p.tok, p, true);
+ IdRegion.Add(newRegions, p.tok, p, true, module);
}
- f.Req.ForEach(e => ExprRegions(e, newRegions));
- f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true));
- f.Ens.ForEach(e => ExprRegions(e, newRegions));
- f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));
+ 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));
if (f.Body != null) {
- ExprRegions(f.Body, newRegions);
+ ExprRegions(f.Body, newRegions, module);
}
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
- IdRegion.Add(newRegions, p.tok, p, true);
+ IdRegion.Add(newRegions, p.tok, p, true, module);
}
foreach (var p in m.Outs) {
- IdRegion.Add(newRegions, p.tok, p, true);
+ IdRegion.Add(newRegions, p.tok, p, true, module);
}
- m.Req.ForEach(e => ExprRegions(e.E, newRegions));
- m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true));
- m.Ens.ForEach(e => ExprRegions(e.E, newRegions));
- m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));
+ 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));
if (m.Body != null) {
- StatementRegions(m.Body, newRegions);
+ StatementRegions(m.Body, newRegions, module);
}
} else if (member is Field) {
var fld = (Field)member;
- IdRegion.Add(newRegions, fld.tok, fld, "field", true);
+ IdRegion.Add(newRegions, fld.tok, fld, "field", true, module);
}
}
}
@@ -167,91 +167,91 @@ namespace DafnyLanguage return true;
}
- static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions) {
+ static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, ModuleDefinition module) {
Contract.Requires(fe != null);
Contract.Requires(regions != null);
if (descendIntoExpressions) {
- ExprRegions(fe.E, regions);
+ ExprRegions(fe.E, regions, module);
}
if (fe.Field != null) {
- IdRegion.Add(regions, fe.tok, fe.Field, "field", false);
+ IdRegion.Add(regions, fe.tok, fe.Field, "field", false, module);
}
}
- static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions) {
+ static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {
Contract.Requires(expr != null);
Contract.Requires(regions != null);
if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- IdRegion.Add(regions, e.tok, e.Var, false);
+ IdRegion.Add(regions, e.tok, e.Var, false, module);
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
- IdRegion.Add(regions, e.tok, e.Field, "field", false);
+ IdRegion.Add(regions, e.tok, e.Field, "field", false, module);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
- IdRegion.Add(regions, bv.tok, bv, true);
+ IdRegion.Add(regions, 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));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, 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));
+ e.Operands.ForEach(ee => ExprRegions(ee, regions, module));
return; // return here, so as to avoid doing the subexpressions below
}
foreach (var ee in expr.SubExpressions) {
- ExprRegions(ee, regions);
+ ExprRegions(ee, regions, module);
}
}
- static void StatementRegions(Statement stmt, List<IdRegion> regions) {
+ static void StatementRegions(Statement stmt, List<IdRegion> regions, ModuleDefinition module) {
Contract.Requires(stmt != null);
Contract.Requires(regions != 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 lhs in s.Lhss) {
- IdRegion.Add(regions, lhs.Tok, lhs, true);
+ IdRegion.Add(regions, lhs.Tok, lhs, true, module);
}
if (s.Update is UpdateStmt) {
var upd = (UpdateStmt)s.Update;
foreach (var rhs in upd.Rhss) {
foreach (var ee in rhs.SubExpressions) {
- ExprRegions(ee, regions);
+ ExprRegions(ee, regions, module);
}
}
} else {
var upd = (AssignSuchThatStmt)s.Update;
- ExprRegions(upd.Expr, regions);
+ ExprRegions(upd.Expr, regions, module);
}
// we're done, so don't do the sub-statements/expressions again
return;
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
- IdRegion.Add(regions, s.Tok, s, true);
+ IdRegion.Add(regions, s.Tok, s, true, module);
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
- s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, 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));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;
if (s.Mod.Expressions != null) {
- s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false));
+ s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));
}
}
foreach (var ee in stmt.SubExpressions) {
- ExprRegions(ee, regions);
+ ExprRegions(ee, regions, module);
}
foreach (var ss in stmt.SubStatements) {
- StatementRegions(ss, regions);
+ StatementRegions(ss, regions, module);
}
}
@@ -262,25 +262,25 @@ namespace DafnyLanguage public readonly string HoverText;
public readonly bool IsDefinition;
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition) {
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
if (!(tok is AutoGeneratedToken)) {
- regions.Add(new IdRegion(tok, v, isDefinition));
+ regions.Add(new IdRegion(tok, v, isDefinition, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
if (!(tok is AutoGeneratedToken)) {
- regions.Add(new IdRegion(tok, decl, kind, isDefinition));
+ regions.Add(new IdRegion(tok, decl, kind, isDefinition, context));
}
}
- private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {
+ private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
Contract.Requires(tok != null);
Contract.Requires(v != null);
Start = tok.pos;
@@ -294,16 +294,16 @@ namespace DafnyLanguage var formal = (Formal)v;
kind = formal.InParam ? "in-parameter" : "out-parameter";
}
- HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(null/*TODO: use context*/), v.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
- private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
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.TypeName(null/*TODO: use context*/), decl.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), decl.Type.TypeName(context), decl.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
}
|