diff options
| -rw-r--r-- | doc/changelog/08-tools/10430-extraction-int63.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 19 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOCamlInt63.v | 52 |
4 files changed, 72 insertions, 5 deletions
diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..070fc44775 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2443,11 +2443,20 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said 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. +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module (excepted :g:`addc`, :g:`addcarryc`, +:g:`subc`, :g:`subcarryc`, and :g:`diveucl` whose implementation in OCaml is +left to the reader). 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 :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). Bidirectionality hints ---------------------- diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..b0e918c013 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native 63-bit machine integers. *) + +From Coq Require Int63 Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +(* TODO: a few primitive operations have no implementation in the kernel module +Uint63. Namely addc, addcarryc, subc, subcarryc, and diveucl. *) + +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". |