Module NativevaluesSource

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.

Sourcetype t = t -> t
Sourcetype accumulator
Sourcetype tag = int
Sourcetype arity = int
Sourcetype reloc_table = (tag * arity) array
Sourcetype annot_sw = {
  1. asw_ind : Names.inductive;
  2. asw_ci : Constr.case_info;
  3. asw_reloc : reloc_table;
  4. asw_finite : bool;
  5. asw_prefix : string;
}
Sourceval eq_annot_sw : annot_sw -> annot_sw -> bool
Sourceval hash_annot_sw : annot_sw -> int
Sourcetype sort_annot = string * int
Sourcetype rec_pos = int array
Sourceval eq_rec_pos : rec_pos -> rec_pos -> bool
Sourcetype atom =
  1. | Arel of int
  2. | Aconstant of Constr.pconstant
  3. | Aind of Constr.pinductive
  4. | Asort of Sorts.t
  5. | Avar of Names.Id.t
  6. | Acase of annot_sw * accumulator * t * t -> t
  7. | Afix of t array * t array * rec_pos * int
  8. | Acofix of t array * t array * int * t
  9. | Acofixe of t array * t array * int * t
  10. | Aprod of Names.Name.t * t * t -> t
  11. | Ameta of Constr.metavariable * t
  12. | Aevar of Evar.t * t array
  13. | Aproj of Names.inductive * int * accumulator
Sourcetype symbol =
  1. | SymbValue of t
  2. | SymbSort of Sorts.t
  3. | SymbName of Names.Name.t
  4. | SymbConst of Names.Constant.t
  5. | SymbMatch of annot_sw
  6. | SymbInd of Names.inductive
  7. | SymbMeta of Constr.metavariable
  8. | SymbEvar of Evar.t
  9. | SymbLevel of Univ.Level.t
  10. | SymbProj of Names.inductive * int
Sourcetype symbols = symbol array
Sourceval empty_symbols : symbols
Sourceval mk_accu : atom -> t
Sourceval mk_rel_accu : int -> t
Sourceval mk_rels_accu : int -> int -> t array
Sourceval mk_constant_accu : Names.Constant.t -> Univ.Level.t array -> t
Sourceval mk_ind_accu : Names.inductive -> Univ.Level.t array -> t
Sourceval mk_sort_accu : Sorts.t -> Univ.Level.t array -> t
Sourceval mk_var_accu : Names.Id.t -> t
Sourceval mk_sw_accu : annot_sw -> accumulator -> t -> t -> t
Sourceval mk_prod_accu : Names.Name.t -> t -> t -> t
Sourceval mk_fix_accu : rec_pos -> int -> t array -> t array -> t
Sourceval mk_cofix_accu : int -> t array -> t array -> t
Sourceval mk_meta_accu : Constr.metavariable -> t
Sourceval mk_evar_accu : Evar.t -> t array -> t
Sourceval mk_proj_accu : (Names.inductive * int) -> accumulator -> t
Sourceval upd_cofix : t -> t -> unit
Sourceval force_cofix : t -> t
Sourceval mk_const : tag -> t
Sourceval mk_block : tag -> t array -> t
Sourceval mk_bool : bool -> t
Sourceval mk_int : int -> t
Sourceval mk_uint : Uint63.t -> t
Sourceval mk_float : Float64.t -> t
Sourceval napply : t -> t array -> t
Sourceval dummy_value : unit -> t
Sourceval atom_of_accu : accumulator -> atom
Sourceval args_of_accu : accumulator -> t array
Sourceval accu_nargs : accumulator -> int
Sourceval cast_accu : t -> accumulator
Sourcetype block
Sourceval block_size : block -> int
Sourceval block_field : block -> int -> t
Sourceval block_tag : block -> int
Sourcetype kind_of_value =
  1. | Vaccu of accumulator
  2. | Vfun of t -> t
  3. | Vconst of int
  4. | Vint64 of int64
  5. | Vfloat64 of float
  6. | Varray of t Parray.t
  7. | Vblock of block
Sourceval kind_of_value : t -> kind_of_value
Sourceval str_encode : 'a -> string
Sourceval str_decode : string -> 'a

Support for machine integers

