Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Pattern

Description

Tools for patterns in concrete syntax.

Synopsis

Documentation

class IsEllipsis a where Source #

Check for ellipsis ....

Methods

isEllipsis :: a -> Bool Source #

Instances

Instances details
IsEllipsis Pattern Source #

Is the pattern just ...?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isEllipsis :: Pattern -> Bool Source #

class HasEllipsis a where Source #

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

Methods

hasEllipsis :: a -> Bool Source #

Instances

Instances details
HasEllipsis LHS Source #

Does the lhs contain an ellipsis?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool Source #

HasEllipsis Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: Pattern -> Bool Source #

class IsWithP p where Source #

Check for with-pattern | p.

Minimal complete definition

Nothing

Methods

isWithP :: p -> Maybe p Source #

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

Instances

Instances details
IsWithP Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Pattern -> Maybe Pattern Source #

IsWithP (Pattern' e) Source #

Check for with-pattern.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

IsWithP p => IsWithP (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

IsWithP p => IsWithP (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Named n p -> Maybe (Named n p) Source #

LHS manipulation (see also 'Pattern')

data LHSPatternView Source #

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

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

Return the view and the remaining patterns.

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

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

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

Add with-patterns to the right.

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

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

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

Modify the Pattern component in LHS.

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

Effectfully modify the Pattern component in LHS.

hasCopatterns :: LHSCore -> Bool Source #

Does the LHS contain projection patterns?

Generic fold

class CPatternLike p where Source #

Generic pattern traversal.

See APatternLike.

Minimal complete definition

Nothing

Methods

foldrCPattern Source #

Arguments

:: Monoid m 
=> (Pattern -> m -> m)

Combine a pattern and the value computed from its subpatterns.

-> p 
-> m 

Fold pattern.

default foldrCPattern :: (Monoid m, Foldable f, CPatternLike q, f q ~ p) => (Pattern -> m -> m) -> p -> m Source #

traverseCPatternA Source #

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 :: (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p Source #

traverseCPatternM Source #

Arguments

:: Monad m 
=> (Pattern -> m Pattern)

pre: Modification before recursion.

-> (Pattern -> m Pattern)

post: Modification after recursion.

-> p 
-> m p 

Traverse pattern.

default traverseCPatternM :: (Traversable f, CPatternLike q, f q ~ p, Monad m) => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p Source #

Instances

Instances details
CPatternLike Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern Source #

CPatternLike p => CPatternLike (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

CPatternLike p => CPatternLike (FieldAssignment' p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

CPatternLike p => CPatternLike (List1 p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

CPatternLike p => CPatternLike (List2 p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

CPatternLike p => CPatternLike (Maybe p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Maybe p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source #

CPatternLike p => CPatternLike [p] Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> [p] -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> [p] -> m [p] Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> [p] -> m [p] Source #

CPatternLike p => CPatternLike (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

(CPatternLike a, CPatternLike b) => CPatternLike (a, b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> (a, b) -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> (a, b) -> m (a, b) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> (a, b) -> m (a, b) Source #

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

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

preTraverseCPatternM Source #

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

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

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

Specific folds.

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

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

Implemented using difference lists.

patternNames :: Pattern -> [Name] Source #

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

hasWithPatterns :: CPatternLike p => p -> Bool Source #

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

numberOfWithPatterns :: CPatternLike p => p -> Int Source #

Count the number of with-subpatterns in a pattern?

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

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.

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

Helpers for pattern and lhs parsing

patternAppView :: Pattern -> List1 (NamedArg Pattern) Source #

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