* (define-fun...) now has proper type checking in non-debug builds

  (resolves bug #212)

* also closed some other type checking loopholes in SmtEngine

* small fixes to define-sort (resolves bug #214)

* infrastructural support for printing expressions in languages
  other than the internal representation language using an IO
  manipulator, e.g.:

    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;

  main() sets the output language for all streams to correspond to
  the input language

* support delaying type checking in debug builds, so that one can debug
  the type checker itself (before it was difficult, because debug builds did
  all the type checking on Node creation!): new command-line flag
  --no-early-type-checking (only makes sense for debug builds)

* disallowed copy-construction of ExprManager and NodeManager, and made other
  constructors explicit; previously it was easy to unintentionally create
  duplicate managers, with really weird results (i.e., disappearing
  attributes!)

16 files changed, 250 insertions, 123 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 98aea9707..f5ecf84c5 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -562,7 +562,8 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
 }
 
 /**
- * Remove all attributes from the table calling the cleanup function if one is defined.
+ * Remove all attributes from the table calling the cleanup function
+ * if one is defined.
  */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
@@ -575,7 +576,7 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
     }
   }
 
-  if(anyRequireClearing){
+  if(anyRequireClearing) {
     typename hash_t::iterator it = table.begin();
     typename hash_t::iterator it_end = table.end();
 
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index bd128267a..0c76ea845 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -136,7 +136,6 @@ Type DeclarationScope::lookupType(const std::string& name,
 
     return instantiation;
   } else {
-    Assert(p.second.isSort());
     if(Debug.isOn("sort")) {
       Debug("sort") << "instantiating using a sort substitution" << endl;
       Debug("sort") << "have formals [";
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 55b59d13c..5cf3373c2 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -34,9 +34,9 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-ExprManager::ExprManager() :
+ExprManager::ExprManager(bool earlyTypeChecking) :
   d_ctxt(new Context),
-  d_nodeManager(new NodeManager(d_ctxt)) {
+  d_nodeManager(new NodeManager(d_ctxt, earlyTypeChecking)) {
 }
 
 ExprManager::~ExprManager() {
@@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   try {
     return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -92,8 +92,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
                                                child1.getNode(),
                                                child2.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -112,8 +111,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child2.getNode(),
                                                child3.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -133,8 +131,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child3.getNode(),
                                                child4.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -156,8 +153,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child4.getNode(),
                                                child5.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -181,8 +177,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   try {
     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -207,7 +202,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   try {
     return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -309,16 +304,19 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
-    t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode(), check)));
+    t = Type(d_nodeManager,
+             new TypeNode(d_nodeManager->getType(e.getNode(), check)));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
   return t;
 }
 
 Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+  Debug("nm") << "set " << name << " on " << *n << std::endl;
+  return Expr(this, n);
 }
 
 Expr ExprManager::mkVar(const Type& type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 92d039bd3..7946a734e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -74,12 +74,18 @@ private:
   /** ExprManagerScope reaches in to get the NodeManager */
   friend class ExprManagerScope;
 
+  // undefined, private copy constructor (disallow copy)
+  ExprManager(const ExprManager&);
+
 public:
 
   /**
    * Creates an expression manager.
+   * @param earlyTypeChecking whether to do type checking early (at Expr
+   * creation time); only used in debug builds---for other builds, type
+   * checking is never done early.
    */
-  ExprManager();
+  explicit ExprManager(bool earlyTypeChecking = true);
 
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 5fb931a65..eb618a8c9 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -39,6 +39,7 @@ namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
 const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
+const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
@@ -47,8 +48,8 @@ std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
 }
 
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
-  e.toStream(out);
-  return out;
+  ExprManagerScope ems(*e.getExprManager());
+  return out << e.getNode();
 }
 
 TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
@@ -61,6 +62,12 @@ TypeCheckingException::TypeCheckingException(const Expr& expr, std::string messa
 {
 }
 
+TypeCheckingException::TypeCheckingException(ExprManager* em,
+                                             const TypeCheckingExceptionPrivate* exc)
+: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode())))
+{
+}
+
 TypeCheckingException::~TypeCheckingException() throw () {
   delete d_expr;
 }
@@ -218,9 +225,10 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
-void Expr::toStream(std::ostream& out, int depth, bool types) const {
+void Expr::toStream(std::ostream& out, int depth, bool types,
+                    OutputLanguage language) const {
   ExprManagerScope ems(*this);
-  d_node->toStream(out, depth, types);
+  d_node->toStream(out, depth, types, language);
 }
 
 Node Expr::getNode() const throw() {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 29164ffa5..2eac4ab62 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -26,6 +26,7 @@
 #include <stdint.h>
 
 #include "util/exception.h"
+#include "util/language.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // 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 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -45,6 +46,8 @@ class Expr;
 class ExprManager;
 class SmtEngine;
 class Type;
+class TypeCheckingException;
+class TypeCheckingExceptionPrivate;
 
 namespace smt {
   class SmtEnginePrivate;
@@ -53,6 +56,7 @@ namespace smt {
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
+  class CVC4_PUBLIC ExprSetLanguage;
 }/* CVC4::expr namespace */
 
 /**
@@ -61,6 +65,7 @@ namespace expr {
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
   friend class SmtEngine;
+  friend class smt::SmtEnginePrivate;
 
 private:
 
@@ -69,8 +74,10 @@ private:
 
 protected:
 
-  TypeCheckingException(): Exception() {}
+  TypeCheckingException() : Exception() {}
   TypeCheckingException(const Expr& expr, std::string message);
+  TypeCheckingException(ExprManager* em,
+                        const TypeCheckingExceptionPrivate* exc);
 
 public:
 
@@ -97,6 +104,14 @@ std::ostream& operator<<(std::ostream& out,
                          const TypeCheckingException& e) CVC4_PUBLIC;
 
 /**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
+/**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
  */
@@ -281,7 +296,7 @@ public:
    * type checking is not requested, getType() will do the minimum
    * amount of checking required to return a valid result.
    *
-   * @param check whether we should check the type as we compute it 
+   * @param check whether we should check the type as we compute it
    * (default: false)
    */
   Type getType(bool check = false) const throw (TypeCheckingException);
@@ -296,7 +311,8 @@ public:
    * Outputs the string representation of the expression to the stream.
    * @param out the output stream
    */
-  void toStream(std::ostream& out, int depth = -1, bool types = false) const;
+  void toStream(std::ostream& out, int depth = -1, bool types = false,
+                OutputLanguage lang = language::output::LANG_AST) const;
 
   /**
    * Check if this is a null expression.
@@ -367,6 +383,11 @@ public:
   typedef expr::ExprPrintTypes printtypes;
 
   /**
+   * IOStream manipulator to set the output language for Exprs.
+   */
+  typedef expr::ExprSetLanguage setlanguage;
+
+  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -402,15 +423,10 @@ protected:
   friend class SmtEngine;
   friend class smt::SmtEnginePrivate;
   friend class ExprManager;
-};
+  friend class TypeCheckingException;
+  friend std::ostream& operator<<(std::ostream& out, const Expr& e);
 
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+};/* class Expr */
 
 /**
  * Extending the expression with the capability to construct Boolean
@@ -551,7 +567,7 @@ public:
   static inline void setDepth(std::ostream& out, long depth) {
     out.iword(s_iosIndex) = depth;
   }
-};
+};/* class ExprSetDepth */
 
 /**
  * IOStream manipulator to print type ascriptions or not.
@@ -598,11 +614,50 @@ public:
   }
 };/* class ExprPrintTypes */
 
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC ExprSetLanguage {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default language to use, for ostreams that haven't yet had a
+   * setlanguage() applied to them.
+   */
+  static const int s_defaultLanguage = language::output::LANG_AST;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  OutputLanguage d_language;
+
+public:
+  /**
+   * Construct a ExprSetLanguage with the given setting.
+   */
+  ExprSetLanguage(OutputLanguage l) : d_language(l) {}
+
+  inline void applyLanguage(std::ostream& out) {
+    out.iword(s_iosIndex) = int(d_language);
+  }
+
+  static inline OutputLanguage getLanguage(std::ostream& out) {
+    return OutputLanguage(out.iword(s_iosIndex));
+  }
+
+  static inline void setLanguage(std::ostream& out, OutputLanguage l) {
+    out.iword(s_iosIndex) = int(l);
+  }
+};/* class ExprSetLanguage */
+
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 566 "${template}"
+#line 659 "${template}"
 
 namespace expr {
 
@@ -634,6 +689,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
   return out;
 }
 
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
+  l.applyLanguage(out);
+  return out;
+}
+
 }/* CVC4::expr namespace */
 
 // for hash_maps, hash_sets..
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index aaecff800..c4968af26 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -198,7 +198,7 @@ function registerOperatorToKind {
 	operatorKind=$1
 	applyKind=$2
 	metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
-"; 
+";
 }
 
 function register_metakind {
diff --git a/src/expr/node.h b/src/expr/node.h
index 871f1e0d7..1427bb9c2 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -36,6 +36,8 @@
 #include "util/Assert.h"
 #include "util/configuration.h"
 #include "util/output.h"
+#include "util/exception.h"
+#include "util/language.h"
 
 namespace CVC4 {
 
@@ -58,7 +60,7 @@ private:
 
 protected:
 
-  TypeCheckingExceptionPrivate(): Exception() {}
+  TypeCheckingExceptionPrivate() : Exception() {}
 
 public:
 
@@ -656,12 +658,12 @@ public:
   /**
    * Converst this node into a string representation and sends it to the
    * given stream
-   * @param out the sream to serialise this node to
+   * @param out the stream to serialize this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1,
-                       bool types = false) const {
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
     assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, types);
+    d_nv->toStream(out, toDepth, types, language);
   }
 
   /**
@@ -692,6 +694,11 @@ public:
   typedef expr::ExprPrintTypes printtypes;
 
   /**
+   * IOStream manipulator to set the output language for Exprs.
+   */
+  typedef expr::ExprSetLanguage setlanguage;
+
+  /**
    * Very basic pretty printer for Node.
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
@@ -720,7 +727,8 @@ public:
 inline std::ostream& operator<<(std::ostream& out, TNode n) {
   n.toStream(out,
              Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out));
+             Node::printtypes::getPrintTypes(out),
+             Node::setlanguage::getLanguage(out));
   return out;
 }
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 2f10668c7..4c8bc578a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -664,11 +664,11 @@ private:
   inline void debugCheckType(const TNode n) const {
     // force an immediate type check, if we are in debug mode
     // and the current node isn't a variable or constant
-    if( IS_DEBUG_BUILD ) {
+    if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) {
       kind::MetaKind mk = n.getMetaKind();
       if( mk != kind::metakind::VARIABLE 
           && mk != kind::metakind::CONSTANT ) {
-        d_nm->getType(n,true);
+        d_nm->getType(n, true);
       }
     }
   }
@@ -692,11 +692,11 @@ public:
   operator Node();
   operator Node() const;
 
-  inline void toStream(std::ostream& out, int depth = -1,
-                       bool types = false) const {
+  inline void toStream(std::ostream& out, int depth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    d_nv->toStream(out, depth, types);
+    d_nv->toStream(out, depth, types, language);
   }
 
   NodeBuilder<nchild_thresh>& operator&=(TNode);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4653ee95f..5c24699b8 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -82,10 +82,11 @@ struct NVReclaim {
 };
 
 
-NodeManager::NodeManager(context::Context* ctxt) :
+NodeManager::NodeManager(context::Context* ctxt, bool earlyTypeChecking) :
   d_attrManager(ctxt),
   d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false) {
+  d_inReclaimZombies(false),
+  d_earlyTypeChecking(earlyTypeChecking) {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0860365bc..6453a84d5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -118,6 +118,12 @@ class NodeManager {
   Node d_operators[kind::LAST_KIND];
 
   /**
+   * Whether to do early type checking (only effective in debug
+   * builds; other builds never do early type checking.
+   */
+  const bool d_earlyTypeChecking;
+
+  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -233,9 +239,12 @@ class NodeManager {
   // bool containsDecision(TNode); // is "atomic"
   // bool properlyContainsDecision(TNode); // all children are atomic
 
+  // undefined private copy constructor (disallow copy)
+  NodeManager(const NodeManager&);
+
 public:
 
-  NodeManager(context::Context* ctxt);
+  explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true);
   ~NodeManager();
 
   /** The node manager in the current context. */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index a10b43c48..004f0c9a9 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "util/language.h"
 #include <sstream>
 
 using namespace std;
@@ -41,53 +42,67 @@ string NodeValue::toString() const {
   return ss.str();
 }
 
-void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const {
-  using namespace CVC4::kind;
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
+                         OutputLanguage language) const {
   using namespace CVC4;
+  using namespace CVC4::kind;
+  using namespace CVC4::language::output;
 
-  if(getKind() == kind::NULL_EXPR) {
-    out << "null";
-  } else if(getMetaKind() == kind::metakind::VARIABLE) {
-    if(getKind() != kind::VARIABLE &&
-       getKind() != kind::SORT_TYPE) {
-      out << getKind() << ':';
-    }
+  switch(language) {
+  case LANG_SMTLIB:
+    // FIXME support smt-lib output language
+  case LANG_SMTLIB_V2:
+    // FIXME support smt-lib v2 output language
+  case LANG_AST:
+    if(getKind() == kind::NULL_EXPR) {
+      out << "null";
+    } else if(getMetaKind() == kind::metakind::VARIABLE) {
+      if(getKind() != kind::VARIABLE &&
+         getKind() != kind::SORT_TYPE) {
+        out << getKind() << ':';
+      }
 
-    string s;
-    NodeManager* nm = NodeManager::currentNM();
+      string s;
+      NodeManager* nm = NodeManager::currentNM();
 
-    // conceptually "this" is const, and hasAttribute() doesn't change
-    // its argument, but it requires a non-const key arg (for now)
-    if(nm->getAttribute(const_cast<NodeValue*>(this),
-                        VarNameAttr(), s)) {
-      out << s;
-    } else {
-      out << "var_" << d_id;
-    }
-    if(types) {
-      // print the whole type, but not *its* type
-      out << ":";
-      nm->getType(TNode(this)).toStream(out, -1, false);
-    }
-  } else {
-    out << '(' << Kind(d_kind);
-    if(getMetaKind() == kind::metakind::CONSTANT) {
-      out << ' ';
-      kind::metakind::NodeValueConstPrinter::toStream(out, this);
+      // conceptually "this" is const, and hasAttribute() doesn't change
+      // its argument, but it requires a non-const key arg (for now)
+      if(nm->getAttribute(const_cast<NodeValue*>(this),
+                          VarNameAttr(), s)) {
+        out << s;
+      } else {
+        out << "var_" << d_id << "[" << this << "]";
+      }
+      if(types) {
+        // print the whole type, but not *its* type
+        out << ":";
+        nm->getType(TNode(this)).toStream(out, -1, false, language);
+      }
     } else {
-      for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
-        if(i != nv_end()) {
-          out << ' ';
-        }
-        if(toDepth != 0) {
-          (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types);
-        } else {
-          out << "(...)";
+      out << '(' << Kind(d_kind);
+      if(getMetaKind() == kind::metakind::CONSTANT) {
+        out << ' ';
+        kind::metakind::NodeValueConstPrinter::toStream(out, this);
+      } else {
+        for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+          if(i != nv_end()) {
+            out << ' ';
+          }
+          if(toDepth != 0) {
+            (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                           types, language);
+          } else {
+            out << "(...)";
+          }
         }
       }
+      out << ')';
     }
-    out << ')';
-  }
+    break;
+
+  default:
+    out << "[output language " << language << " unsupported]";
+  }// end switch(language)
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index b91196559..bc592b4e5 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -29,6 +29,7 @@
 #define __CVC4__EXPR__NODE_VALUE_H
 
 #include "expr/kind.h"
+#include "util/language.h"
 
 #include <stdint.h>
 #include <string>
@@ -260,7 +261,8 @@ public:
   }
 
   std::string toString() const;
-  void toStream(std::ostream& out, int toDepth = -1, bool types = false) const;
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                OutputLanguage = language::output::LANG_AST) const;
 
   static inline unsigned kindToDKind(Kind k) {
     return ((unsigned) k) & kindMask;
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8cf555eb0..b8b2e4754 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -29,9 +29,9 @@ using namespace std;
 
 namespace CVC4 {
 
-ostream& operator<<(ostream& out, const Type& e) {
-  e.toStream(out);
-  return out;
+ostream& operator<<(ostream& out, const Type& t) {
+  NodeManagerScope nms(t.d_nodeManager);
+  return out << *Type::getTypeNode(t);
 }
 
 Type Type::makeType(const TypeNode& typeNode) const {
@@ -123,6 +123,13 @@ void Type::toStream(ostream& out) const {
   return;
 }
 
+string Type::toString() const {
+  NodeManagerScope nms(d_nodeManager);
+  stringstream ss;
+  ss << *d_typeNode;
+  return ss.str();
+}
+
 /** Is this the Boolean type? */
 bool Type::isBoolean() const {
   NodeManagerScope nms(d_nodeManager);
diff --git a/src/expr/type.h b/src/expr/type.h
index 19c3d27f3..435d640d0 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -56,6 +56,14 @@ struct CVC4_PUBLIC TypeHashStrategy {
 };/* struct TypeHashStrategy */
 
 /**
+ * Output operator for types
+ * @param out the stream to output to
+ * @param t the type to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+
+/**
  * Class encapsulating CVC4 expression types.
  */
 class CVC4_PUBLIC Type {
@@ -65,6 +73,7 @@ class CVC4_PUBLIC Type {
   friend class ExprManager;
   friend class TypeNode;
   friend class TypeHashStrategy;
+  friend std::ostream& operator<<(std::ostream& out, const Type& t);
 
 protected:
 
@@ -283,7 +292,12 @@ public:
    * @param out the stream to output to
    */
   void toStream(std::ostream& out) const;
-};
+
+  /**
+   * Constructs a string representation of this type.
+   */
+  std::string toString() const;
+};/* class Type */
 
 /**
  * Singleton class encapsulating the Boolean type.
@@ -294,7 +308,7 @@ public:
 
   /** Construct from the base type */
   BooleanType(const Type& type) throw(AssertionException);
-};
+};/* class BooleanType */
 
 /**
  * Singleton class encapsulating the integer type.
@@ -305,7 +319,7 @@ public:
 
   /** Construct from the base type */
   IntegerType(const Type& type) throw(AssertionException);
-};
+};/* class IntegerType */
 
 /**
  * Singleton class encapsulating the real type.
@@ -316,8 +330,7 @@ public:
 
   /** Construct from the base type */
   RealType(const Type& type) throw(AssertionException);
-};
-
+};/* class RealType */
 
 /**
  * Class encapsulating a function type.
@@ -334,7 +347,7 @@ public:
 
   /** Get the range type (i.e., the type of the result). */
   Type getRangeType() const;
-};
+};/* class FunctionType */
 
 /**
  * Class encapsulating a tuple type.
@@ -348,7 +361,7 @@ public:
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
-};
+};/* class TupleType */
 
 /**
  * Class encapsulating an array type.
@@ -365,7 +378,7 @@ public:
 
   /** Get the constituent type */
   Type getConstituentType() const;
