summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/DafnyAst.cs41
-rw-r--r--Source/Dafny/Rewriter.cs26
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs55
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs2
4 files changed, 80 insertions, 44 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 66ad49e9..722515ce 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -188,6 +188,13 @@ namespace Microsoft.Dafny {
}
}
+ [Pure]
+ public abstract string TypeName(ModuleDecl/*?*/ context);
+ [Pure]
+ public override string ToString() {
+ return TypeName(null);
+ }
+
/// <summary>
/// Return the most constrained version of "this".
/// </summary>
@@ -311,14 +318,14 @@ namespace Microsoft.Dafny {
public class BoolType : BasicType {
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
return "bool";
}
}
public class IntType : BasicType {
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
return "int";
}
}
@@ -326,7 +333,7 @@ namespace Microsoft.Dafny {
public class NatType : IntType
{
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
return "nat";
}
}
@@ -334,7 +341,7 @@ namespace Microsoft.Dafny {
public class ObjectType : BasicType
{
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
return "object";
}
}
@@ -362,10 +369,10 @@ namespace Microsoft.Dafny {
Contract.Requires(arg != null);
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
- return "set<" + base.Arg + ">";
+ return "set<" + base.Arg.TypeName(context) + ">";
}
}
@@ -375,10 +382,10 @@ namespace Microsoft.Dafny {
Contract.Requires(arg != null);
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
- return "multiset<" + base.Arg + ">";
+ return "multiset<" + base.Arg.TypeName(context) + ">";
}
}
@@ -388,10 +395,10 @@ namespace Microsoft.Dafny {
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Arg));
- return "seq<" + base.Arg + ">";
+ return "seq<" + base.Arg.TypeName(context) + ">";
}
}
public class MapType : CollectionType
@@ -405,11 +412,11 @@ namespace Microsoft.Dafny {
get { return Arg; }
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(cce.IsPeerConsistent(Domain));
Contract.Assume(cce.IsPeerConsistent(Range));
- return "map<" + Domain +", " + Range + ">";
+ return "map<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">";
}
}
@@ -531,12 +538,12 @@ namespace Microsoft.Dafny {
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
- string s = Util.Comma(".", Path, i => i.val) + (Path.Count == 0 ? "" : ".") + Name;
+ string s = Util.Comma(".", Path, i => i.val) + (Path.Count == 0 ? "" : ".") + Name; // TODO: use context
if (TypeArgs.Count != 0) {
- s += "<" + Util.Comma(",", TypeArgs, ty => ty.ToString()) + ">";
+ s += "<" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ">";
}
return s;
}
@@ -577,11 +584,11 @@ namespace Microsoft.Dafny {
}
[Pure]
- public override string ToString() {
+ public override string TypeName(ModuleDecl context) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(T == null || cce.IsPeerConsistent(T));
- return T == null ? "?" : T.ToString();
+ return T == null ? "?" : T.TypeName(context);
}
public override bool SupportsEquality {
get {
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index d88830a7..c95be2f4 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -21,6 +21,15 @@ namespace Microsoft.Dafny
}
}
+ public class AutoGeneratedToken : TokenWrapper
+ {
+ public AutoGeneratedToken(Boogie.IToken wrappedToken)
+ : base(wrappedToken)
+ {
+ Contract.Requires(wrappedToken != null);
+ }
+ }
+
/// <summary>
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
/// into a class. From the user's perspective, what needs to be done is simply:
@@ -75,7 +84,7 @@ namespace Microsoft.Dafny
// ...unless a field with that name is already present
if (!cl.Members.Exists(member => member is Field && member.Name == "Repr")) {
Type ty = new SetType(new ObjectType());
- cl.Members.Add(new Field(cl.tok, "Repr", true, ty, null));
+ cl.Members.Add(new Field(new AutoGeneratedToken(cl.tok), "Repr", true, ty, null));
}
foreach (var member in cl.Members) {
@@ -83,7 +92,7 @@ namespace Microsoft.Dafny
if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
continue;
}
- var tok = member.tok;
+ Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
// reads this;
@@ -158,15 +167,16 @@ namespace Microsoft.Dafny
}
Contract.Assert(ReprField != null); // we expect there to be a "Repr" field, since we added one in PreResolve
- Type ty = new UserDefinedType(cl.tok, cl.Name, cl, new List<Type>());
- var self = new ThisExpr(cl.tok);
+ Boogie.IToken clTok = new AutoGeneratedToken(cl.tok);
+ Type ty = new UserDefinedType(clTok, cl.Name, cl, new List<Type>());
+ var self = new ThisExpr(clTok);
self.Type = ty;
- var implicitSelf = new ImplicitThisExpr(cl.tok);
+ var implicitSelf = new ImplicitThisExpr(clTok);
implicitSelf.Type = ty;
- var Repr = new FieldSelectExpr(cl.tok, implicitSelf, "Repr");
+ var Repr = new FieldSelectExpr(clTok, implicitSelf, "Repr");
Repr.Field = ReprField;
Repr.Type = ReprField.Type;
- var cNull = new LiteralExpr(cl.tok);
+ var cNull = new LiteralExpr(clTok);
cNull.Type = new ObjectType();
foreach (var member in cl.Members) {
@@ -174,7 +184,7 @@ namespace Microsoft.Dafny
if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
continue;
}
- var tok = member.tok;
+ Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
if (valid.IsGhost && valid.ResultType is BoolType) {
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 0304dd20..bc35e33c 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) {
- newRegions.Add(new IdRegion(dtor.tok, dtor, "destructor", true));
+ IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true);
}
}
}
@@ -129,7 +129,7 @@ namespace DafnyLanguage
if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
f.Req.ForEach(e => ExprRegions(e, newRegions));
f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true));
@@ -141,10 +141,10 @@ namespace DafnyLanguage
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
foreach (var p in m.Outs) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
m.Req.ForEach(e => ExprRegions(e.E, newRegions));
m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true));
@@ -155,7 +155,7 @@ namespace DafnyLanguage
}
} else if (member is Field) {
var fld = (Field)member;
- newRegions.Add(new IdRegion(fld.tok, fld, "field", true));
+ IdRegion.Add(newRegions, fld.tok, fld, "field", true);
}
}
}
@@ -174,7 +174,7 @@ namespace DafnyLanguage
ExprRegions(fe.E, regions);
}
if (fe.Field != null) {
- regions.Add(new IdRegion(fe.tok, fe.Field, "field", false));
+ IdRegion.Add(regions, fe.tok, fe.Field, "field", false);
}
}
@@ -183,19 +183,19 @@ namespace DafnyLanguage
Contract.Requires(regions != null);
if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- regions.Add(new IdRegion(e.tok, e.Var, false));
+ IdRegion.Add(regions, e.tok, e.Var, false);
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
- regions.Add(new IdRegion(e.tok, e.Field, "field", false));
+ IdRegion.Add(regions, e.tok, e.Field, "field", false);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
- regions.Add(new IdRegion(bv.tok, bv, true));
+ IdRegion.Add(regions, bv.tok, bv, true);
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
foreach (var kase in e.Cases) {
- kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
}
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
@@ -215,7 +215,7 @@ namespace DafnyLanguage
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) {
- regions.Add(new IdRegion(lhs.Tok, lhs, true));
+ IdRegion.Add(regions, lhs.Tok, lhs, true);
}
if (s.Update is UpdateStmt) {
var upd = (UpdateStmt)s.Update;
@@ -232,14 +232,14 @@ namespace DafnyLanguage
return;
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
- regions.Add(new IdRegion(s.Tok, s, true));
+ IdRegion.Add(regions, s.Tok, s, true);
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
- s.BoundVars.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
- kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;
@@ -261,7 +261,26 @@ namespace DafnyLanguage
public readonly int Length;
public readonly string HoverText;
public readonly bool IsDefinition;
- public IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {
+
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition) {
+ Contract.Requires(regions != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(v != null);
+ if (!(tok is AutoGeneratedToken)) {
+ regions.Add(new IdRegion(tok, v, isDefinition));
+ }
+ }
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ 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));
+ }
+ }
+
+ private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {
Contract.Requires(tok != null);
Contract.Requires(v != null);
Start = tok.pos;
@@ -275,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.ToString(), v.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(null/*TODO: use context*/), v.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
- public IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ private IdRegion(Bpl.IToken tok, 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);
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullName, decl.Type.TypeName(null/*TODO: use context*/), decl.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index ff1159ec..34dcce3c 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -30,7 +30,7 @@ namespace DafnyLanguage
}
System.Windows.Shapes.Rectangle sh = new Rectangle() {
- Fill = dtag.Val == 0 ? Brushes.Goldenrod : Brushes.DarkOrange,
+ Fill = dtag.Val == 0 ? new SolidColorBrush(Color.FromRgb(255, 238, 98)) : Brushes.DarkOrange,
Height = 18.0,
Width = 3.0
};
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:37:19 +0000