18.6 Extraction
Once a program is proved, one usually wants to run it, and that's why
this implementation comes with an extraction mechanism.
For the moment, there is only extraction to Objective Caml code.
This functionality is provided by the following module:
Require ProgramsExtraction.
This extraction facility extends the extraction of functional programs
(see chapter 19), on which it is based.
Indeed, the extraction of functional terms (Coq objects) is first
performed by the module Extraction, and the extraction of
imperative programs comes after.
Therefore, we have kept the same syntax as for functional terms:
Write Caml File "string" [ ident1 ... identn ].
where string is the name given to the file to be produced (the suffix
.ml is added if necessary), and ident1 ... identn the
names of the objects to be extracted.
That list may contain functional and imperative objects, and does not need
to be exhaustive.
Of course, you can use the extraction facilities described in
chapter 19, namely the ML Import,
Link and Extract commands.
The case of integers
There is no use of the Objective Caml native integers: indeed, it would not be safe
to use the machine integers while the correctness proof is done
with unbounded integers (nat, Z or whatever type).
But since Objective Caml arrays are indexed over the type int
(the machine integers) arrays indexes are converted from Z
to int when necessary (the conversion is very fast: due
to the binary representation of integers in type Z, it
will never exceed thirty elementary steps).
And it is also safe, since the size of a Objective Caml array can not be greater
than the maximum integer (230-1) and since the correctness proof
establishes that indexes are always within the bounds of arrays
(Therefore, indexes will never be greater than the maximum integer,
and the conversion will never produce an overflow).