Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.Pattern

Synopsis

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 #

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.

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.

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

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

CountPatternVars (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

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 #

PatternVarModalities (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x) 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 #