Module Nativevalues

type t = t -> t
type accumulator
type tag = int
type arity = int
type reloc_table = (tag * arity) array
type annot_sw = {
asw_ind : Names.inductive;
asw_ci : Constr.case_info;
asw_reloc : reloc_table;
asw_finite : bool;
asw_prefix : string;
}
val eq_annot_sw : annot_sw -> annot_sw -> bool
val hash_annot_sw : annot_sw -> int
type sort_annot = string * int
type rec_pos = int array
val eq_rec_pos : rec_pos -> rec_pos -> bool
type atom =
| Arel of int
| Aconstant of Constr.pconstant
| Aind of Constr.pinductive
| Asort of Sorts.t
| Avar of Names.Id.t
| Acase of annot_sw * accumulator * t * t -> t
| Afix of t array * t array * rec_pos * int
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
| Aprod of Names.Name.t * t * t -> t
| Ameta of Constr.metavariable * t
| Aevar of Evar.t * t array
| Aproj of Names.inductive * int * accumulator
type symbol =
| SymbValue of t
| SymbSort of Sorts.t
| SymbName of Names.Name.t
| SymbConst of Names.Constant.t
| SymbMatch of annot_sw
| SymbInd of Names.inductive
| SymbMeta of Constr.metavariable
| SymbEvar of Evar.t
| SymbLevel of Univ.Level.t
| SymbProj of Names.inductive * int
type symbols = symbol array
val empty_symbols : symbols
val mk_accu : atom -> t
val mk_rel_accu : int -> t
val mk_rels_accu : int -> int -> t array
val mk_constant_accu : Names.Constant.t -> Univ.Level.t array -> t
val mk_ind_accu : Names.inductive -> Univ.Level.t array -> t
val mk_sort_accu : Sorts.t -> Univ.Level.t array -> t
val mk_var_accu : Names.Id.t -> t
val mk_sw_accu : annot_sw -> accumulator -> t -> t -> t
val mk_prod_accu : Names.Name.t -> t -> t -> t
val mk_fix_accu : rec_pos -> int -> t array -> t array -> t
val mk_cofix_accu : int -> t array -> t array -> t
val mk_meta_accu : Constr.metavariable -> t
val mk_evar_accu : Evar.t -> t array -> t
val mk_proj_accu : (Names.inductive * int) -> accumulator -> t
val upd_cofix : t -> t -> unit
val force_cofix : t -> t
val mk_const : tag -> t
val mk_block : tag -> t array -> t
val mk_bool : bool -> t
val mk_int : int -> t
val mk_uint : Uint63.t -> t
val mk_float : Float64.t -> t
val napply : t -> t array -> t
val dummy_value : unit -> t
val atom_of_accu : accumulator -> atom
val args_of_accu : accumulator -> t array
val accu_nargs : accumulator -> int
val cast_accu : t -> accumulator
type block
val block_size : block -> int
val block_field : block -> int -> t
val block_tag : block -> int
type kind_of_value =
| Vaccu of accumulator
| Vfun of t -> t
| Vconst of int
| Vint64 of int64
| Vfloat64 of float
| Vblock of block
val kind_of_value : t -> kind_of_value
val str_encode : 'a -> string
val str_decode : string -> 'a
val val_to_int : t -> int
val is_int : t -> bool
val head0 : t -> t -> t
val tail0 : t -> t -> t
val add : t -> t -> t -> t
val sub : t -> t -> t -> t
val mul : t -> t -> t -> t
val div : t -> t -> t -> t
val rem : t -> t -> t -> t
val l_sr : t -> t -> t -> t
val l_sl : t -> t -> t -> t
val l_and : t -> t -> t -> t
val l_xor : t -> t -> t -> t
val l_or : t -> t -> t -> t
val addc : t -> t -> t -> t
val subc : t -> t -> t -> t
val addCarryC : t -> t -> t -> t
val subCarryC : t -> t -> t -> t
val mulc : t -> t -> t -> t
val diveucl : t -> t -> t -> t
val div21 : t -> t -> t -> t -> t
val addMulDiv : t -> t -> t -> t -> t
val eq : t -> t -> t -> t
val lt : t -> t -> t -> t
val le : t -> t -> t -> t
val compare : t -> t -> t -> t
val print : t -> t
val no_check_head0 : t -> t
val no_check_tail0 : t -> t
val no_check_add : t -> t -> t
val no_check_sub : t -> t -> t
val no_check_mul : t -> t -> t
val no_check_div : t -> t -> t
val no_check_rem : t -> t -> t
val no_check_l_sr : t -> t -> t
val no_check_l_sl : t -> t -> t
val no_check_l_and : t -> t -> t
val no_check_l_xor : t -> t -> t
val no_check_l_or : t -> t -> t
val no_check_addc : t -> t -> t
val no_check_subc : t -> t -> t
val no_check_addCarryC : t -> t -> t
val no_check_subCarryC : t -> t -> t
val no_check_mulc : t -> t -> t
val no_check_diveucl : t -> t -> t
val no_check_div21 : t -> t -> t -> t
val no_check_addMulDiv : t -> t -> t -> t
val no_check_eq : t -> t -> t
val no_check_lt : t -> t -> t
val no_check_le : t -> t -> t
val no_check_compare : t -> t -> t
val is_float : t -> bool
val fopp : t -> t -> t
val fabs : t -> t -> t
val feq : t -> t -> t -> t
val flt : t -> t -> t -> t
val fle : t -> t -> t -> t
val fcompare : t -> t -> t -> t
val fclassify : t -> t -> t
val fadd : t -> t -> t -> t
val fsub : t -> t -> t -> t
val fmul : t -> t -> t -> t
val fdiv : t -> t -> t -> t
val fsqrt : t -> t -> t
val float_of_int : t -> t -> t
val normfr_mantissa : t -> t -> t
val frshiftexp : t -> t -> t
val ldshiftexp : t -> t -> t -> t
val next_up : t -> t -> t
val next_down : t -> t -> t
val no_check_fopp : t -> t
val no_check_fabs : t -> t
val no_check_feq : t -> t -> t
val no_check_flt : t -> t -> t
val no_check_fle : t -> t -> t
val no_check_fcompare : t -> t -> t
val no_check_fclassify : t -> t
val no_check_fadd : t -> t -> t
val no_check_fsub : t -> t -> t
val no_check_fmul : t -> t -> t
val no_check_fdiv : t -> t -> t
val no_check_fsqrt : t -> t
val no_check_float_of_int : t -> t
val no_check_normfr_mantissa : t -> t
val no_check_frshiftexp : t -> t
val no_check_ldshiftexp : t -> t -> t
val no_check_next_up : t -> t
val no_check_next_down : t -> t