Names are things that get bound. This type is intentionally abstract; to create a Name you can use string2Name or integer2Name. The type parameter is a tag, or sort, which tells us what sorts of things this name may stand for. The sort must be an instance of the Rep type class.

A name with a hidden (existentially quantified) sort.

The type of a binding. We can Bind an a object in a b object if we can create "fresh" a objects, and a objects can occur unbound in b objects. Often a is Name but that need not be the case.

Like Name, Bind is also abstract. You can create bindings using bind and take them apart with unbind and friends.

An annotation is a "hole" in a pattern where variables can be used, but not bound. For example, patterns may include type annotations, and those annotations can reference variables without binding them. Annotations do nothing special when they appear elsewhere in terms.

Rebind supports "telescopes" --- that is, patterns where bound variables appear in multiple subterms.

Create a Name from an Integer.

Create a Name from a String.

Create a Name from a String and an Integer index.

Get the integer index of a Name.

Get the string part of a Name.

Get the integer index of an AnyName.

Get the string part of an AnyName.

The Alpha type class is for types which may contain names. The Rep1 constraint means that we can only make instances of this class for types that have generic representations (which can be automatically derived by RepLib.)

Note that the methods of Alpha should never be called directly! Instead, use other methods provided by this module which are defined in terms of Alpha methods. (The only reason they are exported is to make them available to automatically-generated code.)

Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring

 instance Alpha MyType 

Apply a permutation to a term.

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

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

Compare two data structures and produce a permutation of their Names that will make them alpha-equivalent to each other (Names that appear in annotations must match exactly). Return Nothing if no such renaming is possible. Note that two terms are alpha-equivalent if the empty permutation is returned.

Compare two patterns, ignoring the names of binders, and produce a permutation of their annotations to make them alpha-equivalent to eachother. Return Nothing if no such renaming is possible.

Compare two patterns for equality and produce a permutation of their binding Names to make them alpha-equivalent to each other (Names that appear in annotations must match exactly). Return Nothing if no such renaming is possible.

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

List variables of a particular sort that occur freely in annotations (not bindings).

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

Determine alpha-equivalence.

Determine (alpha-)equivalence of patterns

A smart constructor for binders, also sometimes known as "close".

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

Type class for monads which can generate new globally unique Names based on a given Name.

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

Unbind (also known as "open") is the destructor for bindings. It ensures that the names in the binding are fresh.

Unbind two terms with the same fresh names, provided the binders match.

Type class for contexts which can generate new globally fresh integers.

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, but not globally fresh. This class has a basic instance based on the reader monad.

"Locally" freshen a term. TODO: explain this type signature a bit better.

Destruct a binding in an LFresh monad.

Unbind two terms with the same fresh names, provided the binders match.

Unbind three terms with the same fresh names, provided the binders match.

Constructor for binding in patterns.

destructor for binding patterns, the names should have already been freshened.

The Subst class governs capture-avoiding substitution. To derive this class, you only need to indicate where the variables are in the data type, by overriding the method isvar.

Match returns a permutation ordering. Either the terms are known to be LT or GT, or there is some permutation that can make them equal to eachother data POrdering = PLT | PEq (Perm AnyName) | PGT

Many of the operations in the Alpha class take an AlphaCtx: stored information about the iteration as it progresses. This type is abstract, as classes that override these operations should just pass the context on.