Agda-2.6.2.2.20221128: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

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 [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

(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 p where Source #

Generic pattern traversal.

Minimal complete definition

Nothing

Associated Types

type ADotT p Source #

Methods

foldrAPattern Source #

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

traverseAPatternM Source #

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

Instances

Instances details
APatternLike (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Arg a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (FieldAssignment' a) Source #

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Maybe a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT [a] Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Named n a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (a, b) Source #

Methods

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

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

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

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

preTraverseAPatternM Source #

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

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

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

Specific folds

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

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

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

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

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

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

Precondition: contains no pattern synonyms.

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

Check if a pattern contains an @-pattern.

checkPatternLinearity :: (Monad m, APatternLike 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 Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS 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 -> [Arg (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 #