Module LibBinding

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:

type access_key

Type of access keys for the State API

module State : sig ... end
Fold Functions for State
val 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.

val 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.

val 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.

val 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
val naming_id : naming_scheme

Identity namming

val naming_hd : naming_scheme

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

val naming_hd_dep : bool -> naming_scheme

naming_dep if true, naming_id otherwise

val naming_hd_fresh : naming_scheme

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

val naming_hd_fresh_dep : bool -> naming_scheme

naming_hd_fresh if true, naming_id otherwise

Create a New Lambda, Product, or LetIn
type freshness =
| Fresh
| Old

Status of the variable to bind

type binder =
| Lambda
| Prod

Which binders to bind

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.

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

Create a new binder using a naming_scheme, for an optional body in the updated state.

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

Create Lambda, Product, or LetIn for Context
val add_context : freshness -> naming_scheme -> EConstr.rel_context -> (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 state * access_key list -> constr.

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

val closure_context_opt : binder -> freshness -> naming_scheme -> EConstr.rel_context -> (access_key list -> EConstr.constr option State.t) -> EConstr.constr option State.t

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

val add_context_sep : freshness -> naming_scheme -> EConstr.rel_context -> ((access_key list * access_key list * 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.

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.

val closure_context_sep_opt : binder -> freshness -> naming_scheme -> EConstr.rel_context -> ((access_key list * access_key list * access_key list) -> EConstr.constr option State.t) -> EConstr.constr option State.t

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

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.

val 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.

val make_cst : (Names.inductive * EConstr.EInstance.t) -> int -> access_key list -> access_key list -> EConstr.constr list -> State.state -> EConstr.constr

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

val make_fix : 'a list -> int -> (int -> 'a -> int) -> (int -> 'a -> Names.Name.t EConstr.binder_annot) -> (int -> 'a -> EConstr.types State.t) -> ((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 list 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