Safe Haskell	Safe-Inferred
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 :: (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 :: (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 Source # 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) Source # 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] Source # 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) Source # 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 :: (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 :: (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 :: (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 :: (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) Source # 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) Source # 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] Source # 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) Source # Methods patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)] Source #

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