DafnyExtension: various improvements

2 files changed, 42 insertions, 25 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 66ad49e9..722515ce 100644
--- a/Dafny/DafnyAst.cs
+++ b/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/Dafny/Rewriter.cs b/Dafny/Rewriter.cs
index d88830a7..c95be2f4 100644
--- a/Dafny/Rewriter.cs
+++ b/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) {