3 files changed, 58 insertions, 0 deletions
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 () =