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
- funArity :: a -> Int
class LabelPatVars a b where
- type PatVarLabel b
- labelPatVars :: a -> State [PatVarLabel b] b
- unlabelPatVars :: b -> a
numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b
unnumberPatVars :: LabelPatVars a b => 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
- mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
class PatternLike a b where
- 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
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
- countPatternVars :: a -> Int
class PatternVarModalities p where
- type PatVar p
- patternVarModalities :: p -> [(PatVar p, Modality)]
hasDefP :: [NamedArg DeBruijnPattern] -> Bool

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 :: forall (f :: Type -> Type) a' b'. (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 :: forall (f :: Type -> Type) a' b'. (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
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

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

unlabelPatVars :: DeBruijnPattern -> Pattern Source #

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Arg b)
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Arg b) = PatVarLabel b

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]
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel [b] = PatVarLabel b

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)
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Named x b) = PatVarLabel b

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.

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

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

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.

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

patternToTerm :: DeBruijnPattern -> Term Source #

class MapNamedArgPattern a p where Source #

Minimal complete definition

Nothing

Methods

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

default mapNamedArgPattern :: forall (f :: Type -> Type) p'. (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 Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
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 :: forall m (f :: Type -> Type) p. (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 :: forall (f :: Type -> Type) p m. (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 :: forall (f :: Type -> Type) b. (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 Methods countPatternVars :: Arg a -> Int Source #
CountPatternVars (Pattern' x) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source #
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 #