[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.

5 files changed, 68 insertions, 8 deletions

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
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
index b0e918c013..a2ee602313 100644
--- a/plugins/extraction/ExtrOCamlInt63.v
+++ b/plugins/extraction/ExtrOCamlInt63.v
@@ -17,6 +17,7 @@ From Coq Require Int63 Extraction.
 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".
@@ -40,9 +41,12 @@ 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.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".