Module `Nativevalues`Source

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

Sourceval apply : t -> t -> t

Sourceval of_fun : (t -> t) -> t

Sourceval eta_expand : t -> t

Sourcetype ('a, 'b) eq = ('a, 'b) Util.eq =

| Refl : ('a, 'a) eq

Sourceval t_eq : (t, t -> t) eq

When -rectypes, matching on this makes t = ('a -> 'a) as 'a. When not -rectypes, it does nothing AFAICT so you have to generalize your problem to use this.

Sourcetype accumulator

Sourcetype tag = int

Sourcetype arity = int

Sourcetype reloc_table = (tag * arity) array

Sourcetype annot_sw = {

asw_ind : Names.inductive;
asw_reloc : reloc_table;
asw_finite : bool;
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 vcofix

Sourcetype 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
| Afix of t array * t array * rec_pos * int
| Acofix of t array * t array * int * vcofix
| Aevar of Evar.t * t array
| Aproj of Names.inductive * int * accumulator

Sourcetype 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
| SymbEvar of Evar.t
| SymbInstance of UVars.Instance.t
| 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 -> UVars.Instance.t -> t

Sourceval mk_ind_accu : Names.inductive -> UVars.Instance.t -> t

Sourceval mk_sort_accu : Sorts.t -> UVars.Instance.t -> t

Sourceval mk_var_accu : Names.Id.t -> t

Sourceval mk_sw_accu : annot_sw -> accumulator -> 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_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_prod : Names.Name.t -> t -> t -> 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 list

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

Source

type kind =
  (t,
    accumulator,
    t ->
    t,
    Names.Name.t * t * t,
    Util.Empty.t,
    Util.Empty.t,
    block)
    Values.kind

Sourceval kind_of_value : t -> kind

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 fequal : 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_fequal : 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 -> t

Sourceval arrayset : t -> t -> t -> t -> t -> t

Sourceval arraycopy : t -> t -> t -> t

Sourceval arraylength : t -> t -> t -> t

Sourceval no_check_arraymake : t -> t -> t

Sourceval no_check_arrayget : 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Nativevalues/index.html

Module `Nativevalues`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Nativevalues/index.html

Module NativevaluesSource

Module `Nativevalues`Source