Datatypes kinds documentation

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index b222738ae0263750429fb8ccec41291fa8687e2e..d8b42111ca4e2bd657eb0e5c56a3d165e330b281 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -7,7 +7,6 @@
 theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
 typechecker "theory/datatypes/theory_datatypes_type_rules.h"
 
-
 properties check presolve parametric propagate
 
 rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"
@@ -36,18 +35,18 @@ cardinality TESTER_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
-parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application"
+parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor"
 
-parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
-parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)"
+parameterized APPLY_SELECTOR SELECTOR_TYPE 1 "selector application; parameter is a datatype term (undefined if mis-applied)"
+parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; parameter is a datatype term (defined rigidly if mis-applied)"
 
-parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
+parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term"
 
 constant DATATYPE_TYPE \
     ::CVC4::Datatype \
     "::CVC4::DatatypeHashFunction" \
     "util/datatype.h" \
-    "datatype type"
+    "a datatype type"
 cardinality DATATYPE_TYPE \
     "%TYPE%.getConst<Datatype>().getCardinality()" \
     "util/datatype.h"
@@ -74,12 +73,12 @@ enumerator PARAMETRIC_DATATYPE \
     "theory/datatypes/type_enumerator.h"
 
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
-    "type ascription, for datatype constructor applications"
+    "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed"
 constant ASCRIPTION_TYPE \
     ::CVC4::AscriptionType \
     ::CVC4::AscriptionTypeHashFunction \
     "util/ascription_type.h" \
-    "a type parameter for type ascription"
+    "a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class"
 
 typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
@@ -102,7 +101,7 @@ enumerator TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleEnumerator" \
     "theory/datatypes/type_enumerator.h"
 
-operator TUPLE 0: "a tuple"
+operator TUPLE 0: "a tuple (N-ary)"
 typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
 construle TUPLE ::CVC4::theory::datatypes::TupleProperties
 
@@ -110,21 +109,21 @@ constant TUPLE_SELECT_OP \
         ::CVC4::TupleSelect \
         ::CVC4::TupleSelectHashFunction \
         "util/tuple.h" \
-        "operator for a tuple select"
-parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select"
+        "operator for a tuple select; payload is an instance of the CVC4::TupleSelect class"
+parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple"
 typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
 
 constant TUPLE_UPDATE_OP \
         ::CVC4::TupleUpdate \
         ::CVC4::TupleUpdateHashFunction \
         "util/tuple.h" \
-        "operator for a tuple update"
-parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update"
+        "operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class"
+parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index"
 typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
 
 constant RECORD_TYPE \
     ::CVC4::Record \
-    "::CVC4::RecordHashFunction" \
+    ::CVC4::RecordHashFunction \
     "util/record.h" \
     "record type"
 cardinality RECORD_TYPE \
@@ -138,7 +137,7 @@ enumerator RECORD_TYPE \
     "::CVC4::theory::datatypes::RecordEnumerator" \
     "theory/datatypes/type_enumerator.h"
 
-parameterized RECORD RECORD_TYPE 0: "a record"
+parameterized RECORD RECORD_TYPE 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order"
 typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
 construle RECORD ::CVC4::theory::datatypes::RecordProperties
 
@@ -146,16 +145,16 @@ constant RECORD_SELECT_OP \
         ::CVC4::RecordSelect \
         ::CVC4::RecordSelectHashFunction \
         "util/record.h" \
-        "operator for a record select"
-parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select"
+        "operator for a record select; payload is an instance CVC4::RecordSelect class"
+parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from"
 typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
 
 constant RECORD_UPDATE_OP \
         ::CVC4::RecordUpdate \
         ::CVC4::RecordUpdateHashFunction \
         "util/record.h" \
-        "operator for a record update"
-parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update"
+        "operator for a record update; payload is an instance CVC4::RecordSelect class"
+parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
 typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 
 endtheory