Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Utilopen Namesopen Valuesopen Constr
(** This module defines the representation of values internally used bythe native compiler *)
type ('a,'b) eq = ('a,'b) Util.eq = Refl : ('a,'a) eq
type tlet t_eq : (t, t -> t) eq = Obj.magic ()let t_eq2 : (t, t -> t -> t) eq = Obj.magic ()let t_eq3 : (t, t -> t -> t -> t) eq = Obj.magic ()let t_eq4 : (t, t -> t -> t -> t -> t) eq = Obj.magic ()
let cast_gen (type a) (type b) (e:(a,b) eq) (x:a) : b = let Refl = e in x
let apply (f:t) : t -> t = cast_gen t_eq f
(* Writing this as [apply2 f x y = apply (apply f x) y] seems to confuse ocaml and it produces less efficient code.
When written with a direct [cast_gen t_eq2] ocaml seems smart enough to fully reduce it where used. *)let apply2 (f:t) : t -> t -> t = cast_gen t_eq2 f
let apply3 (f:t) : t -> t -> t -> t = cast_gen t_eq3 f
let apply4 (f:t) : t -> t -> t -> t -> t = cast_gen t_eq4 f
let of_fun (f:t->t) : t = cast_gen (sym t_eq) f
let eta_expand f = of_fun (fun x -> apply f x)
type accumulator (* = t (* a block [0:code;atom;arguments] *) *)
type tag = int
type arity = int
type reloc_table = (tag * arity) array
type annot_sw = { asw_ind : inductive; asw_reloc : reloc_table; asw_prefix : string }
type sort_annot = string * int
type rec_pos = int array
let eq_rec_pos = Array.equal Int.equal
type vcofix = t Lazy.t
type atom = | Arel of int | Aconstant of pconstant | Aind of pinductive | Asort of Sorts.t | Avar of Id.t | Acase of annot_sw * accumulator * t * t | Afix of t array * t array * rec_pos * int (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t array * vcofix | Aevar of Evar.t * t array | Aproj of (inductive * int) * accumulator
type symbol = | SymbValue of t | SymbSort of Sorts.t | SymbName of Name.t | SymbConst of Constant.t | SymbMatch of annot_sw | SymbInd of inductive | SymbEvar of Evar.t | SymbInstance of UVars.Instance.t | SymbProj of (inductive * int)
type block
type symbols = symbol array
let empty_symbols = [| |]
let accumulate_tag = 0
(** Unique pointer used to drive the accumulator function *)let ret_accu = Obj.repr (ref ())
type accu_val = { acc_atm : atom; acc_arg : t list }
(** Return a pointer to [caml_curry2_1] that is also recognized as an unscannable block *)external get_curry2_1 : unit -> Obj.t = "rocq_curry2_1_addr"
type _ curry2_1_clos = Curry2_1 : Obj.t * int * 'a * ('a -> 'b -> 'c) -> ('b -> 'c) curry2_1_clos
let mk_accu = let curry2_1 = get_curry2_1 () in let rec accumulate data x = if Obj.repr x == ret_accu then Obj.repr data else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Curry2_1 (curry2_1, 2, data, accumulate) in Obj.repr ans in fun (a : atom) -> let data = { acc_atm = a; acc_arg = [] } in let ans = Curry2_1 (curry2_1, 2, data, accumulate) in (Obj.magic ans : t)
let get_accu (k : accumulator) = (Obj.magic k : Obj.t -> accu_val) ret_accu
let mk_rel_accu i = mk_accu (Arel i)
let rel_tbl_size = 100let rel_tbl_init = ref false(* Initialize the table lazily not to generate naked pointers at startup *)let rel_tbl = Array.make rel_tbl_size (Obj.magic 0 : t)
let mk_rel_accu i = if i < rel_tbl_size then let () = if not !rel_tbl_init then begin for i = 0 to rel_tbl_size - 1 do rel_tbl.(i) <- mk_rel_accu i done; rel_tbl_init := true end in rel_tbl.(i) else mk_rel_accu i
let mk_rels_accu lvl len = Array.init len (fun i -> mk_rel_accu (lvl + i))
let napply (f:t) (args: t array) = Array.fold_left (fun f a -> apply f a) f args
let mk_constant_accu kn u = mk_accu (Aconstant (kn,u))
let mk_ind_accu ind u = mk_accu (Aind (ind,u))
let mk_sort_accu s = mk_accu (Asort s)
let mk_var_accu id = mk_accu (Avar id)
let mk_sw_accu annot c p ac = mk_accu (Acase(annot,c,p,ac))
let prod_tag = (* We rely on the tag of Vprod! *) let () = assert (Obj.tag (Obj.repr (Vprod (Anonymous, Obj.magic 0, Obj.magic 0))) == 2) in 2
let mk_prod s dom codom = (* [Prod (s, dom, codom)] is coded as [tag:0|[tag:2|s; dom; codom]] This looks like a PArray but has a tag distinct from all PArray values on the inner block. This cannot be an accumulator because all accumulators have length >= 2. *) let block = Obj.repr (Vprod (s, dom, codom)) in (Obj.magic (ref block) : t)
let mk_evar_accu ev args = mk_accu (Aevar (ev, args))
let mk_proj_accu kn c = mk_accu (Aproj (kn,c))
let atom_of_accu (k:accumulator) = (get_accu k).acc_atm
let accu_nargs (k:accumulator) = List.length (get_accu k).acc_arg
let args_of_accu (k:accumulator) = (get_accu k).acc_arg
let mk_fix_accu rec_pos pos types bodies = mk_accu (Afix(types,bodies,rec_pos, pos))
let mk_cofix_accu pos types norm cofix args = mk_accu (Acofix (types, norm, pos, args, Lazy.from_fun cofix))
let force_cofix (cofix : t) = let accu = (Obj.magic cofix : accumulator) in let atom = atom_of_accu accu in match atom with | Acofix (_, _, _, _, v) -> let () = assert (List.is_empty (args_of_accu accu)) in Lazy.force v | _ -> cofix
let mk_block tag args = let nargs = Array.length args in let r = Obj.new_block tag nargs in for i = 0 to nargs - 1 do Obj.set_field r i (Obj.magic args.(i)) done; (Obj.magic r : t)
external cast_accu : t -> accumulator = "%identity"external mk_const : tag -> t = "%identity"external mk_int : int -> t = "%identity"external mk_uint : Uint63.t -> t = "%identity"external mk_float : Float64.t -> t = "%identity"external mk_string : Pstring.t -> t = "%identity"external mk_bool : bool -> t = "%boolnot" (* Rocq's booleans are reversed... *)
let block_size (b:block) = Obj.size (Obj.magic b)
let block_field (b:block) i = (Obj.magic (Obj.field (Obj.magic b) i) : t)
let block_tag (b:block) = Obj.tag (Obj.magic b)
type kind = (t, accumulator, t -> t, Name.t * t * t, Empty.t, Empty.t, block) Values.kind
let kind_of_value (v:t) = let o = Obj.repr v in if Obj.is_int o then Vconst (Obj.magic v) else let tag = Obj.tag o in if Int.equal tag accumulate_tag then if Int.equal (Obj.size o) 1 then let w = Obj.field o 0 in let tag = Obj.tag w in if Int.equal tag prod_tag then Obj.magic w else Varray (Obj.magic v) else Vaccu (Obj.magic v) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else if Int.equal tag Obj.string_tag then Vstring (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*) Vfun (apply v)
(** Support for machine integers *)
let is_int (x:t) = let o = Obj.repr x in Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag[@@ocaml.inline always]
let val_to_int (x:t) = (Obj.magic x : int)[@@ocaml.inline always]
let to_uint (x:t) = (Obj.magic x : Uint63.t)[@@ocaml.inline always]
let no_check_head0 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 apply accu x
let no_check_tail0 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 apply accu x
let no_check_add x 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 apply2 accu x y
let no_check_sub x 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 apply2 accu x y
let no_check_mul x 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 apply2 accu x y
let no_check_div x 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 apply2 accu x y
let no_check_rem x 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 apply2 accu x y
let no_check_divs x y = mk_uint (Uint63.divs (to_uint x) (to_uint y))[@@ocaml.inline always]
let divs accu x y = if is_int x && is_int y then no_check_divs x y else apply2 accu x y
let no_check_rems x y = mk_uint (Uint63.rems (to_uint x) (to_uint y))[@@ocaml.inline always]
let rems accu x y = if is_int x && is_int y then no_check_rems x y else apply2 accu x y
let no_check_l_sr x 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 apply2 accu x y
let no_check_l_sl x 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 apply2 accu x y
let no_check_a_sr x y = mk_uint (Uint63.a_sr (to_uint x) (to_uint y))[@@ocaml.inline always]
let a_sr accu x y = if is_int x && is_int y then no_check_a_sr x y else apply2 accu x y
let no_check_l_and x 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 apply2 accu x y
let no_check_l_xor x 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 apply2 accu x y
let no_check_l_or x 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 else apply2 accu x y
[@@@ocaml.warning "-37"]type rocq_carry = | Caccu of t | C0 of t | C1 of t
type rocq_pair = | Paccu of t | PPair of t * t
let mkCarry b i = 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 = 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 apply2 accu x y
let no_check_subc x y = 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 apply2 accu x y
let no_check_addCarryC x y = let 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 else apply2 accu x y
let no_check_subCarryC x y = let 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 else apply2 accu x y
let of_pair (x, y) = (Obj.magic (PPair(mk_uint x, mk_uint y)):t)[@@ocaml.inline always]
let no_check_mulc x 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 else apply2 accu x y
let no_check_diveucl x y = let i1, i2 = to_uint x, to_uint y in 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 else apply2 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 (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 apply3 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 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 else apply3 accu x y z
[@@@ocaml.warning "-34"]type rocq_bool = | Baccu of t | Btrue | Bfalse
type rocq_cmp = | CmpAccu of t | CmpEq | CmpLt | CmpGt
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 apply2 accu x y
let no_check_lt x 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 apply2 accu x y
let no_check_le x 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 apply2 accu x y
let no_check_lts x y = mk_bool (Uint63.lts (to_uint x) (to_uint y))[@@ocaml.inline always]
let lts accu x y = if is_int x && is_int y then no_check_lts x y else apply2 accu x y
let no_check_les x y = mk_bool (Uint63.les (to_uint x) (to_uint y))[@@ocaml.inline always]
let les accu x y = if is_int x && is_int y then no_check_les x y else apply2 accu x y
let no_check_compare x y = 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)
let compare accu x y = if is_int x && is_int y then no_check_compare x y else apply2 accu x y
let no_check_compares x y = match Uint63.compares (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 compares accu x y = if is_int x && is_int y then no_check_compares x y else apply2 accu x y
let print x = Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x)); flush stderr; x
(** Support for machine floating point values *)
external is_float : t -> bool = "rocq_is_double"[@@noalloc]
let to_float (x:t) = (Obj.magic x : Float64.t)[@@ocaml.inline always]
let no_check_fopp x = mk_float (Float64.opp (to_float x))[@@ocaml.inline always]
let fopp accu x = if is_float x then no_check_fopp x else apply accu x
let no_check_fabs x = mk_float (Float64.abs (to_float x))[@@ocaml.inline always]
let fabs accu x = if is_float x then no_check_fabs x else apply accu x
let no_check_feq x y = mk_bool (Float64.eq (to_float x) (to_float y))[@@ocaml.inline always]
let feq accu x y = if is_float x && is_float y then no_check_feq x y else apply2 accu x y
let no_check_flt x y = mk_bool (Float64.lt (to_float x) (to_float y))[@@ocaml.inline always]
let flt accu x y = if is_float x && is_float y then no_check_flt x y else apply2 accu x y
let no_check_fle x y = mk_bool (Float64.le (to_float x) (to_float y))[@@ocaml.inline always]
let fle accu x y = if is_float x && is_float y then no_check_fle x y else apply2 accu x y
type rocq_fcmp = | CFcmpAccu of t | CFcmpEq | CFcmpLt | CFcmpGt | CFcmpNotComparable
let no_check_fcompare x y = let c = Float64.compare (to_float x) (to_float y) in (Obj.magic c:t)[@@ocaml.inline always]
let fcompare accu x y = if is_float x && is_float y then no_check_fcompare x y else apply2 accu x y
let no_check_fequal x y = mk_bool (Float64.equal (to_float x) (to_float y))[@@ocaml.inline always]
let fequal accu x y = if is_float x && is_float y then no_check_fequal x y else apply2 accu x y
type rocq_fclass = | CFclassAccu of t | CFclassPNormal | CFclassNNormal | CFclassPSubn | CFclassNSubn | CFclassPZero | CFclassNZero | CFclassPInf | CFclassNInf | CFclassNaN
let no_check_fclassify x = let c = Float64.classify (to_float x) in (Obj.magic c:t)[@@ocaml.inline always]
let fclassify accu x = if is_float x then no_check_fclassify x else apply accu x
let no_check_fadd x y = mk_float (Float64.add (to_float x) (to_float y))[@@ocaml.inline always]
let fadd accu x y = if is_float x && is_float y then no_check_fadd x y else apply2 accu x y
let no_check_fsub x y = mk_float (Float64.sub (to_float x) (to_float y))[@@ocaml.inline always]
let fsub accu x y = if is_float x && is_float y then no_check_fsub x y else apply2 accu x y
let no_check_fmul x y = mk_float (Float64.mul (to_float x) (to_float y))[@@ocaml.inline always]
let fmul accu x y = if is_float x && is_float y then no_check_fmul x y else apply2 accu x y
let no_check_fdiv x y = mk_float (Float64.div (to_float x) (to_float y))[@@ocaml.inline always]
let fdiv accu x y = if is_float x && is_float y then no_check_fdiv x y else apply2 accu x y
let no_check_fsqrt x = mk_float (Float64.sqrt (to_float x))[@@ocaml.inline always]
let fsqrt accu x = if is_float x then no_check_fsqrt x else apply accu x
let no_check_float_of_int x = mk_float (Float64.of_uint63 (to_uint x))[@@ocaml.inline always]
let float_of_int accu x = if is_int x then no_check_float_of_int x else apply accu x
let no_check_normfr_mantissa x = mk_uint (Float64.normfr_mantissa (to_float x))[@@ocaml.inline always]
let normfr_mantissa accu x = if is_float x then no_check_normfr_mantissa x else apply accu x
let no_check_frshiftexp x = let f, e = Float64.frshiftexp (to_float x) in (Obj.magic (PPair(mk_float f, mk_uint e)):t)[@@ocaml.inline always]
let frshiftexp accu x = if is_float x then no_check_frshiftexp x else apply accu x
let no_check_ldshiftexp x e = mk_float (Float64.ldshiftexp (to_float x) (to_uint e))[@@ocaml.inline always]
let ldshiftexp accu x e = if is_float x && is_int e then no_check_ldshiftexp x e else apply2 accu x e
let no_check_next_up x = mk_float (Float64.next_up (to_float x))[@@ocaml.inline always]
let next_up accu x = if is_float x then no_check_next_up x else apply accu x
let no_check_next_down x = mk_float (Float64.next_down (to_float x))[@@ocaml.inline always]
let next_down accu x = if is_float x then no_check_next_down x else apply accu x
(** Support for primitive strings *)
let is_string (x:t) = let o = Obj.repr x in Int.equal (Obj.tag o) Obj.string_tag
let to_string (x:t) = (Obj.magic x : Pstring.t)[@@ocaml.inline always]
let no_check_string_make n c = mk_string (Pstring.make (to_uint n) (to_uint c))[@@ocaml.inline always]
let no_check_string_length s = mk_uint (Pstring.length (to_string s))[@@ocaml.inline always]
let no_check_string_get s i = mk_uint (Pstring.get (to_string s) (to_uint i))[@@ocaml.inline always]
let no_check_string_sub s off len = mk_string (Pstring.sub (to_string s) (to_uint off) (to_uint len))[@@ocaml.inline always]
let no_check_string_cat s1 s2 = mk_string (Pstring.cat (to_string s1) (to_string s2))[@@ocaml.inline always]
let no_check_string_compare s1 s2 = match Pstring.compare (to_string s1) (to_string s2) with | x when x < 0 -> (Obj.magic CmpLt:t) | 0 -> (Obj.magic CmpEq:t) | _ -> (Obj.magic CmpGt:t)
let string_make accu n c = if is_int n && is_int c then no_check_string_make n c else apply2 accu n c
let string_length accu s = if is_string s then no_check_string_length s else apply accu s
let string_get accu s i = if is_string s && is_int i then no_check_string_get s i else apply2 accu s i
let string_sub accu s off len = if is_string s && is_int off && is_int len then no_check_string_sub s off len else apply3 accu s off len
let string_cat accu s1 s2 = if is_string s1 && is_string s2 then no_check_string_cat s1 s2 else apply2 accu s1 s2
let string_compare accu s1 s2 = if is_string s1 && is_string s2 then no_check_string_compare s1 s2 else apply2 accu s1 s2
(** Support for primitive arrays *)
let is_parray t = (* This is only used over values known to inhabit an array type, so we just have to discriminate between actual arrays and accumulators. The latter are always closures with the tag set to 0, so they have size >= 2. *) let t = Obj.magic t in Obj.is_block t && Obj.size t = 1
let to_parray t = Obj.magic tlet of_parray t = Obj.magic t
let no_check_arraymake n def = of_parray (Parray.make (to_uint n) def)[@@ocaml.inline always]
let arraymake accu vA n def = if is_int n then no_check_arraymake n def else apply3 accu vA n def
let no_check_arrayget t n = Parray.get (to_parray t) (to_uint n)[@@ocaml.inline always]
let arrayget accu vA t n = if is_parray t && is_int n then no_check_arrayget t n else apply3 accu vA t n
let no_check_arraydefault t = Parray.default (to_parray t)[@@ocaml.inline always]
let arraydefault accu vA t = if is_parray t then no_check_arraydefault t else apply2 accu vA t
let no_check_arrayset t n v = of_parray (Parray.set (to_parray t) (to_uint n) v)[@@ocaml.inline always]
let arrayset accu vA t n v = if is_parray t && is_int n then no_check_arrayset t n v else apply4 accu vA t n v
let no_check_arraycopy t = of_parray (Parray.copy (to_parray t))[@@ocaml.inline always]
let arraycopy accu vA t = if is_parray t then no_check_arraycopy t else apply2 accu vA t
let no_check_arraylength t = mk_uint (Parray.length (to_parray t))[@@ocaml.inline always]
let arraylength accu vA t = if is_parray t then no_check_arraylength t else apply2 accu vA t
let parray_of_array t def = (Obj.magic (Parray.unsafe_of_obj (Obj.repr t) def) : t)
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) - (if 0x41 <= i then 0x7 else 0) - (if 0x61 <= i then 0x20 else 0))
let hex_of_bin ch = hobcnv.(int_of_char ch)let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1]))
let str_encode expr = let mshl_expr = Marshal.to_string expr [] in let payload = Buffer.create (String.length mshl_expr * 2) in String.iter (fun c -> Buffer.add_string payload (hex_of_bin c)) mshl_expr; Buffer.contents payload
let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do Bytes.blit_string s (2*i) buf 0 2; Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0