Documentation

A smart constructor for binders, also sometimes referred to as "close". Free variables in the term are taken to be references to matching binders in the pattern. (Free variables with no matching binders will remain free.)

A destructor for binders that does not guarantee fresh names for the binders.

Bind the pattern in the term "up to permutation" of bound variables. For example, the following 4 terms are all alpha-equivalent:

 permbind [a,b] (a,b)
 permbind [a,b] (b,a)
 permbind [b,a] (a,b)
 permbind [b,a] (b,a)

Note that none of these terms is equivalent to a term with a redundant pattern such as

 permbind [a,b,c] (a,b)

For binding constructors which do render these equivalent, see setbind and setbindAny.

Bind the list of names in the term up to permutation and dropping of unused variables.

For example, the following 5 terms are all alpha-equivalent:

 setbind [a,b] (a,b)
 setbind [a,b] (b,a)
 setbind [b,a] (a,b)
 setbind [b,a] (b,a)
 setbind [a,b,c] (a,b)

There is also a variant, setbindAny, which ignores name sorts.

Bind the list of (any-sorted) names in the term up to permutation and dropping of unused variables. See setbind.

Constructor for rebinding patterns.

Destructor for rebinding patterns. It does not need a monadic context for generating fresh names, since Rebind can only occur in the pattern of a Bind; hence a previous call to unbind (or something similar) must have already freshened the names at this point.

Constructor for recursive patterns.

Destructor for recursive patterns.

Constructor for recursive abstractions.

Destructor for recursive abstractions which picks globally fresh names for the binders.

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

Determine the alpha-equivalence of two terms.

Determine (alpha-)equivalence of patterns. Do they bind the same variables in the same patterns and have alpha-equivalent annotations in matching positions?

An alpha-respecting total order on terms involving binders.

Calculate the free variables (of any sort) contained in a term.

Calculate the free variables of a particular sort contained in a term.

Calculate the variables (of any sort) that occur freely in terms embedded within a pattern (but are not bound by the pattern).

Calculate the variables of a particular sort that occur freely in terms embedded within a pattern (but are not bound by the pattern).

Calculate the binding variables (of any sort) in a pattern.

Calculate the binding variables (of a particular sort) in a pattern.

Apply a permutation to a term.

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

Apply a permutation to the embedded terms in a pattern. Binding names are left alone by the permutation.

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

Freshen a pattern by replacing all old binding Names with new fresh Names, returning a new pattern and a Perm Name specifying how Names were replaced.

Unbind (also known as "open") is the simplest destructor for bindings. It ensures that the names in the binding are globally fresh, using a monad which is an instance of the Fresh type class.

Unbind two terms with the same fresh names, provided the binders have the same binding variables (both number and sort). If the patterns have different binding variables, return Nothing. Otherwise, return the renamed patterns and the associated terms.

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 for more details.

lunbind opens a binding in an LFresh monad, ensuring that the names chosen for the binders are locally fresh. The components of the binding are passed to a continuation, and the resulting monadic action is run in a context extended to avoid choosing new names which are the same as the ones chosen for this binding.

For more information, see the documentation for the LFresh type class.

Unbind two terms with the same locally fresh names, provided the patterns have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

Unbind three terms with the same locally fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.