From 3083b2dcd9da8108df8118be2bc87f955311d2bd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 5 Jul 2019 15:01:26 +0200
Subject: Simplify picking between uint63_63.ml and uint63_31.ml

- remove the architecture component (we don't do anything
  arch-specific so it was just a rewording of int_size)
- have configure tell the make build system about int_size instead of
  reimplementing cp

As a bonus, add the copyright header to uint63.mli.
---
 kernel/dune               |   4 +-
 kernel/uint63.mli         |  10 ++
 kernel/uint63_31.ml       | 216 +++++++++++++++++++++++++++++++++++++++++++
 kernel/uint63_63.ml       | 227 ++++++++++++++++++++++++++++++++++++++++++++++
 kernel/uint63_amd64_63.ml | 227 ----------------------------------------------
 kernel/uint63_i386_31.ml  | 216 -------------------------------------------
 kernel/write_uint63.ml    |  38 --------
 7 files changed, 455 insertions(+), 483 deletions(-)
 create mode 100644 kernel/uint63_31.ml
 create mode 100644 kernel/uint63_63.ml
 delete mode 100644 kernel/uint63_amd64_63.ml
 delete mode 100644 kernel/uint63_i386_31.ml
 delete mode 100644 kernel/write_uint63.ml

(limited to 'kernel')

