# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

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"

# constructor type has a list of selector types followed by a return type
operator CONSTRUCTOR_TYPE 1: "constructor"
cardinality CONSTRUCTOR_TYPE \
    "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"
well-founded CONSTRUCTOR_TYPE \
    "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"

# selector type has domain type and a range type
operator SELECTOR_TYPE 2 "selector"
# can re-use function cardinality
cardinality SELECTOR_TYPE \
    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"

# tester type has a constructor type
operator TESTER_TYPE 1 "tester"
# can re-use function cardinality
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_SELECTOR SELECTOR_TYPE 1: "selector application"

parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"

constant DATATYPE_TYPE \
    ::CVC4::Datatype \
    "::CVC4::DatatypeHashFunction" \
    "util/datatype.h" \
    "datatype type"
cardinality DATATYPE_TYPE \
    "%TYPE%.getConst<Datatype>().getCardinality()" \
    "util/datatype.h"
well-founded DATATYPE_TYPE \
    "%TYPE%.getConst<Datatype>().isWellFounded()" \
    "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
    "util/datatype.h"

enumerator DATATYPE_TYPE \
    "::CVC4::theory::datatypes::DatatypesEnumerator" \
    "theory/datatypes/type_enumerator.h"

operator PARAMETRIC_DATATYPE 1: "parametric datatype"
cardinality PARAMETRIC_DATATYPE \
    "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
    "util/datatype.h"
well-founded PARAMETRIC_DATATYPE \
    "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
    "util/datatype.h"

enumerator PARAMETRIC_DATATYPE \
    "::CVC4::theory::datatypes::DatatypesEnumerator" \
    "theory/datatypes/type_enumerator.h"

parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
    "type ascription, for datatype constructor applications"
constant ASCRIPTION_TYPE \
    ::CVC4::AscriptionType \
    ::CVC4::AscriptionTypeHashFunction \
    "util/ascription_type.h" \
    "a type parameter for type ascription"

typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule
typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule

# constructor applications are constant if they are applied only to constants
construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule

operator TUPLE_TYPE 0: "tuple type"
cardinality TUPLE_TYPE \
    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"
well-founded TUPLE_TYPE \
    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"
enumerator TUPLE_TYPE \
    "::CVC4::theory::datatypes::TupleEnumerator" \
    "theory/datatypes/type_enumerator.h"

operator TUPLE 0: "a tuple"
typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
construle TUPLE ::CVC4::theory::datatypes::TupleProperties

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"
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"
typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule

constant RECORD_TYPE \
    ::CVC4::Record \
    "::CVC4::RecordHashFunction" \
    "util/record.h" \
    "record type"
cardinality RECORD_TYPE \
    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"
well-founded RECORD_TYPE \
    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"
enumerator RECORD_TYPE \
    "::CVC4::theory::datatypes::RecordEnumerator" \
    "theory/datatypes/type_enumerator.h"

parameterized RECORD RECORD_TYPE 0: "a record"
typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
construle RECORD ::CVC4::theory::datatypes::RecordProperties

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"
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"
typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule

endtheory
