From c878a5e2c0c2a01512e263d3ed2dfdd8e611086f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 25 Jun 2019 09:10:44 +0000 Subject: [Extraction] Add support for primitive integers The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel). --- doc/changelog/08-tools/10430-extraction-int63.rst | 5 +++++ doc/sphinx/language/gallina-extensions.rst | 19 ++++++++++++++----- doc/stdlib/hidden-files | 1 + 3 files changed, 20 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/08-tools/10430-extraction-int63.rst (limited to 'doc') 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 `_, + fixes `#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 -- cgit v1.2.3 From 8675b9d1a574aceb9a9d40c9c135db9c042e00b1 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 22 Jul 2019 12:47:53 +0000 Subject: [Int63] Implement all primitives in OCaml Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives. --- doc/sphinx/language/gallina-extensions.rst | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 070fc44775..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2446,12 +2446,10 @@ operations. 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. +and functions of a :g:`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 :g:`Int63.int`) are extracted to literal OCaml values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on -- cgit v1.2.3