diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 294df3d2..06af76d1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1208,6 +1208,7 @@ UnaryExpression<out Expression/*!*/ e> | DottedIdentifiersAndFunction<out e>
{ Suffix<ref e> }
| DisplayExpr<out e>
+ | MultiSetExpr<out e>
| ConstAtomExpression<out e>
{ Suffix<ref e> }
)
@@ -1259,18 +1260,30 @@ DisplayExpr<out Expression e> = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- bool isMulti = false;
.)
- ( [ "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 SetDisplayExpr(x, elements);.)
"}"
| "[" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
"]"
)
.
+MultiSetExpr<out Expression e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
+ e = dummyExpr;
+ .)
+ "multiset" (. x = t; .)
+ ( "{" (. elements = new List<Expression/*!*/>(); .)
+ [ Expressions<elements> ] (. e = new MultiSetDisplayExpr(x, elements);.)
+ "}"
+ | "(" (. x = t; elements = new List<Expression/*!*/>(); .)
+ Expression<out e> (. e = new MultiSetFormingExpr(x, e); .)
+ ")"
+ | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
+ )
+ .
EndlessExpression<out Expression e>
= (. IToken/*!*/ x;
|