| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract.Pattern
Description
Auxiliary functions to handle patterns in the abstract syntax.
Generic and specific traversals.
Synopsis
- type NAP = NamedArg Pattern
- class MapNamedArgPattern a where
- mapNamedArgPattern :: (NAP -> NAP) -> a -> a
- class APatternLike a p | p -> a where
- foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> p -> m
- traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> p -> m p
- 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
- mapAPattern :: APatternLike a p => (Pattern' a -> Pattern' a) -> p -> p
- 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
- checkPatternLinearity :: (Monad m, APatternLike a p) => p -> ([Name] -> m ()) -> m ()
- substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
- substPattern' :: (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
- splitOffTrailingWithPatterns :: Patterns -> (Patterns, Patterns)
- trailingWithPatterns :: Patterns -> Patterns
- data LHSPatternView e
- = LHSAppP (NAPs e)
- | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
- | LHSWithP [Pattern' e]
- lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
- class LHSToSpine a b where
- lhsToSpine :: a -> b
- spineToLhs :: b -> a
- lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]
- spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreWith :: LHSCore' e -> [Pattern' e] -> LHSCore' e
- lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
- lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
- lhsCoreToPattern :: LHSCore -> Pattern
- mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
Generic traversals
class MapNamedArgPattern a where Source #
Minimal complete definition
Nothing
Methods
mapNamedArgPattern :: (NAP -> NAP) -> a -> a Source #
default mapNamedArgPattern :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a Source #
Instances
| MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| MapNamedArgPattern a => MapNamedArgPattern [a] Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> [a] -> [a] Source # | |
| MapNamedArgPattern a => MapNamedArgPattern (Maybe a) Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source # | |
| (MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a, b) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> (a, b) -> (a, b) Source # | |
class APatternLike a p | p -> a where Source #
Generic pattern traversal.
Minimal complete definition
Nothing
Methods
Arguments
| :: Monoid m | |
| => (Pattern' a -> m -> m) | Combine a pattern and the value computed from its subpatterns. |
| -> p | |
| -> m |
Fold pattern.
default foldrAPattern :: (Monoid m, Foldable f, APatternLike a b, f b ~ p) => (Pattern' a -> m -> m) -> p -> m Source #
Arguments
| :: Monad m | |
| => (Pattern' a -> m (Pattern' a)) |
|
| -> (Pattern' a -> m (Pattern' a)) |
|
| -> p | |
| -> m p |
Traverse pattern.
default traverseAPatternM :: (Traversable f, APatternLike a q, f q ~ p, Monad m) => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> p -> m p Source #
Instances
| APatternLike a b => APatternLike a (FieldAssignment' b) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> FieldAssignment' b -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> FieldAssignment' b -> m (FieldAssignment' b) Source # | |
| APatternLike a b => APatternLike a (Maybe b) Source # | |
| APatternLike a b => APatternLike a [b] Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| APatternLike a b => APatternLike a (Arg b) Source # | |
| APatternLike a (Pattern' a) Source # | |
| (APatternLike a b, APatternLike a c) => APatternLike a (b, c) Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| 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.
mapAPattern :: APatternLike a p => (Pattern' a -> Pattern' a) -> p -> p Source #
Map 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.
checkPatternLinearity :: (Monad m, APatternLike a p) => p -> ([Name] -> m ()) -> m () Source #
Check if any user-written pattern variables occur more than once, and throw the given error if they do.
Specific traversals
substPattern :: [(Name, Pattern)] -> Pattern -> Pattern Source #
Pattern substitution.
For the embedded expression, the given pattern substitution is turned into an expression substitution.
Arguments
| :: (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.
Other pattern utilities
splitOffTrailingWithPatterns :: Patterns -> (Patterns, Patterns) Source #
Split patterns into (patterns, trailing with-patterns).
trailingWithPatterns :: Patterns -> Patterns Source #
Get the tail of with-patterns of a pattern spine.
data LHSPatternView e Source #
The next patterns are ...
(This view discards PatInfo.)
Constructors
| LHSAppP (NAPs e) | Application patterns (non-empty list). |
| LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e)) | A projection pattern. Is also stored unmodified here. |
| LHSWithP [Pattern' e] | With patterns (non-empty list).
These patterns are not prefixed with |
Instances
| Show e => Show (LHSPatternView e) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods showsPrec :: Int -> LHSPatternView e -> ShowS # show :: LHSPatternView e -> String # showList :: [LHSPatternView e] -> ShowS # | |
lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e) Source #
Construct the LHSPatternView of the given list (if not empty).
Return the view and the remaining patterns.
Left-hand-side manipulation
class LHSToSpine a b where Source #
Convert a focused lhs to spine view and back.
Instances
| LHSToSpine LHS SpineLHS Source # | LHS instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| LHSToSpine Clause SpineClause Source # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| LHSToSpine a b => LHSToSpine [a] [b] Source # | List instance (for clauses). |
Defined in Agda.Syntax.Abstract.Pattern | |
lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #
Add applicative patterns (non-projection / non-with patterns) to the right.
lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e Source #
lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #
Add projection, with, and applicative patterns to the right.
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e] Source #
Used for checking pattern linearity.
lhsCoreToPattern :: LHSCore -> Pattern Source #
Used in 'AbstractToConcrete'.
Returns a DefP.