Module Nativevalues

This modules defines the representation of values internally used by the native compiler. Be careful when removing apparently dead code from this interface, as it may be used by programs generated at runtime.

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