Agda.Syntax.Concrete.Pattern

Tools for patterns in concrete syntax.

Documentation

class IsEllipsis a where

Check for ellipsis ....

Methods

isEllipsis :: a -> Bool

Instances

IsEllipsis Pattern

Is the pattern just ...?

Defined in Agda.Syntax.Concrete.Pattern

Methods

isEllipsis :: Pattern -> Bool

class HasEllipsis a where

Has the lhs an occurrence of the ellipsis ...?

Methods

hasEllipsis :: a -> Bool

Instances

HasEllipsis LHS

Does the lhs contain an ellipsis?

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool

HasEllipsis Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: Pattern -> Bool

class IsWithP p where

Check for with-pattern | p.

Minimal complete definition

Nothing

Methods

isWithP :: p -> Maybe p

default isWithP :: forall q (f :: Type -> Type). (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p

Instances

IsWithP Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Pattern -> Maybe Pattern

IsWithP (Pattern' e)

Check for with-pattern.

Defined in Agda.Syntax.Abstract.Pattern

Methods

isWithP :: Pattern' e -> Maybe (Pattern' e)

IsWithP p => IsWithP (Arg p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Arg p -> Maybe (Arg p)

IsWithP p => IsWithP (Named n p)

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.

Minimal complete definition

Nothing

Methods

foldrCPattern

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

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.

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

traverseCPatternM

Arguments

:: Monad m

=> (Pattern -> m Pattern)

pre: Modification before recursion.

-> (Pattern -> m Pattern)

post: Modification after recursion.

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

Instances

CPatternLike Pattern

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 (Arg p)

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)

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 p => CPatternLike (List1 p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List1 p -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List1 p -> m (List1 p)

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List1 p -> m (List1 p)

CPatternLike p => CPatternLike (List2 p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List2 p -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List2 p -> m (List2 p)

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List2 p -> m (List2 p)

CPatternLike p => CPatternLike (Maybe p)

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 [p]

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 (Named n p)

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)

(CPatternLike a, CPatternLike b) => CPatternLike (a, b)

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)

foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m

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

preTraverseCPatternM

Arguments

:: (CPatternLike p, Monad m)

=> (Pattern -> m Pattern)

pre: Modification before recursion.

-> p

-> m p

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

postTraverseCPatternM

Arguments

:: (CPatternLike p, Monad m)

=> (Pattern -> m Pattern)

post: Modification after recursion.

-> p

-> m p

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

mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p

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

Specific folds.

patternQNames :: CPatternLike p => p -> [QName]

Get all the identifiers in a pattern in left-to-right order.

Implemented using difference lists.

patternNames :: Pattern -> [Name]

Get all the identifiers in a pattern in left-to-right order.

hasWithPatterns :: CPatternLike p => p -> Bool

Does the pattern contain a with-pattern? (Shortcutting.)

isWithPattern :: Pattern -> Bool

Is WithP?

numberOfWithPatterns :: CPatternLike p => p -> Int

Count the number of with-subpatterns in a pattern?

hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p

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

splitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p])

Helpers for pattern and lhs parsing

patternAppView :: Pattern -> List1 (NamedArg Pattern)

View a pattern p as a list p0 .. pn where p0 is the identifier (in most cases a constructor).

Pattern needs to be parsed already (operators resolved).