Add an infinite set collection type.

1 files changed, 6 insertions, 6 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 1361ad85..962b07b9 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -89,7 +89,7 @@ namespace Microsoft.Dafny
       // Add:  ghost var Repr: set<object>;

       // ...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());

+        Type ty = new SetType(true, new ObjectType());

         cl.Members.Add(new Field(new AutoGeneratedToken(cl.tok), "Repr", true, ty, null));

       }

 

@@ -119,7 +119,7 @@ namespace Microsoft.Dafny
           // ensures fresh(Repr - {this});

           var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,

             new MemberSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"),

-            new SetDisplayExpr(tok, new List<Expression>() { new ThisExpr(tok) })));

+            new SetDisplayExpr(tok, true, new List<Expression>() { new ThisExpr(tok) })));

           ctor.Ens.Insert(1, new MaybeFreeExpression(freshness));

         } else if (member is Method && !member.IsStatic) {

           var m = (Method)member;

@@ -246,8 +246,8 @@ namespace Microsoft.Dafny
           if (ctor.Body != null) {

             var bodyStatements = ((BlockStmt)ctor.Body).Body;

             // Repr := {this};

-            var e = new SetDisplayExpr(tok, new List<Expression>() { self });

-            e.Type = new SetType(new ObjectType());

+            var e = new SetDisplayExpr(tok, true, new List<Expression>() { self });

+            e.Type = new SetType(true, new ObjectType());

             Statement s = new AssignStmt(tok, tok, Repr, new ExprRhs(e));

             s.IsGhost = true;

             bodyStatements.Add(s);

@@ -297,8 +297,8 @@ namespace Microsoft.Dafny
 

       foreach (var ff in subobjects) {

         var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null);  // create a resolved MemberSelectExpr

-        Expression e = new SetDisplayExpr(tok, new List<Expression>() { F });

-        e.Type = new SetType(new ObjectType());  // resolve here

+        Expression e = new SetDisplayExpr(tok, true, new List<Expression>() { F });

+        e.Type = new SetType(true, new ObjectType());  // resolve here

         var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);

         rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here

         rhs.Type = Repr.Type;  // resolve here