diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 222 |
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; |