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
class LabelPatVars a b i | b -> i where
numberPatVars :: LabelPatVars a b Int => Int -> Permutation -> a -> b
unnumberPatVars :: LabelPatVars a b i => 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
class PatternLike a b where
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
class PatternVarModalities p x | p -> x where

Tools for clauses

clauseArgs :: Clause -> Args #

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

Precondition: no projection patterns.

clauseElims :: Clause -> Elims #

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

class FunArity a where #

Arity of a function, computed from clauses.

Minimal complete definition

funArity

Methods

funArity :: a -> Int #

Instances

FunArity Clause #	Get the number of initial `Apply` patterns in a clause.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: Clause -> Int #
IsProjP p => FunArity [p] #	Get the number of initial `Apply` patterns.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: [p] -> Int #
FunArity [Clause] #	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 #

Tools for patterns

class LabelPatVars a b i | b -> i where #

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

Methods

labelPatVars :: a -> State [i] b #

unlabelPatVars :: b -> a #

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

labelPatVars :: (Traversable f, LabelPatVars a' b' i, f a' ~ a, f b' ~ b) => a -> State [i] b #

unlabelPatVars :: (Traversable f, LabelPatVars a' b' i, f a' ~ a, f b' ~ b) => b -> a #

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

Instances

LabelPatVars Pattern DeBruijnPattern Int #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern # unlabelPatVars :: DeBruijnPattern -> Pattern #
LabelPatVars a b i => LabelPatVars [a] [b] i #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: [a] -> State [i] [b] # unlabelPatVars :: [b] -> [a] #
LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Arg a -> State [i] (Arg b) # unlabelPatVars :: Arg b -> Arg a #
LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Named x a -> State [i] (Named x b) # unlabelPatVars :: Named x b -> Named x a #

numberPatVars :: LabelPatVars a b Int => Int -> Permutation -> a -> b #

Augment pattern variables with their de Bruijn index.

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

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

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

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 #

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 #

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

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

patternToTerm :: DeBruijnPattern -> Term #

class MapNamedArgPattern a p where #

Methods

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

mapNamedArgPattern :: (Functor f, MapNamedArgPattern a p', p ~ f p') => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p #

Instances

MapNamedArgPattern a p => MapNamedArgPattern a [p] #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> [p] -> [p] #
MapNamedArgPattern a (NamedArg (Pattern' a)) #	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) #

class PatternLike a b where #

Generic pattern traversal.

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

Methods

foldrPattern #

Arguments

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

Fold pattern.

foldrPattern #

Arguments

:: (Monoid m, Foldable f, PatternLike a p, f p ~ b)
=> (Pattern' a -> m -> m)	Combine a pattern and the value computed from its subpatterns.
-> b
-> m

Fold pattern.

traversePatternM #

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.

traversePatternM #

Arguments

:: (Traversable f, PatternLike a p, f p ~ b, 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.

Instances

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

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

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

preTraversePatternM #

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 #

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 #

Methods

countPatternVars :: a -> Int #

countPatternVars :: (Foldable f, CountPatternVars b, f b ~ a) => a -> Int #

Instances

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

class PatternVarModalities p x | p -> x where #

Minimal complete definition

patternVarModalities

Methods

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

Get the list of pattern variables annotated with modalities.

Instances

PatternVarModalities a x => PatternVarModalities [a] x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: [a] -> [(x, Modality)] #
PatternVarModalities a x => PatternVarModalities (Arg a) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Arg a -> [(x, Modality)] #
PatternVarModalities (Pattern' x) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Pattern' x -> [(x, Modality)] #
PatternVarModalities a x => PatternVarModalities (Elim' a) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Elim' a -> [(x, Modality)] #
PatternVarModalities a x => PatternVarModalities (Named s a) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Named s a -> [(x, Modality)] #