Sourceval val_to_int : t -> int
Sourceval is_int : t -> bool
Sourceval head0 : t -> t -> t
Sourceval tail0 : t -> t -> t
Sourceval add : t -> t -> t -> t
Sourceval sub : t -> t -> t -> t
Sourceval mul : t -> t -> t -> t
Sourceval div : t -> t -> t -> t
Sourceval rem : t -> t -> t -> t
Sourceval divs : t -> t -> t -> t
Sourceval rems : t -> t -> t -> t
Sourceval l_sr : t -> t -> t -> t
Sourceval l_sl : t -> t -> t -> t
Sourceval a_sr : t -> t -> t -> t
Sourceval l_and : t -> t -> t -> t
Sourceval l_xor : t -> t -> t -> t
Sourceval l_or : t -> t -> t -> t
Sourceval addc : t -> t -> t -> t
Sourceval subc : t -> t -> t -> t
Sourceval addCarryC : t -> t -> t -> t
Sourceval subCarryC : t -> t -> t -> t
Sourceval mulc : t -> t -> t -> t
Sourceval diveucl : t -> t -> t -> t
Sourceval div21 : t -> t -> t -> t -> t
Sourceval addMulDiv : t -> t -> t -> t -> t
Sourceval eq : t -> t -> t -> t
Sourceval lt : t -> t -> t -> t
Sourceval le : t -> t -> t -> t
Sourceval lts : t -> t -> t -> t
Sourceval les : t -> t -> t -> t
Sourceval compare : t -> t -> t -> t
Sourceval compares : t -> t -> t -> t
Sourceval print : t -> t
Sourceval no_check_head0 : t -> t
Sourceval no_check_tail0 : t -> t
Sourceval no_check_add : t -> t -> t
Sourceval no_check_sub : t -> t -> t
Sourceval no_check_mul : t -> t -> t
Sourceval no_check_div : t -> t -> t
Sourceval no_check_rem : t -> t -> t
Sourceval no_check_divs : t -> t -> t
Sourceval no_check_rems : t -> t -> t
Sourceval no_check_l_sr : t -> t -> t
Sourceval no_check_l_sl : t -> t -> t
Sourceval no_check_a_sr : t -> t -> t
Sourceval no_check_l_and : t -> t -> t
Sourceval no_check_l_xor : t -> t -> t
Sourceval no_check_l_or : t -> t -> t
Sourceval no_check_addc : t -> t -> t
Sourceval no_check_subc : t -> t -> t
Sourceval no_check_addCarryC : t -> t -> t
Sourceval no_check_subCarryC : t -> t -> t
Sourceval no_check_mulc : t -> t -> t
Sourceval no_check_diveucl : t -> t -> t
Sourceval no_check_div21 : t -> t -> t -> t
Sourceval no_check_addMulDiv : t -> t -> t -> t
Sourceval no_check_eq : t -> t -> t
Sourceval no_check_lt : t -> t -> t
Sourceval no_check_le : t -> t -> t
Sourceval no_check_lts : t -> t -> t
Sourceval no_check_les : t -> t -> t
Sourceval no_check_compare : t -> t -> t
Sourceval no_check_compares : t -> t -> t

Support for machine floating point values

Sourceval is_float : t -> bool
Sourceval fopp : t -> t -> t
Sourceval fabs : t -> t -> t
Sourceval feq : t -> t -> t -> t
Sourceval flt : t -> t -> t -> t
Sourceval fle : t -> t -> t -> t
Sourceval fcompare : t -> t -> t -> t
Sourceval fclassify : t -> t -> t
Sourceval fadd : t -> t -> t -> t
Sourceval fsub : t -> t -> t -> t
Sourceval fmul : t -> t -> t -> t
Sourceval fdiv : t -> t -> t -> t
Sourceval fsqrt : t -> t -> t
Sourceval float_of_int : t -> t -> t
Sourceval normfr_mantissa : t -> t -> t
Sourceval frshiftexp : t -> t -> t
Sourceval ldshiftexp : t -> t -> t -> t
Sourceval next_up : t -> t -> t
Sourceval next_down : t -> t -> t
Sourceval no_check_fopp : t -> t
Sourceval no_check_fabs : t -> t
Sourceval no_check_feq : t -> t -> t
Sourceval no_check_flt : t -> t -> t
Sourceval no_check_fle : t -> t -> t
Sourceval no_check_fcompare : t -> t -> t
Sourceval no_check_fclassify : t -> t
Sourceval no_check_fadd : t -> t -> t
Sourceval no_check_fsub : t -> t -> t
Sourceval no_check_fmul : t -> t -> t
Sourceval no_check_fdiv : t -> t -> t
Sourceval no_check_fsqrt : t -> t
Sourceval no_check_float_of_int : t -> t
Sourceval no_check_normfr_mantissa : t -> t
Sourceval no_check_frshiftexp : t -> t
Sourceval no_check_ldshiftexp : t -> t -> t
Sourceval no_check_next_up : t -> t
Sourceval no_check_next_down : t -> t

Support for arrays

Sourceval parray_of_array : t -> t -> t
Sourceval is_parray : t -> bool
Sourceval arraymake : t -> t -> t -> t -> t
Sourceval arrayget : t -> t -> t -> t -> t
Sourceval arraydefault : t -> t -> t
Sourceval arrayset : t -> t -> t -> t -> t -> t
Sourceval arraycopy : t -> t -> t -> t
Sourceval arraylength : t -> t -> t -> t
Sourceval arrayinit : t -> t -> t -> t
Sourceval arraymap : t -> t -> t
Sourceval no_check_arraymake : t -> t -> t
Sourceval no_check_arrayget : t -> t -> t -> t
Sourceval no_check_arraydefault : t -> t
Sourceval no_check_arrayset : t -> t -> t -> t
Sourceval no_check_arraycopy : t -> t
Sourceval no_check_arraylength : t -> t