3.2 Types

CVC's presentation language is typed. The type system currently is fairly simple. There is no polymorphism or subtyping (although a form of the latter will be added in a later release). In addition to built-in basic types, there are tuple types, record types, array types, scalar types (aka, enumerations) inductive datatypes, and function types. Structural equivalence is used to compare all types except scalar types and inductive datatypes, where name equivalence is used (see the remarks on type definitions).

Remark: CVC works with first-order logic only. Types must therefore be first-order. So no type T can contain a function type as a subexpression, unless T is itself a function type.

3.2.1 Basic types

The basic types in CVC are REAL and BOOLEAN. REAL is the type of numbers, and BOOLEAN is the type of formulas.

Technically, since CVC's language is first-order, types should not contain BOOLEAN, except as the range of a function type (which is then the type of a predicate). In CVC, however, BOOLEAN may appear arbitrarily in types. This is achieved by having two versions of the BOOLEAN type, one for formulas and one for boolean terms. This distinction is made only internally; the input language just has a single type BOOLEAN.

3.2.2 Tuple types

The types for tuples are of the form

[ t_0, ..., t_(n-1) ]

where n is at least 2, and t_0, ..., t_(n-1) are types. For example, the following declares a, b, and c to be various tuples:

a : [ REAL, REAL ];
b : [ REAL, BOOLEAN, [ REAL, REAL, REAL] ];
c : [ BOOLEAN, BOOLEAN, [ REAL, BOOLEAN] ];
3.2.3 Function types

The types of functions are of the form

[ Domain -> Range ];

where Domain and Range are types (recall that by the remark above, they cannot be function types). For example, this declares a function F from tuples to tuples:

F : [ [ REAL, REAL ] -> [ BOOLEAN, BOOLEAN ] ];
3.2.4 Record types

The types for records are of the form

[# f_1 : t_1, ..., f_n : t_n #]

where n is at least 1; f_1, ..., f_n are identifiers; and t_1, ..., t_n are types. f_1, ..., f_n are called the fieldnames of the record type. The fieldnames f_1, ..., f_n may be the same as the names of fields of other records or other declared or defined constants and types.

Here is an example (see also the records example):

f : REAL;
r : [# f : BOOLEAN, f2 : REAL #];

3.2.5 Inductive datatypes and scalar types

An example of an inductive datatype (also known as an abstract datatype, or ADT) is

DATATYPE cons (car : REAL, cdr : rList), null END

 This is the type of finite lists of REALs (see the ADTs example).

The general form for inductive datatypes is

DATATYPE constructor_def_1, ... , contructor_def_n END

where each constructor_def_i is of the form

c (s_1 : t_1, ..., s_m : t_m)

Here, c is the name of the constructor (like "cons"). s_1, ..., s_m are the names of the selectors (aka, destructors) for the constructor c (like "car" and "cdr"). t_1, ..., t_m are the domain types for the constructor c. They are also the range types for s_1, ..., s_m, respectively. If m is 0 (as for "null"), then the list of selectors is omitted from the constructor_def.

When a datatype is declared, CVC automatically declares each constructor c as the appropriate function; if c has no selectors, it is declared as a constant. The selectors for c are also declared as the appropriate functions. Applying the i'th selector of c to c(a_1, ..., a_n) returns a_i. Selectors are treated as partial functions in CVC. So "car(null)" is considered to be undefined (see the section on partiality).

CVC automatically declares a tester "c?", which is a predicate on the datatype. It returns true for a given element e of that datatype iff e was constructed using constructor c.

Scalar types are a special case of inductive datatypes. They are of the form

{ c_1, ..., c_n }

where n is at least 1, and c_1, ..., c_n are new identifiers.
As noted already, the use of inductive datatypes and scalar types is restricted in a way that the user of other types is not. See the section on type definitions.
3.2.6 Array types

The types for arrays are of the form

ARRAY I OF R

where I and R are types, and I is not allowed to be an array type.

This example declares a multi-dimensional array (see also the arrays example):

a : ARRAY REAL OF ARRAY REAL OF ARRAY REAL OF REAL;