Agda-2.6.20240714: 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 :: forall (f :: Type -> Type) a'. (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 :: forall m (f :: Type -> Type) b. (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 :: forall (f :: Type -> Type) q m. (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) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Pattern' a) = a

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) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Arg a) = ADotT a

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) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Maybe a) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Maybe a) = ADotT a

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] 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT [a] = ADotT a

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) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Named n a) = ADotT a

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) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (a, b) = ADotT a

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.

patternToExpr :: Pattern -> Expr Source #

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

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

default patToExpr :: forall (t :: Type -> Type) p' e'. (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e') => p -> Reader Hiding e Source #

Instances

Instances details
PatternToExpr Pattern Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

patToExpr :: Pattern -> Reader Hiding Expr Source #

PatternToExpr p e => PatternToExpr (Arg p) (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

PatternToExpr p e => PatternToExpr [p] [e] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

PatternToExpr p e => PatternToExpr (Named n p) (Named n e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

Methods

showsPrec :: Int -> LHSPatternView e -> ShowS

show :: LHSPatternView e -> String

showList :: [LHSPatternView e] -> ShowS

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 #