-};
+};/* class ArrayType */
 
 /**
  * Class encapsulating a user-defined sort.
@@ -379,7 +392,7 @@ public:
 
   /** Get the name of the sort */
   std::string getName() const;
-};
+};/* class SortType */
 
 /**
  * Class encapsulating a user-defined sort constructor.
@@ -399,7 +412,7 @@ public:
 
   /** Instantiate a sort using this sort constructor */
   SortType instantiate(const std::vector<Type>& params) const;
-};
+};/* class SortConstructorType */
 
 /**
  * Class encapsulating the kind type (the type of types).
@@ -410,8 +423,7 @@ public:
 
   /** Construct from the base type */
   KindType(const Type& type) throw(AssertionException);
-};
-
+};/* class KindType */
 
 /**
  * Class encapsulating the bit-vector type.
@@ -428,15 +440,7 @@ public:
    * @return the width of the bit-vector type (> 0)
    */
   unsigned getSize() const;
-};
-
-/**
- * Output operator for types
- * @param out the stream to output to
- * @param t the type to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+};/* class BitVectorType */
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0e763128f..cc368e8c0 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -310,14 +310,14 @@ public:
   }
 
   /**
-   * Converst this node into a string representation and sends it to the
+   * Converts this node into a string representation and sends it to the
    * given stream
    *
-   * @param out the sream to serialise this node to
+   * @param out the stream to serialize this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1,
-                       bool types = false) const {
-    d_nv->toStream(out, toDepth, types);
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
+    d_nv->toStream(out, toDepth, types, language);
   }
 
   /**