Agda.Syntax.Internal.Pattern

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.

Methods

funArity :: Clause -> Int

IsProjP p => FunArity [p]

Get the number of initial Apply patterns.

Methods

funArity :: [p] -> Int

FunArity [Clause]

Get the number of common initial Apply patterns in a list of clauses.

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

Methods

labelPatVars :: Pattern -> State [Int] DeBruijnPattern

unlabelPatVars :: DeBruijnPattern -> Pattern

LabelPatVars a b i => LabelPatVars [a] [b] i

Methods

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

unlabelPatVars :: [b] -> [a]

LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i

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

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 MapNamedArg f where

Minimal complete definition

mapNamedArg

Methods

mapNamedArg :: (NamedArg a -> NamedArg b) -> NamedArg (f a) -> NamedArg (f b)

Instances

MapNamedArg Pattern'

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.

Methods

mapNamedArg :: (NamedArg a -> NamedArg b) -> NamedArg (Pattern' a) -> NamedArg (Pattern' b)

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)

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]

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)

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)

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.