diff --git a/kernel/dune b/kernel/dune
index 4038bf5638..5f7502ef6b 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
  (synopsis "The Coq Kernel")
  (public_name coq.kernel)
  (wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
  (libraries lib byterun dynlink))
 
 (executable
@@ -16,7 +16,7 @@
 
 (rule
  (targets uint63.ml)
- (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml))
+ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
  (action (copy# %{gen-file} %{targets})))
 
 (documentation
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 5542716af2..d22ba3468f 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
 type t
 
 val uint_size : int
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
new file mode 100644
index 0000000000..b8eccd19fb
--- /dev/null
+++ b/kernel/uint63_31.ml
@@ -0,0 +1,216 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(* Invariant: the msb should be 0 *)
+type t = Int64.t
+
+let _ = assert (Sys.word_size = 32)
+
+let uint_size = 63
+
+let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
+let maxuint31 = Int64.of_string "0x7FFFFFFF"
+
+let zero = Int64.zero
+let one = Int64.one
+
+    (* conversion from an int *)
+let mask63 i = Int64.logand i maxuint63
+let of_int i = 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 hash i =
+  let (h,l) = to_int2 i in
+  (*Hashset.combine h l*)
+  h * 65599 + l
+
+    (* 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
+
+    (* comparison *)
+let lt x y =
+  Int64.compare x y < 0
+
+let le x y =
+  Int64.compare x y <= 0
+
+    (* logical shift *)
+let l_sl x y =
+  if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L
+
+let l_sr x y =
+  if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L
+
+let l_and x y = Int64.logand x y
+let l_or x y = Int64.logor x y
+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
+
+    (* subtraction *)
+let sub x y = mask63 (Int64.sub x y)
+
+let subcarry x y = sub (sub x y) Int64.one
+
+    (* multiplication *)
+let mul x y = mask63 (Int64.mul x y)
+
+    (* division *)
+let div x y =
+  if y = 0L then 0L else Int64.div x y
+
+    (* modulo *)
+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))
+
+    (* division of two numbers by one *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
+let div21 xh xl y =
+  let nh = ref xh in
+  let nl = ref xl in
+  let q = ref 0L in
+  for _i = 0 to 62 do
+    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
+       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+    nl := Int64.shift_left !nl 1;
+    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
+    q := Int64.shift_left !q 1;
+    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+       once OCaml 4.08 becomes the minimal required version *)
+    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+      begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
+  done;
+  !q, !nh
+
+let div21 xh xl y =
+  if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
+
+     (* exact multiplication *)
+let mulc x y =
+  let lx = ref (Int64.logand x maxuint31) in
+  let ly = ref (Int64.logand y maxuint31) in
+  let hx = Int64.shift_right x 31 in
+  let hy = Int64.shift_right y 31 in
+  let hr = ref (Int64.mul hx hy) in
+  let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
+  hr := (Int64.shift_right_logical !hr 1);
+  lx := Int64.mul !lx hy;
+  ly := Int64.mul hx !ly;
+  hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
+  lr := Int64.add !lr (Int64.shift_left !lx 31);
+  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
+  lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
+  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
+  if Int64.logand !lr Int64.min_int <> 0L
+  then Int64.(sub !hr one, mask63 !lr)
+  else (!hr, !lr)
+
+let equal x y = mask63 x = mask63 y
+
+let compare x y = Int64.compare x y
+
+(* Number of leading zeroes *)
+let head0 x =
+  let r = ref 0 in
+  let x = ref x in
+  if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31
+  else x := Int64.shift_right !x 31;
+  if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16);
+  if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8);
+  if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4);
+  if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2);
+  if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1);
+  if Int64.logand !x 0x80000000L = 0L then (r := !r + 1);
+  Int64.of_int !r
+
+(* Number of trailing zeroes *)
+let tail0 x =
+  let r = ref 0 in
+  let x = ref x in
+  if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32);
+  if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16);
+  if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8);
+  if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4);
+  if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2);
+  if Int64.logand !x 0x1L = 0L then (r := !r + 1);
+  Int64.of_int !r
+
+(* May an object be safely cast into an Uint63.t ? *)
+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 () =
+  Callback.register "uint63 add" add;
+  Callback.register "uint63 addcarry" addcarry;
+  Callback.register "uint63 addmuldiv" addmuldiv;
+  Callback.register "uint63 div" div;
+  Callback.register "uint63 div21_ml" div21;
+  Callback.register "uint63 eq" equal;
+  Callback.register "uint63 eq0" (equal Int64.zero);
+  Callback.register "uint63 head0" head0;
+  Callback.register "uint63 land" l_and;
+  Callback.register "uint63 leq" le;
+  Callback.register "uint63 lor" l_or;
+  Callback.register "uint63 lsl" l_sl;
+  Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one);
+  Callback.register "uint63 lsr" l_sr;
+  Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one);
+  Callback.register "uint63 lt" lt;
+  Callback.register "uint63 lxor" l_xor;
+  Callback.register "uint63 mod" rem;
+  Callback.register "uint63 mul" mul;
+  Callback.register "uint63 mulc_ml" mulc;
+  Callback.register "uint63 one" one;
+  Callback.register "uint63 sub" sub;
+  Callback.register "uint63 subcarry" subcarry;
+  Callback.register "uint63 tail0" tail0
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
new file mode 100644
index 0000000000..5c4028e1c8
--- /dev/null
+++ b/kernel/uint63_63.ml
@@ -0,0 +1,227 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+type t = int
+
+let _ = assert (Sys.word_size = 64)
+
+let uint_size = 63
+
+let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
+let maxuint31 = 0x7FFFFFFF
+
+    (* conversion from an int *)
+let to_uint64 i = Int64.logand (Int64.of_int i) maxuint63
+
+let of_int i = i
+[@@ocaml.inline always]
+
+let to_int2 i = (0,i)
+
+let of_int64 _i = assert false
+
+let hash i = i
+[@@ocaml.inline always]
+
+    (* 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
+
+let zero = 0
+let one = 1
+
+    (* logical shift *)
+let l_sl x y =
+  if 0 <= y && y < 63 then x lsl y else 0
+
+let l_sr x y =
+  if 0 <= y && y < 63 then x lsr y else 0
+
+let l_and x y = x land y
+[@@ocaml.inline always]
+
+let l_or x y = x lor y
+[@@ocaml.inline always]
+
+let l_xor x y = x lxor y
+[@@ocaml.inline always]
+
+    (* addition of int63 *)
+let add x y = x + y
+[@@ocaml.inline always]
+
+    (* subtraction *)
+let sub x y = x - y
+[@@ocaml.inline always]
+
+    (* multiplication *)
+let mul x y = x * y
+[@@ocaml.inline always]
+
+    (* division *)
+let div (x : int) (y : int) =
+  if y = 0 then 0 else Int64.to_int (Int64.div (to_uint64 x) (to_uint64 y))
+
+    (* modulo *)
+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))
+
+    (* comparison *)
+let lt (x : int) (y : int) =
+  (x lxor 0x4000000000000000) < (y lxor 0x4000000000000000)
+[@@ocaml.inline always]
+
+let le (x : int) (y : int) =
+  (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
+[@@ocaml.inline always]
+
+    (* division of two numbers by one *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
+let div21 xh xl y =
+  (* nh might temporarily grow as large as 2*y - 1 in the loop body,
+     so we store it as a 64-bit unsigned integer *)
+  let nh = ref xh in
+  let nl = ref xl in
+  let q = ref 0 in
+  for _i = 0 to 62 do
+    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63,
+       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.of_int (!nl lsr 62));
+    nl := !nl lsl 1;
+    q := !q lsl 1;
+    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+       once OCaml 4.08 becomes the minimal required version *)
+    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+      begin q := !q lor 1; nh := Int64.sub !nh y; end
+  done;
+  !q, Int64.to_int !nh
+
+let div21 xh xl y =
+  let xh = to_uint64 xh in
+  let y = to_uint64 y in
+  if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y
+
+     (* exact multiplication *)
+(* TODO: check that none of these additions could be a logical or *)
+
+
+(* size = 32 + 31
+   (hx << 31 + lx) * (hy << 31 + ly) =
+   hxhy << 62 + (hxly + lxhy) << 31 + lxly
+*)
+
+(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *)
+let mulc_aux x y =
+  let lx = x land maxuint31 in
+  let ly = y land maxuint31 in
+  let hx = x lsr 31  in
+  let hy = y lsr 31 in
+    (* hx and hy are 32 bits value but at most one is 32 *)
+  let hxy  = hx * hy in (* 63 bits *)
+  let hxly = hx * ly in (* 63 bits *)
+  let lxhy = lx * hy in (* 63 bits *)
+  let lxy  = lx * ly in (* 62 bits *)
+  let l  = lxy lor (hxy lsl 62) (* 63 bits *) in
+  let h  = hxy lsr 1 in (* 62 bits *)
+  let hl = hxly + lxhy in (* We can have a carry *)
+  let h  = if lt hl hxly then h + (1 lsl 31) else h in
+  let hl'= hl lsl 31 in
+  let l  = l + hl' in
+  let h  = if lt l hl' then h + 1 else h in
+  let h  = h + (hl lsr 32) in
+  (h,l)
+
+let mulc x y =
+  if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y
+  else
+    let yl = y lxor (1 lsl 62) in
+    let (h,l) = mulc_aux x yl in
+    (* h << 63 + l = x * yl
+       x * y = x * (1 << 62 + yl)  =
+       x << 62 + x*yl = x << 62 + h << 63 + l *)
+    let l' = l + (x lsl 62) in
+    let h = if lt l' l then h + 1 else h in
+    (h + (x lsr 1), l')
+
+let equal (x : int) (y : int) = x = y
+[@@ocaml.inline always]
+
+let compare (x:int) (y:int) =
+  let x = x lxor 0x4000000000000000 in
+  let y = y lxor 0x4000000000000000 in
+  if x > y then 1
+  else if y > x then -1
+  else 0
+
+    (* head tail *)
+
+let head0 x =
+  let r = ref 0 in
+  let x = ref x in
+  if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31
+  else x := !x lsr 31;
+  if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16);
+  if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8);
+  if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4);
+  if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2);
+  if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1);
+  if !x land 0x80000000 = 0 then (               r := !r + 1);
+  !r;;
+
+let tail0 x =
+  let r = ref 0 in
+  let x = ref x in
+  if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32);
+  if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16);
+  if !x land 0xFF = 0   then (x := !x lsr 8;  r := !r + 8);
+  if !x land 0xF = 0    then (x := !x lsr 4;  r := !r + 4);
+  if !x land 0x3 = 0    then (x := !x lsr 2;  r := !r + 2);
+  if !x land 0x1 = 0    then (                r := !r + 1);
+  !r
+
+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_amd64_63.ml b/kernel/uint63_amd64_63.ml
deleted file mode 100644
index 5c4028e1c8..0000000000
--- a/kernel/uint63_amd64_63.ml
+++ /dev/null
@@ -1,227 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-type t = int
-
-let _ = assert (Sys.word_size = 64)
-
-let uint_size = 63
-
-let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
-let maxuint31 = 0x7FFFFFFF
-
-    (* conversion from an int *)
-let to_uint64 i = Int64.logand (Int64.of_int i) maxuint63
-
-let of_int i = i
-[@@ocaml.inline always]
-
-let to_int2 i = (0,i)
-
-let of_int64 _i = assert false
-
-let hash i = i
-[@@ocaml.inline always]
-
-    (* 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
-
-let zero = 0
-let one = 1
-
-    (* logical shift *)
-let l_sl x y =
-  if 0 <= y && y < 63 then x lsl y else 0
-
-let l_sr x y =
-  if 0 <= y && y < 63 then x lsr y else 0
-
-let l_and x y = x land y
-[@@ocaml.inline always]
-
-let l_or x y = x lor y
-[@@ocaml.inline always]
-
-let l_xor x y = x lxor y
-[@@ocaml.inline always]
-
-    (* addition of int63 *)
-let add x y = x + y
-[@@ocaml.inline always]
-
-    (* subtraction *)
-let sub x y = x - y
-[@@ocaml.inline always]
-
-    (* multiplication *)
-let mul x y = x * y
-[@@ocaml.inline always]
-
-    (* division *)
-let div (x : int) (y : int) =
-  if y = 0 then 0 else Int64.to_int (Int64.div (to_uint64 x) (to_uint64 y))
-
-    (* modulo *)
-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))
-
-    (* comparison *)
-let lt (x : int) (y : int) =
-  (x lxor 0x4000000000000000) < (y lxor 0x4000000000000000)
-[@@ocaml.inline always]
-
-let le (x : int) (y : int) =
-  (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
-[@@ocaml.inline always]
-
-    (* division of two numbers by one *)
-(* precondition: xh < y *)
-(* outputs: q, r s.t. x = q * y + r, r < y *)
-let div21 xh xl y =
-  (* nh might temporarily grow as large as 2*y - 1 in the loop body,
-     so we store it as a 64-bit unsigned integer *)
-  let nh = ref xh in
-  let nl = ref xl in
-  let q = ref 0 in
-  for _i = 0 to 62 do
-    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63,
-       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
-    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.of_int (!nl lsr 62));
-    nl := !nl lsl 1;
-    q := !q lsl 1;
-    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
-       once OCaml 4.08 becomes the minimal required version *)
-    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
-      begin q := !q lor 1; nh := Int64.sub !nh y; end
-  done;
-  !q, Int64.to_int !nh
-
-let div21 xh xl y =
-  let xh = to_uint64 xh in
-  let y = to_uint64 y in
-  if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y
-
-     (* exact multiplication *)
-(* TODO: check that none of these additions could be a logical or *)
-
-
-(* size = 32 + 31
-   (hx << 31 + lx) * (hy << 31 + ly) =
-   hxhy << 62 + (hxly + lxhy) << 31 + lxly
-*)
-
-(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *)
-let mulc_aux x y =
-  let lx = x land maxuint31 in
-  let ly = y land maxuint31 in
-  let hx = x lsr 31  in
-  let hy = y lsr 31 in
-    (* hx and hy are 32 bits value but at most one is 32 *)
-  let hxy  = hx * hy in (* 63 bits *)
-  let hxly = hx * ly in (* 63 bits *)
-  let lxhy = lx * hy in (* 63 bits *)
-  let lxy  = lx * ly in (* 62 bits *)
-  let l  = lxy lor (hxy lsl 62) (* 63 bits *) in
-  let h  = hxy lsr 1 in (* 62 bits *)
-  let hl = hxly + lxhy in (* We can have a carry *)
-  let h  = if lt hl hxly then h + (1 lsl 31) else h in
-  let hl'= hl lsl 31 in
-  let l  = l + hl' in
-  let h  = if lt l hl' then h + 1 else h in
-  let h  = h + (hl lsr 32) in
-  (h,l)
-
-let mulc x y =
-  if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y
-  else
-    let yl = y lxor (1 lsl 62) in
-    let (h,l) = mulc_aux x yl in
-    (* h << 63 + l = x * yl
-       x * y = x * (1 << 62 + yl)  =
-       x << 62 + x*yl = x << 62 + h << 63 + l *)
-    let l' = l + (x lsl 62) in
-    let h = if lt l' l then h + 1 else h in
-    (h + (x lsr 1), l')
-
-let equal (x : int) (y : int) = x = y
-[@@ocaml.inline always]
-
-let compare (x:int) (y:int) =
-  let x = x lxor 0x4000000000000000 in
-  let y = y lxor 0x4000000000000000 in
-  if x > y then 1
-  else if y > x then -1
-  else 0
-
-    (* head tail *)
-
-let head0 x =
-  let r = ref 0 in
-  let x = ref x in
-  if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31
-  else x := !x lsr 31;
-  if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16);
-  if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8);
-  if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4);
-  if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2);
-  if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1);
-  if !x land 0x80000000 = 0 then (               r := !r + 1);
-  !r;;
-
-let tail0 x =
-  let r = ref 0 in
-  let x = ref x in
-  if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32);
-  if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16);
-  if !x land 0xFF = 0   then (x := !x lsr 8;  r := !r + 8);
-  if !x land 0xF = 0    then (x := !x lsr 4;  r := !r + 4);
-  if !x land 0x3 = 0    then (x := !x lsr 2;  r := !r + 2);
-  if !x land 0x1 = 0    then (                r := !r + 1);
-  !r
-
-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
deleted file mode 100644
index b8eccd19fb..0000000000
--- a/kernel/uint63_i386_31.ml
+++ /dev/null
@@ -1,216 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-(* Invariant: the msb should be 0 *)
-type t = Int64.t
-
-let _ = assert (Sys.word_size = 32)
-
-let uint_size = 63
-
-let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
-let maxuint31 = Int64.of_string "0x7FFFFFFF"
-
-let zero = Int64.zero
-let one = Int64.one
-
-    (* conversion from an int *)
-let mask63 i = Int64.logand i maxuint63
-let of_int i = 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 hash i =
-  let (h,l) = to_int2 i in
-  (*Hashset.combine h l*)
-  h * 65599 + l
-
-    (* 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
-
-    (* comparison *)
-let lt x y =
-  Int64.compare x y < 0
-
-let le x y =
-  Int64.compare x y <= 0
-
-    (* logical shift *)
-let l_sl x y =
-  if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L
-
-let l_sr x y =
-  if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L
-
-let l_and x y = Int64.logand x y
-let l_or x y = Int64.logor x y
-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
-
-    (* subtraction *)
-let sub x y = mask63 (Int64.sub x y)
-
-let subcarry x y = sub (sub x y) Int64.one
-
-    (* multiplication *)
-let mul x y = mask63 (Int64.mul x y)
-
-    (* division *)
-let div x y =
-  if y = 0L then 0L else Int64.div x y
-
-    (* modulo *)
-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))
-
-    (* division of two numbers by one *)
-(* precondition: xh < y *)
-(* outputs: q, r s.t. x = q * y + r, r < y *)
-let div21 xh xl y =
-  let nh = ref xh in
-  let nl = ref xl in
-  let q = ref 0L in
-  for _i = 0 to 62 do
-    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
-       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
-    nl := Int64.shift_left !nl 1;
-    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
-    q := Int64.shift_left !q 1;
-    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
-       once OCaml 4.08 becomes the minimal required version *)
-    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
-      begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
-  done;
-  !q, !nh
-
-let div21 xh xl y =
-  if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
-
-     (* exact multiplication *)
-let mulc x y =
-  let lx = ref (Int64.logand x maxuint31) in
-  let ly = ref (Int64.logand y maxuint31) in
-  let hx = Int64.shift_right x 31 in
-  let hy = Int64.shift_right y 31 in
-  let hr = ref (Int64.mul hx hy) in
-  let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
-  hr := (Int64.shift_right_logical !hr 1);
-  lx := Int64.mul !lx hy;
-  ly := Int64.mul hx !ly;
-  hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
-  lr := Int64.add !lr (Int64.shift_left !lx 31);
-  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
-  lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
-  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
-  if Int64.logand !lr Int64.min_int <> 0L
-  then Int64.(sub !hr one, mask63 !lr)
-  else (!hr, !lr)
-
-let equal x y = mask63 x = mask63 y
-
-let compare x y = Int64.compare x y
-
-(* Number of leading zeroes *)
-let head0 x =
-  let r = ref 0 in
-  let x = ref x in
-  if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31
-  else x := Int64.shift_right !x 31;
-  if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16);
-  if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8);
-  if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4);
-  if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2);
-  if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1);
-  if Int64.logand !x 0x80000000L = 0L then (r := !r + 1);
-  Int64.of_int !r
-
-(* Number of trailing zeroes *)
-let tail0 x =
-  let r = ref 0 in
-  let x = ref x in
-  if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32);
-  if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16);
-  if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8);
-  if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4);
-  if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2);
-  if Int64.logand !x 0x1L = 0L then (r := !r + 1);
-  Int64.of_int !r
-
-(* May an object be safely cast into an Uint63.t ? *)
-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 () =
-  Callback.register "uint63 add" add;
-  Callback.register "uint63 addcarry" addcarry;
-  Callback.register "uint63 addmuldiv" addmuldiv;
-  Callback.register "uint63 div" div;
-  Callback.register "uint63 div21_ml" div21;
-  Callback.register "uint63 eq" equal;
-  Callback.register "uint63 eq0" (equal Int64.zero);
-  Callback.register "uint63 head0" head0;
-  Callback.register "uint63 land" l_and;
-  Callback.register "uint63 leq" le;
-  Callback.register "uint63 lor" l_or;
-  Callback.register "uint63 lsl" l_sl;
-  Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one);
-  Callback.register "uint63 lsr" l_sr;
-  Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one);
-  Callback.register "uint63 lt" lt;
-  Callback.register "uint63 lxor" l_xor;
-  Callback.register "uint63 mod" rem;
-  Callback.register "uint63 mul" mul;
-  Callback.register "uint63 mulc_ml" mulc;
-  Callback.register "uint63 one" one;
-  Callback.register "uint63 sub" sub;
-  Callback.register "uint63 subcarry" subcarry;
-  Callback.register "uint63 tail0" tail0
diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml
deleted file mode 100644
index 57a170c8f5..0000000000
--- a/kernel/write_uint63.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-(** Equivalent of rm -f *)
-let safe_remove f =
-  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
-
-(** * Generate an implementation of 63-bit arithmetic *)
-let ml_file_copy input output =
-  safe_remove output;
-  let i = open_in input in
-  let o = open_out output in
-  let pr s = Printf.fprintf o s in
-  pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n";
-  pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n";
-  try
-    while true do
-      output_string o (input_line i); output_char o '\n'
-    done
-  with End_of_file ->
-    close_in i;
-    close_out o;
-    Unix.chmod output 0o444
-
-let write_uint63 () =
-  ml_file_copy
-    (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml"
-     else (* 64 bits *) "uint63_amd64_63.ml")
-    "uint63.ml"
-
-let () = write_uint63 ()
-- 
cgit v1.2.3