diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 99de2757..70ea9ae8 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -745,28 +745,32 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> | "int" (. tok = t; ty = new IntType(); .)
| "real" (. tok = t; ty = new RealType(); .)
| "set" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("set type expects exactly one type argument");
+ [ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
+ SemErr("set type expects only one type argument");
}
- ty = new SetType(gt[0]);
+ ty = new SetType(gt.Count == 1 ? gt[0] : null);
.)
| "multiset" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("multiset type expects exactly one type argument");
+ [ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
+ SemErr("multiset type expects only one type argument");
}
- ty = new MultiSetType(gt[0]);
+ ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);
.)
| "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("seq type expects exactly one type argument");
+ [ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
+ SemErr("seq type expects only one type argument");
}
- ty = new SeqType(gt[0]);
+ ty = new SeqType(gt.Count == 1 ? gt[0] : null);
.)
| "map" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 2) {
- SemErr("map type expects exactly two type arguments");
+ [ GenericInstantiation<gt> ] (. if (gt.Count == 0) {
+ ty = new MapType(null, null);
+ } else if (gt.Count != 2) {
+ SemErr("map type expects two type arguments");
+ ty = new MapType(gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);
+ } else {
+ ty = new MapType(gt[0], gt[1]);
}
- else { ty = new MapType(gt[0], gt[1]); }
.)
| ReferenceType<out tok, out ty>
)
|