| 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 p where
- foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m
- preTraverseAPatternM :: (APatternLike p, Monad m) => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
- postTraverseAPatternM :: (APatternLike p, Monad m) => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
- mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
- patternVars :: APatternLike p => p -> [Name]
- containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool
- containsAbsurdPattern :: APatternLike p => p -> Bool
- containsAsPattern :: APatternLike p => p -> Bool
- checkPatternLinearity :: (Monad m, APatternLike 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 -> [Arg (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 :: forall (f :: Type -> Type) a'. (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 (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source # | |
| MapNamedArgPattern a => MapNamedArgPattern (Maybe a) 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 b) => MapNamedArgPattern (a, b) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> (a, b) -> (a, b) Source # | |
class APatternLike p where Source #
Generic pattern traversal.
Minimal complete definition
Nothing
Methods
Arguments
| :: Monoid m | |
| => (Pattern' (ADotT p) -> m -> m) | Combine a pattern and the value computed from its subpatterns. |
| -> p | |
| -> m |
Fold pattern.
default foldrAPattern :: forall m (f :: Type -> Type) b. (Monoid m, Foldable f, APatternLike b, ADotT p ~ ADotT b, f b ~ p) => (Pattern' (ADotT p) -> m -> m) -> p -> m Source #
Arguments
| :: Monad m | |
| => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) |
|
| -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) |
|
| -> p | |
| -> m p |
Traverse pattern.
Instances
foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m Source #
Compute from each subpattern a value and collect them all in a monoid.
Arguments
| :: (APatternLike p, Monad m) | |
| => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) |
|
| -> p | |
| -> m p |
Traverse pattern(s) with a modification before the recursive descent.
postTraverseAPatternM Source #
Arguments
| :: (APatternLike p, Monad m) | |
| => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) |
|
| -> p | |
| -> m p |
Traverse pattern(s) with a modification after the recursive descent.
mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p Source #
Map pattern(s) with a modification after the recursive descent.
Specific folds
patternVars :: APatternLike p => p -> [Name] Source #
Collect pattern variables in left-to-right textual order.
containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool Source #
Check if a pattern contains a specific (sub)pattern.
containsAbsurdPattern :: APatternLike p => p -> Bool Source #
Check if a pattern contains an absurd pattern.
For instance, suc (), does so.
Precondition: contains no pattern synonyms.
containsAsPattern :: APatternLike p => p -> Bool Source #
Check if a pattern contains an @-pattern.
checkPatternLinearity :: (Monad m, APatternLike 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 Clause SpineClause Source # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| LHSToSpine LHS SpineLHS Source # | LHS 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.
lhsCoreWith :: LHSCore' e -> [Arg (Pattern' e)] -> LHSCore' e Source #
Add 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.