From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 16 Feb 2018 01:02:17 +0100
Subject: Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
---
 kernel/nativevalues.ml | 210 ++++++++++++++++++++-----------------------------
 1 file changed, 87 insertions(+), 123 deletions(-)

(limited to 'kernel/nativevalues.ml')

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
-- 
cgit v1.2.3