Module `Vmvalues`Source

Values

Sourcetype values

Sourcetype structured_values

Sourcetype vm_env

Sourcetype vprod

Sourcetype vfun

Sourcetype vfix

Sourcetype vcofix

Sourcetype vblock

Sourcetype arguments

Sourcetype vstack = values array

Sourcetype to_update

Sourcetype tag = int

Sourceval type_atom_tag : tag

Sourceval max_atom_tag : tag

Sourceval proj_tag : tag

Sourceval fix_app_tag : tag

Sourceval switch_tag : tag

Sourceval cofix_tag : tag

Sourceval cofix_evaluated_tag : tag

Sourcetype structured_constant =

| Const_sort of Sorts.t
| Const_ind of Names.inductive
| Const_b0 of tag
| Const_univ_level of Univ.Level.t
| Const_val of structured_values
| Const_uint of Uint63.t
| Const_float of Float64.t

Sourceval pp_struct_const : structured_constant -> Pp.t

Sourcetype reloc_table = (tag * int) array

Sourcetype annot_switch = {

rtbl : reloc_table;
tailcall : bool;
max_stack_size : int;

}

Sourceval eq_structured_constant : structured_constant -> structured_constant -> bool

Sourceval hash_structured_constant : structured_constant -> int

Sourceval eq_annot_switch : annot_switch -> annot_switch -> bool

Sourceval hash_annot_switch : annot_switch -> int

Sourceval fun_val : vfun -> values

Sourceval fix_val : vfix -> values

Sourceval cofix_upd_val : to_update -> values

Sourceval inj_env : values array -> vm_env

Sourceval fun_env : vfun -> vm_env

Sourceval fix_env : vfix -> vm_env

Sourceval cofix_env : vcofix -> vm_env

Sourceval cofix_upd_env : to_update -> vm_env

Sourceval fun_of_val : values -> vfun

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

Sourceval crazy_val : values

Machine code

Sourcetype tcode

Sourcetype vswitch = {

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

}

Sourceval mkAccuCode : int -> tcode

Sourceval fun_code : vfun -> tcode

Sourceval fix_code : vfix -> tcode

Sourceval cofix_upd_code : to_update -> tcode

Sourcetype id_key =

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

Sourceval eq_id_key : id_key -> id_key -> bool

Sourcetype atom =

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

Sourceval get_atom_rel : unit -> atom array

Global table of rels

Zippers

Sourcetype zipper =

| Zapp of arguments
| Zfix of vfix * arguments
(*
might be empty
*)
| Zswitch of vswitch
| Zproj of int

Sourcetype stack = zipper list

Sourcetype accumulator = atom * stack

Source

type kind =
  (values,
    accumulator,
    vfun,
    vprod,
    vfix * arguments option,
    vcofix * to_update * arguments option,
    vblock)
    Values.kind

For debugging purposes only

Sourceval pr_atom : atom -> Pp.t

Sourceval pr_kind : kind -> Pp.t

Sourceval pr_stack : stack -> Pp.t

Constructors

Sourceval val_of_str_const : structured_constant -> values

Sourceval val_of_rel : int -> values

Sourceval val_of_named : Names.Id.t -> values

Sourceval val_of_constant : Names.Constant.t -> values

Sourceval val_of_evar : Evar.t -> values

Sourceval val_of_proj : int -> values -> values

Sourceval val_of_atom : atom -> values

Sourceval val_of_int : int -> structured_values

Sourceval val_of_block : tag -> structured_values array -> structured_values

Sourceval val_of_uint : Uint63.t -> structured_values

Sourceval val_of_annot_switch : annot_switch -> values

Destructors

Sourceval whd_val : values -> kind

Sourceval uni_lvl_val : values -> Univ.Level.t

Arguments

Sourceval nargs : arguments -> int

Sourceval arg : arguments -> int -> values

Product

Sourceval dom : vprod -> values

Sourceval codom : vprod -> vfun

Sourceval closure_arity : vfun -> int

Fun

Fix

Sourceval current_fix : vfix -> int

Sourceval check_fix : vfix -> vfix -> bool

Sourceval rec_args : vfix -> int array

Sourceval first_fix : vfix -> vfix

Sourceval fix_types : vfix -> tcode array

Sourceval cofix_types : vcofix -> tcode array

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

CoFix

Sourceval current_cofix : vcofix -> int

Sourceval check_cofix : vcofix -> vcofix -> bool

Source

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

Block

Sourceval btag : vblock -> int

Sourceval bsize : vblock -> int

Sourceval bfield : vblock -> int -> values

Switch

Sourceval check_switch : vswitch -> vswitch -> bool

Sourceval branch_arg : int -> (tag * int) -> values

Sourceval parray_make : values

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

Sourceval parray_get : values

Sourceval parray_get_default : values

Sourceval parray_set : values

Sourceval parray_copy : values

Sourceval parray_length : values

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Vmvalues/index.html

Module `Vmvalues`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Vmvalues/index.html

Module VmvaluesSource

Module `Vmvalues`Source