Documentation

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 almost never be called directly. Instead, use other methods provided by this module which are defined in terms of Alpha methods.

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

Occasionally, however, it may be useful to override the default implementations of one or more Alpha methods for a particular type. For example, consider a type like

 data Term = ...
           | Annotation Stuff Term

where the Annotation constructor of Term associates some sort of annotation with a term --- say, information obtained from a parser about where in an input file the term came from. This information is needed to produce good error messages, but should not be taken into consideration when, say, comparing two Terms for alpha-equivalence. In order to make aeq ignore annotations, you can override the implementation of aeq' like so:

 instance Alpha Term where
   aeq' c (Annotation _ t1) t2 = aeq' c t1 t2
   aeq' c t1 (Annotation _ t2) = aeq' c t1 t2
   aeq' c t1 t2 = aeqR1 rep1 t1 t2

Note how the call to aeqR1 handles all the other cases generically.

Type class for embedded terms (either Embed or Shift).

The result of a findpatrec operation.

Find the (first) index of the name in the pattern, if it exists.

The result of an nthpatrec operation.

A continuation which takes the remaining index and searches for that location in a pattern, yielding a name or a remaining index if the end of the pattern was reached too soon.

If we see a name, check whether the index is 0: if it is, we've found the name we're looking for, otherwise continue with a decremented index.

nthpat b n looks up up the nth name in the pattern b (zero-indexed). PRECONDITION: the number of names in the pattern must be at least n.

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.

A mode is basically a flag that tells us whether we should be looking at the names in the term, or if we are in a pattern and should only be looking at the names in the annotations. The standard mode is to use Term; many functions do this by default.

Open a term using the given pattern.

openP p1 p2 opens the pattern p2 using the pattern p1.

Close a term using the given pattern.

closeP p1 p2 closes the pattern p2 using the pattern p1.

Class constraint hackery to allow us to override the default definitions for certain classes. AlphaD is essentially a reified dictionary for the Alpha class.