Module InnerTerm.DB

module DB: sig .. end

type env = InnerTerm.t DBEnv.t

val closed : InnerTerm.t -> bool

check whether the term is closed (all DB vars are bound within the term). If this returns true then the term doesn't depend on its environment.

val contains : InnerTerm.t -> int -> bool

Does t contains the De Bruijn variable of index n?

val shift : int -> InnerTerm.t -> InnerTerm.t

shift the non-captured De Bruijn indexes in the term by n

val unshift : int -> InnerTerm.t -> InnerTerm.t

unshift n t unshifts the term t's bound variables by n. In other words it decrements indices of all free De Bruijn variables inside by n. Variables bound within t are left untouched.

val replace : InnerTerm.t -> sub:InnerTerm.t -> InnerTerm.t

db_from_term t ~sub replaces sub by a fresh De Bruijn index in t.

val from_var : InnerTerm.t -> var:InnerTerm.t -> InnerTerm.t

db_from_var t ~var replace var by a De Bruijn symbol in t. Same as InnerTerm.DB.replace.

val eval : env -> InnerTerm.t -> InnerTerm.t

Evaluate the term in the given De Bruijn environment, by replacing De Bruijn indices by their value in the environment.

val apply_subst : InnerTerm.t InnerTerm.VarMap.t -> InnerTerm.t -> InnerTerm.t

Apply the given simple substitution to variables in t; if some variable v is bound to t', then t' can be open and will be shifted as required. Traverses the whole term.