Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

1 files changed, 62 insertions, 3 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6e8b6c63c..21fc0a4a1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -2,10 +2,10 @@
 /*! \file expr_manager_template.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -22,13 +22,15 @@
 #include "util/options.h"
 #include "util/stats.h"
 
+#include <map>
+
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 34 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
+DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+  NodeManagerScope nms(d_nodeManager);
+  TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype));
+  Type type(d_nodeManager, typeNode);
+  DatatypeType dtt(type);
+  const Datatype& dt = typeNode->getConst<Datatype>();
+  if(!dt.isResolved()) {
+    std::map<std::string, DatatypeType> resolutions;
+    resolutions.insert(std::make_pair(datatype.getName(), dtt));
+    const_cast<Datatype&>(dt).resolve(this, resolutions);
+  }
+  return dtt;
+}
+
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+  NodeManagerScope nms(d_nodeManager);
+  std::map<std::string, DatatypeType> resolutions;
+  std::vector<DatatypeType> dtts;
+  for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+    Type type(d_nodeManager, typeNode);
+    DatatypeType dtt(type);
+    CheckArgument(resolutions.find((*i).getName()) == resolutions.end(),
+                  datatypes,
+                  "cannot construct two datatypes at the same time with the same name `%s'",
+                  (*i).getName().c_str());
+    resolutions.insert(std::make_pair((*i).getName(), dtt));
+    dtts.push_back(dtt);
+  }
+  for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end();
+      i != i_end;
+      ++i) {
+    const Datatype& dt = (*i).getDatatype();
+    if(!dt.isResolved()) {
+      const_cast<Datatype&>(dt).resolve(this, resolutions);
+    }
+  }
+  return dtts;
+}
+
+ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
+}
+
+SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
+}
+
+TesterType ExprManager::mkTesterType(Type domain) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
+}
+
 SortType ExprManager::mkSort(const std::string& name) const {
   NodeManagerScope nms(d_nodeManager);
   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));