From aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 6 Apr 2014 12:41:26 -0400 Subject: Partial support for open terms in int31. --- kernel/nativevalues.ml | 59 ++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 57 insertions(+), 2 deletions(-) (limited to 'kernel/nativevalues.ml') diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 98094f795..2a0052a60 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -221,7 +221,8 @@ let dummy_value : unit -> t = let cast_accu v = (Obj.magic v:accumulator) -let mk_int x = Obj.magic x +let mk_int (x : int) = (Obj.magic x : t) +let mk_uint (x : Uint31.t) = (Obj.magic x : t) type block @@ -253,6 +254,12 @@ let kind_of_value (v:t) = or ??? what is 1002*) Vfun v +(** Support for machine integers *) + +let is_int (x:t) = + let o = Obj.repr x in + Obj.is_int o + let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i) let bohcnv = Array.init 256 (fun i -> i - (if 0x30 <= i then 0x30 else 0) - @@ -278,4 +285,52 @@ let str_decode s = done; Marshal.from_string (Buffer.contents 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 -- cgit v1.2.3