lambdapi 2.5.1 · OCaml Package

Basic operations on terms.

val is_kind : Term.term -> bool

is_kind t tells whether t is of the form Π x1, .., Π xn, TYPE.

val to_tvar : Term.term -> Term.tvar

to_tvar t returns x if t is of the form Vari x and fails otherwise.

NOTE the Array.map to_tvar function is useful when working with multiple binders. For example, this is the case when manipulating pattern variables (Patt constructor) or metatavariables (Meta constructor). Remark that it is important for these constructors to hold an array of terms, rather than an array of variables: a variable can only be substituted when if it is injected in a term (using the Vari constructor).

NOTE the result of to_tvar can generally NOT be precomputed. A first reason is that we cannot know in advance what variable identifier is going to arise when working under binders, for which fresh variables will often be generated. A second reason is that free variables should never be “marshaled” (e.g., by the Sign module), as this would break the freshness invariant of new variables.

val remove_impl_args : Term.sym -> Term.term list -> Term.term list

Given a symbol s, remove_impl_args s ts returns the non-implicit arguments of s among ts.

val iter : (Term.term -> unit) -> Term.term -> unit

iter f t applies the function f to every node of the term t with bound variables replaced by Kind. Note: f is called on already unfolded terms only.

val unbind_name : string -> Term.tbinder -> Term.tvar * Term.term

unbind_name b s is like Bindlib.unbind b but returns a valid variable name when b binds no variable. The string s is the prefix of the variable's name.

val unbind2_name : 
  string ->
  Term.tbinder ->
  Term.tbinder ->
  Term.tvar * Term.term * Term.term

unbind2_name b1 b2 s is like Bindlib.unbind2 b1 b2 but returns a valid variable name when b1 or b2 binds no variable. The string s is the prefix of the variable's name.

val distinct_vars : Term.ctxt -> Term.term array -> Term.tvar array option

distinct_vars ctx ts checks that the terms ts are distinct variables. If so, the variables are returned.

val nl_distinct_vars : 
  Term.ctxt ->
  Term.term array ->
  (Term.tvar array * Term.tvar Lplib.Extra.StrMap.t) option

If ts is not made of variables or function symbols prefixed by '$' only, then nl_distinct_vars ctx ts returns None. Otherwise, it returns a pair (vs, map) where vs is an array of variables made of the linear variables of ts and fresh variables for the non-linear variables and the symbols prefixed by '$', and map records by which variable each linear symbol prefixed by '$' is replaced.

Variables defined in ctx are unfolded.

The symbols prefixed by '$' are introduced by infer.ml which converts metavariables into fresh symbols, and those metavariables are introduced by sr.ml which replaces pattern variables by metavariables.

val sym_to_var : Term.tvar Lplib.Extra.StrMap.t -> Term.term -> Term.term

sym_to_var m t replaces in t every symbol f by a variable according to the map map.

val codom_binder : int -> Term.term -> Term.tbinder

codom_binder n t returns the n-th binder of t if t is a product of arith >= n.

package lambdapi