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.

patternToExpr :: Pattern -> Expr

Convert a pattern to an expression.

Does not support all cases of patterns. Result has no Range' info, except in identifiers.

This function is only used in expanding pattern synonyms and in Agda.Syntax.Translation.InternalToAbstract, so we can cut some corners.

class PatternToExpr p e where

Converting a pattern to an expression.

The Hiding context is remembered to create instance metas when translating absurd patterns in instance position.

Minimal complete definition

Nothing

Methods

patToExpr :: p -> Reader Hiding e

default patToExpr :: (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e') => p -> Reader Hiding e

Instances

PatternToExpr Pattern Expr

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: Pattern -> Reader Hiding Expr

PatternToExpr p e => PatternToExpr (Arg p) (Arg e)

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: Arg p -> Reader Hiding (Arg e)

PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e)

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e)

PatternToExpr p e => PatternToExpr [p] [e]

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: [p] -> Reader Hiding [e]

PatternToExpr p e => PatternToExpr (Named n p) (Named n e)

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: Named n p -> Reader Hiding (Named n e)

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)