| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Concrete.Pattern
Description
Tools for patterns in concrete syntax.
Synopsis
- class IsEllipsis a where
- isEllipsis :: a -> Bool
- class HasEllipsis a where
- hasEllipsis :: a -> Bool
- class IsWithP p where
- data LHSPatternView
- lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
- lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
- lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
- lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
- mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
- mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
- hasCopatterns :: LHSCore -> Bool
- class CPatternLike p where
- foldrCPattern :: Monoid m => (Pattern -> m -> m) -> p -> m
- traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p
- traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
- foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
- preTraverseCPatternM :: (CPatternLike p, Monad m) => (Pattern -> m Pattern) -> p -> m p
- postTraverseCPatternM :: (CPatternLike p, Monad m) => (Pattern -> m Pattern) -> p -> m p
- mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
- patternQNames :: CPatternLike p => p -> [QName]
- patternNames :: Pattern -> [Name]
- hasWithPatterns :: CPatternLike p => p -> Bool
- isWithPattern :: Pattern -> Bool
- numberOfWithPatterns :: CPatternLike p => p -> Int
- hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
- reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
- splitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p])
- patternAppView :: Pattern -> List1 (NamedArg Pattern)
Documentation
class IsEllipsis a where Source #
Check for ellipsis ....
Methods
isEllipsis :: a -> Bool Source #
Instances
| IsEllipsis Pattern Source # | Is the pattern just |
Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source # | |
class HasEllipsis a where Source #
Has the lhs an occurrence of the ellipsis ...?
Methods
hasEllipsis :: a -> Bool Source #
Instances
| HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool Source # | |
| HasEllipsis Pattern Source # | |
Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source # | |
class IsWithP p where Source #
Check for with-pattern | p.
Minimal complete definition
Nothing
Methods
LHS manipulation (see also 'Pattern')
data LHSPatternView Source #
The next patterns are ...
(This view discards PatInfo.)
lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern]) Source #
Construct the LHSPatternView of the given list (if not empty).
Return the view and the remaining patterns.
lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore Source #
Add applicative patterns (non-projection / non-with patterns) to the right.
lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore Source #
Append patterns to LHSCore, separating with patterns from the rest.
mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS Source #
hasCopatterns :: LHSCore -> Bool Source #
Does the LHS contain projection patterns?
Generic fold
class CPatternLike p where Source #
Generic pattern traversal.
See APatternLike.
Minimal complete definition
Nothing
Methods
Arguments
| :: Monoid m | |
| => (Pattern -> m -> m) | Combine a pattern and the value computed from its subpatterns. |
| -> p | |
| -> m |
Fold pattern.
default foldrCPattern :: forall m (f :: Type -> Type) q. (Monoid m, Foldable f, CPatternLike q, f q ~ p) => (Pattern -> m -> m) -> p -> m Source #
Arguments
| :: (Applicative m, Functor m) | |
| => (Pattern -> m Pattern -> m Pattern) | Combine a pattern and the its recursively computed version. |
| -> p | |
| -> m p |
Traverse pattern with option of post-traversal modification.
default traverseCPatternA :: forall (f :: Type -> Type) q m. (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p Source #
Arguments
| :: Monad m | |
| => (Pattern -> m Pattern) |
|
| -> (Pattern -> m Pattern) |
|
| -> p | |
| -> m p |
Traverse pattern.
default traverseCPatternM :: forall (f :: Type -> Type) q m. (Traversable f, CPatternLike q, f q ~ p, Monad m) => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p Source #
Instances
foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m Source #
Compute a value from each subpattern and collect all values in a monoid.
Arguments
| :: (CPatternLike p, Monad m) | |
| => (Pattern -> m Pattern) |
|
| -> p | |
| -> m p |
Traverse pattern(s) with a modification before the recursive descent.
postTraverseCPatternM Source #
Arguments
| :: (CPatternLike p, Monad m) | |
| => (Pattern -> m Pattern) |
|
| -> p | |
| -> m p |
Traverse pattern(s) with a modification after the recursive descent.
mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p Source #
Map pattern(s) with a modification after the recursive descent.
Specific folds.
patternQNames :: CPatternLike p => p -> [QName] Source #
Get all the identifiers in a pattern in left-to-right order.
Implemented using difference lists.
patternNames :: Pattern -> [Name] Source #
Get all the identifiers in a pattern in left-to-right order.
hasWithPatterns :: CPatternLike p => p -> Bool Source #
Does the pattern contain a with-pattern? (Shortcutting.)
isWithPattern :: Pattern -> Bool Source #
Is WithP?
numberOfWithPatterns :: CPatternLike p => p -> Int Source #
Count the number of with-subpatterns in a pattern?
hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p Source #
Compute the context in which the ellipsis occurs, if at all. If there are several occurrences, this is an error. This only counts ellipsis that haven't already been expanded.
reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern Source #
splitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p]) Source #