Agda.Syntax.Abstract

Expressions after scope checking (operators parsed, names resolved).

Types are just expressions. Use this type synonym for hinting that an expression should be a type.

Record field assignment f = e.

Pattern synonym for regular Def.

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

A lambda binding is either domain free or typed.

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

1. We would have to typecheck the type A several times.

2. If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Only Axioms.

Renaming (generic).

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Extra information that is attached to a typed binding, that plays a role during type checking but strictly speaking is not part of the name : type" relation which a makes up a binding.

Parameterised over the type of dot patterns.

The lhs in projection-application and with-pattern view. Parameterised over the type e of dot patterns.

A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.

With --caching on we compare abstract syntax to determine if we can reuse previous typechecking results: during that comparison two names can have the same nameId but be semantically different, e.g. in {_ : A} -> .. vs. {r : A} -> ...

Bindings that are valid in a let.

Smart constructor for Generalized.

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) Axiom.

Are we in an abstract block?

In that case some definition is abstract.

Turn a name into an expression.

Declaration spines. Used in debugging to make it easy to see where constructors such as ScopedDecl and Mutual are placed.

Clause spines.

Right-hand side spines.