Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341(************************************************************************)(* * 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 Constropen Names
(** This modules defines the representation of values internally used bythe native compiler. Be careful when removing apparently dead code from thisinterface, as it may be used by programs generated at runtime. *)
type t
val apply : t -> t -> tval of_fun : (t -> t) -> t
val eta_expand : t -> t
type ('a,'b) eq = ('a,'b) Util.eq = Refl : ('a,'a) eqval 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. *)
type accumulator
type tag = inttype 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
val eq_rec_pos : rec_pos -> rec_pos -> bool
type vcofix
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 | Acofix of t array * t array * int * t array * vcofix | Aevar of Evar.t * t array (* arguments *) | 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 symbols = symbol array
val empty_symbols : symbols
(* Constructors *)
val mk_accu : atom -> tval mk_rel_accu : int -> tval mk_rels_accu : int -> int -> t arrayval mk_constant_accu : Constant.t -> UVars.Instance.t -> tval mk_ind_accu : inductive -> UVars.Instance.t -> tval mk_sort_accu : Sorts.t -> tval mk_var_accu : Id.t -> tval mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)val mk_fix_accu : rec_pos -> int -> t array -> t array -> tval mk_cofix_accu : int -> t array -> t array -> (unit -> t) -> t array -> tval mk_evar_accu : Evar.t -> t array -> tval mk_proj_accu : (inductive * int) -> accumulator -> tval force_cofix : t -> texternal mk_const : tag -> t = "%identity"val mk_block : tag -> t array -> tval mk_prod : Name.t -> t -> t -> t
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"
val napply : t -> t array -> t(* Functions over accumulators *)
val atom_of_accu : accumulator -> atomval args_of_accu : accumulator -> t listval accu_nargs : accumulator -> int
external cast_accu : t -> accumulator = "%identity"
(* Functions over block: i.e constructors *)
type block
val block_size : block -> intval block_field : block -> int -> tval block_tag : block -> int
(* kind_of_value *)
type kind = (t, accumulator, t -> t, Name.t * t * t, Util.Empty.t, Util.Empty.t, block) Values.kind
val kind_of_value : t -> kind
val str_encode : 'a -> stringval str_decode : string -> 'a
(** Support for machine integers *)
val val_to_int : t -> int
val is_int : t -> bool
(* function with check *)val head0 : t -> t -> tval tail0 : t -> t -> t
val add : t -> t -> t -> tval sub : t -> t -> t -> tval mul : t -> t -> t -> tval div : t -> t -> t -> tval rem : t -> t -> t -> tval divs : t -> t -> t -> tval rems : t -> t -> t -> t
val l_sr : t -> t -> t -> tval l_sl : t -> t -> t -> tval a_sr : t -> t -> t -> tval l_and : t -> t -> t -> tval l_xor : t -> t -> t -> tval l_or : t -> t -> t -> t
val addc : t -> t -> t -> tval subc : t -> t -> t -> tval addCarryC : t -> t -> t -> tval subCarryC : t -> t -> t -> t
val mulc : t -> t -> t -> tval diveucl : t -> t -> t -> t
val div21 : t -> t -> t -> t -> tval addMulDiv : t -> t -> t -> t -> t
val eq : t -> t -> t -> tval lt : t -> t -> t -> tval le : t -> t -> t -> tval lts : t -> t -> t -> tval les : t -> t -> t -> tval compare : t -> t -> t -> tval compares : t -> t -> t -> t
val print : t -> t
(* Function without check *)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_divs : t -> t -> t
val no_check_rems : t -> t -> t
val no_check_l_sr : t -> t -> t
val no_check_l_sl : t -> t -> t
val no_check_a_sr : 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_lts : t -> t -> t
val no_check_les : t -> t -> t
val no_check_compare : t -> t -> t
val no_check_compares : t -> t -> t
(** Support for machine floating point values *)
val is_float : t -> bool
val fopp : t -> t -> tval fabs : t -> t -> tval feq : t -> t -> t -> tval flt : t -> t -> t -> tval fle : t -> t -> t -> tval fcompare : t -> t -> t -> tval fequal : t -> t -> t -> tval fclassify : t -> t -> tval fadd : t -> t -> t -> tval fsub : t -> t -> t -> tval fmul : t -> t -> t -> tval fdiv : t -> t -> t -> tval fsqrt : t -> t -> tval float_of_int : t -> t -> tval normfr_mantissa : t -> t -> tval frshiftexp : t -> t -> tval ldshiftexp : t -> t -> t -> tval next_up : t -> t -> tval next_down : t -> t -> t
(* Function without check *)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_fequal : 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
(** Support for strings *)
val is_string : t -> bool
val no_check_string_make : t -> t -> tval no_check_string_length : t -> tval no_check_string_get : t -> t -> tval no_check_string_sub : t -> t -> t -> tval no_check_string_cat : t -> t -> tval no_check_string_compare : t -> t -> t
val string_make : t -> t -> t -> tval string_length : t -> t -> tval string_get : t -> t -> t -> tval string_sub : t -> t -> t -> t -> tval string_cat : t -> t -> t -> tval string_compare : t -> t -> t -> t
(** Support for arrays *)
val parray_of_array : t -> t -> tval is_parray : t -> bool
val arraymake : t -> t -> t -> t -> t (* accu A n def *)val arrayget : t -> t -> t -> t -> t (* accu A t n *)val arraydefault : t -> t -> t -> t (* accu A t *)val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *)val arraycopy : t -> t -> t -> t (* accu A t *)val arraylength : t -> t -> t -> t (* accu A t *)
val no_check_arraymake : t -> t -> t
val no_check_arrayget : t -> t -> t
val no_check_arraydefault : t -> t
val no_check_arrayset : t -> t -> t -> t
val no_check_arraycopy : t -> t
val no_check_arraylength : t -> t