package lambdapi

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 then one of Term.ctxt, a tuple (x,a,t) is a variable x, its type a and possibly its definition t

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 / let-bindings 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 not defined 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 not defined variables in env and injects them in the tbox type. 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.

fresh_meta_type p env creates a fresh metavariable of type Type in environment env, and adds it to the metas of p.

fresh_meta_tbox p env creates a _Meta tbox from a fresh metavariable whose type is itself a fresh metavariable of type fresh_meta_type env, and add them to the metas of p.

fresh_meta_term p env creates a Meta term from a fresh metavariable whose type is a fresh metavariable of type to_prod env Type, and adds it to the metas of p.

app_fresh_metas p t n env returns the application of t to n fresh meta terms, and adds them to p.