Agda.Syntax.Abstract.Pattern

Generic pattern traversal.

Compute from each subpattern a value and collect them all in a monoid.

Traverse pattern(s) with a modification before the recursive descent.

Traverse pattern(s) with a modification after the recursive descent.

Map pattern(s) with a modification after the recursive descent.

Collect pattern variables in left-to-right textual order.

Check if a pattern contains a specific (sub)pattern.

Check if a pattern contains an absurd pattern. For instance, suc (), does so.

Precondition: contains no pattern synonyms.

Check if a pattern contains an @-pattern.

Check if any user-written pattern variables occur more than once, and throw the given error if they do.

Pattern substitution.

For the embedded expression, the given pattern substitution is turned into an expression substitution.

Pattern substitution, parametrized by substitution function for embedded expressions.

Convert a pattern to an expression.

Does not support all cases of patterns. Result has no Range info, except in identifiers.

This function is only used in expanding pattern synonyms and in Agda.Syntax.Translation.InternalToAbstract, so we can cut some corners.

Converting a pattern to an expression.

The Hiding context is remembered to create instance metas when translating absurd patterns in instance position.

Make sure that there are no dot or equality patterns (called on pattern synonyms). Also disallows annotated patterns.

Split patterns into (patterns, trailing with-patterns).

Get the tail of with-patterns of a pattern spine.

The next patterns are ...

(This view discards PatInfo.)

Construct the LHSPatternView of the given list (if not empty).

Return the view and the remaining patterns.

Convert a focused lhs to spine view and back.

Add applicative patterns (non-projection / non-with patterns) to the right.

Add with-patterns to the right.

Add projection, with, and applicative patterns to the right.

Used for checking pattern linearity.

Used in 'Agda.Syntax.Translation.AbstractToConcrete'. Returns a DefP.