Support empty (and 1-ary) tuples and records.

5 files changed, 13 insertions, 16 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 424ebab11..a838d6d30 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -509,7 +509,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 
 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( types.size() >= 1 );
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f44c7e78b..7c84f3f15 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1090,7 +1090,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
 }
 
 inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  Assert(types.size() >= 1);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,
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)); }
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 2e58677df..81ef32b32 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -88,7 +88,7 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 
-operator TUPLE_TYPE 1: "tuple type"
+operator TUPLE_TYPE 0: "tuple type"
 cardinality TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
@@ -100,7 +100,7 @@ enumerator TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleEnumerator" \
     "theory/datatypes/type_enumerator.h"
 
-operator TUPLE 1: "a tuple"
+operator TUPLE 0: "a tuple"
 typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
 construle TUPLE ::CVC4::theory::datatypes::TupleProperties
 
diff --git a/src/util/record.h b/src/util/record.h
index 3d6481320..63c54930e 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -91,7 +91,6 @@ public:
 
   Record(const std::vector< std::pair<std::string, Type> >& fields) :
     d_fields(fields) {
-    CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty");
   }
 
   const_iterator find(std::string name) const {