Documentation

An identifier that is not in scope becomes a hole under a marked name.

A free-foil term refers to a variable by name, and an unresolved identifier has none — so the term cannot represent it. Elaboration marks it instead, and the checker reports it when it reaches it, which is what keeps the error where the identifier was used (inside the binders and topes it was written under) rather than at the top of the declaration.

The marker cannot be mistaken for a hole the user wrote: the grammar forbids # in an identifier.

What a bound name is shown as: the display name standing for the variable itself, and the (freshened) binder, which gives the pattern to print and the component names to fold projections back to.

The annotation on every node of a typed term: its type, plus its memoised weak head and normal forms.

The display name of a hole from its surface token text. The token includes the leading ?; an anonymous hole (bare ?) has no name.

The surface token text (including the leading ?) for a hole name.

The name(s) a binder introduces. A binder may name a single (possibly anonymous) variable, or destructure a pair/tuple via a pattern. The pattern structure is kept around purely so that goals, holes and error messages can show the user's original names (e.g. t and s for \ (t , s) -> …) instead of projections of a fresh variable (e.g. π₁ x₄ and π₂ x₄).

Operationally a pair pattern still binds a single variable; the components are projections of it (see toScopePattern). Binder only records the names so they can be restored when rendering.

The single name of a binder, if it binds exactly one named variable. A pair/unit pattern has no single name, so this is Nothing for them. Used wherever the old Maybe VarIdent binder name is still sufficient.

A tuple pattern is sugar for nested pairs.

Split a binder term into the individual variables it names. A multi-variable binder like (x y : A) is parsed as the application spine x y; this returns [x, y] so each can become its own nested binder. A single binder term (a variable, a pair pattern, …) is returned unchanged as a singleton.

A projection step: first (π₁) or second (π₂) component.

Render a Binder as a surface pattern (used to display the binder itself, e.g. (t , s)). Anonymous variables become _.

A VarIdent that prints as the binder's surface pattern, e.g. (t , s). Used to display a pattern binder in a hole's local context as the pattern itself rather than as the underlying single variable.

The named leaves of a binder, each paired with the projection path that reaches it from the bound variable. For example (t , (a , b)) yields [([PFst], t), ([PSnd, PFst], a), ([PSnd, PSnd], b)].

The names appearing in a binder.

Does this binder destructure a pair/tuple (as opposed to naming a single variable or _)?

Refresh the named leaves of a binder so they avoid the given names (and one another). Anonymous leaves and the unit pattern are left unchanged.

Decompose a chain of projections applied to a variable into the projection path from the variable outwards, matching binderPaths. The outermost projection is applied last, so it goes at the end of the path: e.g. π₂ (π₁ x) (select π₁ first, then π₂) becomes Just ([PFst, PSnd], x).

Given a list of used variable names in the current context, generate a unique fresh name based on a given one.

>>> print $ refreshVar ["x", "y", "x₁", "z"] "x"
x₂

Refresh a name against a set of taken ones.

The list version above is O(taken) per call, and naming a whole context calls it once per entry, which made reading the naming off a context with every top-level definition of a project in it quadratic.

>>> print $ refreshVarIn (Set.fromList ["x", "y", "x₁", "z"]) "x"
x₂

freshenBinderLeaves against a set of taken names, for the same reason refreshVarIn exists beside refreshVar.

Increment the subscript number at the end of the indentifier.

>>> putStrLn $ T.unpack $ incIndex "x"
x₁
>>> putStrLn $ T.unpack $ incIndex "x₁₉"
x₂₀