Type of an environment, used in scoping to associate names to corresponding Bindlib variables and types. Note that it cannot be implemented by a map as the order is important. The structure is similar to Term.ctxt, a tuple (x,a,t) is a variable x, its type a and possibly its definition t. The typing environment x1:A1,..,xn:An is represented by the list xn:An;..;x1:A1 in reverse order (last added variable comes first).

empty is the empty environment.

add v a t env extends the environment env by mapping the string Bindlib.name_of v to (v,a,t).

find n env returns the Bindlib variable associated to the variable name n in the environment env. If none is found, Not_found is raised.

mem n env returns true iff n is mapped to a variable in env.

to_prod env t builds a sequence of products/lets whose domains are the variables of the environment env (from left to right), and whose body is the term t. By calling to_prod [(xn,an,None);⋯;(x1,a1,None)] t you obtain a term of the form Πx1:a1,..,Πxn:an,t.

to_prod is an “unboxed” version of to_prod_box.

to_abst env t builds a sequence of abstractions or let bindings, depending on the definition of the elements in the environment whose domains are the variables of the environment env (from left to right), and which body is the term t: to_abst [(xn,an,None);..;(x1,a1,None)] t = λx1:a1,..,λxn:an,t.

vars env extracts the array of the Bindlib variables in env. Note that the order is reversed: vars [(xn,an);..;(x1,a1)] = [|x1;..;xn|].

appl t env applies t to the variables of env.

to_tbox env extracts the array of the variables in env and injects them in tbox. This is the same as Array.map _Vari (vars env). Note that the order is reversed: to_tbox [(xn,an);..;(x1,a1)] = [|x1;..;xn|].

to_ctxt e converts an environment into a context.

match_prod c t f returns f a b if t matches Prod(a,b) possibly after reduction.

• raises [Invalid_argument]

  if t is not a product.

of_prod c s t returns a tuple (env,b) where b is constructed from the term t by unbinding as much dependent products as possible in the head of t. The free variables created by this process, prefixed by s, are given (with their types) in the environment env (in reverse order). For instance, if t is of the form Πx1:a1, ⋯, Πxn:an, b, then the function returns b and the environment (xn,an); ⋯;(x1,a1).

of_prod_nth c n t returns a tuple (env,b) where b is constructed from the term t by unbinding n dependent products. The free variables created by this process are given (with their types) in the environment env (in reverse order). For instance, if t is of the form Πx1:a1, ⋯, Πxn:an, b then the function returns b and the environment (xn,an); ⋯;(x1,a1). n must be non-negative.

• raises [Invalid_argument]

  if t does not evaluate to a series of (at least) n products.

of_prod_using c xs t is similar to of_prod s c n t where n = Array.length xs except that it replaces unbound variables by those of xs.

• raises [Invalid_argument]

  if t does not evaluate to a series of (at least) n products.