From 4d6d4e0b4082d4c8624e04d040f84070138c3f72 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 30 Nov 2012 18:11:48 +0000
Subject: [PATCH] Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/printer/cvc/cvc_printer.cpp        | 14 +++++++++++---
 src/theory/datatypes/kinds             |  6 +++++-
 src/theory/datatypes/type_enumerator.h |  5 +++++
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a61d2d4c0..a9d439a0f 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -290,6 +290,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     // DATATYPES
+    case kind::PARAMETRIC_DATATYPE:
+      out << n[0].getConst<Datatype>().getName() << '[';
+      for(unsigned i = 1; i < n.getNumChildren(); ++i) {
+        if(i > 1) {
+          out << ',';
+        }
+        out << n[i];
+      }
+      out << ']';
+      return;
+      break;
     case kind::APPLY_TYPE_ASCRIPTION: {
         toStream(out, n[0], depth, types, false);
         out << "::";
@@ -462,9 +473,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << ">=";
       opType = INFIX;
       break;
-    case kind::PARAMETRIC_DATATYPE:
-      out << n[0].getConst<Datatype>().getName();
-      break;
 
     // BITVECTORS
     case kind::BITVECTOR_XOR:
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d1fbf82bc..3968af4dd 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -63,11 +63,15 @@ operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
     "util/datatype.h"
-well-founded PARAMETRIC_DATATYPE\
+well-founded PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
     "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
+enumerator PARAMETRIC_DATATYPE \
+    "::CVC4::theory::datatypes::DatatypesEnumerator" \
+    "theory/datatypes/type_enumerator.h"
+
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
     "type ascription, for datatype constructor applications"
 constant ASCRIPTION_TYPE \
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index ea68e8957..d8557fcaf 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -66,6 +66,11 @@ public:
     d_zeroCtor(0),
     d_argEnumerators(NULL) {
 
+    //Assert(type.isDatatype());
+    Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
+    Debug("te") << "datatype is kind " << type.getKind() << std::endl;
+    Debug("te") << "datatype is " << type << std::endl;
+
     /* find the "zero" constructor (the first non-recursive one) */
     /* FIXME: this isn't sufficient for mutually-recursive datatypes! */
     while(d_zeroCtor < d_datatype.getNumConstructors()) {
-- 
2.30.2