diff options
| author |  Jason Koenig <unknown> | 2011-07-11 15:33:45 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-11 15:33:45 -0700 |
| commit | f72015819c90a23b150b1d70147eb51c51e2d5ed (patch) | |
| tree | a07b8d9094f028d5ea071e46dbaf818b5bb8d5fe /Source/Dafny/Dafny.atg | |
| parent | d5bf8e1275ae1cc79ddb7048d2015160bdf2bddc (diff) | |
Partial implementation of multisets.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f6e40722..3f6c64b8 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -518,6 +518,12 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> }
ty = new SetType(gt[0]);
.)
+ | "multiset" (. tok = t; gt = new List<Type/*!*/>(); .)
+ GenericInstantiation<gt> (. if (gt.Count != 1) {
+ SemErr("multiset type expects exactly one type argument");
+ }
+ ty = new MultiSetType(gt[0]);
+ .)
| "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
@@ -1251,11 +1257,14 @@ ConstAtomExpression<out Expression/*!*/ e> DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
+ bool isMulti = false;
.)
- ( "{" (. x = t; elements = new List<Expression/*!*/>(); .)
- [ Expressions<elements> ] (. e = new SetDisplayExpr(x, elements); .)
+ ( [ "multi" (. x = t; isMulti = true; .) ]
+ "{" (. if (!isMulti) x = t; elements = new List<Expression/*!*/>(); .)
+ [ Expressions<elements> ] (. if (isMulti) e = new MultiSetDisplayExpr(x, elements);
+ else e = new SetDisplayExpr(x, elements);.)
"}"
| "[" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
|