Add initial support for co-datatypes.

2 files changed, 20 insertions, 0 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index b3383e6c4..d140d1990 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,6 +302,7 @@ variable SKOLEM "skolem var"
 operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
+operator MU 2 "mu"
 
 parameterized CHAIN CHAIN_OP 2: "chained operator"
 constant CHAIN_OP \
@@ -334,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+typerule MU ::CVC4::theory::builtin::MuTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index c7143bdeb..f35286f05 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -164,6 +164,24 @@ public:
   }
 };/* class LambdaTypeRule */
 
+class MuTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
+      std::stringstream ss;
+      ss << "expected a bound var list for MU expression, got `"
+         << n[0].getType().toString() << "'";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+    std::vector<TypeNode> argTypes;
+    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
+      argTypes.push_back((*i).getType());
+    }
+    TypeNode rangeType = n[1].getType(check);
+    return nodeManager->mkFunctionType(argTypes, rangeType);
+  }
+};/* class MuTypeRule */
+
 class ChainTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {