package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Values

type values
type structured_values
type vm_env
type vprod
type vfun
type vfix
type vcofix
type vblock
type arguments
type vstack = values array
type to_update
type tag = int
val type_atom_tag : tag
val max_atom_tag : tag
val proj_tag : tag
val fix_app_tag : tag
val switch_tag : tag
val cofix_tag : tag
val cofix_evaluated_tag : tag
type structured_constant =
  1. | Const_sort of Sorts.t
  2. | Const_ind of Names.inductive
  3. | Const_b0 of tag
  4. | Const_univ_level of Univ.Level.t
  5. | Const_val of structured_values
  6. | Const_uint of Uint63.t
  7. | Const_float of Float64.t
val pp_struct_const : structured_constant -> Pp.t
type reloc_table = (tag * int) array
type annot_switch = {
  1. rtbl : reloc_table;
  2. tailcall : bool;
  3. max_stack_size : int;
}
val eq_structured_constant : structured_constant -> structured_constant -> bool
val hash_structured_constant : structured_constant -> int
val eq_annot_switch : annot_switch -> annot_switch -> bool
val hash_annot_switch : annot_switch -> int
val fun_val : vfun -> values
val fix_val : vfix -> values
val cofix_upd_val : to_update -> values
val inj_env : values array -> vm_env
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

Cast a value known to be a function, unsafe in general

val crazy_val : values

Machine code

type tcode
type vswitch = {
  1. sw_type_code : tcode;
  2. sw_code : tcode;
  3. sw_annot : annot_switch;
  4. sw_stk : vstack;
  5. 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 =
  1. | ConstKey of Names.Constant.t
  2. | VarKey of Names.Id.t
  3. | RelKey of Int.t
  4. | EvarKey of Evar.t
val eq_id_key : id_key -> id_key -> bool
type atom =
  1. | Aid of id_key
  2. | Aind of Names.inductive
  3. | Asort of Sorts.t
val get_atom_rel : unit -> atom array

Global table of rels

Zippers

type zipper =
  1. | Zapp of arguments
  2. | Zfix of vfix * arguments
    (*

    might be empty

    *)
  3. | Zswitch of vswitch
  4. | Zproj of int
type stack = zipper list
type whd =
  1. | Vprod of vprod
  2. | Vfun of vfun
  3. | Vfix of vfix * arguments option
  4. | Vcofix of vcofix * to_update * arguments option
  5. | Vconstr_const of int
  6. | Vconstr_block of vblock
  7. | Vint64 of int64
  8. | Vfloat64 of float
  9. | Varray of values Parray.t
  10. | Vatom_stk of atom * stack
  11. | Vuniv_level of Univ.Level.t

For debugging purposes only

val pr_atom : atom -> Pp.t
val pr_whd : whd -> Pp.t
val pr_stack : stack -> Pp.t

Constructors

val val_of_str_const : 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 : int -> values -> values
val val_of_atom : atom -> values
val val_of_int : int -> structured_values
val val_of_block : tag -> structured_values array -> structured_values
val val_of_uint : Uint63.t -> structured_values
val val_of_annot_switch : annot_switch -> values

Destructors

val whd_val : values -> whd
val uni_lvl_val : values -> Univ.Level.t

Arguments

val nargs : arguments -> int
val arg : arguments -> int -> values

Product

val dom : vprod -> values
val codom : vprod -> vfun
val closure_arity : vfun -> int

Fun

Fix

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 mk_fix_body : int -> int -> vfix -> vfun array

CoFix

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

Block

val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> values

Switch

val check_switch : vswitch -> vswitch -> bool
val branch_arg : int -> (tag * int) -> values
val parray_make : values

Primitives implemented in OCaml, seen as values (to be used as globals)

val parray_get : values
val parray_get_default : values
val parray_set : values
val parray_copy : values
val parray_length : values
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct