package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

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

Module VmvaluesSource

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 =
  1. | Const_sort of Sorts.t
  2. | Const_ind of Names.inductive
  3. | Const_evar of Evar.t
  4. | Const_b0 of tag
  5. | Const_quality of Sorts.Quality.t
  6. | Const_univ_level of Univ.Level.t
  7. | Const_univ_instance of UVars.Instance.t
  8. | Const_val of structured_values
  9. | Const_uint of Uint63.t
  10. | 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 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 = {
  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 int
Sourcetype stack = zipper list
Sourcetype accumulator = atom * stack

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_instance : values -> UVars.Instance.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