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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.pretyping/LibBinding/index.html

Module LibBindingSource

This file contain a lightweight API for meta-programming: to traverse binders and either keep them, create new ones.

With this API, variables are refered abstractly using access_key. For instance, to compute the term associated to a variable (debruijn variable) one should use get_term : acces_key -> constr t. Such terms can easily be created using the monadic bind: let* t = get_term k in ....

So that the users do not have to create access_key themselves, and make mistakes, the creation of access_key is directly handled by the functions creating binders. For instance, to create a product Prod A B, the body B has type access_key -> constr t where the access_key of the variable A. To easily write code, it recomended to use the notation let@: let@ key_A = make_binder naming na A in (* def of B : constr t *) .

It also provides facilities for naming variables, the different functions taking type naming_scheme = rel_declaration -> rel_declaration t as arguments. A few basic ones are provided.

To do so, the API uses a reader monad with a state that contains:

  • the environment (Declarations + local context),
  • the evar_map,
  • the set of names already used,
  • a substitution from the former context of the term being traversed, to the context of the term being created which may differ due to addition of new binders
Sourcemodule State : sig ... end
Fold Functions for State
Sourceval fold_right_state : ('c -> 'b list -> 'b list) -> 'a list -> (int -> 'a -> ('c -> 'd State.t) -> 'd State.t) -> ('b list -> 'd State.t) -> 'd State.t

This function is meant to iterate a function creating binders. 'c -> 'b list -> 'b list explains which access_key to save, e.g. :: to save them all.

Sourceval fold_left_state : ('c -> 'b list -> 'b list) -> 'a list -> (int -> 'a -> ('c -> 'd State.t) -> 'd State.t) -> ('b list -> 'd State.t) -> 'd State.t

This function is meant to iterate a function creating binders: int -> 'a -> ('c -> 'd t) -> 'd t. 'c -> 'b list -> 'b list explains which access_key to save, e.g. :: to save them all.

Sourceval fold_right_state_3 : ('c -> 'b list -> 'b list) -> 'a list -> (int -> 'a -> (('c * 'c * 'c) -> 'd State.t) -> 'd State.t) -> (('b list * 'b list * 'b list) -> 'd State.t) -> 'd State.t

This function is meant to iterate a function creating binders. 'c -> 'b list -> 'b list explains which access_key to save, e.g. :: to save them all.

Sourceval fold_left_state_3 : ('c -> 'b list -> 'b list) -> 'a list -> (int -> 'a -> (('c * 'c * 'c) -> 'd State.t) -> 'd State.t) -> (('b list * 'b list * 'b list) -> 'd State.t) -> 'd State.t

This function is meant to iterate a function creating binders: int -> 'a -> ('c -> 'd t) -> 'd t. 'c -> 'b list -> 'b list explains which access_key to save, e.g. :: to save them all.

Naming Schemes for Binders
Sourceval naming_id : naming_scheme

Identity namming

Sourceval naming_hd : naming_scheme

Name the binder using the head of the declaration's type if it Anonymous.

Sourceval naming_hd_dep : bool -> naming_scheme

naming_dep if true, naming_id otherwise

Sourceval naming_hd_fresh : naming_scheme

Uses the next fresh names available, using the head of the declaration's type if it Anonymous.

Sourceval naming_hd_fresh_dep : bool -> naming_scheme

naming_hd_fresh if true, naming_id otherwise

Functions on Terms
Sourceval whd_decompose_prod_decls : EConstr.constr -> (EConstr.rel_context * EConstr.constr) State.t
Sourceval eta_expand_instantiation : EConstr.constr array -> EConstr.rel_context -> EConstr.constr array State.t
Sourceval fresh_inductive_instance : Names.inductive -> Evd.einstance State.t
Sourceval fresh_sort_ql : ?sort_rigid:bool -> ?name:Names.variable -> Evd.rigid -> (Sorts.QVar.t * Univ.Universe.t) State.t
Sourceval new_univ_level_variable : ?name:Names.variable -> Evd.rigid -> Univ.Level.t State.t
Sourceval typing_checked_appvect : EConstr.constr -> EConstr.constr array -> EConstr.constr State.t
Sourceval typing_check_actual_type : EConstr.unsafe_judgment -> EConstr.types -> unit State.t
Sourceval retyping_sort_of : EConstr.constr -> Evd.esorts State.t
Sourceval print_term : CDebug.t -> string -> EConstr.constr -> unit State.t
Sourceval print_current_context : CDebug.t -> string -> unit State.t
Create a New Lambda, Product, or LetIn
Sourcetype freshness =
  1. | Fresh
  2. | Old

Status of the variable to bind

Sourcetype binder =
  1. | Lambda
  2. | Prod

Which binders to bind

Sourceval fid : ('a -> 'b) -> 'a -> 'b
Sourceval fleft : ('a -> 'b) -> ('a * 'c) -> 'b * 'c
Sourceval fright : ('a -> 'b) -> ('c * 'a) -> 'c * 'b
Sourceval fopt : ('a -> 'b) -> 'a option -> 'b option
Sourceval fropt : ('a -> 'b) -> ('c * 'a) option -> ('c * 'b) option

Add a declaration to the state given its freshness and a naming_scheme, for a body defined in the updated state.

Bind a declaration with binder or LetIn, given its freshness and a naming_scheme, for a body defined in the updated state.

Create a new binder using a naming_scheme, for a body in the updated state. When creating a fresh binder, the type of the variable needs to type check in the current context.

Keep a former binder using a naming_scheme, for a body defined in the updated state.

Create Lambda, Product, or LetIn for Context

Add a context to the state given its freshness and a naming_scheme, for a body defined in the updated state state * access_key list -> constr.

Sourceval add_context_sep : freshness -> naming_scheme -> EConstr.rel_context -> ((State.access_key list * State.access_key list * State.access_key list) -> 'a State.t) -> 'a State.t

Add a context to the state given its freshness and a naming_scheme, for a body defined in the updated state, where the access_key are split between key_vars, key_letin, key_both.

Sourceval closure_context : ((EConstr.constr -> EConstr.constr) -> 'a -> 'a) -> binder -> freshness -> naming_scheme -> EConstr.rel_context -> (State.access_key list -> 'a State.t) -> 'a State.t

Bind a context with binder or LetIn, given its freshness and a naming_scheme, for a body defined in the updated state.

Sourceval closure_context_sep : ((EConstr.constr -> EConstr.constr) -> 'a -> 'a) -> binder -> freshness -> naming_scheme -> EConstr.rel_context -> ((State.access_key list * State.access_key list * State.access_key list) -> 'a State.t) -> 'a State.t

Bind a context with binder or LetIn, given its freshness and a naming_scheme, for a body defined in the updated state, where the access_key are split between key_vars, key_letin, key_both.

Decompose a constr as binder(s) local hd, then rebind it as binder(s) local, binder hd, cc

reads cxt binder cc_letin cc_var go through a context cxt, apply binder to each context declaration decl to it, then apply cc_letin if decl is a LetIn, and cc_var otherwise.

Given a mutual inductive body and an instance, it recovers the context of argument and the return indices of the constructor out of mind_nf_lc

Sourceval iterate_ctors : Declarations.mutual_inductive_body -> Declarations.one_inductive_body -> Evd.einstance -> (int -> (EConstr.rel_context * EConstr.constr array) -> ('a -> 'b State.t) -> 'b State.t) -> ('a list -> 'b State.t) -> 'b State.t

Iterate a binding function to each constructor or an inductive type.

Functions on Inductives

Create a term refering to an inductive type given the access_key for uniform paramters, non-uniform parameters, and indices.

Create a term refering to the constructor of an inductive type given the access_key for uniform paramters, non-uniform parameters, and indices.

Sourceval make_fix : 'a list -> int -> (int -> 'a -> int) -> (int -> 'a -> Names.Name.t EConstr.binder_annot) -> (int -> 'a -> EConstr.types State.t) -> ((State.access_key list * int * 'a) -> EConstr.constr State.t) -> EConstr.constr State.t

Create a term refering to an inductive type given the access_key for uniform paramters, non-uniform parameters, and indices.

Recover the indices of an inductive block, and weaken them in the current context.

Create a new match given:

  • A naming_scheme for the fresh indices, and arguments
  • The mutual_inductive_body, inductive, one_inductive_body, instance on which the match is performed
  • The access keys for its uniform and non-uniform parameters
  • The parameters constr array, and indices constr array of the term being matched
  • The return type of the match access_key list -> access_key -> constr t
  • The relevance of the match
  • The term being matched constr