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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract.Pattern

Contents

- Generic traversals
- Specific folds
- Specific traversals
- Other pattern utilities
- Left-hand-side manipulation
- Orphan instances

Description

Auxiliary functions to handle patterns in the abstract syntax.

Generic and specific traversals.

Synopsis

- type NAP = NamedArg Pattern
- class MapNamedArgPattern a where
  - mapNamedArgPattern :: (NAP -> NAP) -> a -> a
- class APatternLike p where
  - type ADotT p
  - foldrAPattern :: Monoid m => (Pattern' (ADotT p) -> m -> m) -> p -> m
  - traverseAPatternM :: Monad m => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
- foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m
- preTraverseAPatternM :: (APatternLike p, Monad m) => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
- postTraverseAPatternM :: (APatternLike p, Monad m) => (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
- mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
- patternVars :: APatternLike p => p -> [Name]
- containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool
- containsAbsurdPattern :: APatternLike p => p -> Bool
- containsAsPattern :: APatternLike p => p -> Bool
- checkPatternLinearity :: (Monad m, APatternLike p) => p -> (List1 Name -> m ()) -> m ()
- substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
- substPattern' :: (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
- patternToExpr :: Pattern -> Expr
- class PatternToExpr p e where
  - patToExpr :: p -> Reader Hiding e
- noDotOrEqPattern :: Monad m => m (Pattern' Void) -> Pattern' e -> m (Pattern' Void)
- splitOffTrailingWithPatterns :: Patterns -> (Patterns, Patterns)
- trailingWithPatterns :: Patterns -> Patterns
- data LHSPatternView e
  - = LHSAppP (NAPs1 e)
  - | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
  - | LHSWithP (List1 (Pattern' e))
- lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
- class LHSToSpine a b where
  - 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
- lhsCoreWith :: LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
- lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
- lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
- lhsCoreToPattern :: LHSCore -> Pattern
- mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore

# Generic traversals

type NAP = NamedArg Pattern Source #

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 Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source #
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 type ADotT (FieldAssignment' a) = ADotT a

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m Source #

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

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 -> (List1 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 Methods patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e) Source #
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 #

noDotOrEqPattern Source #

Arguments

:: Monad m |
=> m (Pattern' Void) | Exception or replacement for dot (etc.) patterns.
-> Pattern' e | In pattern.
-> m (Pattern' Void) | Out pattern.

Make sure that there are no dot or equality patterns (called on pattern synonyms). Also disallows annotated patterns.

# 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 (NAPs1 e) | Application patterns (non-empty list).
LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e)) | A projection pattern. Is also stored unmodified here.
LHSWithP (List1 (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 Source # show :: LHSPatternView e -> String Source # showList :: [LHSPatternView e] -> ShowS Source #

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 Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source # | LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
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 #

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)] Source #

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e Source #

lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #

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

lhsCoreWith :: LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e Source #

Add with-patterns to the right.

lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e Source #

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.

lhsCoreToPattern :: LHSCore -> Pattern Source #

Used in '`AbstractToConcrete'`. Returns a `DefP`.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore Source #

# Orphan instances

IsWithP (Pattern' e) Source # | Check for with-pattern.
Instance details Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #