| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract.Pattern
Contents
Description
Auxiliary functions to handle patterns in the abstract syntax.
Generic and specific traversals.
- type NAP = NamedArg Pattern
- class MapNamedArgPattern a where
- class APatternLike a p | p -> a where
- foldAPattern :: (APatternLike a p, Monoid m) => (Pattern' a -> m) -> p -> m
- preTraverseAPatternM :: (APatternLike a b, Monad m) => (Pattern' a -> m (Pattern' a)) -> b -> m b
- postTraverseAPatternM :: (APatternLike a b, Monad m) => (Pattern' a -> m (Pattern' a)) -> b -> m b
- patternVars :: forall a p. APatternLike a p => p -> [Name]
- containsAPattern :: APatternLike a p => (Pattern' a -> Bool) -> p -> Bool
- containsAbsurdPattern :: APatternLike a p => p -> Bool
- containsAsPattern :: APatternLike a p => p -> Bool
Generic traversals
class MapNamedArgPattern a where Source #
Methods
mapNamedArgPattern :: (NAP -> NAP) -> a -> a Source #
mapNamedArgPattern :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a Source #
Instances
class APatternLike a p | p -> a where Source #
Generic pattern traversal.
Methods
Arguments
| :: Monoid m | |
| => (Pattern' a -> m -> m) | Combine a pattern and the value computed from its subpatterns. |
| -> p | |
| -> m |
Fold pattern.
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.
Arguments
| :: Monad m | |
| => (Pattern' a -> m (Pattern' a)) |
|
| -> (Pattern' a -> m (Pattern' a)) |
|
| -> p | |
| -> m p |
Traverse pattern.
Arguments
| :: (Traversable f, APatternLike a q, f q ~ p, Monad m) | |
| => (Pattern' a -> m (Pattern' a)) |
|
| -> (Pattern' a -> m (Pattern' a)) |
|
| -> p | |
| -> m p |
Traverse pattern.
Instances
| APatternLike a b => APatternLike a (FieldAssignment' b) Source # | |
| APatternLike a b => APatternLike a (Maybe b) Source # | |
| APatternLike a b => APatternLike a [b] Source # | |
| APatternLike a b => APatternLike a (Arg b) Source # | |
| APatternLike a (Pattern' a) Source # | |
| APatternLike a b => APatternLike a (Named n b) Source # | |
foldAPattern :: (APatternLike a p, Monoid m) => (Pattern' a -> m) -> p -> m Source #
Compute from each subpattern a value and collect them all in a monoid.
Arguments
| :: (APatternLike a b, Monad m) | |
| => (Pattern' a -> m (Pattern' a)) |
|
| -> b | |
| -> m b |
Traverse pattern(s) with a modification before the recursive descent.
postTraverseAPatternM Source #
Arguments
| :: (APatternLike a b, Monad m) | |
| => (Pattern' a -> m (Pattern' a)) |
|
| -> b | |
| -> m b |
Traverse pattern(s) with a modification after the recursive descent.
Specific folds
patternVars :: forall a p. APatternLike a p => p -> [Name] Source #
Collect pattern variables in left-to-right textual order.
containsAPattern :: APatternLike a p => (Pattern' a -> Bool) -> p -> Bool Source #
Check if a pattern contains a specific (sub)pattern.
containsAbsurdPattern :: APatternLike a p => p -> Bool Source #
Check if a pattern contains an absurd pattern.
For instance, suc (), does so.
Precondition: contains no pattern synonyms.
containsAsPattern :: APatternLike a p => p -> Bool Source #
Check if a pattern contains an @-pattern.
Precondition: contains no pattern synonyms.