Skip to content

[michocoq] Simplify extraction of uint63

Raphaël Cauderlier requested to merge rafoo@simplify-uint63-extraction into dev

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 function of_int (on 64-bit architecture) from OCaml's standard int type and Uint63.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.

Edited by Raphaël Cauderlier

Merge request reports