package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.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_univ_instance of UVars.Instance.t
  6. | Const_val of structured_values
  7. | Const_uint of Uint63.t
  8. | Const_float of Float64.t
  9. | Const_string of Pstring.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_float : Float64.t -> structured_values
Sourceval val_of_string : Pstring.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
Sourceval pstring_make : values
Sourceval pstring_length : values
Sourceval pstring_get : values
Sourceval pstring_sub : values
Sourceval pstring_cat : values
Sourceval pstring_compare : values