package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.kernel/Nativevalues/index.html

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
Sourceval apply : t -> t -> t
Sourceval of_fun : (t -> t) -> t
Sourceval eta_expand : t -> t
Sourcetype ('a, 'b) eq = ('a, 'b) Util.eq =
  1. | 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 = {
  1. asw_ind : Names.inductive;
  2. asw_reloc : reloc_table;
  3. asw_finite : bool;
  4. 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 =
  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
  7. | Afix of t array * t array * rec_pos * int
  8. | Acofix of t array * t array * int * vcofix
  9. | Aevar of Evar.t * t array
  10. | 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. | SymbEvar of Evar.t
  8. | SymbInstance of UVars.Instance.t
  9. | 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 mk_string : Pstring.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
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 strings

Sourceval is_string : t -> bool
Sourceval no_check_string_make : t -> t -> t
Sourceval no_check_string_length : t -> t
Sourceval no_check_string_get : t -> t -> t
Sourceval no_check_string_sub : t -> t -> t -> t
Sourceval no_check_string_cat : t -> t -> t
Sourceval no_check_string_compare : t -> t -> t
Sourceval string_make : t -> t -> t -> t
Sourceval string_length : t -> t -> t
Sourceval string_get : t -> t -> t -> t
Sourceval string_sub : t -> t -> t -> t -> t
Sourceval string_cat : t -> t -> t -> t
Sourceval string_compare : t -> t -> 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