<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Bindlib (bindlib.Bindlib)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">bindlib</a> &#x00BB; Bindlib</nav><header class="odoc-preamble"><h1>Module <code><span>Bindlib</span></code></h1><p>The <code>Bindlib</code> library provides support for free and bound variables in the OCaml language. The main application is the representation of types with a binding structure (e.g., abstract syntax trees).</p><ul class="at-tags"><li class="author"><span class="at-tag">author</span> Christophe Raffalli</li></ul><ul class="at-tags"><li class="author"><span class="at-tag">author</span> Rodolphe Lepigre</li></ul><ul class="at-tags"><li class="version"><span class="at-tag">version</span> 6.0.0</li></ul></header><nav class="odoc-toc"><ul><li><a href="#variables,-binders-and-substitution">Variables, binders and substitution</a></li><li><a href="#constructing-terms-and-binders-in-the-binding-box">Constructing terms and binders in the binding box</a></li><li><a href="#working-in-a-context-and-variable-printing">Working in a context and variable printing</a></li><li><a href="#more-binding-box-manipulation-functions">More binding box manipulation functions</a></li><li><a href="#attributes-of-variables-and-utilities">Attributes of variables and utilities</a></li><li><a href="#attributes-of-binders-and-utilities">Attributes of binders and utilities</a></li><li><a href="#attributes-of-binding-boxes-and-utilities">Attributes of binding boxes and utilities</a></li><li><a href="#custom-context-and-variable-renaming">Custom context and variable renaming</a></li><li><a href="#unsafe,-advanced-features">Unsafe, advanced features</a></li></ul></nav><div class="odoc-content"><h3 id="variables,-binders-and-substitution"><a href="#variables,-binders-and-substitution" class="anchor"></a>Variables, binders and substitution</h3><p>The <code>Bindlib</code> library provides two type constructors for building abstract syntax trees: type <code>'a var</code> representing a free variable of type <code>'a</code>, and type <code>('a,'b) binder</code> representing a binding of a variable of type <code>'a</code> in a value of type <code>'b</code>. Intuitively, type <code>('a,'b) binder</code> can be thought of as <code>'a -&gt; 'b</code>. Types <code>'a mvar</code> and <code>('a,'b) mbinder</code> are also provided for handling arrays of variables more efficiently.</p><div class="odoc-spec"><div class="spec type" id="type-var" class="anchored"><a href="#type-var" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a var</span></span></code></div><div class="spec-doc"><p>Type of a free variable of type <code>'a</code>.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-mvar" class="anchored"><a href="#type-mvar" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a mvar</span></span><span> = <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> array</span></span></code></div><div class="spec-doc"><p>Type of an array of variables of type <code>'a</code>.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-binder" class="anchored"><a href="#type-binder" class="anchor"></a><code><span><span class="keyword">type</span> <span>('a, 'b) binder</span></span></code></div><div class="spec-doc"><p>Type of a binder for a variable of type <code>'a</code> into an element of type <code>'b</code>. In terms of higher order abstract syntax, it can be seen as <code>'a -&gt; 'b</code>.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-mbinder" class="anchored"><a href="#type-mbinder" class="anchor"></a><code><span><span class="keyword">type</span> <span>('a, 'b) mbinder</span></span></code></div><div class="spec-doc"><p>Type of a binder for an array of variables of type <code>'a</code> into an element of type <code>'b</code>. This representation is more efficient than a nesting of binders of type <code>('a,'b) binder</code>, but substitution can only be performed the whole array of variables at once.</p></div></div><p>As an example, a type representing the terms of the pure λ-calculus can be defined as follows using types <code>'a var</code> and <code>('a,'b) binder</code>.</p><pre><code>type term =
  | Var of term var
  | Abs of (term, term) binder
  | App of term * term </code></pre><div class="odoc-spec"><div class="spec value" id="val-subst" class="anchored"><a href="#val-subst" class="anchor"></a><code><span><span class="keyword">val</span> subst : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span></span></code></div><div class="spec-doc"><p><code>subst b v</code> substitutes the variable bound by <code>b</code> with the value <code>v</code>. This operation is very efficient.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-msubst" class="anchored"><a href="#val-msubst" class="anchor"></a><code><span><span class="keyword">val</span> msubst : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> array</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span></span></code></div><div class="spec-doc"><p><code>msubst b vs</code> substitutes the variables bound by <code>b</code> with the values <code>vs</code>. This operation is very efficient. Note however that the length of the <code>vs</code> array should match the arity of <code>b</code> (as given by <code>mbinder_arity b</code>). If it is not the case, the exception <code>Invalid_argument &quot;Bad arity in msubst&quot;</code> is raised.</p></div></div><p>Coming back to our pure λ-calculus example, call-by-name evaluation can be defined as a simple recursive function using <code>subst</code>.</p><pre><code>let rec eval : term -&gt; term = fun t -&gt;
  match t with
  | App(f,a) -&gt;
      begin
        match eval f with
        | Abs(b) -&gt; eval (subst b a)
        | _      -&gt; t
      end
  | _        -&gt; t </code></pre><div class="odoc-spec"><div class="spec value" id="val-new_var" class="anchored"><a href="#val-new_var" class="anchor"></a><code><span><span class="keyword">val</span> new_var : <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span></span></code></div><div class="spec-doc"><p><code>new_var mkfree name</code> creates a new variable using a function <code>mkfree</code> and a <code>name</code>. The <code>mkfree</code> function is used to inject variables in the type of the corresponding objects: it is a form of syntactic wrapper that is often defined to be a constructor (see the example below).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-new_mvar" class="anchored"><a href="#val-new_mvar" class="anchor"></a><code><span><span class="keyword">val</span> new_mvar : <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span>string array</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span></span></code></div><div class="spec-doc"><p><code>new_mvar mkfree names</code> creates an array of new variables using a function <code>mkfree</code> (see <code>new_var</code>) and an array of variable <code>names</code>.</p></div></div><p>For our pure λ-calculus example, where variables have type <code>term var</code>, the <code>mkfree</code> function would simply be defined as follows.</p><pre><code>let mkfree : term var -&gt; term = fun x -&gt; Var(x) </code></pre><div class="odoc-spec"><div class="spec value" id="val-name_of" class="anchored"><a href="#val-name_of" class="anchor"></a><code><span><span class="keyword">val</span> name_of : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>name_of x</code> returns the name corresponding to variable <code>x</code>. Note that this name is generally not safe for printing since names are not updated when a substitution is performed. For instance, variables may appear to have been captured in the text representation of a structure with variable bindings. To circumvent this issue, one must be particularly careful when converting binders into text, and rely on contexts (see type <code>ctxt</code> below).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-names_of" class="anchored"><a href="#val-names_of" class="anchor"></a><code><span><span class="keyword">val</span> names_of : <span><span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> <span class="arrow">&#45;&gt;</span></span> <span>string array</span></span></code></div><div class="spec-doc"><p><code>names_of xs</code> returns names corresponding to variables <code>xs</code>. As when using <code>name_of</code>, care should be taken when converting objects with bindings into a text representation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind" class="anchored"><a href="#val-unbind" class="anchor"></a><code><span><span class="keyword">val</span> unbind : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span> * <span class="type-var">'b</span></span></code></div><div class="spec-doc"><p><code>unbind b</code> substitutes the binder <code>b</code> using a fresh variable. The variable and the result of the substitution are returned. Note that the name of the fresh variable is based on that of the binder, but it is not guaranteed to be safe for printing (see <code>new_var</code> and <code>unbind_in</code>). However, there is no problem for other operations such as re-establishing the binding. When the fresh variable is created, the <code>mkfree</code> function that is used is that that was specified when creating the variable that was originally bound by <code>b</code>, at the time of its creation (see <code>new_var</code> and <code>bind_var</code>).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind2" class="anchored"><a href="#val-unbind2" class="anchor"></a><code><span><span class="keyword">val</span> unbind2 : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span></span></code></div><div class="spec-doc"><p><code>unbind2 f g</code> is similar to <code>unbind f</code>, but it substitutes two binders <code>f</code> and <code>g</code> at once using the same fresh variable. The name of the variable is based on that of the binder <code>f</code>. Similarly, the <code>mkfree</code> syntactic wrapper that is used for the fresh variable is the one that was given for creating the variable that was bound to construct <code>f</code> (see <code>bind_var</code> and <code>new_var</code> for details on this process). In particular, the use of <code>unbind2</code> may lead to unexpected results if the binders <code>f</code> and <code>g</code> were not built using free variables created with the same <code>mkfree</code>. Moreover, as with <code>unbind</code>, the name of the fresh variable is not guaranteed to be safe for printing.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-eq_binder" class="anchored"><a href="#val-eq_binder" class="anchor"></a><code><span><span class="keyword">val</span> eq_binder : 
  <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> bool )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  bool</span></code></div><div class="spec-doc"><p><code>eq_binder eq f g</code> tests the equality between <code>f</code> and <code>g</code>. The binders are first substituted with the same fresh variable (using <code>unbind2</code>), and <code>eq</code> is called on the resulting values. Note that <code>eq_binder</code> may not have the expected result if <code>f</code> and <code>g</code> were not built by binding variables with an identical <code>mkfree</code> syntactic wrapper.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind" class="anchored"><a href="#val-unmbind" class="anchor"></a><code><span><span class="keyword">val</span> unmbind : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> * <span class="type-var">'b</span></span></code></div><div class="spec-doc"><p><code>unmbind b</code> substitutes the multiple binder <code>b</code> with fresh variables. This function is analogous to <code>unbind</code> for binders. Note that the names used to create the fresh variables are based on those of the multiple binder. The syntactic wrapper (of <code>mkfree</code>) that is used to build the variables is the one that was given when creating the multiple variables that were bound in <code>b</code> (see <code>new_mvar</code> and <code>bind_mvar</code>). Moreover, note that as for <code>unbind</code>, the names of the fresh variables may not be safe for printing.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind2" class="anchored"><a href="#val-unmbind2" class="anchor"></a><code><span><span class="keyword">val</span> unmbind2 : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span></span></code></div><div class="spec-doc"><p><code>unmbind2 f g</code> is similar to <code>unmbind f</code>, but it substitutes two multiple binder <code>f</code> and <code>g</code> at once, using the same fresh variables. Note that the two binders must have the same arity. This function may have an unexpected results in some cases, and the fresh variables may have names that are not safe for printing (see <code>unbind2</code>).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-eq_mbinder" class="anchored"><a href="#val-eq_mbinder" class="anchor"></a><code><span><span class="keyword">val</span> eq_mbinder : 
  <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> bool )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  bool</span></code></div><div class="spec-doc"><p><code>eq_mbinder eq f g</code> tests the equality of the two multiple binders <code>f</code> and <code>g</code>. They are substituted with the same fresh variables (using <code>unmbind2</code>) and <code>eq</code> is called on the resulting values. This function may not have the expected result in some cases, for reasons explained in the documentation of <code>eq_binder</code>. It is safe to use this function on multiple binders with a different arity (they are considered different).</p></div></div><p>The <code>unbind</code> function is often useful for term traversals. For instance, a function computing the size of a pure λ-term can be defined as follows.</p><pre><code>let rec size : term -&gt; int = fun t -&gt;
  match t with
  | Var(_)   -&gt; 0
  | Abs(b)   -&gt; let (_,t) = unbind b in
                1 + size t
  | App(t,u) -&gt; 1 + size t + size u </code></pre><p>Note however that it is not a good idea to define a term-printing function using a combination of <code>unbind</code> and <code>name_of</code>. Indeed, as explained in the documentation of <code>name_of</code>, contexts must be used to ensure that displayed variable names are correct.</p><h3 id="constructing-terms-and-binders-in-the-binding-box"><a href="#constructing-terms-and-binders-in-the-binding-box" class="anchor"></a>Constructing terms and binders in the binding box</h3><p>To obtain fast substitutions, a price must be paid at the construction of terms. Indeed, binders (i.e., element of type <code>('a,'b) binder</code>) cannot be defined directly. Instead, they are put together in the type <code>'a box</code>. It correspond to a term of type <code>'a</code> whose free variables may be bound.</p><div class="odoc-spec"><div class="spec type" id="type-box" class="anchored"><a href="#type-box" class="anchor"></a><code><span><span class="keyword">type</span> <span>+'a box</span></span></code></div><div class="spec-doc"><p>Type of a term of type <code>'a</code> under construction. Using this representation, the free variables of the term can be bound easily.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_var" class="anchored"><a href="#val-box_var" class="anchor"></a><code><span><span class="keyword">val</span> box_var : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_var x</code> injects variable <code>x</code> into the <code>'a box</code> type, so that it can be bound using <code>bind_var</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box" class="anchored"><a href="#val-box" class="anchor"></a><code><span><span class="keyword">val</span> box : <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box e</code> injects the value <code>e</code> into the <code>'a box</code> type, assuming that it is closed. Thus, if <code>e</code> contains variables, then they will not be considered free. This means that no variable of <code>e</code> will be available for binding.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-apply_box" class="anchored"><a href="#val-apply_box" class="anchor"></a><code><span><span class="keyword">val</span> apply_box : <span><span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span> )</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>apply_box bf ba</code> applies the boxed function <code>bf</code> to a boxed argument <code>ba</code> inside the <code>box</code> type. This function is used to build new expressions by applying a function with free variables to an argument with free variables (the <code>'a box</code> type is an applicative functor whose application operator is <code>apply_box</code>, and whose unit is <code>box</code>).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_apply" class="anchored"><a href="#val-box_apply" class="anchor"></a><code><span><span class="keyword">val</span> box_apply : <span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_apply f ba</code> applies the function <code>f</code> to a boxed argument <code>ba</code>. It is equivalent to <code>apply_box (box f) ba</code>, but is more efficient.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_apply2" class="anchored"><a href="#val-box_apply2" class="anchor"></a><code><span><span class="keyword">val</span> box_apply2 : <span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'c</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'c</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_apply2 f ba bb</code> applies the function <code>f</code> to two boxed arguments: <code>ba</code> and <code>bb</code>. It is equivalent to <code>apply_box (apply_box (box f) ba) bb</code> but it is more efficient.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-bind_var" class="anchored"><a href="#val-bind_var" class="anchor"></a><code><span><span class="keyword">val</span> bind_var : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>bind_var x b</code> binds the variable <code>x</code> in <code>b</code>, producing a boxed binder.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-bind_mvar" class="anchored"><a href="#val-bind_mvar" class="anchor"></a><code><span><span class="keyword">val</span> bind_mvar : <span><span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>bind_mvar xs b</code> binds the variables of <code>xs</code> in <code>b</code> to get a boxed binder. It is the equivalent of <code>bind_var</code> to build a multiple binder.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_binder" class="anchored"><a href="#val-box_binder" class="anchor"></a><code><span><span class="keyword">val</span> box_binder : <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_binder f b</code> boxes the binder <code>b</code> using the boxing function <code>f</code>. Note that when <code>b</code> is closed, it is immediately boxed using the <code>box</code> function. In that case, the function <code>f</code> is not used at all.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_mbinder" class="anchored"><a href="#val-box_mbinder" class="anchor"></a><code><span><span class="keyword">val</span> box_mbinder : 
  <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_mbinder f b</code> boxes the multiple binder <code>b</code> using the boxing function <code>f</code>. Note that if <code>b</code> is closed then it is immediately boxed (with <code>box</code>), without relying on <code>f</code> at all.</p></div></div><p>As mentioned earlier, terms with bound variables can only be built in the <code>'a box</code> type. To ease the construction of terms, it is a good practice to implement “smart constructors” at the <code>'a box</code> level. Coming back to our λ-calculus example, we can give the following smart constructors.</p><pre><code>let var : term var -&gt; term box =
  fun x -&gt; box_var x

