4.9.8 Record

A record over n features, where each of these features consists of a field field_i and a value term_i of type type_i (1<=i<=n). We call the set of fields of a record its arity.

4.9.8.1 Top value

For each field field_i in the arity of the record, its value is the top value of the corresponding type type_i.

4.9.8.2 Bottom value

For each field field_i in the arity of the record, its value is the bottom value of the corresponding type type_i.

4.9.8.3 Greatest lower bound operation

Recursively, the greatest lower bound of two records A and B is the record where the value of each field field_i is the result of the greatest lower bound of the value at field_i in record A, and the value field_i in record B.

Notice that you can also use the greatest lower bound operation (conjunction) on the features in a record specification. The conjunction of two features field_1:term_1 and field_2:term_2 is defined as:

• If field_1 and field_2 are equal, then replace the two features by field_1:term in the record specification, where term is the conjunction of term_1 and term_2.
• Otherwise, keep the two features in the record specification.

4.9.8.4 Example

Here is an example record type definition with three fields in its arity (field_1, field_2 and field_3). These have types ref("type_1"), ref("type_2") and ref("type_3"), respectively:

     deftype "record" {field_1: ref("type_1")
                       field_2: ref("type_2")
                       field_3: ref("type_3")}