Scoped term under a (single) name binder.

Since: 0.0.1

A term, generated by a signature Bifunctor sig, with (free) variables in scope n.

Since: 0.0.1

Substitution for free (scoped monads).

Since: 0.0.1

Substitution for free (scoped monads).

This is a version of substitute that forces refreshing of all name binders, resulting in a term with normalized binders:

substituteRefreshed scope subst = refreshAST scope . subtitute scope subst

In general, substitute is more efficient since it does not always refresh binders.

Since: 0.0.3

Substitution for a single generalized pattern.

Since: 0.2.0

Refresh (force) all binders in a term, minimizing the used indices.

Since: 0.0.3

Similar to refreshAST, but for scoped terms.

Since: 0.0.3

\(\alpha\)-equivalence check for two terms in one scope via normalization of bound identifiers (via refreshAST).

Compared to alphaEquiv, this function renames every binder on both sides unconditionally, so it does strictly more work. It remains as an independent implementation of the same test.

Since: 0.0.3

\(\alpha\)-equivalence check for two terms in one scope via unification of bound variables (via unifyNameBinders).

When two matching binders coincide, comparison continues with no work at all. When they differ, the prescribed renaming is /threaded down the recursion/ (see alphaEquivEnv) and consulted at variables only, so nothing is ever copied. Applying the renaming eagerly instead would materialise a renamed copy of the remaining body at every mismatched binder, which is quadratic on a chain of them.

Since: 0.0.3

Same as alphaEquiv but for scoped terms.

While the binders of the two sides coincide, this runs with no renaming state at all. The first pair that differs switches to alphaEquivEnv, which threads the renamings down and switches back when they empty out.

Since: 0.0.3

The raw name a verdict's renaming assigns to a pattern's name.

Since: 0.4.0

Bind the paired names of a binder pair. A pair whose names coincide shadows both sides identically and is deleted from the environments. A pair whose names differ binds both to one fresh level. Continues with alphaEquivEnv on the bodies.

Since: 0.4.0

The renaming-threading worker behind alphaEquiv: compare two terms under partial renamings of their names into shared levels.

Each environment maps a raw name to the level of the binder pair that bound it on the comparison path, and a name outside its environment stands for itself. A variable occurrence then compares as a level against a level, or as a raw name against a raw name, and the two can never be conflated. This is what makes threading sound where applying a raw renaming at the variables would not be, since a renamed name could collide with one that passes through unchanged and happens to share the target spelling. Levels are also why no capture check is needed: a level is never a name, so there is nothing for a binder to capture.

A binder pair whose names coincide deletes those names from both environments, the pair shadowing both sides identically. When the environments empty out the comparison drops back to the stateless alphaEquiv, so only the region of the terms below a mismatched binder, and above the point where the mismatch is shadowed away, pays for the threading at all.

The indices of the two terms are deliberately independent, in the style of unsafeEqAST: the terms are never renamed into a common scope, so no common index exists to give them.

Since: 0.4.0

The scoped half of alphaEquivEnv: get the verdict from unifyPatternsIn, extend the environments as it prescribes, and recurse into the bodies as they stand.

Since: 0.4.0

Unsafe equality check for two terms. This check ignores the possibility that two terms might have different scope extensions under binders (which might happen due to substitution under a binder in absence of name conflicts).

Since: 0.0.3

A version of unsafeEqAST for scoped terms.

Since: 0.0.3

An identifier a raw term mentions that the names given for conversion do not account for.

Note what this does and does not carry. It cannot carry a position: the conversion functions are generic in the raw term and only ever see it through toSig, so a source location, if the syntax has one, is not theirs to read. What they do know, and a caller checking names beforehand does not, is which names were in scope at the occurrence, the binders passed on the way down included. That is what a "did you mean" needs.

Since: 0.4.0

The identifiers a raw term mentions that a set of names cannot resolve, in the order they occur.

This is unsafeConvertToAST with the conversion left out, so it descends under binders in the same way and accounts for what they bind.

Since: 0.4.0

Convert a raw term into a scope-safe term, reporting the first identifier that does not resolve.

One pass, short-circuiting at the first failure, so a term that resolves costs no more than unsafeConvertToAST does. The report is complete for that one identifier, since unresolvedInScope is built where the conversion fails and is never computed on the way through.

A caller wanting every unresolved identifier rather than the first pays a second pass for it, with unresolvedNames. The successful path stays fast that way, and a failure can afford to be walked again for a better message.

Since: 0.4.0

Convert a raw term into a scope-safe term, resolving some identifiers to whole terms rather than to variables.

The extra table is what a language with constants needs: an identifier that denotes a top-level declaration, a primitive, or an abbreviation stands for something that is not a variable, and resolving it during conversion is the only place where the binders are known. Doing it in a pass of one's own means writing a binder-aware traversal of the raw syntax by hand.

Variables win: the table of names is consulted first, so a binder shadows an entry here, and an entry here shadows nothing. The table is sunk when going under a binder, exactly as the names are, so its entries may mention anything in scope where conversion started and need not be closed.

Since: 0.4.0

Convert a raw term into a scope-safe term, calling error on an identifier that does not resolve.

Prefer tryConvertToAST, which reports such identifiers. This is for callers that have already established that every name resolves.

Since: 0.4.0

Same as unsafeConvertToAST but for scoped terms.

Since: 0.4.0

Convert a raw term into a scope-safe term.

Since: 0.0.3

Same as convertToAST but for scoped terms.

Since: 0.0.3

Convert a scope-safe term back into a raw term.

Since: 0.0.3

Same as convertFromAST but for scoped terms.

Since: 0.0.3

Convert a scope-safe term back into a raw term, naming the variables that occur free in the whole term separately from the bound ones.

convertFromAST applies one naming function to every variable it meets, bound or free, and gives it only a raw name. That is often not enough, since raw names are not unique across scope indices: a binder inside a term may share one with a name of the ambient scope, so naming by raw name alone can print a bound variable as whatever the ambient scope calls that name.

Keeping the typed name is what distinguishes them, and unsinkNamePattern is the operation for it: composing one per binder on the way down builds a Name x -> Maybe (Name n) that answers exactly the question.

Since: 0.4.0

The support of a term: exactly the names that occur free in it.

This is the annotation that co-de-Bruijn syntax carries intrinsically and that the foil, having global names and therefore free weakening, does not. Computing it is \(O(size)\); a client that restricts often should cache it.

Since: 0.4.0

The support of a scoped term, in the scope outside its binder.

Since: 0.4.0

Cut a term down to the scope of exactly the names it uses.

This is the a-priori form of restriction, and the cheap one: the term inhabits the smaller scope by construction, so nothing is tested and nothing can fail. Ext m n comes back with it, so the term can be sinked to where it came from for free.

Verifying a declared dependency, such as a uses clause or a module's parameters, is this plus a comparison: compute the scope a term really inhabits, and check the declared one against it.

Since: 0.4.0

Unsink an AST from a larger scope to a smaller scope.

This is the a-posteriori form, and the one that has to be paid for: the term's support is computed and compared against the scope. When it succeeds the term itself is untouched, since restriction of a term that does inhabit the smaller scope is a coercion.

Since: 0.3.0

Get the free variables of an AST.

These come from supportOf, so they are distinct and in ascending order of their identifiers.

Since: 0.3.0

Get the free variables of a scoped AST, in the scope outside its binder.

Since: 0.3.0