Agda.Syntax.Abstract.Pattern

Auxiliary functions to handle patterns in the abstract syntax.

Generic and specific traversals.

Generic traversals

type NAP = NamedArg Pattern

class MapNamedArgPattern a where

Minimal complete definition

Nothing

Methods

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

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

Instances

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a

MapNamedArgPattern a => MapNamedArgPattern (Maybe a)

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

MapNamedArgPattern a => MapNamedArgPattern [a]

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> [a] -> [a]

(MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a, b)

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> (a, b) -> (a, b)

class APatternLike p where

Generic pattern traversal.

Minimal complete definition

Nothing

Associated Types

type ADotT p

Methods

foldrAPattern

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

traverseAPatternM

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

Instances

APatternLike (Pattern' a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m

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)

APatternLike a => APatternLike (Arg a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Arg a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Arg a)) -> m -> m) -> Arg a -> m

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)

APatternLike a => APatternLike (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (FieldAssignment' a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m

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)

APatternLike a => APatternLike (Maybe a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Maybe a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Maybe a)) -> m -> m) -> Maybe a -> m

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)

APatternLike a => APatternLike [a]

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT [a]

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT [a]) -> m -> m) -> [a] -> m

traverseAPatternM :: Monad m => (Pattern' (ADotT [a]) -> m (Pattern' (ADotT [a]))) -> (Pattern' (ADotT [a]) -> m (Pattern' (ADotT [a]))) -> [a] -> m [a]

APatternLike a => APatternLike (Named n a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Named n a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m

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)

(APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (a, b)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (a, b)) -> m -> m) -> (a, b) -> m

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)

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

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

preTraverseAPatternM

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

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

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

Specific folds

patternVars :: APatternLike p => p -> [Name]

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

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

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

containsAbsurdPattern :: APatternLike p => p -> Bool

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

Precondition: contains no pattern synonyms.

containsAsPattern :: APatternLike p => p -> Bool

Check if a pattern contains an @-pattern.

checkPatternLinearity :: (Monad m, APatternLike 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)

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.

Methods

lhsToSpine :: a -> b

spineToLhs :: b -> a

Instances

LHSToSpine Clause SpineClause

Clause instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

LHSToSpine LHS SpineLHS

LHS instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine a b => LHSToSpine [a] [b]

List instance (for clauses).

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 -> [Arg (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.

Methods

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