Add an infinite set collection type.

1 files changed, 33 insertions, 9 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 16cc09eb..b2b40629 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -175,6 +175,9 @@ bool IsMapDisplay() {
 bool IsIMapDisplay() {

   return la.kind == _imap && scanner.Peek().kind == _lbracket;

 }

+bool IsISetDisplay() {

+  return la.kind == _iset && scanner.Peek().kind == _lbrace;

+}

 

 bool IsSuffix() {

   return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;

@@ -334,6 +337,7 @@ bool IsType(ref IToken pt) {
       return true;

     case _arrayToken:

     case _set:

+    case _iset:

     case _multiset:

     case _seq:

     case _map:

@@ -416,6 +420,7 @@ TOKENS
   object = "object".

   string = "string".

   set = "set".

+  iset = "iset".

   multiset = "multiset".

   seq = "seq".

   map = "map".

@@ -754,7 +759,7 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>
   "="

   ( IF(IsIdentColonOrBar())

     NoUSIdent<out bvId>

-    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .)

+    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false, false); } .)

     "|"

     Expression<out wh, false, true>  (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)

   | Type<out baseType>               (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .)

@@ -1139,7 +1144,13 @@ TypeAndToken<out IToken tok, out Type ty>
     [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

                                          SemErr("set type expects only one type argument");

                                        }

-                                       ty = new SetType(gt.Count == 1 ? gt[0] : null);

+                                       ty = new SetType(true, gt.Count == 1 ? gt[0] : null);

+                                    .)

+  | "iset"                          (. tok = t;  gt = new List<Type>(); .)

+    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

+                                         SemErr("set type expects only one type argument");

+                                       }

+                                       ty = new SetType(false, gt.Count == 1 ? gt[0] : null);

                                     .)

   | "multiset"                      (. tok = t;  gt = new List<Type>(); .)

     [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {

@@ -2324,10 +2335,13 @@ UnaryExpression<out Expression e, bool allowSemi, bool allowLambda>
     "imap"                                          (. x = t; .)

     MapDisplayExpr<x, false, out e>

     { IF(IsSuffix()) Suffix<ref e> }

+  | IF(IsISetDisplay())  /* this alternative must be checked before going into EndlessExpression, where there is another "iset" */

+    "iset"                                          (. x = t; .)

+    ISetDisplayExpr<x, false, out e>

+    { IF(IsSuffix()) Suffix<ref e> }

   | IF(IsLambda(allowLambda))

     LambdaExpression<out e, allowSemi>  /* this is an endless expression */

   | EndlessExpression<out e, allowSemi, allowLambda>

-

   | NameSegment<out e>

     { IF(IsSuffix()) Suffix<ref e> }

   | DisplayExpr<out e>

@@ -2432,13 +2446,22 @@ ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
      }

   .)

   .

+ISetDisplayExpr<IToken/*!*/ setToken, bool finite, out Expression e>

+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

+     List<Expression> elements = new List<Expression/*!*/>();;

+     e = dummyExpr;

+  .)

+  "{"

+      [ Expressions<elements> ]                (. e = new SetDisplayExpr(setToken, finite, elements);.)

+  "}"

+  .

 DisplayExpr<out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      IToken x;  List<Expression> elements;

      e = dummyExpr;

   .)

   ( "{"                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

-      [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements);.)

+      [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, true, elements);.)

     "}"

   | "["                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

       [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)

@@ -2503,7 +2526,10 @@ EndlessExpression<out Expression e, bool allowSemi, bool allowLambda>
     "else" Expression<out e1, allowSemi, allowLambda>    (. e = new ITEExpr(x, e, e0, e1); .)

   | MatchExpression<out e, allowSemi, allowLambda>

   | QuantifierGuts<out e, allowSemi, allowLambda>

-  | SetComprehensionExpr<out e, allowSemi, allowLambda>

+  | "set"                           (. x = t; .)

+    SetComprehensionExpr<x, true, out e, allowSemi, allowLambda>

+  | "iset"                           (. x = t; .)

+    SetComprehensionExpr<x, false, out e, allowSemi, allowLambda>

   | StmtInExpr<out s>

     Expression<out e, allowSemi, allowLambda>            (. e = new StmtExpr(s.Tok, s, e); .)

   | LetExpr<out e, allowSemi, allowLambda>

@@ -2842,16 +2868,14 @@ QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression
   ]

   .

 

-SetComprehensionExpr<out Expression q, bool allowSemi, bool allowLambda>

+SetComprehensionExpr<IToken setToken, bool finite, out Expression q, bool allowSemi, bool allowLambda>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);

-     IToken x = Token.NoToken;

      BoundVar bv;

      List<BoundVar/*!*/> bvars = new List<BoundVar>();

      Expression range;

      Expression body = null;

      Attributes attrs = null;

   .)

-  "set"                                        (. x = t; .)

   IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

   { ","

     IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)

@@ -2863,7 +2887,7 @@ SetComprehensionExpr<out Expression q, bool allowSemi, bool allowLambda>
     Expression<out body, allowSemi, allowLambda>

   ]

   (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

-     q = new SetComprehension(x, bvars, range, body, attrs);

+     q = new SetComprehension(setToken, finite, bvars, range, body, attrs);

   .)

   .

 Expressions<.List<Expression> args.>