Merge PR #13540: Clean support of primitive integers

Reviewed-by: ppedrot
Reviewed-by: proux01

4 files changed, 12 insertions, 24 deletions

diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index d92bbe87eb..13568957c2 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -20,7 +20,7 @@
 
 # define DECLARE_NULLOP(name) \
 value uint63_##name() { \
-  static value* cb = 0; \
+  static value const *cb = 0; \
   CAMLparam0(); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(*cb); \
@@ -28,7 +28,7 @@ value uint63_##name() { \
 
 # define DECLARE_UNOP(name) \
 value uint63_##name##_ml(value x) { \
-  static value* cb = 0; \
+  static value const *cb = 0; \
   CAMLparam1(x); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback(*cb, x)); \
@@ -53,7 +53,7 @@ value uint63_##name##_ml(value x) { \
 
 # define DECLARE_BINOP(name) \
 value uint63_##name##_ml(value x, value y) { \
-  static value* cb = 0; \
+  static value const *cb = 0; \
   CAMLparam2(x, y); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback2(*cb, x, y)); \
@@ -79,7 +79,7 @@ value uint63_##name##_ml(value x, value y) { \
 
 # define DECLARE_TEROP(name) \
 value uint63_##name##_ml(value x, value y, value z) { \
-  static value* cb = 0; \
+  static value const *cb = 0; \
   CAMLparam3(x, y, z); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback3(*cb, x, y, z)); \
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 6b47dfc61d..6b2519918a 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -17,6 +17,7 @@ val maxuint31 : t
 val of_int : int -> t
 val to_int2 : t -> int * int (* msb, lsb *)
 val of_int64 : Int64.t -> t
+val to_int64 : t -> Int64.t
 (*
 val of_uint : int -> t
  *)
@@ -32,7 +33,6 @@ val hash : t -> int
 
      (* conversion to a string *)
 val to_string : t -> string
-val of_string : string -> t
 
 val compile : t -> string
 
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 5b2d934b5d..988611df3e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -23,9 +23,10 @@ let one = Int64.one
 
     (* conversion from an int *)
 let mask63 i = Int64.logand i maxuint63
-let of_int i = Int64.of_int i
+let of_int i = mask63 (Int64.of_int i)
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
-let of_int64 i = i
+let of_int64 = mask63
+let to_int64 i = i
 
 let to_int_min n m =
   if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
@@ -41,13 +42,6 @@ let hash i =
     (* conversion of an uint63 to a string *)
 let to_string i = Int64.to_string i
 
-let of_string s =
-  let i64 = Int64.of_string s in
-  if Int64.compare Int64.zero i64 <= 0
-      && Int64.compare i64 maxuint63 <= 0
-  then i64
-  else raise (Failure "Int63.of_string")
-
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i
 
@@ -72,12 +66,12 @@ let l_xor x y = Int64.logxor x y
     (* addition of int63 *)
 let add x y = mask63 (Int64.add x y)
 
-let addcarry x y = add (add x y) Int64.one
+let addcarry x y = mask63 Int64.(add (add x y) one)
 
     (* subtraction *)
 let sub x y = mask63 (Int64.sub x y)
 
-let subcarry x y = sub (sub x y) Int64.one
+let subcarry x y = mask63 Int64.(sub (sub x y) one)
 
     (* multiplication *)
 let mul x y = mask63 (Int64.mul x y)
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 21f57e2bfb..8d052d6593 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -25,7 +25,8 @@ let of_int i = i
 
 let to_int2 i = (0,i)
 
-let of_int64 _i = assert false
+let of_int64 = Int64.to_int
+let to_int64 = to_uint64
 
 let of_float = int_of_float
 
@@ -39,13 +40,6 @@ let hash i = i
     (* conversion of an uint63 to a string *)
 let to_string i = Int64.to_string (to_uint64 i)
 
-let of_string s =
-  let i64 = Int64.of_string s in
-  if Int64.compare Int64.zero i64 <= 0
-      && Int64.compare i64 maxuint63 <= 0
-  then Int64.to_int i64
-  else raise (Failure "Int64.of_string")
-
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int (%i)" i