ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Abstract.Pattern

Auxiliary functions to handle patterns in the abstract syntax.

Generic and specific traversals.

2 types
4 classes
25 values

PackageAgda-2.8.0.2
Exports31
LanguageHaskell2010
LicenceMIT
SourcePattern.hs

Generic traversals

7 declarations

typetype NAP = NamedArg Pattern

classclass MapNamedArgPattern a where

Methods

mapNamedArgPattern :: (NAP -> NAP) -> a -> a

Instances5MapNamedArgPattern

MapNamedArgPattern NAPDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
MapNamedArgPattern a => MapNamedArgPattern (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
MapNamedArgPattern a => MapNamedArgPattern [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
(MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern

classclass APatternLike p where

Generic pattern traversal.

Associated types

type family ADotT p

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT p) -> m -> m) -> p -> m
Fold pattern.
traverseAPatternM :: Monad m => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
Traverse pattern.

Instances7APatternLike, …

APatternLike (Pattern' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
APatternLike a => APatternLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
APatternLike a => APatternLike (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
APatternLike a => APatternLike (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
APatternLike a => APatternLike [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
APatternLike a => APatternLike (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
(APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern

valuefoldAPattern

:: (APatternLike p, Monoid m)
=> Pattern' (ADotT p) -> m
-> p
-> m

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

valuepreTraverseAPatternM

:: (APatternLike p, Monad m)
=> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
pre: Modification before recursion.
-> p
-> m p

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

valuepostTraverseAPatternM

:: (APatternLike p, Monad m)
=> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
post: Modification after recursion.
-> p
-> m p

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

valuemapAPattern

:: APatternLike p
=> Pattern' (ADotT p) -> Pattern' (ADotT p)
-> p
-> p

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

Specific folds

5 declarations

valuepatternVars :: APatternLike p => p -> [Name]

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

valuecontainsAPattern

:: APatternLike p
=> Pattern' (ADotT p) -> Bool
-> p
-> Bool

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

valuecontainsAbsurdPattern :: APatternLike p => p -> Bool

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

Precondition: contains no pattern synonyms.

valuecontainsAsPattern :: APatternLike p => p -> Bool

Check if a pattern contains an @-pattern.

valuecheckPatternLinearity

:: (Monad m, APatternLike p)
=> p
-> List1 Name -> m ()
-> m ()

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

Specific traversals

5 declarations

valuesubstPattern :: [(Name, Pattern)] -> Pattern -> Pattern

Pattern substitution.

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

valuesubstPattern'

:: (e -> e)
Substitution function for expressions.
-> [(Name, Pattern' e)]
(Parallel) substitution.
-> Pattern' e
Input pattern.
-> Pattern' e

Pattern substitution, parametrized by substitution function for embedded expressions.

valuepatternToExpr :: Pattern -> Expr

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.

classclass PatternToExpr p e where

Converting a pattern to an expression.

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

Methods

patToExpr :: p -> Reader Hiding e

Instances5PatternToExpr

PatternToExpr Pattern ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
PatternToExpr p e => PatternToExpr (Arg p) (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
PatternToExpr p e => PatternToExpr [p] [e]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
PatternToExpr p e => PatternToExpr (Named n p) (Named n e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern

valuenoDotOrEqPattern

:: Monad m
=> m (Pattern' Void)
Exception or replacement for dot (etc.) patterns.
-> Pattern' e
In pattern.
-> m (Pattern' Void)
Out pattern.

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

Other pattern utilities

4 declarations

valuesplitOffTrailingWithPatterns :: Patterns -> (Patterns, Patterns)

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

valuetrailingWithPatterns :: Patterns -> Patterns

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

datadata LHSPatternView e

The next patterns are ...

(This view discards PatInfo.)

Constructors

LHSAppP (NAPs1 e)
Application patterns (non-empty list).
LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
A projection pattern. Is also stored unmodified here.
LHSWithP (List1 (Pattern' e))
With patterns (non-empty list). These patterns are not prefixed with WithP.

Instances1Show

Show e => Show (LHSPatternView e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern

valuelhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)

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

Return the view and the remaining patterns.

Left-hand-side manipulation

10 declarations

classclass LHSToSpine a b where

Convert a focused lhs to spine view and back.

Methods

lhsToSpine :: a -> b
spineToLhs :: b -> a

Instances3LHSToSpine

LHSToSpine Clause SpineClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
Clause instance.
LHSToSpine LHS SpineLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
LHS instance.
LHSToSpine a b => LHSToSpine [a] [b]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
List instance (for clauses).

valuelhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]

valuespineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e

valuelhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e

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

valuelhsCoreWith :: LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e

Add with-patterns to the right.

valuelhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e

valuelhsCoreAddSpine

:: IsProjP e
=> LHSCore' e
-> [NamedArg (Pattern' e)]
-> LHSCore' e

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

valuelhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]

Used for checking pattern linearity.

valuelhsCoreToPattern :: LHSCore -> Pattern

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

valuemapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore

Orphan instances

1 instance

IsWithP (Pattern' e)
Check for with-pattern.