2.1 Record types
The Record
function is a macro allowing
the definition of records as is done in many programming languages.
Its syntax is described on figure 2.1.
sentence |
::= |
record |
|
|
|
record |
::= |
Record ident [ params ] : sort
:= [ident] {
[field ; ... ; field]
} . |
|
|
|
field |
::= |
ident : term |
Figure 2.1: Syntax for the definition of Record
In the command
``Record ident [ params ] :
sort := ident0 {
ident1 : term1;
...identn : termn }
.'',
the identifier ident is the name of the defined record and sort
is its type. The identifier ident0 is the name of its
constructor. The identifiers ident1, .., identn are the
names of its fields and term1, .., termn their respective
types. Records can have parameters.
Example: The set of rational numbers may be defined as:
Coq < Record Rat : Set := mkRat {
Coq < top : nat;
Coq < bottom : nat;
Coq < Rat_cond : (gt bottom O) }.
Rat_ind is defined
Rat_rec is defined
Rat_rect is defined
Rat is defined
A field may depend on other fields appearing before it.
For instance in the above example, the field
Rat_cond
depends on the field bottom
. Thus the order of
the fields is important.
Let us now see the work done by the Record macro.
First the macro generates a inductive definition
with just one constructor:
Inductive ident [ params ] : sort :=
ident0 : (ident1:term1) ..
(identn:termn)(ident params).
To build an object of type ident, one should provide the
constructor ident0 with n terms filling the fields of
the record.
Let us define the rational 1/2.
Coq < Theorem two_is_positive : (gt (S (S O)) O).
Coq < Repeat Constructor.
Coq < Save.
Coq < Definition half := (mkRat (S O) (S (S O)) two_is_positive).
Coq < Check half.
half
: Rat
The macro generates also, when it is possible, the projection
functions for destructuring an object of type ident.
These projection functions have the same name that the corresponding
field. In our example:
Coq < Eval Compute in (top half).
= (S O)
: nat
Coq < Eval Compute in (bottom half).
= (S (S O))
: nat
Coq < Eval Compute in (Rat_cond half).
= two_is_positive
: (gt (bottom half) O)
Warnings:
-
Warning: identi cannot be defined.
It can happens that the definition of a projection is impossible.
This message is followed by an explanation of this impossibility.
There may be three reasons:
-
The name identi already exists in the environment (see
section 1.3.1).
- The body of identi uses a incorrect elimination for
ident (see sections 1.3.4 and 4.5.4).
- The projections [ idents ] were not defined.
The body of termi uses the projections idents
which are not defined for one of these three reasons listed here.
Error messages:
-
A record cannot be recursive
The record name ident appears in the type of its fields.
During the definition of the one-constructor inductive definition,
all the errors of inductive definitions, as described in section
1.3.3, may occur.
Variants:
-
Record ident [ params ] : sort :=
{
ident1 : term1;
...
identn : termn }
.
One can omit the constructor name in which case the system will use
the name Build_ident.