let abs_raw : (term, term) binder box -&gt; term box =
  fun b -&gt; box_apply (fun b -&gt; Abs(b)) b

let abs : term var -&gt; term box -&gt; term box =
  fun x t -&gt; abs_raw (bind_var x t)

let app : term box -&gt; term box -&gt; term box =
  fun t u -&gt; box_apply2 (fun t u -&gt; App(t,u)) t u </code></pre><p>Additionally, it is a good idea to define a “boxing function”: a function used to turn terms into a boxed terms. It is sometimes necessary to do so, as we will see when we define a printing function.</p><pre><code>let rec box_term : term -&gt; term box = fun t -&gt;
  match t with
  | Var(x)   -&gt; var x
  | Abs(b)   -&gt; abs_raw (box_binder box_term b)
  | App(t,u) -&gt; app (box_term t) (box_term u) </code></pre><div class="odoc-spec"><div class="spec value" id="val-unbox" class="anchored"><a href="#val-unbox" class="anchor"></a><code><span><span class="keyword">val</span> unbox : <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>unbox e</code> can be called when the construction of a term is finished (i.e., when the desired variable bindings have been created).</p></div></div><p>We can then easily define terms of the λ-calculus as follows.</p><pre><code>(* λx.x *)
let id : term =
  let x = new_var &quot;x&quot; mkfree in
  unbox (abs x (var x))

