If the expression is a variable, then look it up. Recursing until we can finally return some syntax.

The raw view of abstract binding trees, to separate out variables and binders from (1) the rest of syntax (cf., Term), and (2) whatever annotations (cf., the ABT instances).

The first parameter gives the generating signature for the signature. The second index gives the number and types of locally-bound variables. And the final parameter gives the type of the whole expression.

HACK: We only want to expose the patterns generated by this type, not the constructors themselves. That way, callers must use the smart constructors of the ABT class. But if we don't expose this type, then clients can't define their own ABT instances (without reinventing their own copy of this type)...

The class interface for abstract binding trees. The first argument, syn, gives the syntactic signature of the ABT; whereas, the second argument, abt, is thing being declared as an ABT for syn. The first three methods (syn, var, bind) alow us to inject any View into the abt. The other methods provide various views for extracting information from the abt.

At present we're using fundeps in order to restrict the relationship between abt and syn. However, in the future we may move syn into being an associated type, if that helps to clean things up (since fundeps and type families don't play well together). The idea behind the fundep is that certain abt implementations may only be able to work for particular syn signatures. This isn't the case for TrivialABT nor MemoizedABT, but isn't too far-fetched.

Since the first argument to abt is '[], we know it must be either Syn of Var. So we do case analysis with those two constructors.

Call bind repeatedly.

A specialization of binds for when ys ~ '[]. We define this to avoid the need for using eqAppendIdentity on the result of binds itself.

Call caseBind repeatedly. (Actually we use viewABT.)

Transform expression under binds

Call nextFree on all the terms and return the maximum.

Call nextBind on all the terms and return the maximum.

Call nextFreeOrBind on all the terms and return the maximum.

Rename a free variable. Does nothing if the variable is bound.

Perform capture-avoiding substitution. This function will either preserve type-safety or else throw an VarEqTypeError (depending on which interpretation of varEq is chosen). N.B., to ensure timely throwing of exceptions, the Term and ABT should have strict fmap21 definitions.

The parallel version of subst for performing multiple substitutions at once.

A combinator for defining a HOAS-like API for our syntax. Because our Term is first-order, we cannot actually have any exotic terms in our language. In principle, this function could be used to do exotic things when constructing those non-exotic terms; however, trying to do anything other than change the variable's name hint will cause things to explode (since it'll interfere with our tying-the-knot).

N.B., if you manually construct free variables and use them in the body (i.e., via var), they may become captured by the new binding introduced here! This is inevitable since nextBind never looks at variable use sites; it only ever looks at binding sites. On the other hand, if you manually construct a bound variable (i.e., manually calling bind yourself), then the new binding introduced here will respect the old binding and avoid that variable ID.

The catamorphism (aka: iterator) for ABTs. While this is equivalent to paraABT in terms of the definable functions, it is weaker in terms of definable algorithms. If you need access to (subterms of) the original ABT, it is more efficient to use paraABT than to rebuild them. However, if you never need access to the original ABT, then this function has somewhat less overhead.

A monadic variant of cataABT, which may not fit the precise definition of a catamorphism? The bind and syn operations receive monadic actions as their inputs, which allows the bind and syn operations to update the monadic context in which the subterms are evaluated if need be.

The paramorphism (aka: recursor) for ABTs. While this is equivalent to cataABT in terms of the definable functions, it is stronger in terms of definable algorithms. If you need access to (subterms of) the original ABT, it is more efficient to use this function than to use cataABT and rebuild them. However, if you never need access to the original ABT, then cataABT has somewhat less overhead.

The provided type is slightly non-uniform since we inline (i.e., curry) the definition of Pair2 in the type of the bind_ argument. But we can't inline Pair2 away in the type of the syn_ argument. N.B., if you treat the second component of the Pair2 (either the real ones or the curried ones) lazily, then this is a top-down function; however, if you treat them strictly then it becomes a bottom-up function.

Makes a copy of an ABT at another type

A trivial ABT with no annotations.

The Show instance does not expose the raw underlying data types, but rather prints the smart constructors var, syn, and bind. This makes things prettier, but also means that if you paste the string into a Haskell file you can use it for any ABT instance.

The freeVars, nextFree, and nextBind methods are all very expensive for this ABT, because we have to traverse the term every time we want to call them. The MemoizedABT implementation fixes this.

An ABT which memoizes freeVars, nextBind, and nextFree, thereby making them take only O(1) time.

N.B., the memoized set of free variables is lazy so that we can tie-the-knot in binder without interfering with our memos. The memoized nextFree must be lazy for the same reason.

An ABT which carries around metadata at each node.

Right now this essentially inlines the the TrivialABT instance but it would be nice if it was abstract in the choice of ABT.