Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 87 insertions, 123 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 93e74af845..a6b48cd7e3 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -196,11 +196,17 @@ let dummy_value : unit -> t =
   fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.")
 
 let cast_accu v = (Obj.magic v:accumulator)
+[@@ocaml.inline always]
 
 let mk_int (x : int) = (Obj.magic x : t)
+[@@ocaml.inline always]
+
 (* Coq's booleans are reversed... *)
 let mk_bool (b : bool) = (Obj.magic (not b) : t)
-let mk_uint (x : Uint31.t) = (Obj.magic x : t)
+[@@ocaml.inline always]
+
+let mk_uint (x : Uint63.t) = (Obj.magic x : t)
+[@@ocaml.inline always]
 
 type block
 
@@ -216,8 +222,9 @@ type kind_of_value =
   | Vaccu of accumulator
   | Vfun of (t -> t)
   | Vconst of int
+  | Vint64 of int64
   | Vblock of block
-	
+
 let kind_of_value (v:t) =
   let o = Obj.repr v in
   if Obj.is_int o then Vconst (Obj.magic v)
@@ -225,8 +232,8 @@ let kind_of_value (v:t) =
     let tag = Obj.tag o in
     if Int.equal tag accumulate_tag then
       Vaccu (Obj.magic v)
-    else 
-      if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
+    else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+    else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
       else
         (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); 
            or ??? what is 1002*)
@@ -236,92 +243,105 @@ let kind_of_value (v:t) =
 
 let is_int (x:t) =
   let o = Obj.repr x in
-  Obj.is_int o
+  Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag
 
 let val_to_int (x:t) = (Obj.magic x : int)
+[@@ocaml.inline always]
 
-let to_uint (x:t) = (Obj.magic x : Uint31.t)
-let of_uint (x: Uint31.t) = (Obj.magic x : t)
+let to_uint (x:t) = (Obj.magic x : Uint63.t)
+[@@ocaml.inline always]
 
 let no_check_head0 x =
- of_uint (Uint31.head0 (to_uint x))
+ mk_uint (Uint63.head0 (to_uint x))
+[@@ocaml.inline always]
 
 let head0 accu x =
  if is_int x then  no_check_head0 x
  else accu x
 
 let no_check_tail0 x =
-  of_uint (Uint31.tail0 (to_uint x))
+  mk_uint (Uint63.tail0 (to_uint x))
+[@@ocaml.inline always]
 
 let tail0 accu x =
  if is_int x then no_check_tail0 x
  else accu x
 
 let no_check_add  x y =
