5 files changed, 30 insertions, 6 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index d170469e0..83a372726 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -36,7 +36,6 @@
 #       check             the theory supports the check() function
 #       propagate         the theory supports propagate() (and explain())
 #       staticLearning    the theory supports staticLearning()
-#       registerTerm      the theory supports registerTerm()
 #       notifyRestart     the theory supports notifyRestart()
 #       presolve          the theory supports presolve()
 #
@@ -59,6 +58,12 @@
 #     future, so if possible, do not rely on them being called (and
 #     implement them as a no-op).
 #
+#   typechecker header
+#
+#     Declare that this theory's typechecker class is defined in the
+#     given header.  (#include'd by the TypeChecker class in the expr
+#     package.)
+#
 #   variable K ["comment"]
 #
 #     This declares a kind K that has no operator (it's conceptually a
@@ -122,6 +127,19 @@
 #     For consistency, constants taking a non-void payload should
 #     start with "CONST_", but this is not enforced.
 #
+#   typerule K typechecker-class
+#
+#     Declares that a (previously-declared) kind K is typechecked by
+#     the typechecker-class.  This class should be defined by the
+#     header given to the "typechecker" command, above.  The
+#     typechecker-class is used this way by the main TypeChecker code:
+#
+#       typechecker-class::computeType(NodeManager* nm, TNode n, bool check)
+#
+#     It returns TypeNode.  It should compute the type of n and return it,
+#     and if "check" is true, should actually perform type checking instead
+#     of simply type computation.
+#
 #   sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"]
 #
 #     This creates a kind K that represents a sort (a "type constant").
@@ -217,6 +235,7 @@
 #
 
 theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
+typechecker "theory/builtin/theory_builtin_type_rules.h"
 
 properties stable-infinite
 
@@ -282,4 +301,9 @@ well-founded TUPLE_TYPE \
     "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
+typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
+typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
+typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
+typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+
 endtheory
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1c779bd79..e955539d5 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** 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
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 4e62401ff..5c3c70443 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): barrett
+ ** 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
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index b71d66c03..f62140263 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_builtin_rewriter.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 3bfb7fdc5..ce06b4259 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -5,7 +5,7 @@
  ** 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