package lambdapi
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c
doc/lambdapi.core/Core/LibTerm/index.html
Module Core.LibTermSource
Basic operations on terms.
to_var t returns x if t is of the form Vari x and fails otherwise.
NOTE the Array.map to_var 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_var 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.
Given a symbol s, remove_impl_args s ts returns the non-implicit arguments of s among ts.
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.
distinct_vars ctx ts checks that the terms ts are distinct variables. If so, the variables are returned.
val nl_distinct_vars :
Term.term array ->
(Term.var array * Term.var Lplib.Extra.StrMap.t) optionIf ts is not made of variables or function symbols prefixed by '$' only, then nl_distinct_vars 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.
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.
sym_to_var m t replaces in t every symbol f by a variable according to the map map.
eq_alpha a b tests the equality modulo alpha of a and b.
fold id t a returns term binder b with binder name id such that subst b t ≡ a.
Free variables of a term.