-  of_uint (Uint31.add (to_uint x) (to_uint y))
+  mk_uint (Uint63.add (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let add accu x y =
   if is_int x && is_int y then no_check_add x y 
   else accu x y
 
 let no_check_sub x y =
-     of_uint (Uint31.sub (to_uint x) (to_uint y))
+  mk_uint (Uint63.sub (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let sub accu x y =
   if is_int x && is_int y then no_check_sub x y
   else accu x y
 
 let no_check_mul x y =
-  of_uint (Uint31.mul (to_uint x) (to_uint y))
+  mk_uint (Uint63.mul (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let mul accu x y =
   if is_int x && is_int y then no_check_mul x y
   else accu x y
 
 let no_check_div x y =
-  of_uint (Uint31.div (to_uint x) (to_uint y))
+  mk_uint (Uint63.div (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let div accu x y =
   if is_int x && is_int y then no_check_div x y 
   else accu x y
 
 let no_check_rem x y =
-  of_uint (Uint31.rem (to_uint x) (to_uint y))
+  mk_uint (Uint63.rem (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let rem accu x y =
   if is_int x && is_int y then no_check_rem x y
   else accu x y
 
 let no_check_l_sr x y =
-  of_uint (Uint31.l_sr (to_uint x) (to_uint y))
+  mk_uint (Uint63.l_sr (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let l_sr accu x y =
   if is_int x && is_int y then no_check_l_sr x y
   else accu x y
 
 let no_check_l_sl x y =
-  of_uint (Uint31.l_sl (to_uint x) (to_uint y))
+  mk_uint (Uint63.l_sl (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let l_sl accu x y =
   if is_int x && is_int y then no_check_l_sl x y
   else accu x y
 
 let no_check_l_and x y =
-  of_uint (Uint31.l_and (to_uint x) (to_uint y))
+  mk_uint (Uint63.l_and (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let l_and accu x y =
   if is_int x && is_int y then no_check_l_and x y
   else accu x y
 
 let no_check_l_xor x y =
-  of_uint (Uint31.l_xor (to_uint x) (to_uint y))
+  mk_uint (Uint63.l_xor (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let l_xor accu x y =
   if is_int x && is_int y then no_check_l_xor x y
   else accu x y
 
 let no_check_l_or x y =
-  of_uint (Uint31.l_or (to_uint x) (to_uint y))
+  mk_uint (Uint63.l_or (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let l_or accu x y =
   if is_int x && is_int y then no_check_l_or x y
@@ -337,61 +357,57 @@ type coq_pair =
   | Paccu of t
   | PPair of t * t
 
-type coq_zn2z =
-  | Zaccu of t
-  | ZW0
-  | ZWW of t * t
-
 let mkCarry b i =
-  if b then (Obj.magic (C1(of_uint i)):t)
-  else (Obj.magic (C0(of_uint i)):t)
+  if b then (Obj.magic (C1(mk_uint i)):t)
+  else (Obj.magic (C0(mk_uint i)):t)
 
 let no_check_addc x y =
-  let s = Uint31.add (to_uint x) (to_uint y) in
-  mkCarry (Uint31.lt s (to_uint x)) s
+  let s = Uint63.add (to_uint x) (to_uint y) in
+  mkCarry (Uint63.lt s (to_uint x)) s
+[@@ocaml.inline always]
 
 let addc accu x y =
   if is_int x && is_int y then no_check_addc x y
   else accu x y
 
 let no_check_subc x y =
-  let s = Uint31.sub (to_uint x) (to_uint y) in
-  mkCarry (Uint31.lt (to_uint x) (to_uint y)) s
+  let s = Uint63.sub (to_uint x) (to_uint y) in
+  mkCarry (Uint63.lt (to_uint x) (to_uint y)) s
+[@@ocaml.inline always]
 
 let subc accu x y =
   if is_int x && is_int y then no_check_subc x y
   else accu x y
 
-let no_check_addcarryc x y =
+let no_check_addCarryC x y =
   let s = 
-    Uint31.add (Uint31.add (to_uint x) (to_uint y))
-      (Uint31.of_int 1) in
-  mkCarry (Uint31.le s (to_uint x)) s
+    Uint63.add (Uint63.add (to_uint x) (to_uint y))
+      (Uint63.of_int 1) in
+  mkCarry (Uint63.le s (to_uint x)) s
+[@@ocaml.inline always]
 
-let addcarryc accu x y =
-  if is_int x && is_int y then no_check_addcarryc x y
+let addCarryC accu x y =
+  if is_int x && is_int y then no_check_addCarryC x y
   else accu x y 
 
-let no_check_subcarryc x y =
+let no_check_subCarryC x y =
   let s = 
-    Uint31.sub (Uint31.sub (to_uint x) (to_uint y))
-      (Uint31.of_int 1) in
-  mkCarry (Uint31.le (to_uint x) (to_uint y)) s
+    Uint63.sub (Uint63.sub (to_uint x) (to_uint y))
+      (Uint63.of_int 1) in
+  mkCarry (Uint63.le (to_uint x) (to_uint y)) s
+[@@ocaml.inline always]
 
-let subcarryc accu x y =
-  if is_int x && is_int y then no_check_subcarryc x y
+let subCarryC accu x y =
+  if is_int x && is_int y then no_check_subCarryC x y
   else accu x y 
 
 let of_pair (x, y) =
-  (Obj.magic (PPair(of_uint x, of_uint y)):t)
-
-let zn2z_of_pair (x,y) =
-  if Uint31.equal x (Uint31.of_uint 0) &&
-    Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0
-  else (Obj.magic (ZWW(of_uint x, of_uint y)) : t)
+  (Obj.magic (PPair(mk_uint x, mk_uint y)):t)
+[@@ocaml.inline always]
 
 let no_check_mulc x y =
-  zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y))
+  of_pair (Uint63.mulc (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let mulc accu x y =
   if is_int x && is_int y then no_check_mulc x y
@@ -399,7 +415,8 @@ let mulc accu x y =
 
 let no_check_diveucl x y =
   let i1, i2 = to_uint x, to_uint y in
-  of_pair(Uint31.div i1 i2, Uint31.rem i1 i2)
+  of_pair(Uint63.div i1 i2, Uint63.rem i1 i2)
+[@@ocaml.inline always]
 
 let diveucl accu x y =
   if is_int x && is_int y then no_check_diveucl x y
@@ -407,21 +424,20 @@ let diveucl accu x y =
 
 let no_check_div21 x y z =
   let i1, i2, i3 = to_uint x, to_uint y, to_uint z in
-  of_pair (Uint31.div21 i1 i2 i3)
+  of_pair (Uint63.div21 i1 i2 i3)
+[@@ocaml.inline always]
 
 let div21 accu x y z =
   if is_int x && is_int y && is_int z then no_check_div21 x y z
   else accu x y z
 
-let no_check_addmuldiv x y z =
+let no_check_addMulDiv x y z =
   let p, i, j = to_uint x, to_uint y, to_uint z in
-  let p' = Uint31.to_int p in
-  of_uint (Uint31.l_or 
-	     (Uint31.l_sl i p) 
-	     (Uint31.l_sr j (Uint31.of_int (31 - p'))))
+  mk_uint (Uint63.addmuldiv p i j)
+[@@ocaml.inline always]
 
-let addmuldiv accu x y z =
-  if is_int x && is_int y && is_int z then no_check_addmuldiv x y z
+let addMulDiv accu x y z =
+  if is_int x && is_int y && is_int z then no_check_addMulDiv x y z
   else accu x y z
 
 [@@@ocaml.warning "-34"]
@@ -436,29 +452,32 @@ type coq_cmp =
   | CmpLt
   | CmpGt
 
-let no_check_eq x y =     
-  mk_bool (Uint31.equal (to_uint x) (to_uint y))
+let no_check_eq x y =
+  mk_bool (Uint63.equal (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let eq accu x y =
   if is_int x && is_int y then no_check_eq x y
   else accu x y
 
 let no_check_lt x y =
-  mk_bool (Uint31.lt (to_uint x) (to_uint y))
+  mk_bool (Uint63.lt (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let lt accu x y =
   if is_int x && is_int y then no_check_lt x y
   else accu x y
 
 let no_check_le x y =
-  mk_bool (Uint31.le (to_uint x) (to_uint y))
+  mk_bool (Uint63.le (to_uint x) (to_uint y))
+[@@ocaml.inline always]
 
 let le accu x y =
   if is_int x && is_int y then no_check_le x y
   else accu x y
 
 let no_check_compare x y =
-  match Uint31.compare (to_uint x) (to_uint y) with
+  match Uint63.compare (to_uint x) (to_uint y) with
   | x when x < 0 -> (Obj.magic CmpLt:t)
   | 0 -> (Obj.magic CmpEq:t)
   | _ -> (Obj.magic CmpGt:t)
@@ -467,6 +486,11 @@ let compare accu x y =
   if is_int x && is_int y then no_check_compare x y
   else accu x y
 
+let print x =
+  Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x));
+  flush stderr;
+  x
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -
@@ -491,63 +515,3 @@ let str_decode s =
     Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf))
   done;
   Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0
-
-(** Retroknowledge, to be removed when we switch to primitive integers *)
-
-(* This will be unsafe with 63-bits integers *)
-let digit_to_uint d = (Obj.magic d : Uint31.t)
-
-let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
-		  x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 =
-  if is_int x0 && is_int x1 && is_int x2 && is_int x3 && is_int x4 && is_int x5
-     && is_int x6 && is_int x7 && is_int x8 && is_int x9 && is_int x10
-     && is_int x11 && is_int x12 && is_int x13 && is_int x14 && is_int x15
-     && is_int x16 && is_int x17 && is_int x18 && is_int x19 && is_int x20
-     && is_int x21 && is_int x22 && is_int x23 && is_int x24 && is_int x25
-     && is_int x26 && is_int x27 && is_int x28 && is_int x29 && is_int x30
-  then
-    let r = digit_to_uint x0 in
-    let r = Uint31.add_digit r (digit_to_uint x1) in
-    let r = Uint31.add_digit r (digit_to_uint x2) in
-    let r = Uint31.add_digit r (digit_to_uint x3) in
-    let r = Uint31.add_digit r (digit_to_uint x4) in
-    let r = Uint31.add_digit r (digit_to_uint x5) in
-    let r = Uint31.add_digit r (digit_to_uint x6) in
-    let r = Uint31.add_digit r (digit_to_uint x7) in
-    let r = Uint31.add_digit r (digit_to_uint x8) in
-    let r = Uint31.add_digit r (digit_to_uint x9) in
-    let r = Uint31.add_digit r (digit_to_uint x10) in
-    let r = Uint31.add_digit r (digit_to_uint x11) in
-    let r = Uint31.add_digit r (digit_to_uint x12) in
-    let r = Uint31.add_digit r (digit_to_uint x13) in
-    let r = Uint31.add_digit r (digit_to_uint x14) in
-    let r = Uint31.add_digit r (digit_to_uint x15) in
-    let r = Uint31.add_digit r (digit_to_uint x16) in
-    let r = Uint31.add_digit r (digit_to_uint x17) in
-    let r = Uint31.add_digit r (digit_to_uint x18) in
-    let r = Uint31.add_digit r (digit_to_uint x19) in
-    let r = Uint31.add_digit r (digit_to_uint x20) in
-    let r = Uint31.add_digit r (digit_to_uint x21) in
-    let r = Uint31.add_digit r (digit_to_uint x22) in
-    let r = Uint31.add_digit r (digit_to_uint x23) in
-    let r = Uint31.add_digit r (digit_to_uint x24) in
-    let r = Uint31.add_digit r (digit_to_uint x25) in
-    let r = Uint31.add_digit r (digit_to_uint x26) in
-    let r = Uint31.add_digit r (digit_to_uint x27) in
-    let r = Uint31.add_digit r (digit_to_uint x28) in
-    let r = Uint31.add_digit r (digit_to_uint x29) in
-    let r = Uint31.add_digit r (digit_to_uint x30) in
-    mk_uint r
-  else
-    c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
-      x21 x22 x23 x24 x25 x26 x27 x28 x29 x30
-
-let decomp_uint c v =
-  if is_int v then
-    let r = ref c in
-    let v = val_to_int v in
-    for i = 30 downto 0 do
-      r := (!r) (mk_int ((v lsr i) land 1));
-    done;
-    !r
-  else v