Safe Haskell	None
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
class APatternLike a p | p -> a where
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
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

type NAP = NamedArg Pattern #

class MapNamedArgPattern a where #

Methods

mapNamedArgPattern :: (NAP -> NAP) -> a -> a #

mapNamedArgPattern :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a #

Instances

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

class APatternLike a p | p -> a where #

Generic pattern traversal.

Methods

foldrAPattern #

Arguments

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

Fold pattern.

foldrAPattern #

Arguments

:: (Monoid m, Foldable f, APatternLike a b, f b ~ p)
=> (Pattern' a -> m -> m)	Combine a pattern and the value computed from its subpatterns.
-> p
-> m

Fold pattern.

traverseAPatternM #

Arguments

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

Traverse pattern.

traverseAPatternM #

Arguments

:: (Traversable f, APatternLike a q, f q ~ p, Monad m)
=> (Pattern' a -> m (Pattern' a))	`pre`: Modification before recursion.
-> (Pattern' a -> m (Pattern' a))	`post`: Modification after recursion.
-> p
-> m p

Traverse pattern.

Instances

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

foldAPattern :: (APatternLike a p, Monoid m) => (Pattern' a -> m) -> p -> m #

Compute from each subpattern a value and collect them all in a monoid.

preTraverseAPatternM #

Arguments

:: (APatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))	`pre`: Modification before recursion.
-> b
-> m b

Traverse pattern(s) with a modification before the recursive descent.

postTraverseAPatternM #

Arguments

:: (APatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))	`post`: Modification after recursion.
-> b
-> m b

Traverse pattern(s) with a modification after the recursive descent.

mapAPattern :: APatternLike a p => (Pattern' a -> Pattern' a) -> p -> p #

Map pattern(s) with a modification after the recursive descent.

Specific folds

patternVars :: forall a p. APatternLike a p => p -> [Name] #

Collect pattern variables in left-to-right textual order.

containsAPattern :: APatternLike a p => (Pattern' a -> Bool) -> p -> Bool #

Check if a pattern contains a specific (sub)pattern.

containsAbsurdPattern :: APatternLike a p => p -> Bool #

Check if a pattern contains an absurd pattern. For instance, suc (), does so.

Precondition: contains no pattern synonyms.

containsAsPattern :: APatternLike a p => p -> Bool #

Check if a pattern contains an @-pattern.

Precondition: contains no pattern synonyms.

checkPatternLinearity :: (Monad m, APatternLike a p) => p -> ([Name] -> m ()) -> m () #

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 #

Pattern substitution.

For the embedded expression, the given pattern substitution is turned into an expression substitution.

substPattern' #

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) #

Split patterns into (patterns, trailing with-patterns).

trailingWithPatterns :: Patterns -> Patterns #

Get the tail of with-patterns of a pattern spine.

data LHSPatternView e #

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

Show e => Show (LHSPatternView e) #
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) #

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 #

Convert a focused lhs to spine view and back.

Minimal complete definition

lhsToSpine, spineToLhs

Methods

lhsToSpine :: a -> b #

spineToLhs :: b -> a #

Instances

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

Add applicative patterns (non-projection / non-with patterns) to the right.

lhsCoreWith :: LHSCore' e -> [Pattern' e] -> LHSCore' e #

Add with-patterns to the right.

lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e #

lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e #

Add projection, with, and applicative patterns to the right.

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e] #

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern #

Used in 'AbstractToConcrete'. Returns a DefP.

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

Orphan instances

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