package bindlib

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Module type giving the specification of a renaming policy, to be used with the Ctxt functor.

type ctxt

Type representing a set of variable names.

val empty_ctxt : ctxt

empty_ctxt represents an empty context.

val reset_context_for_closed_terms : bool

reset_context_for_closed_terms indicates whether the context should be reset to the empty context when calling unbind_in or munbind_in on a closed binder (which cannot capture names). If set to true, printing a λ-term will produce “λx.λx.x” rather than “λx.λx0.x0”, or “λx.x (λx.x)” rather than “λx.x (λx0.x0)”.

val skip_constant_binders : bool

skip_constant_binders indicates whether binders that are constant must be skipped (i.e., not recorded in the context). This permits reusing the name in a lower binder like in “λx.λx.x”, but not in “λx.x (λx.x)”.

val constant_binder_name : string option

constant_binder_name optionally provides a representation for a binder that is constant, to highlight the absence of a name. When this value is defined to be Some(s), then s is used as name for all such binders. For example, if s is "_" then we would get “λ_.λx.x”. Note that if the value of constant_binder_name is not None, skip_constant_binder is ignored.

val new_name : string -> ctxt -> string * ctxt

new_name name ctxt creates a name that is fresh in context ctxt. The given name indicates a prefered name (or base for the name). Note that the returned context extends ctxt with the new name.

val reserve_name : string -> ctxt -> ctxt

reserve_name name ctxt extends context ctxt by reserving name as a free variable name.