ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Concrete.Pattern

Tools for patterns in concrete syntax.

1 type
4 classes
20 values

PackageAgda-2.7.0.1
Exports25
LanguageHaskell2010
LicenceMIT
SourcePattern.hs

classclass IsEllipsis a where

Check for ellipsis ....

Methods

isEllipsis :: a -> Bool

Instances1IsEllipsis

IsEllipsis PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
Is the pattern just ...?

classclass HasEllipsis a where

Has the lhs an occurrence of the ellipsis ...?

Methods

hasEllipsis :: a -> Bool

Instances2HasEllipsis

HasEllipsis LHSDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
Does the lhs contain an ellipsis?
HasEllipsis PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern

classclass IsWithP p where

Check for with-pattern | p.

Methods

isWithP :: p -> Maybe p

Instances4IsWithP

IsWithP PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
IsWithP (Pattern' e)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Pattern · orphan
Check for with-pattern.
IsWithP p => IsWithP (Arg p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
IsWithP p => IsWithP (Named n p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern

LHS manipulation (see also 'Pattern')

8 declarations

datadata LHSPatternView

The next patterns are ...

(This view discards PatInfo.)

Constructors

LHSAppP [NamedArg Pattern]
Application patterns (non-empty list).
LHSWithP [Pattern]
With patterns (non-empty list). These patterns are not prefixed with WithP.

valuelhsPatternView

:: [NamedArg Pattern]
-> Maybe (LHSPatternView, [NamedArg Pattern])

Construct the LHSPatternView of the given list (if not empty).

Return the view and the remaining patterns.

valuelhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore

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

valuelhsCoreWith :: LHSCore -> [Pattern] -> LHSCore

Add with-patterns to the right.

valuelhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore

Append patterns to LHSCore, separating with patterns from the rest.

valuemapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS

Modify the Pattern component in LHS.

valuemapLhsOriginalPatternM

:: (Functor m, Applicative m)
=> Pattern -> m Pattern
-> LHS
-> m LHS

Effectfully modify the Pattern component in LHS.

valuehasCopatterns :: LHSCore -> Bool

Does the LHS contain projection patterns?

Generic fold

5 declarations

classclass CPatternLike p where

Generic pattern traversal.

See APatternLike.

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> p -> m
Fold pattern.
traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p
Traverse pattern with option of post-traversal modification.
traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
Traverse pattern.

Instances9CPatternLike, …

CPatternLike PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (Arg p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (FieldAssignment' p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (List1 p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (List2 p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (Maybe p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike [p]Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
CPatternLike p => CPatternLike (Named n p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
(CPatternLike a, CPatternLike b) => CPatternLike (a, b)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern

valuefoldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m

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

valuepreTraverseCPatternM

:: (CPatternLike p, Monad m)
=> (Pattern -> m Pattern)
pre: Modification before recursion.
-> p
-> m p

Traverse pattern(s) with a modification before the recursive descent.

valuepostTraverseCPatternM

:: (CPatternLike p, Monad m)
=> (Pattern -> m Pattern)
post: Modification after recursion.
-> p
-> m p

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

valuemapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p

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

Specific folds.

8 declarations

valuepatternQNames :: CPatternLike p => p -> [QName]

Get all the identifiers in a pattern in left-to-right order.

Implemented using difference lists.

valuepatternNames :: Pattern -> [Name]

Get all the identifiers in a pattern in left-to-right order.

valuehasWithPatterns :: CPatternLike p => p -> Bool

Does the pattern contain a with-pattern? (Shortcutting.)

valueisWithPattern :: Pattern -> Bool

Is WithP?

valuenumberOfWithPatterns :: CPatternLike p => p -> Int

Count the number of with-subpatterns in a pattern?

valuehasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p

Compute the context in which the ellipsis occurs, if at all. If there are several occurrences, this is an error. This only counts ellipsis that haven't already been expanded.

valuereintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern

valuesplitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p])

Helpers for pattern and lhs parsing

1 declaration

valuepatternAppView :: Pattern -> List1 (NamedArg Pattern)

View a pattern p as a list p0 .. pn where p0 is the identifier (in most cases a constructor).

Pattern needs to be parsed already (operators resolved).