Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Pattern

Description

Auxiliary functions to handle patterns in the abstract syntax.

Generic and specific traversals.

Synopsis

Generic traversals

class MapNamedArgPattern a where Source #

Minimal complete definition

Nothing

Methods

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

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

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

MapNamedArgPattern a => MapNamedArgPattern [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

MapNamedArgPattern a => MapNamedArgPattern (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

class APatternLike a p | p -> a where Source #

Generic pattern traversal.

Minimal complete definition

Nothing

Methods

foldrAPattern Source #

Arguments

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

Combine a pattern and the value computed from its subpatterns.

-> p 
-> m 

Fold pattern.

default foldrAPattern :: (Monoid m, Foldable f, APatternLike a b, f b ~ p) => (Pattern' a -> m -> m) -> p -> m Source #

traverseAPatternM Source #

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.

default traverseAPatternM :: (Traversable f, APatternLike a q, f q ~ p, Monad m) => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> p -> m p Source #

Instances

Instances details
APatternLike a b => APatternLike a (FieldAssignment' b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> FieldAssignment' b -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> FieldAssignment' b -> m (FieldAssignment' b) Source #

APatternLike a b => APatternLike a (Maybe b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Maybe b -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Maybe b -> m (Maybe b) Source #

APatternLike a b => APatternLike a [b] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> [b] -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> [b] -> m [b] Source #

APatternLike a b => APatternLike a (Arg b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #

APatternLike a (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #

(APatternLike a b, APatternLike a c) => APatternLike a (b, c) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> (b, c) -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> (b, c) -> m (b, c) Source #

APatternLike a b => APatternLike a (Named n b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Named n b -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n b) Source #

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

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

preTraverseAPatternM Source #

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

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

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

Specific folds

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

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

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

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

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

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

Precondition: contains no pattern synonyms.

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

Check if a pattern contains an @-pattern.

Precondition: contains no pattern synonyms.

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

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

Pattern substitution.

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

substPattern' Source #

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

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

trailingWithPatterns :: Patterns -> Patterns Source #

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

data LHSPatternView e Source #

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

Instances details
Show e => Show (LHSPatternView e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e) Source #

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

Convert a focused lhs to spine view and back.

Methods

lhsToSpine :: a -> b Source #

spineToLhs :: b -> a Source #

Instances

Instances details
LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine a b => LHSToSpine [a] [b] Source #

List instance (for clauses).

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: [a] -> [b] Source #

spineToLhs :: [b] -> [a] Source #

lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #

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

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

Add with-patterns to the right.

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

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

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

Used for checking pattern linearity.

Orphan instances

IsWithP (Pattern' e) Source #

Check for with-pattern.

Instance details

Methods

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