HasEllipsis LHS #	Does the lhs contain an ellipsis?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool #
HasEllipsis Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool #

class IsWithP p where #

Check for with-pattern | p.

Methods

isWithP :: p -> Maybe p #

isWithP :: (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p #

Instances

IsWithP Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Pattern -> Maybe Pattern #
IsWithP p => IsWithP (Arg p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Arg p -> Maybe (Arg p) #
IsWithP (Pattern' e) #	Check for with-pattern.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) #
IsWithP p => IsWithP (Named n p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Named n p -> Maybe (Named n p) #

LHS manipulation (see also '`Pattern'`)

data LHSPatternView #

The next patterns are ...

(This view discards PatInfo.)

Constructors

LHSAppP [NamedArg Pattern]	Application patterns (non-empty list).
LHSWithP [Pattern]	With patterns (non-empty list). These patterns are not prefixed with `WithP`.

lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern]) #

Construct the LHSPatternView of the given list (if not empty).

Return the view and the remaining patterns.

lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore #

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

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

Add with-patterns to the right.

lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore #

Append patterns to LHSCore, separating with patterns from the rest.

mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS #

Modify the Pattern component in LHS.

mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS #

Effectfully modify the Pattern component in LHS.

hasCopatterns :: LHSCore -> Bool #

Does the LHS contain projection patterns?

Generic fold

class CPatternLike p where #

Generic pattern traversal.

See APatternLike.

Methods

foldrCPattern #

Arguments

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

Fold pattern.

foldrCPattern #

Arguments

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

Fold pattern.

traverseCPatternA #

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.

traverseCPatternA #

Arguments

:: (Traversable f, CPatternLike q, f q ~ p, 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.

traverseCPatternM #

Arguments

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

Traverse pattern.

traverseCPatternM #

Arguments

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

Traverse pattern.

Instances

CPatternLike Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern #
CPatternLike p => CPatternLike [p] #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods 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] #
CPatternLike p => CPatternLike (Maybe p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Maybe p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Maybe p -> m (Maybe p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Maybe p -> m (Maybe p) #
CPatternLike p => CPatternLike (Arg p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) #
CPatternLike p => CPatternLike (FieldAssignment' p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) #
(CPatternLike a, CPatternLike b) => CPatternLike (a, b) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> (a, b) -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> (a, b) -> m (a, b) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> (a, b) -> m (a, b) #
CPatternLike p => CPatternLike (Named n p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) #