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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Internal.Pattern

Contents

- Tools for clauses
- Tools for patterns

Synopsis

- clauseArgs :: Clause -> Args
- clauseElims :: Clause -> Elims
- class FunArity a where
  - funArity :: a -> Int
- class LabelPatVars a b where
  - type PatVarLabel b
  - labelPatVars :: a -> State [PatVarLabel b] b
  - unlabelPatVars :: b -> a
- numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b
- unnumberPatVars :: LabelPatVars a b => b -> a
- dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
- dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
- clausePerm :: Clause -> Maybe Permutation
- patternToElim :: Arg DeBruijnPattern -> Elim
- patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
- patternToTerm :: DeBruijnPattern -> Term
- class MapNamedArgPattern a p where
  - mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
- class PatternLike a b where
  - foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> b -> m
  - traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> b -> m b
- foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m
- preTraversePatternM :: (PatternLike a b, Monad m) => (Pattern' a -> m (Pattern' a)) -> b -> m b
- postTraversePatternM :: (PatternLike a b, Monad m) => (Pattern' a -> m (Pattern' a)) -> b -> m b
- class CountPatternVars a where
  - countPatternVars :: a -> Int
- class PatternVarModalities p where
  - type PatVar p
  - patternVarModalities :: p -> [(PatVar p, Modality)]
- hasDefP :: [NamedArg DeBruijnPattern] -> Bool

# Tools for clauses

clauseArgs :: Clause -> Args Source #

Translate the clause patterns to terms with free variables bound by the clause telescope.

Precondition: no projection patterns.

clauseElims :: Clause -> Elims Source #

Translate the clause patterns to an elimination spine with free variables bound by the clause telescope.

class FunArity a where Source #

Arity of a function, computed from clauses.

Methods

funArity :: a -> Int Source #

#### Instances

Instances details

FunArity Clause Source # | Get the number of initial `Apply` patterns in a clause.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: Clause -> Int Source #
FunArity [Clause] Source # | Get the number of common initial `Apply` patterns in a list of clauses.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: [Clause] -> Int Source #
IsProjP p => FunArity [p] Source # | Get the number of initial `Apply` patterns.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: [p] -> Int Source #

# Tools for patterns

class LabelPatVars a b where Source #

Label the pattern variables from left to right using one label for each variable pattern and one for each dot pattern.

Minimal complete definition

Nothing

Associated Types

type PatVarLabel b Source #

Methods

labelPatVars :: a -> State [PatVarLabel b] b Source #

default labelPatVars :: forall (f :: Type -> Type) a' b'. (Traversable f, LabelPatVars a' b', PatVarLabel b ~ PatVarLabel b', f a' ~ a, f b' ~ b) => a -> State [PatVarLabel b] b Source #

unlabelPatVars :: b -> a Source #

Intended, but unpractical due to the absence of type-level lambda, is: `labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))`

default unlabelPatVars :: forall (f :: Type -> Type) a' b'. (Traversable f, LabelPatVars a' b', f a' ~ a, f b' ~ b) => b -> a Source #

#### Instances

Instances details

LabelPatVars Pattern DeBruijnPattern Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source #

unlabelPatVars :: DeBruijnPattern -> Pattern Source #

LabelPatVars a b => LabelPatVars (Arg a) (Arg b) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Arg b) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Arg b) = PatVarLabel b

Methods

labelPatVars :: Arg a -> State [PatVarLabel (Arg b)] (Arg b) Source #

unlabelPatVars :: Arg b -> Arg a Source #

LabelPatVars a b => LabelPatVars [a] [b] Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel [b] |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel [b] = PatVarLabel b

Methods

labelPatVars :: [a] -> State [PatVarLabel [b]] [b] Source #

unlabelPatVars :: [b] -> [a] Source #

LabelPatVars a b => LabelPatVars (Named x a) (Named x b) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Named x b) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Named x b) = PatVarLabel b

Methods

labelPatVars :: Named x a -> State [PatVarLabel (Named x b)] (Named x b) Source #

unlabelPatVars :: Named x b -> Named x a Source #

numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b Source #

Augment pattern variables with their de Bruijn index.

unnumberPatVars :: LabelPatVars a b => b -> a Source #

dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation Source #

dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation Source #

Computes the permutation from the clause telescope to the pattern variables.

Use as `fromMaybe IMPOSSIBLE . dbPatPerm` to crash in a controlled way if a de Bruijn index is out of scope here.

The first argument controls whether dot patterns counts as variables or not.

clausePerm :: Clause -> Maybe Permutation Source #

Computes the permutation from the clause telescope to the pattern variables.

Use as `fromMaybe IMPOSSIBLE . clausePerm` to crash in a controlled way if a de Bruijn index is out of scope here.

patternToElim :: Arg DeBruijnPattern -> Elim Source #

Turn a pattern into a term. Projection patterns are turned into projection eliminations, other patterns into apply elimination.

patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim] Source #

patternToTerm :: DeBruijnPattern -> Term Source #

class MapNamedArgPattern a p where Source #

Minimal complete definition

Nothing

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p Source #

default mapNamedArgPattern :: forall (f :: Type -> Type) p'. (Functor f, MapNamedArgPattern a p', p ~ f p') => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p Source #

#### Instances

Instances details

MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
MapNamedArgPattern a p => MapNamedArgPattern a [p] Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> [p] -> [p] Source #

class PatternLike a b where Source #

Generic pattern traversal.

Pre-applies a pattern modification, recurses, and post-applies another one.

Minimal complete definition

Nothing

Methods

foldrPattern Source #

Arguments

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

Fold pattern.

default foldrPattern :: forall m (f :: Type -> Type) p. (Monoid m, Foldable f, PatternLike a p, f p ~ b) => (Pattern' a -> m -> m) -> b -> m Source #

traversePatternM Source #

Arguments

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

Traverse pattern.

default traversePatternM :: forall (f :: Type -> Type) p m. (Traversable f, PatternLike a p, f p ~ b, Monad m) => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> b -> m b Source #

#### Instances

Instances details

PatternLike a b => PatternLike a (Arg b) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #
PatternLike a (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #
PatternLike a b => PatternLike a [b] Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> [b] -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> [b] -> m [b] Source #
PatternLike a b => PatternLike a (Named x b) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b) Source #

foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m Source #

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

preTraversePatternM Source #

Arguments

:: (PatternLike a b, Monad m) |
=> (Pattern' a -> m (Pattern' a)) | `pre`: Modification before recursion.
-> b |
-> m b |

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

postTraversePatternM Source #

Arguments

:: (PatternLike a b, Monad m) |
=> (Pattern' a -> m (Pattern' a)) | `post`: Modification after recursion.
-> b |
-> m b |

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

class CountPatternVars a where Source #

Minimal complete definition

Nothing

Methods

countPatternVars :: a -> Int Source #

default countPatternVars :: forall (f :: Type -> Type) b. (Foldable f, CountPatternVars b, f b ~ a) => a -> Int Source #

#### Instances

Instances details

CountPatternVars a => CountPatternVars (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Arg a -> Int Source #
CountPatternVars (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source #
CountPatternVars a => CountPatternVars [a] Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: [a] -> Int Source #
CountPatternVars a => CountPatternVars (Named x a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int Source #

class PatternVarModalities p where Source #

Associated Types

type PatVar p Source #

Methods

patternVarModalities :: p -> [(PatVar p, Modality)] Source #

Get the list of pattern variables annotated with modalities.

#### Instances

Instances details

PatternVarModalities a => PatternVarModalities (Arg a) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Arg a) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Arg a) = PatVar a

Methods

patternVarModalities :: Arg a -> [(PatVar (Arg a), Modality)] Source #

PatternVarModalities (Pattern' x) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Pattern' x) = x

Methods

patternVarModalities :: Pattern' x -> [(PatVar (Pattern' x), Modality)] Source #

PatternVarModalities a => PatternVarModalities [a] Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar [a] |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar [a] = PatVar a

Methods

patternVarModalities :: [a] -> [(PatVar [a], Modality)] Source #

PatternVarModalities a => PatternVarModalities (Named s a) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Named s a) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Named s a) = PatVar a

Methods

patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)] Source #

hasDefP :: [NamedArg DeBruijnPattern] -> Bool Source #