Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208(************************************************************************)(* * 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 Names
(** Values *)
type valuestype structured_valuestype vm_envtype vprodtype vfuntype vfixtype vcofixtype vblocktype argumentstype vstack = values arraytype to_update
type tag = int
val type_atom_tag : tagval max_atom_tag : tagval proj_tag : tagval fix_app_tag : tagval switch_tag : tagval cofix_tag : tagval cofix_evaluated_tag : tag
type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive | Const_var of Id.t | Const_evar of Evar.t | Const_b0 of tag | Const_univ_instance of UVars.Instance.t | Const_val of structured_values | Const_uint of Uint63.t | Const_float of Float64.t | Const_string of Pstring.t
val pp_struct_const : structured_constant -> Pp.t
type reloc_table = (tag * int) array
type annot_switch = { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
val eq_structured_constant : structured_constant -> structured_constant -> boolval hash_structured_constant : structured_constant -> int
val eq_annot_switch : annot_switch -> annot_switch -> boolval hash_annot_switch : annot_switch -> int
val fun_val : vfun -> valuesval fix_val : vfix -> valuesval cofix_upd_val : to_update -> values
val inj_env : values array -> vm_envval fun_env : vfun -> vm_envval fix_env : vfix -> vm_envval fix_self : vfix -> vm_envval cofix_env : vcofix -> vm_envval cofix_upd_env : to_update -> vm_env
(** Cast a value known to be a function, unsafe in general *)val fun_of_val : values -> vfun
val crazy_val : values
(** Machine code *)
type tcode
type vswitch = { sw_type_code : tcode; sw_code : tcode; sw_annot : annot_switch; sw_stk : vstack; sw_env : vm_env }
external mkAccuCode : int -> tcode = "rocq_makeaccu"
val fun_code : vfun -> tcodeval fix_code : vfix -> tcodeval cofix_upd_code : to_update -> tcode
type id_key =| ConstKey of Constant.t| VarKey of 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 inductive | Asort of Sorts.t
val get_atom_rel : unit -> atom array(** Global table of rels *)
(** Zippers *)
type zipper = | Zapp of arguments | Zfix of vfix * arguments (** might be empty *) | Zswitch of vswitch | Zproj of int (* index of the projection as in Projection.Repr *)
type stack = zipper list
type accumulator = atom * stack
type kind = (values, accumulator, vfun, vprod, vfix * arguments option, vcofix * to_update * arguments option, vblock) Values.kind
(** For debugging purposes only *)
val pr_atom : atom -> Pp.tval pr_kind : kind -> Pp.tval pr_stack : stack -> Pp.t
(** Constructors *)
val val_of_str_const : structured_constant -> valuesval val_of_rel : int -> valuesval val_of_named : Id.t -> valuesval val_of_constant : Constant.t -> valuesval val_of_evar : Evar.t -> valuesval val_of_proj : int -> values -> valuesval val_of_atom : atom -> valuesval val_of_int : int -> structured_valuesval val_of_block : tag -> structured_values array -> structured_valuesval val_of_uint : Uint63.t -> structured_valuesval val_of_float : Float64.t -> structured_valuesval val_of_string : Pstring.t -> structured_values
external val_of_annot_switch : annot_switch -> values = "%identity"
(** Destructors *)
val whd_val : values -> kindval uni_instance : values -> UVars.Instance.t
(** Arguments *)
val nargs : arguments -> intval arg : arguments -> int -> values
(** Product *)
val dom : vprod -> valuesval codom : vprod -> vfun
(** Fun *)external closure_arity : vfun -> int = "rocq_closure_arity"
(** Fix *)
val current_fix : vfix -> intval check_fix : vfix -> vfix -> boolval rec_args : vfix -> int arrayval first_fix : vfix -> vfixval fix_types : vfix -> tcode arrayval cofix_types : vcofix -> tcode arrayval mk_fix_body : int -> int -> vfix -> vfun array
(** CoFix *)
val current_cofix : vcofix -> intval check_cofix : vcofix -> vcofix -> boolval mk_cofix_body : (vfun -> vstack -> values) -> int -> int -> vcofix -> values array
(** Block *)
val btag : vblock -> intval bsize : vblock -> intval bfield : vblock -> int -> values
(** Switch *)
val check_switch : vswitch -> vswitch -> boolval branch_arg : int -> tag * int -> values
(** Primitives implemented in OCaml, seen as values (to be used as globals) *)val parray_make : valuesval parray_get : valuesval parray_get_default : valuesval parray_set : valuesval parray_copy : valuesval parray_length : values
val pstring_make : valuesval pstring_length : valuesval pstring_get : valuesval pstring_sub : valuesval pstring_cat : valuesval pstring_compare : values