diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-04 19:55:16 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 17:21:42 -0400 |
| commit | 42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f (patch) | |
| tree | a1183f01ad74389d5e6c5d9c949e18d25f75d1cd /src/parser | |
| parent | 9d0734cf73454ecfd51556ca84daaba9025b28f8 (diff) | |
Support empty (and 1-ary) tuples and records.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 51ea87e39..cbdee9c74 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1163,15 +1163,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } /* tuple types / old-style function types */ - | LBRACKET type[t,check] { types.push_back(t); } - ( COMMA type[t,check] { types.push_back(t); } )* RBRACKET - { if(types.size() == 1) { - if(types.front().isFunction()) { - // old style function syntax [ T -> U ] - PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax"); - } else { - PARSER_STATE->parseError("I'm not sure what you're trying to do here; tuples must have > 1 type"); - } + | LBRACKET ( type[t,check] { types.push_back(t); } + ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET + { if(types.size() == 1 && types.front().isFunction()) { + // old style function syntax [ T -> U ] + PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax"); } else { // tuple type [ T, U, V... ] t = EXPR_MANAGER->mkTupleType(types); @@ -1179,8 +1175,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } /* record types */ - | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } - ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ + | SQHASH ( identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } + ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* )? HASHSQ { t = EXPR_MANAGER->mkRecordType(typeIds); } /* bitvector types */ @@ -1846,6 +1842,10 @@ simpleTerm[CVC4::Expr& f] } } + /* empty tuple literal */ + | LPAREN RPAREN + { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); } + /* boolean literals */ | TRUE_TOK { f = MK_CONST(bool(true)); } | FALSE_TOK { f = MK_CONST(bool(false)); } |