Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Abstract.Pattern

Contents

Generic traversals
Specific folds
Specific traversals
Other pattern utilities
Left-hand-side manipulation
Orphan instances

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
- type ADotT p
- foldrAPattern :: Monoid m => (Pattern' (ADotT p) -> m -> m) -> p -> m
- traverseAPatternM :: Monad m => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
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

type NAP = NamedArg Pattern Source #

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

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source #
MapNamedArgPattern a => MapNamedArgPattern (Maybe a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> Maybe a -> Maybe a Source #
MapNamedArgPattern a => MapNamedArgPattern [a] Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> [a] -> [a] Source #
(MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a, b) Source #
Instance details 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

Associated Types

type ADotT p Source #

Methods

foldrAPattern Source #

Arguments

:: Monoid m
=> (Pattern' (ADotT p) -> m -> m)	Combine a pattern and the value computed from its subpatterns.
-> p
-> m

Fold pattern.

default foldrAPattern :: (Monoid m, Foldable f, APatternLike b, ADotT p ~ ADotT b, f b ~ p) => (Pattern' (ADotT p) -> m -> m) -> p -> m Source #

traverseAPatternM Source #

Arguments

:: Monad m
=> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))	`pre`: Modification before recursion.
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))	`post`: Modification after recursion.
-> p
-> m p

Traverse pattern.

default traverseAPatternM :: (Traversable f, APatternLike q, ADotT p ~ ADotT q, f q ~ p, Monad m) => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p Source #

Instances

Instances details

APatternLike (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Pattern' a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> Pattern' a -> m (Pattern' a) Source #
APatternLike a => APatternLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Arg a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Arg a)) -> m -> m) -> Arg a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> Arg a -> m (Arg a) Source #
APatternLike a => APatternLike (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (FieldAssignment' a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> FieldAssignment' a -> m (FieldAssignment' a) Source #
APatternLike a => APatternLike (Maybe a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Maybe a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Maybe a)) -> m -> m) -> Maybe a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Maybe a)) -> m (Pattern' (ADotT (Maybe a)))) -> (Pattern' (ADotT (Maybe a)) -> m (Pattern' (ADotT (Maybe a)))) -> Maybe a -> m (Maybe a) Source #
APatternLike a => APatternLike [a] Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT [a] Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT [a]) -> m -> m) -> [a] -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT [a]) -> m (Pattern' (ADotT [a]))) -> (Pattern' (ADotT [a]) -> m (Pattern' (ADotT [a]))) -> [a] -> m [a] Source #
APatternLike a => APatternLike (Named n a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Named n a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> Named n a -> m (Named n a) Source #
(APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (a, b) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (a, b)) -> m -> m) -> (a, b) -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))) -> (Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))) -> (a, b) -> m (a, b) Source #

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.

preTraverseAPatternM Source #

Arguments

:: (APatternLike p, Monad m)
=> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))	`pre`: Modification before recursion.
-> 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)))	`post`: Modification after recursion.
-> 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.

substPattern' Source #

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 `WithP`.

Instances

Instances details

Show e => Show (LHSPatternView e) Source #
Instance details 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.

Methods

lhsToSpine :: a -> b Source #

spineToLhs :: b -> a Source #

Instances

Instances details

LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
LHSToSpine a b => LHSToSpine [a] [b] Source #	List instance (for clauses).
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: [a] -> [b] Source # spineToLhs :: [b] -> [a] Source #

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)] Source #

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e Source #

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.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore Source #

Orphan instances

IsWithP (Pattern' e) Source #	Check for with-pattern.
Instance details Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #