Machine arithmetic operations for native compiler.

This completes the port of the native compiler to retroknowledge.
However, some testing and optimizations are still to be done.

1 files changed, 220 insertions, 2 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 7f2785cf9..ab56c4be0 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -222,6 +222,8 @@ let dummy_value : unit -> t =
 let cast_accu v = (Obj.magic v:accumulator)
 
 let mk_int (x : int) = (Obj.magic x : t)
+(* 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)
 
 type block
@@ -260,7 +262,223 @@ let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o
 
-let to_int (x:t) = (Obj.magic x : int)
+let val_to_int (x:t) = (Obj.magic x : int)
+
+let to_uint (x:t) = (Obj.magic x : Uint31.t)
+let of_uint (x: Uint31.t) = (Obj.magic x : t)
+
+let no_check_head0 x =
+ of_uint (Uint31.head0 (to_uint x))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+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))
+
+let l_or accu x y =
+  if is_int x && is_int y then no_check_l_or x y
+  else accu x y
+
+type coq_carry = 
+  | Caccu of t
+  | C0 of t
+  | C1 of t
+
+type coq_pair = 
+  | Paccu of t
+  | PPair 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)
+
+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 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 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 s = 
+    Uint31.add (Uint31.add (to_uint x) (to_uint y))
+      (Uint31.of_int 1) in
+  mkCarry (Uint31.le s (to_uint x)) s
+
+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 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
+
+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 no_check_mulc x y =
+    of_pair(Uint31.mulc (to_uint x) (to_uint y))
+
+let mulc accu x y =
+  if is_int x && is_int y then no_check_mulc x y
+  else 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)
+
+let diveucl accu x y =
+  if is_int x && is_int y then no_check_diveucl x y
+  else 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)
+
+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 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'))))
+
+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
+
+
+type coq_bool =
+  | Baccu of t
+  | Btrue
+  | Bfalse
+
+type coq_cmp =
+  | CmpAccu of t
+  | CmpEq 
+  | CmpLt
+  | CmpGt
+
+let no_check_eq x y =     
+  mk_bool (Uint31.equal (to_uint x) (to_uint y))
+
+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))
+
+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))
+
+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
+  | x when x < 0 -> (Obj.magic CmpLt:t)
+  | 0 -> (Obj.magic CmpEq:t)
+  | _ -> (Obj.magic CmpGt:t)
+
+let compare accu x y =
+  if is_int x && is_int y then no_check_compare x y
+  else accu x y
 
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
 let bohcnv = Array.init 256 (fun i -> i -
@@ -340,7 +558,7 @@ let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
 let decomp_uint c v =
   if is_int v then
     let r = ref c in
-    let v = to_int v in
+    let v = val_to_int v in
     for i = 30 downto 0 do
       r := (!r) (mk_int ((v lsr i) land 1));
     done;