Type of an environment, used in scoping to associate names to corresponding 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).

pp ppf env prints the environment env on the formatter ppf (for debug).

empty is the empty environment.

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

find n env returns the 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_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 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_terms env extracts the array of the variables in env and injects them in tbox. This is the same as Array.map mk_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 None b if t matches Prod(a,b), and f a d b if t matches LLet(a,d,b), possibly after reduction.

• raises [Invalid_argument]

  if the whnf of 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.

names env returns the set of names in env.

gen_valid_idopts env ids generates a list of pairwise distinct identifiers distinct from those of env to replace ids.