(* λx.λy.x *)
let fst   : term =
  let x = new_var &quot;x&quot; mkfree in
  let y = new_var &quot;y&quot; mkfree in
  unbox (abs x (abs y (var x)))

(* λx.(x) x) (boxed) *)
let delta : term box =
  let x = new_var &quot;x&quot; mkfree in
  abs x (app (var x) (var x))

(* (λx.(x) x) λx.(x) x *)
let omega : term =
  unbox (app delta delta)

(* λx.(x) x) *)
let delta : term =
  unbox delta </code></pre><h3 id="working-in-a-context-and-variable-printing"><a href="#working-in-a-context-and-variable-printing" class="anchor"></a>Working in a context and variable printing</h3><p>For variable substitution to be as fast as possible, the <code>Bindlib</code> library does not do any work to maintain variable names at substitution time. This work is instead delayed until it becomes necessary: at the time of turning objects with binders into a textual representation (e.g., for printing the result of a computation). Such operations must hence maintain a context of variable names using the functions of this section.</p><div class="odoc-spec"><div class="spec type" id="type-ctxt" class="anchored"><a href="#type-ctxt" class="anchor"></a><code><span><span class="keyword">type</span> ctxt</span></code></div><div class="spec-doc"><p>Type of a context.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-empty_ctxt" class="anchored"><a href="#val-empty_ctxt" class="anchor"></a><code><span><span class="keyword">val</span> empty_ctxt : <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>empty_ctxt</code> denotes the empty context.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-free_vars" class="anchored"><a href="#val-free_vars" class="anchor"></a><code><span><span class="keyword">val</span> free_vars : <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>free_vars b</code> returns a context containing the free variables of <code>b</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-reserve_name" class="anchored"><a href="#val-reserve_name" class="anchor"></a><code><span><span class="keyword">val</span> reserve_name : <span>string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>reserve_name name ctxt</code> extends context <code>ctxt</code> by reserving variable name <code>name</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-new_var_in" class="anchored"><a href="#val-new_var_in" class="anchor"></a><code><span><span class="keyword">val</span> new_var_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>new_var_in ctxt mkfree name</code> is similar to <code>new_var mkfree name</code>, but the name actually used for the newly created variable is chosen to not collide with the variables of context <code>ctxt</code>. Said otherwise, argument <code>name</code> only gives a preferred name: if it is not available then a fresh name is picked by appending a decimal number at the end of <code>name</code>. Moreover, the obtained variable has a name that is safe for printing (see <code>name_of</code>), at least as long as binders are not substituted in objects containing it. Finally, the context that is returned is extended to contain the new variable name.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-new_mvar_in" class="anchored"><a href="#val-new_mvar_in" class="anchor"></a><code><span><span class="keyword">val</span> new_mvar_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span>string array</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>new_mvar_in ctxt mkfree names</code> is similar to <code>new_mvar mkfree names</code>, but it handles renaming based on context <code>ctxt</code> (see <code>new_var_in</code>).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind_in" class="anchored"><a href="#val-unbind_in" class="anchor"></a><code><span><span class="keyword">val</span> unbind_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span> * <span class="type-var">'b</span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>unbind_in ctxt b</code> is similar to <code>unbind b</code>, but it handles the context as explained in the documentation of <code>new_mvar_in</code>. This function can be used for maintaining correct names in printing functions: it is safe to use the <code>name_of</code> function on the returned variable (as long as no substitution is performed in the involved objects, see <code>new_var_in</code>).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind2_in" class="anchored"><a href="#val-unbind2_in" class="anchor"></a><code><span><span class="keyword">val</span> unbind2_in : 
  <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'a</span> <a href="#type-var">var</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>unbind2_in ctxt f g</code> is similar to <code>unbind2 f g</code>, but handles the context as explained in the documentation of <code>new_mvar_in</code> and <code>unbind_in</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind_in" class="anchored"><a href="#val-unmbind_in" class="anchor"></a><code><span><span class="keyword">val</span> unmbind_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> * <span class="type-var">'b</span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>unmbind_in ctxt b</code> is similar to <code>unmbind b</code>, but it handles the context as is explained in the documentation of <code>new_mvar_in</code>. As <code>unbind_in</code>, the <code>unmbind_in</code> function can be used to implement printing functions.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind2_in" class="anchored"><a href="#val-unmbind2_in" class="anchor"></a><code><span><span class="keyword">val</span> unmbind2_in : 
  <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span> * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>unmbind2_in ctxt f g</code> is similar to <code>unmbind2 f g</code>, but it uses a context similrly to <code>new_mvar_in</code> or <code>unmbind_in</code>.</p></div></div><p>Going back to our λ-calculus example, the <code>unbind_in</code> function can be used to implement the following function transforming a λ-term into a <code>string</code>. Here, thanks to the use of <code>unbind_in</code>, it is safe to rely on <code>name_of</code> to print variables.</p><pre><code>let to_string : ctxt -&gt; term -&gt; string = fun ctxt t -&gt;
  match t with
  | Var(x)   -&gt; name_of x
  | Abs(b)   -&gt; let (x,t,ctxt) = unbind_in ctxt b in
                &quot;λ&quot; ^ name_of x ^ &quot;.&quot; ^ to_string ctxt t
  | App(t,u) -&gt; &quot;(&quot; ^ to_string ctxt t ^ &quot;) &quot; ^ to_string ctxt u </code></pre><p>The above <code>to_string</code> must not only receive the term to display (i.e., the second argument), but also a context containing all free variables in the term. To avoid maintain such a context we can rely on function <code>free_vars</code> together with the term boxing function <code>box_term</code> defined earlier.</p><pre><code>let to_string : term -&gt; term = fun t -&gt;
  to_string (free_vars (box_term t)) t </code></pre><h3 id="more-binding-box-manipulation-functions"><a href="#more-binding-box-manipulation-functions" class="anchor"></a>More binding box manipulation functions</h3><p>In general, it is not difficult to use the <code>box</code> and <code>apply_box</code> functions to manipulate any kind of data in the <code>'a box</code> type. However, working with these functions alone can be tedious. The following functions can be used to manipulate standard data types in an optimised way.</p><div class="odoc-spec"><div class="spec value" id="val-box_opt" class="anchored"><a href="#val-box_opt" class="anchor"></a><code><span><span class="keyword">val</span> box_opt : <span><span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> option</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> option</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_opt bo</code> shifts the <code>option</code> type of <code>bo</code> into the <code>box</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_list" class="anchored"><a href="#val-box_list" class="anchor"></a><code><span><span class="keyword">val</span> box_list : <span><span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> list</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_list bs</code> shifts the <code>list</code> type of <code>bs</code> into the <code>box</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_rev_list" class="anchored"><a href="#val-box_rev_list" class="anchor"></a><code><span><span class="keyword">val</span> box_rev_list : <span><span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> list</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> list</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_rev_list bs</code> is similar to <code>box_list bs</code>, but the produced boxed list is reversed (it is hence more efficient).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_array" class="anchored"><a href="#val-box_array" class="anchor"></a><code><span><span class="keyword">val</span> box_array : <span><span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> array</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> array</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_array bs</code> shifts the <code>array</code> type of <code>bs</code> into the <code>box</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_apply3" class="anchored"><a href="#val-box_apply3" class="anchor"></a><code><span><span class="keyword">val</span> box_apply3 : 
  <span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'c</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'d</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'c</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'d</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_apply3</code> is similar to <code>box_apply2</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_apply4" class="anchored"><a href="#val-box_apply4" class="anchor"></a><code><span><span class="keyword">val</span> box_apply4 : 
  <span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'c</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'d</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'e</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'c</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span class="type-var">'d</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'e</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_apply4</code> is similar to <code>box_apply2</code> and <code>box_apply3</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_pair" class="anchored"><a href="#val-box_pair" class="anchor"></a><code><span><span class="keyword">val</span> box_pair : <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span>(<span class="type-var">'a</span> * <span class="type-var">'b</span>)</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_pair ba bb</code> is the same as <code>box_apply2 (fun a b -&gt; (a,b)) ba bb</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-box_triple" class="anchored"><a href="#val-box_triple" class="anchor"></a><code><span><span class="keyword">val</span> box_triple : <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'c</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span>(<span class="type-var">'a</span> * <span class="type-var">'b</span> * <span class="type-var">'c</span>)</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>box_triple</code> is similar to <code>box_pair</code>, but for triples.</p></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-Map" class="anchored"><a href="#module-type-Map" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-Map/index.html">Map</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Type of a module equipped with a <code>map</code> function.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Lift" class="anchored"><a href="#module-Lift" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Lift/index.html">Lift</a></span><span> (<a href="Lift/argument-1-M/index.html">M</a> : <a href="module-type-Map/index.html">Map</a>) : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Functorial interface used to build lifting functions for any type equipped with a <code>map</code> function. In other words, this function can be used to allow the permutation of the <code>'a box</code> type with another type constructor.</p></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-Map2" class="anchored"><a href="#module-type-Map2" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-Map2/index.html">Map2</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Type of a module equipped with a &quot;binary&quot; <code>map</code> function.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Lift2" class="anchored"><a href="#module-Lift2" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Lift2/index.html">Lift2</a></span><span> (<a href="Lift2/argument-1-M/index.html">M</a> : <a href="module-type-Map2/index.html">Map2</a>) : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Similar to the <code>Lift</code> functor, but handles &quot;binary&quot; <code>map</code> functions.</p></div></div><h3 id="attributes-of-variables-and-utilities"><a href="#attributes-of-variables-and-utilities" class="anchor"></a>Attributes of variables and utilities</h3><div class="odoc-spec"><div class="spec value" id="val-hash_var" class="anchored"><a href="#val-hash_var" class="anchor"></a><code><span><span class="keyword">val</span> hash_var : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>hash_var x</code> computes a hash for variable <code>x</code>. Note that this function can be used with the <code>Hashtbl</code> module.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-compare_vars" class="anchored"><a href="#val-compare_vars" class="anchor"></a><code><span><span class="keyword">val</span> compare_vars : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>compare_vars x y</code> safely compares <code>x</code> and <code>y</code>. Note that it is unsafe to compare variables using <code>Stdlib.compare</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-eq_vars" class="anchored"><a href="#val-eq_vars" class="anchor"></a><code><span><span class="keyword">val</span> eq_vars : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>eq_vars x y</code> safely computes the equality of <code>x</code> and <code>y</code>. Note that it is unsafe to compare variables with <code>Stdlib.(=)</code>.</p></div></div><h3 id="attributes-of-binders-and-utilities"><a href="#attributes-of-binders-and-utilities" class="anchor"></a>Attributes of binders and utilities</h3><div class="odoc-spec"><div class="spec value" id="val-binder_name" class="anchored"><a href="#val-binder_name" class="anchor"></a><code><span><span class="keyword">val</span> binder_name : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>binder_name b</code> returns the name of the variable bound by binder <code>b</code>. This name is generally not safe for printing, since it is not updated after the binder is created, even when a substitution is performed (see <code>unbind_in</code> and <code>name_of</code> to learn how to print terms with binders).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-binder_occur" class="anchored"><a href="#val-binder_occur" class="anchor"></a><code><span><span class="keyword">val</span> binder_occur : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>binder_occur b</code> returns a boolean indicating if the variable bound by <code>b</code> occurs (i.e., is used). This is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-binder_constant" class="anchored"><a href="#val-binder_constant" class="anchor"></a><code><span><span class="keyword">val</span> binder_constant : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>binder_constant b</code> is the same as <code>not (binder_occur b)</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-binder_closed" class="anchored"><a href="#val-binder_closed" class="anchor"></a><code><span><span class="keyword">val</span> binder_closed : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>binder_closed b</code> indicates whether the <code>b</code> is closed (i.e., does not have any free variables). This is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-binder_rank" class="anchored"><a href="#val-binder_rank" class="anchor"></a><code><span><span class="keyword">val</span> binder_rank : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>binder_rank b</code> gives the number of free variables contained in <code>b</code>. This is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_arity" class="anchored"><a href="#val-mbinder_arity" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_arity : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>mbinder_arity b</code> gives the arity of <code>b</code> (i.e., the number of variables it is binding). This is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_names" class="anchored"><a href="#val-mbinder_names" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_names : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span>string array</span></span></code></div><div class="spec-doc"><p><code>mbinder_names b</code> returns the names of the variables bound by the multiple binder <code>b</code> as an array. Similarly the result of <code>binder_name</code>, these names are not generally safe for printing.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_occurs" class="anchored"><a href="#val-mbinder_occurs" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_occurs : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span>bool array</span></span></code></div><div class="spec-doc"><p><code>mbinder_occurs b</code> returns an array of booleans indicating whether each of the variables that are bound occur (i.e., are used). It is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_constant" class="anchored"><a href="#val-mbinder_constant" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_constant : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>mbinder_constant b</code> indicates whether the <code>mbinder</code> <code>b</code> is constant. This means that none of its variables are used.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_closed" class="anchored"><a href="#val-mbinder_closed" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_closed : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>mbinder_closed b</code> indicates whether the multiple binder <code>b</code> is closed. It is a constant time operation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_rank" class="anchored"><a href="#val-mbinder_rank" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_rank : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>mbinder_rank b</code> gives the number of free variables contained in <code>b</code>. This is a constant time operation.</p></div></div><h3 id="attributes-of-binding-boxes-and-utilities"><a href="#attributes-of-binding-boxes-and-utilities" class="anchor"></a>Attributes of binding boxes and utilities</h3><div class="odoc-spec"><div class="spec value" id="val-is_closed" class="anchored"><a href="#val-is_closed" class="anchor"></a><code><span><span class="keyword">val</span> is_closed : <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>is_closed b</code> checks whether <code>b</code> is closed (in constant time).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-occur" class="anchored"><a href="#val-occur" class="anchor"></a><code><span><span class="keyword">val</span> occur : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'b</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p><code>occur x b</code> indicates whether variable <code>x</code> occurs in <code>b</code>. This is done in linear time with respect to the number of free variables in <code>b</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-bind_apply" class="anchored"><a href="#val-bind_apply" class="anchor"></a><code><span><span class="keyword">val</span> bind_apply : <span><span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>bind_apply bb barg</code> is the same as <code>box_apply2 subst bb barg</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbind_apply" class="anchored"><a href="#val-mbind_apply" class="anchor"></a><code><span><span class="keyword">val</span> mbind_apply : <span><span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span><span><span class="type-var">'a</span> array</span> <a href="#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>mbind_apply bb bargs</code> is the same as <code>box_apply2 msubst bb bargs</code>.</p></div></div><h3 id="custom-context-and-variable-renaming"><a href="#custom-context-and-variable-renaming" class="anchor"></a>Custom context and variable renaming</h3><p>The variable renaming performed by functions like <code>new_var_in</code> is somewhat arbitrary, and may not fit every application. As a consequence, we provide a functor <code>Ctxt</code> that can be used to define a new renaming policy based on a custom notion of context and several configuration options.</p><div class="odoc-spec"><div class="spec module-type" id="module-type-Renaming" class="anchored"><a href="#module-type-Renaming" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-Renaming/index.html">Renaming</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Module type giving the specification of a renaming policy, to be used with the <code>Ctxt</code> functor.</p></div></div><p>The renaming policy used by the default context-manipulating function like <code>new_var_in</code> or <code>unbind_in</code> uses the following configuration: the value of <code>reset_context_for_closed_terms = false</code>, <code>skip_constant_binders = false</code>, and <code>constant_binder_name = None</code>.</p><p>The default <code>new_name</code> function is not exposed in the interface. It splits the <code>name</code> into a pair <code>(prefix,n)</code> containing the largest <code>n</code> and longest <code>prefix</code> such that <code>name = prefix ^ string_of_int n</code>. For instance, if we have <code>name = &quot;xy023&quot;</code> then <code>(prefix,n) = (&quot;xy0&quot;,23)</code>. In the case where no <code>n</code> exists, we take <code>(prefix,n) = (name,0)</code>. The prefix is preserved, and only the value of <code>n</code> is changed for renaming.</p><div class="odoc-spec"><div class="spec module" id="module-Ctxt" class="anchored"><a href="#module-Ctxt" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Ctxt/index.html">Ctxt</a></span><span> (<a href="Ctxt/argument-1-R/index.html">R</a> : <a href="module-type-Renaming/index.html">Renaming</a>) : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>A functor that can be used to obtain context-manipulating functions, given the specification of a renaming policy. The defined <code>ctxt</code> type as well as the obtained functions can then be used as a drop-in replacement for their default counterparts (found at the top level of the <code>Bindlib</code> module).</p></div></div><h3 id="unsafe,-advanced-features"><a href="#unsafe,-advanced-features" class="anchor"></a>Unsafe, advanced features</h3><div class="odoc-spec"><div class="spec value" id="val-uid_of" class="anchored"><a href="#val-uid_of" class="anchor"></a><code><span><span class="keyword">val</span> uid_of : <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p><code>uid_of x</code> returns the unique identifier of the given variable.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-uids_of" class="anchored"><a href="#val-uids_of" class="anchor"></a><code><span><span class="keyword">val</span> uids_of : <span><span><span class="type-var">'a</span> <a href="#type-mvar">mvar</a></span> <span class="arrow">&#45;&gt;</span></span> <span>int array</span></span></code></div><div class="spec-doc"><p><code>uids_of xs</code> returns the unique identifiers of the variables of <code>xs</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-copy_var" class="anchored"><a href="#val-copy_var" class="anchor"></a><code><span><span class="keyword">val</span> copy_var : <span><span><span class="type-var">'b</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="#type-var">var</a></span></span></code></div><div class="spec-doc"><p><code>copy_var x mkfree name</code> makes a copy of variable <code>x</code>, with a potentially different name and <code>mkfree</code> function. However, the copy is treated exactly as the original in terms of binding and substitution. The main application of this function is for translating abstract syntax trees while preserving binders. In particular, variables at two different types should never live together (this may produce segmentation faults).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-reset_counter" class="anchored"><a href="#val-reset_counter" class="anchor"></a><code><span><span class="keyword">val</span> reset_counter : <span>unit <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>reset_counter ()</code> resets the unique identifier counter on which <code>Bindlib</code> relies. This function should only be called when previously generated data (e.g., variables) cannot be accessed anymore.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-dummy_box" class="anchored"><a href="#val-dummy_box" class="anchor"></a><code><span><span class="keyword">val</span> dummy_box : <span><span class="type-var">'a</span> <a href="#type-box">box</a></span></span></code></div><div class="spec-doc"><p><code>dummy_box</code> can be used for initialising structures like arrays. Note that if <code>unbox</code> is called on a data structure containing <code>dummy_box</code>, then the exception <code>Failure &quot;Invalid use of dummy_box&quot;</code> is raised.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-binder_compose" class="anchored"><a href="#val-binder_compose" class="anchor"></a><code><span><span class="keyword">val</span> binder_compose : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'c</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-binder">binder</a></span></span></code></div><div class="spec-doc"><p><code>binder_compose b f</code> postcomposes the binder <code>b</code> with the function <code>f</code>. In the process, the binding structure is not changed. Note that this function is not always safe. Use it with care.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mbinder_compose" class="anchored"><a href="#val-mbinder_compose" class="anchor"></a><code><span><span class="keyword">val</span> mbinder_compose : <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span class="type-var">'b</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'c</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="#type-mbinder">mbinder</a></span></span></code></div><div class="spec-doc"><p><code>mbinder_compose b f</code> postcomposes the multiple binder <code>b</code> with <code>f</code>. This function is similar to <code>binder_compose</code>, and it is not always safe.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-raw_binder" class="anchored"><a href="#val-raw_binder" class="anchor"></a><code><span><span class="keyword">val</span> raw_binder : 
  <span>string <span class="arrow">&#45;&gt;</span></span>
  <span>bool <span class="arrow">&#45;&gt;</span></span>
  <span>int <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-binder">binder</a></span></span></code></div><div class="spec-doc"><p><code>raw_binder name bind rank mkfree value</code> builds a binder using the <code>value</code> function as its definition. The parameter <code>name</code> correspond to a preferred name of the bound variable, the boolean <code>bind</code> indicates whether the bound variable occurs, and <code>rank</code> gives the number of distinct free variables in the produced binder. The <code>mkfree</code> function injecting variables in the type <code>'a</code> of the domain of the binder must also be given. This function must be considered unsafe because it is the responsibility of the user to give the accurate value for <code>bind</code> and <code>rank</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-raw_mbinder" class="anchored"><a href="#val-raw_mbinder" class="anchor"></a><code><span><span class="keyword">val</span> raw_mbinder : 
  <span><span>string array</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span>bool array</span> <span class="arrow">&#45;&gt;</span></span>
  <span>int <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span><span><span class="type-var">'a</span> <a href="#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span><span><span class="type-var">'a</span> array</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span> )</span> <span class="arrow">&#45;&gt;</span></span>
  <span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="#type-mbinder">mbinder</a></span></span></code></div><div class="spec-doc"><p><code>raw_mbinder names binds rank mk_free value</code> is similar to <code>raw_binder</code>, but it is applied to a multiple binder. As for <code>raw_binder</code>, this function has to be considered unsafe because the user must enforce invariants.</p></div></div></div></body></html>