Merge PR #10430: [Extraction] Add support for primitive integers

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

7 files changed, 129 insertions, 2 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..acf68e9fd2 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2443,12 +2443,19 @@ 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
+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. 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/kernel/uint63.mli b/kernel/uint63.mli
index 93632da110..5542716af2 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -37,6 +37,8 @@ val mul     : t -> t -> t
 val div     : t -> t -> t
 val rem     : t -> t -> t
 
+val diveucl : t -> t -> t * t
+
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
@@ -57,3 +59,13 @@ val head0   : t -> t
 val tail0   : t -> t
 
 val is_uint63 : Obj.t -> bool
+
+(* Arithmetic with explicit carries *)
+
+(* Analog of Numbers.Abstract.Cyclic.carry *)
+type 'a carry = C0 of 'a | C1 of 'a
+
+val addc : t -> t -> t carry
+val addcarryc : t -> t -> t carry
+val subc : t -> t -> t carry
+val subcarryc : t -> t -> t carry
diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml
index 20b2f58496..d6b077a9f5 100644
--- a/kernel/uint63_amd64_63.ml
+++ b/kernel/uint63_amd64_63.ml
@@ -82,6 +82,8 @@ let div (x : int) (y : int) =
 let rem (x : int) (y : int) =
   if y = 0 then 0 else Int64.to_int (Int64.rem (to_uint64 x) (to_uint64 y))
 
+let diveucl x y = (div x y, rem x y)
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y (uint_size - p))
 
@@ -225,3 +227,24 @@ let tail0 x =
 let is_uint63 t =
   Obj.is_int t
 [@@ocaml.inline always]
+
+(* Arithmetic with explicit carries *)
+
+(* Analog of Numbers.Abstract.Cyclic.carry *)
+type 'a carry = C0 of 'a | C1 of 'a
+
+let addc x y =
+  let r = x + y in
+  if lt r x then C1 r else C0 r
+
+let addcarryc x y =
+  let r = x + y + 1 in
+  if le r x then C1 r else C0 r
+
+let subc x y =
+  let r = x - y in
+  if le y x then C0 r else C1 r
+
+let subcarryc x y =
+  let r = x - y - 1 in
+  if lt y x then C0 r else C1 r
diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml
index c3279779e1..2a3fc75ec1 100644
--- a/kernel/uint63_i386_31.ml
+++ b/kernel/uint63_i386_31.ml
@@ -83,6 +83,8 @@ let div x y =
 let rem x y =
   if y = 0L then 0L else Int64.rem x y
 
+let diveucl x y = (div x y, rem x y)
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
 
@@ -191,6 +193,27 @@ let is_uint63 t =
   Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag
   && le (Obj.magic t) maxuint63
 
+(* Arithmetic with explicit carries *)
+
+(* Analog of Numbers.Abstract.Cyclic.carry *)
+type 'a carry = C0 of 'a | C1 of 'a
+
+let addc x y =
+  let r = add x y in
+  if lt r x then C1 r else C0 r
+
+let addcarryc x y =
+  let r = addcarry x y in
+  if le r x then C1 r else C0 r
+
+let subc x y =
+  let r = sub x y in
+  if le y x then C0 r else C1 r
+
+let subcarryc x y =
+  let r = subcarry x y in
+  if lt y x then C0 r else C1 r
+
 (* Register all exported functions so that they can be called from C code *)
 
 let () =
diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v
new file mode 100644
index 0000000000..a2ee602313
--- /dev/null
+++ b/plugins/extraction/ExtrOCamlInt63.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   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" ].
+Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ].
+
+(** 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".
+
+Extract Constant Int63.addc => "Uint63.addc".
+Extract Constant Int63.addcarryc => "Uint63.addcarryc".
+Extract Constant Int63.subc => "Uint63.subc".
+Extract Constant Int63.subcarryc => "Uint63.subcarryc".
+
+Extract Constant Int63.diveucl => "Uint63.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".