lambdapi 2.5.1 · OCaml Package

Scoping environment for variables.

type env = (string * (Term.tvar * Term.tbox * Term.tbox option)) list

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).

type t = env

val empty : env

empty is the empty environment.

val add : Term.tvar -> Term.tbox -> Term.tbox option -> env -> env

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

val find : string -> env -> Term.tvar

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.

val mem : string -> env -> bool

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

val to_prod_box : env -> Term.tbox -> Term.tbox

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.

val to_prod : env -> Term.tbox -> Term.term

to_prod is an “unboxed” version of to_prod_box.

val to_abst : env -> Term.tbox -> Term.term

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.

val vars : env -> Term.tvar array

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|].

val appl : Term.tbox -> env -> Term.tbox

appl t env applies t to the variables of env.

val to_tbox : env -> Term.tbox array

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|].

val to_ctxt : env -> Term.ctxt

to_ctxt e converts an environment into a context.

val match_prod : 
  Term.ctxt ->
  Term.term ->
  (Term.term -> Term.tbinder -> 'a) ->
  'a

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.

val of_prod : Term.ctxt -> string -> Term.term -> env * Term.term

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).

val of_prod_nth : Term.ctxt -> int -> Term.term -> env * Term.term

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.

val of_prod_using : 
  Term.ctxt ->
  Term.tvar array ->
  Term.term ->
  env * Term.term

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.

package lambdapi