| 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
- patternToExpr :: Pattern -> Expr
- class PatternToExpr p e where
- 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.
patternToExpr :: Pattern -> Expr Source #
Convert a pattern to an expression.
Does not support all cases of patterns.
Result has no Range info, except in identifiers.
This function is only used in expanding pattern synonyms and in Agda.Syntax.Translation.InternalToAbstract, so we can cut some corners.
class PatternToExpr p e where Source #
Converting a pattern to an expression.
The Hiding context is remembered to create instance metas
when translating absurd patterns in instance position.
Minimal complete definition
Nothing
Methods
patToExpr :: p -> Reader Hiding e Source #
default patToExpr :: forall (t :: Type -> Type) p' e'. (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e') => p -> Reader Hiding e Source #
Instances
| PatternToExpr Pattern Expr Source # | |
| PatternToExpr p e => PatternToExpr (Arg p) (Arg e) Source # | |
| PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # | |
Defined in Agda.Syntax.Abstract.Pattern Methods patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e) Source # | |
| PatternToExpr p e => PatternToExpr [p] [e] Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| PatternToExpr p e => PatternToExpr (Named n p) (Named n e) Source # | |
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.