From 07019586cd7ef6f77ce675eb594f6e3cc2f2502e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 20 Jun 2014 20:00:36 -0400 Subject: [PATCH] Datatypes kinds documentation --- src/theory/datatypes/kinds | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index b222738ae..d8b42111c 100644 --- 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().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 -- 2.30.2