Check for ellipsis ....
Methods
isEllipsis :: a -> Bool
Instances1IsEllipsis
IsEllipsis PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternIs the pattern just
...?
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Concrete.Pattern
Tools for patterns in concrete syntax.
Contents
Synopsis
- class IsEllipsis
- class HasEllipsis
- class IsWithP
- data LHSPatternView
- value lhsPatternView
- value lhsCoreApp
- value lhsCoreWith
- value lhsCoreAddSpine
- value mapLhsOriginalPattern
- value mapLhsOriginalPatternM
- value hasCopatterns
- class CPatternLike
- value foldCPattern
- value preTraverseCPatternM
- value postTraverseCPatternM
- value mapCPattern
- value patternQNames
- value patternNames
- value hasWithPatterns
- value isWithPattern
- value numberOfWithPatterns
- value hasEllipsis'
- value reintroduceEllipsis
- value splitEllipsis
- value patternAppView
- PackageAgda-2.8.0.2
- Exports25
- LanguageHaskell2010
- LicenceMIT
- SourcePattern.hs
Has the lhs an occurrence of the ellipsis ...?
Methods
hasEllipsis :: a -> Bool
Instances2HasEllipsis
HasEllipsis LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternDoes the lhs contain an ellipsis?
HasEllipsis PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
Instances4IsWithP
IsWithP PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternIsWithP (Pattern' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern · orphanCheck for with-pattern.
IsWithP p => IsWithP (Arg p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternIsWithP p => IsWithP (Named n p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
LHS manipulation (see also 'Pattern')
Construct the LHSPatternView of the given list (if not empty).
Return the view and the remaining patterns.
Add applicative patterns (non-projection / non-with patterns) to the right.
Add with-patterns to the right.
Append patterns to LHSCore, separating with patterns from the rest.
Does the LHS contain projection patterns?
Generic fold
Generic pattern traversal.
See APatternLike.
Methods
foldrCPattern :: Monoid m => (Pattern -> m -> m) -> p -> mFold pattern.
traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m pTraverse pattern with option of post-traversal modification.
traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m pTraverse pattern.
Instances9CPatternLike, …
CPatternLike PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (Arg p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (FieldAssignment' p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (List1 p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (List2 p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (Maybe p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike [p]Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.PatternCPatternLike p => CPatternLike (Named n p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern(CPatternLike a, CPatternLike b) => CPatternLike (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
Compute a value from each subpattern and collect all values in a monoid.
value
preTraverseCPatternM :: (CPatternLike p, Monad m)=> (Pattern -> m Pattern)pre: Modification before recursion.-> p-> m p
Traverse pattern(s) with a modification before the recursive descent.
value
postTraverseCPatternM :: (CPatternLike p, Monad m)=> (Pattern -> m Pattern)post: Modification after recursion.-> p-> m p
Traverse pattern(s) with a modification after the recursive descent.
Map pattern(s) with a modification after the recursive descent.
Specific folds.
Get all the identifiers in a pattern in left-to-right order.
Implemented using difference lists.
Get all the identifiers in a pattern in left-to-right order.
Does the pattern contain a with-pattern? (Shortcutting.)
Is WithP?
Count the number of with-subpatterns in a pattern?
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.
Helpers for pattern and lhs parsing
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).