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.

Methods

funArity :: a -> Int

Instances

FunArity Clause

Get the number of initial Apply patterns in a clause.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int

FunArity [Clause]

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

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int

IsProjP p => FunArity [p]

Get the number of initial Apply patterns.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [p] -> Int

Tools for patterns

class LabelPatVars a b where

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

Methods

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

default labelPatVars :: (Traversable f, LabelPatVars a' b', PatVarLabel b ~ PatVarLabel b', f a' ~ a, f b' ~ b) => a -> State [PatVarLabel b] 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)))

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

Instances

LabelPatVars Pattern DeBruijnPattern

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern

Methods

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

unlabelPatVars :: DeBruijnPattern -> Pattern

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Arg b)

Methods

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

unlabelPatVars :: Arg b -> Arg a

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel [b]

Methods

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

unlabelPatVars :: [b] -> [a]

LabelPatVars a b => LabelPatVars (Named x a) (Named x b)

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Named x b)

Methods

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

unlabelPatVars :: Named x b -> Named x a

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

Augment pattern variables with their de Bruijn index.

unnumberPatVars :: LabelPatVars a b => 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

Minimal complete definition

Nothing

Methods

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

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

Instances

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.

Defined in Agda.Syntax.Internal.Pattern

Methods

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

MapNamedArgPattern a p => MapNamedArgPattern a [p]

Defined in Agda.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> [p] -> [p]

class PatternLike a b where

Generic pattern traversal.

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

Minimal complete definition

Nothing

Methods

foldrPattern

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

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.

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

Instances

PatternLike a b => PatternLike a (Arg b)

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 (Pattern' a)

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 [b]

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 b => PatternLike a (Named x b)

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

Minimal complete definition

Nothing

Methods

countPatternVars :: a -> Int

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

Instances

CountPatternVars a => CountPatternVars (Arg a)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Arg a -> Int

CountPatternVars (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Pattern' x -> Int

CountPatternVars a => CountPatternVars [a]

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: [a] -> Int

CountPatternVars a => CountPatternVars (Named x a)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int

class PatternVarModalities p where

Associated Types

type PatVar p

Methods

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

Get the list of pattern variables annotated with modalities.

Instances

PatternVarModalities a => PatternVarModalities (Arg a)

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Arg a)

Methods

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

PatternVarModalities (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x)

Methods

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

PatternVarModalities a => PatternVarModalities [a]

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar [a]

Methods

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

PatternVarModalities a => PatternVarModalities (Named s a)

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Named s a)

Methods

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

hasDefP :: [NamedArg DeBruijnPattern] -> Bool