ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Internal.Pattern

6 classes
14 values

PackageAgda-2.7.0.1
Exports20
LanguageHaskell2010
LicenceMIT
SourcePattern.hs

Tools for clauses

3 declarations

valueclauseArgs :: Clause -> Args

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

Precondition: no projection patterns.

valueclauseElims :: Clause -> Elims

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

classclass FunArity a where

Arity of a function, computed from clauses.

Methods

funArity :: a -> Int

Instances3FunArity

FunArity ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
Get the number of initial Apply patterns in a clause.
IsProjP p => FunArity [p]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
Get the number of initial Apply patterns.
FunArity [Clause]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
Get the number of common initial Apply patterns in a list of clauses.

Tools for patterns

17 declarations

classclass 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.

Associated types

type family PatVarLabel b

Methods

labelPatVars :: 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)))

Instances4LabelPatVars

LabelPatVars Pattern DeBruijnPatternDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
LabelPatVars a b => LabelPatVars (Arg a) (Arg b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
LabelPatVars a b => LabelPatVars [a] [b]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
LabelPatVars a b => LabelPatVars (Named x a) (Named x b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern

valuenumberPatVars

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

Augment pattern variables with their de Bruijn index.

valueunnumberPatVars :: LabelPatVars a b => b -> a

valuedbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation

valuedbPatPerm' :: 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.

valueclausePerm :: 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.

valuepatternToElim :: Arg DeBruijnPattern -> Elim

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

valuepatternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]

valuepatternToTerm :: DeBruijnPattern -> Term

classclass MapNamedArgPattern a p where

Methods

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

Instances2MapNamedArgPattern

MapNamedArgPattern a (NamedArg (Pattern' a))Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.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.
MapNamedArgPattern a p => MapNamedArgPattern a [p]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern

classclass PatternLike a b where

Generic pattern traversal.

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

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> b -> m
Fold pattern.
traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> b -> m b
Traverse pattern.

Instances4PatternLike

PatternLike a (Pattern' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternLike a b => PatternLike a (Arg b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternLike a b => PatternLike a [b]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternLike a b => PatternLike a (Named x b)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern

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

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

valuepreTraversePatternM

:: (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.

valuepostTraversePatternM

:: (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.

classclass CountPatternVars a where

Methods

countPatternVars :: a -> Int

Instances4CountPatternVars

CountPatternVars (Pattern' x)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
CountPatternVars a => CountPatternVars (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
CountPatternVars a => CountPatternVars [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
CountPatternVars a => CountPatternVars (Named x a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern

classclass PatternVarModalities p where

Associated types

type family PatVar p

Methods

patternVarModalities :: p -> [(PatVar p, Modality)]
Get the list of pattern variables annotated with modalities.

Instances4PatternVarModalities

PatternVarModalities (Pattern' x)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternVarModalities a => PatternVarModalities (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternVarModalities a => PatternVarModalities [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern
PatternVarModalities a => PatternVarModalities (Named s a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Pattern

valuehasDefP :: [NamedArg DeBruijnPattern] -> Bool