new domain-specific language for kinds files: permits characterization of different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them

1 files changed, 48 insertions, 5 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index 806f4f402..f687e3b81 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -1,5 +1,48 @@
-EQUAL
-ITE
-SKOLEM
-VARIABLE
-TUPLE
+# builtin_kinds                                                       -*- sh -*-
+#
+# This "kinds" file is written in a domain-specific language for
+# declaring CVC4 kinds.  Comments are marked with #, as this line is.
+# There are four basic commands:
+#
+#   special K ["comment"]
+#   operator K ["comment"]
+#   parameterized K ["comment"]
+#   constant K T ["comment"]
+#
+# special K (with an optional comment) declares a kind K that has no
+# operator (it's not conceptually an APPLY of an operator to
+# operands).  This is appropriate for special built-ins,
+# e.g. VARIABLE.
+#
+# operator K (with an optional comment) declares a "built-in"
+# operator.  Really this is the same as "special" except that it has
+# an operator (automatically generated by NodeManager).
+#
+# parameterized K (with an optional comment) declares a "built-in"
+# parameterized operator.  This is a theory-specific APPLY, e.g.,
+# APPLY_UF, which applies its first parameter (say, "f"), to its
+# operands (say, "x" and "y", making the full application "f(x,y)").
+# Nodes with such a kind will have an operator (Node::hasOperator()
+# returns true, and Node::getOperator() returns the Node of functional
+# type representing "f" here), and the "children" are defined to be
+# this operator's parameters, and don't include the operator itself
+# (here, there are only two children "x" and "y").  For consistency
+# these should probably start with "APPLY_", but this is not enforced.
+#
+# constant K T (with an optional comment) declares a constant kind.  T
+# is the C++ type representing the constant internally.  For
+# consistency, these should probably start with "CONST_", but this is
+# not enforced.
+#
+# This file is actually an executable Bourne shell script (sourced by
+# the processing scripts after defining functions called "special,"
+# "operator," "parameterized," and "constant").  So if you need a
+# multi-line comment string, do it the Bourne-like way.  Please don't
+# do anything else in this file than using these commands though.
+#
+
+operator EQUAL "equality"
+operator ITE "if-then-else"
+special SKOLEM "skolem var"
+special VARIABLE "variable"
+operator TUPLE "a tuple"