Primitive objects¶
Primitive Integers¶
The language of terms features 63-bit machine integers as values. The type of
such a value is axiomatized; it is declared through the following sentence
(excerpt from the Int63 module):
This type is equipped with a few operators, that must be similarly declared.
For instance, equality of two primitive integers can be decided using the Int63.eqb function,
declared and specified as follows:
The complete set of such operators can be obtained looking at the Int63 module.
These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
Print Assumptions command, as in the following example.
- From Coq Require Import Int63.
- [Loading ML file newring_plugin.cmxs ... done] [Loading ML file zify_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done] [Loading ML file int63_syntax_plugin.cmxs ... done]
- Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63.
- 1 subgoal ============================ (1 - 1)%int63 = 0%int63
- Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
- No more subgoals.
- Print Assumptions one_minus_one_is_zero.
- Axioms: sub : int -> int -> int eqb_correct : forall i j : int, (i == j)%int63 = true -> i = j eqb : int -> int -> bool
The reduction machines (vm_compute, native_compute) implement
dedicated, efficient, rules to reduce the applications of these primitive
operations.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlInt63
module can be used when extracting to OCaml: it maps the Coq primitives to types
and functions of a Uint63 module. Said OCaml module is not produced by
extraction. Instead, it has to be provided by the user (if they want to compile
or execute the extracted code). For instance, an implementation of this module
can be taken from the kernel of Coq.
Literal values (at type Int63.int) are extracted to literal OCaml values
wrapped into the Uint63.of_int (resp. Uint63.of_int64) constructor on
64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
function Uint63.compile from the kernel).
Primitive Floats¶
The language of terms features Binary64 floating-point numbers as values.
The type of such a value is axiomatized; it is declared through the
following sentence (excerpt from the PrimFloat module):
This type is equipped with a few operators, that must be similarly declared.
For instance, the product of two primitive floats can be computed using the
PrimFloat.mul function, declared and specified as follows:
where Prim2SF is defined in the FloatOps module.
The set of such operators is described in section Floats library.
These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the
Print Assumptions command.
The reduction machines (vm_compute, native_compute) implement
dedicated, efficient rules to reduce the applications of these primitive
operations, using the floating-point processor operators that are assumed
to comply with the IEEE 754 standard for floating-point arithmetic.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlFloats
module can be used when extracting to OCaml: it maps the Coq primitives to types
and functions of a Float64 module. Said OCaml module is not produced by
extraction. Instead, it has to be provided by the user (if they want to compile
or execute the extracted code). For instance, an implementation of this module
can be taken from the kernel of Coq.
Literal values (of type Float64.t) are extracted to literal OCaml
values (of type float) written in hexadecimal notation and
wrapped into the Float64.of_float constructor, e.g.:
Float64.of_float (0x1p+0).