Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Pattern

Contents

- LHS manipulation (see also '`Pattern'`)
- Generic fold
- Specific folds.
- Helpers for pattern and lhs parsing

Description

Tools for patterns in concrete syntax.

Synopsis

- class IsEllipsis a where
  - isEllipsis :: a -> Bool
- class HasEllipsis a where
  - hasEllipsis :: a -> Bool
- class IsWithP p where
  - isWithP :: p -> Maybe p
- data LHSPatternView
  - = LHSAppP (List1 (NamedArg Pattern))
  - | LHSWithP (List1 Pattern)
- lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
- lhsCoreApp :: LHSCore -> List1 (NamedArg Pattern) -> LHSCore
- lhsCoreWith :: LHSCore -> List1 Pattern -> LHSCore
- lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
- mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
- mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
- hasCopatterns :: LHSCore -> Bool
- class CPatternLike p where
  - foldrCPattern :: Monoid m => (Pattern -> m -> m) -> p -> m
  - traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p
  - traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
- foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
- preTraverseCPatternM :: (CPatternLike p, Monad m) => (Pattern -> m Pattern) -> p -> m p
- postTraverseCPatternM :: (CPatternLike p, Monad m) => (Pattern -> m Pattern) -> p -> m p
- mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
- patternQNames :: CPatternLike p => p -> [QName]
- patternNames :: Pattern -> [Name]
- hasWithPatterns :: CPatternLike p => p -> Bool
- isWithPattern :: Pattern -> Bool
- numberOfWithPatterns :: CPatternLike p => p -> Int
- hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
- reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
- splitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p])
- patternAppView :: Pattern -> List1 (NamedArg Pattern)

# Documentation

class IsEllipsis a where Source #

Check for ellipsis `...`.

Methods

isEllipsis :: a -> Bool Source #

#### Instances

Instances details

IsEllipsis Pattern Source # | Is the pattern just `...`?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source #

class HasEllipsis a where Source #

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

Methods

hasEllipsis :: a -> Bool Source #

#### Instances

Instances details

HasEllipsis LHS Source # | Does the lhs contain an ellipsis?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool Source #
HasEllipsis Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source #

class IsWithP p where Source #

Check for with-pattern `| p`.

Minimal complete definition

Nothing

Methods

isWithP :: p -> Maybe p Source #

default isWithP :: forall q (f :: Type -> Type). (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p Source #

#### Instances

Instances details

IsWithP Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Pattern -> Maybe Pattern Source #
IsWithP (Pattern' e) Source # | Check for with-pattern.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #
IsWithP p => IsWithP (Arg p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Arg p -> Maybe (Arg p) Source #
IsWithP p => IsWithP (Named n p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Named n p -> Maybe (Named n p) Source #

# LHS manipulation (see also '`Pattern'`)

data LHSPatternView Source #

The next patterns are ...

(This view discards `PatInfo`.)

Constructors

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

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

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

Return the view and the remaining patterns.

lhsCoreApp :: LHSCore -> List1 (NamedArg Pattern) -> LHSCore Source #

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

lhsCoreWith :: LHSCore -> List1 Pattern -> LHSCore Source #

Add with-patterns to the right.

lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore Source #

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

mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS Source #

Modify the `Pattern` component in `LHS`.

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

Effectfully modify the `Pattern` component in `LHS`.

hasCopatterns :: LHSCore -> Bool Source #

Does the LHS contain projection patterns?

# Generic fold

class CPatternLike p where Source #

Generic pattern traversal.

See `APatternLike`.

Minimal complete definition

Nothing

Methods

foldrCPattern Source #

Arguments

:: Monoid m |
=> (Pattern -> m -> m) | Combine a pattern and the value computed from its subpatterns.
-> p |
-> m |

Fold pattern.

default foldrCPattern :: forall m (f :: Type -> Type) q. (Monoid m, Foldable f, CPatternLike q, f q ~ p) => (Pattern -> m -> m) -> p -> m Source #

traverseCPatternA Source #

Arguments

:: (Applicative m, Functor m) |
=> (Pattern -> m Pattern -> m Pattern) | Combine a pattern and the its recursively computed version.
-> p |
-> m p |

Traverse pattern with option of post-traversal modification.

default traverseCPatternA :: forall (f :: Type -> Type) q m. (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> p -> m p Source #

traverseCPatternM Source #

Arguments

:: Monad m |
=> (Pattern -> m Pattern) | `pre`: Modification before recursion.
-> (Pattern -> m Pattern) | `post`: Modification after recursion.
-> p |
-> m p |

Traverse pattern.

default traverseCPatternM :: forall (f :: Type -> Type) q m. (Traversable f, CPatternLike q, f q ~ p, Monad m) => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p Source #

#### Instances

Instances details

CPatternLike Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern Source #
CPatternLike p => CPatternLike (Arg p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #
CPatternLike p => CPatternLike (FieldAssignment' p) Source # |

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

CPatternLike p => CPatternLike (List1 p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List1 p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List1 p -> m (List1 p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List1 p -> m (List1 p) Source #
CPatternLike p => CPatternLike (List2 p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List2 p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List2 p -> m (List2 p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List2 p -> m (List2 p) Source #
CPatternLike p => CPatternLike (Maybe p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Maybe p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source #
CPatternLike p => CPatternLike [p] Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> [p] -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> [p] -> m [p] Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> [p] -> m [p] Source #
CPatternLike p => CPatternLike (Named n p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #
(CPatternLike a, CPatternLike b) => CPatternLike (a, b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> (a, b) -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> (a, b) -> m (a, b) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> (a, b) -> m (a, b) Source #

foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m Source #

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

preTraverseCPatternM Source #

Arguments

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

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

postTraverseCPatternM Source #

Arguments

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

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

mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p Source #

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

# Specific folds.

patternQNames :: CPatternLike p => p -> [QName] Source #

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

Implemented using difference lists.

patternNames :: Pattern -> [Name] Source #

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

hasWithPatterns :: CPatternLike p => p -> Bool Source #

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

isWithPattern :: Pattern -> Bool Source #

Is `WithP`?

numberOfWithPatterns :: CPatternLike p => p -> Int Source #

Count the number of with-subpatterns in a pattern?

hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p Source #

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.

reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern Source #

splitEllipsis :: IsWithP p => Int -> [p] -> ([p], [p]) Source #

# Helpers for pattern and lhs parsing

patternAppView :: Pattern -> List1 (NamedArg Pattern) Source #

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).