Agda.Syntax.Abstract.Pattern

Auxiliary functions to handle patterns in the abstract syntax.

Generic and specific traversals.

Generic traversals

type NAP = NamedArg Pattern

class MapNamedArgPattern a where

Methods

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

mapNamedArgPattern :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a

Instances

MapNamedArgPattern NAP

Methods

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

MapNamedArgPattern a => MapNamedArgPattern [a]

Methods

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

MapNamedArgPattern a => MapNamedArgPattern (Maybe a)

Methods

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

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a)

Methods

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

class APatternLike a p | p -> a where

Generic pattern traversal.

Methods

foldrAPattern

Arguments

:: Monoid m

=> (Pattern' a -> m -> m)

Combine a pattern and the value computed from its subpatterns.

-> p

-> m

Fold pattern.

foldrAPattern

Arguments

:: (Monoid m, Foldable f, APatternLike a b, f b ~ p)

=> (Pattern' a -> m -> m)

Combine a pattern and the value computed from its subpatterns.

-> p

-> m

Fold pattern.

traverseAPatternM

Arguments

:: Monad m

=> (Pattern' a -> m (Pattern' a))

pre: Modification before recursion.

-> (Pattern' a -> m (Pattern' a))

post: Modification after recursion.

-> p

-> m p

Traverse pattern.

traverseAPatternM

Arguments

:: (Traversable f, APatternLike a q, f q ~ p, Monad m)

=> (Pattern' a -> m (Pattern' a))

pre: Modification before recursion.

-> (Pattern' a -> m (Pattern' a))

post: Modification after recursion.

-> p

-> m p

Traverse pattern.

Instances

APatternLike a b => APatternLike a (FieldAssignment' b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> FieldAssignment' b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> FieldAssignment' b -> m (FieldAssignment' b)

APatternLike a b => APatternLike a (Maybe b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Maybe b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Maybe b -> m (Maybe b)

APatternLike a b => APatternLike a [b]

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> [b] -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> [b] -> m [b]

APatternLike a b => APatternLike a (Arg b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b)

APatternLike a (Pattern' a)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)

APatternLike a b => APatternLike a (Named n b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Named n b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n b)

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

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

preTraverseAPatternM

Arguments

:: (APatternLike a b, Monad m)

=> (Pattern' a -> m (Pattern' a))

pre: Modification before recursion.

-> b

-> m b

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

postTraverseAPatternM

Arguments

:: (APatternLike a b, Monad m)

=> (Pattern' a -> m (Pattern' a))

post: Modification after recursion.

-> b

-> m b

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

Specific folds

patternVars :: forall a p. APatternLike a p => p -> [Name]

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

containsAPattern :: APatternLike a p => (Pattern' a -> Bool) -> p -> Bool

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

containsAbsurdPattern :: APatternLike a p => p -> Bool

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

Precondition: contains no pattern synonyms.

containsAsPattern :: APatternLike a p => p -> Bool

Check if a pattern contains an @-pattern.

Precondition: contains no pattern synonyms.