package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

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

Module VmvaluesSource

Values

Sourcetype values
Sourcetype structured_values
Sourcetype vm_env
Sourcetype vm_global
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 =
  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
Sourceval pp_struct_const : structured_constant -> Pp.t
Sourcetype reloc_table = (tag * int) array
Sourcetype annot_switch = {
  1. rtbl : reloc_table;
  2. tailcall : bool;
  3. 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 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 vm_global : values array -> vm_global
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 = {
  1. sw_type_code : tcode;
  2. sw_code : tcode;
  3. sw_annot : annot_switch;
  4. sw_stk : vstack;
  5. 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 =
  1. | ConstKey of Names.Constant.t
  2. | VarKey of Names.Id.t
  3. | RelKey of Int.t
  4. | EvarKey of Evar.t
Sourceval eq_id_key : id_key -> id_key -> bool
Sourcetype atom =
  1. | Aid of id_key
  2. | Aind of Names.inductive
  3. | Asort of Sorts.t
Sourceval get_atom_rel : unit -> atom array

Global table of rels

Zippers

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

    might be empty

    *)
  3. | Zswitch of vswitch
  4. | Zproj of Names.Projection.Repr.t
Sourcetype stack = zipper list
Sourcetype 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

Sourceval pr_atom : atom -> Pp.t
Sourceval pr_whd : whd -> 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_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
Sourceval val_of_proj_name : Names.Projection.Repr.t -> values

Destructors

Sourceval whd_val : values -> whd
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
Sourceval 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
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