coq 8.8.1 · OCaml Package

type values

type vm_env

type vprod

type vfun

type vfix

type vcofix

type vblock

type arguments

type vstack = values array

type to_update

val fun_val : vfun -> values

val fix_val : vfix -> values

val cofix_upd_val : to_update -> values

val fun_env : vfun -> vm_env

val fix_env : vfix -> vm_env

val cofix_env : vcofix -> vm_env

val cofix_upd_env : to_update -> vm_env

val fun_of_val : values -> vfun

val crazy_val : values

type tcode

type vswitch = {

sw_type_code : tcode;
sw_code : tcode;
sw_annot : Cbytecodes.annot_switch;
sw_stk : vstack;
sw_env : vm_env;

}

val mkAccuCode : int -> tcode

val fun_code : vfun -> tcode

val fix_code : vfix -> tcode

val cofix_upd_code : to_update -> tcode

type id_key =

| ConstKey of Names.Constant.t
| VarKey of Names.Id.t
| RelKey of Int.t
| EvarKey of Evar.t

val eq_id_key : id_key -> id_key -> bool

type atom =

| Aid of id_key
| Aind of Names.inductive
| Asort of Sorts.t

type zipper =

| Zapp of arguments
| Zfix of vfix * arguments
| Zswitch of vswitch
| Zproj of Names.Constant.t

type stack = zipper list

type whd =

| Vprod of vprod
| Vfun of vfun
| Vfix of vfix * arguments option
| Vcofix of vcofix * to_update * arguments option
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
| Vuniv_level of Univ.Level.t

val pr_atom : atom -> Pp.t

val pr_whd : whd -> Pp.t

val pr_stack : stack -> Pp.t

val val_of_str_const : Cbytecodes.structured_constant -> values

val val_of_rel : int -> values

val val_of_named : Names.Id.t -> values

val val_of_constant : Names.Constant.t -> values

val val_of_evar : Evar.t -> values

val val_of_proj : Names.Constant.t -> values -> values

val val_of_atom : atom -> values

val val_of_annot_switch : Cbytecodes.annot_switch -> values

val whd_val : values -> whd

val uni_lvl_val : values -> Univ.Level.t

val nargs : arguments -> int

val arg : arguments -> int -> values

val dom : vprod -> values

val codom : vprod -> vfun

val closure_arity : vfun -> int

val current_fix : vfix -> int

val check_fix : vfix -> vfix -> bool

val rec_args : vfix -> int array

val first_fix : vfix -> vfix

val fix_types : vfix -> tcode array

val cofix_types : vcofix -> tcode array

val offset_closure_fix : vfix -> int -> vm_env

val mk_fix_body : int -> int -> vfix -> vfun array

val current_cofix : vcofix -> int

val check_cofix : vcofix -> vcofix -> bool

val mk_cofix_body : 
  (vfun -> vstack -> values) ->
  int ->
  int ->
  vcofix ->
  values array

val btag : vblock -> int

val bsize : vblock -> int

val bfield : vblock -> int -> values

val check_switch : vswitch -> vswitch -> bool

val branch_arg : int -> (Cbytecodes.tag * int) -> values

package coq