[michocoq] Simplify extraction of uint63
The recommended way of extracting primitive integers in Coq is essentially to:
- provide a manually-written ml file which must be named
uint63.ml
and must define a conversion functionof_int
(on 64-bit architecture) from OCaml's standardint
type andUint63.t
, - require the
ExtrOCamlInt63
module.
Unfortunately, new versions of Coq Stdlib introduce a Uint63
module which clashes with this uint63
OCaml module upon extraction. As a result the extracted Uint63
modules gets overridden and the functions Uint63.of_Z
and Uint63.to_Z
which we use a lot, directly or not, in tez.v
are missing.
In this MR we use another extraction strategy; we simply extract explicitly the few primitive integer functions declared in the PrimInt63
module, we and let Coq extraction work as usual on everything else, including the Uint63
module which is extracted to another name to avoid the clash (using Extraction Blacklist Uint63
). The hand-written uint63.ml
is minimal; it only defined of_int
as the identity function.
Unfortunately, this only works for newer versions of Coq Stdlib (since the introduction of the PrimInt63
and Uint63
). So we should wait for !170 (merged) dropping support for old Coq versions before merging this MR.