| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal.Pattern
- clauseArgs :: Clause -> Args
- clauseElims :: Clause -> Elims
- class FunArity a where
- class LabelPatVars a b i | b -> i where
- numberPatVars :: LabelPatVars a b Int => Int -> Permutation -> a -> b
- unnumberPatVars :: LabelPatVars a b i => 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 MapNamedArg f where
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.
Minimal complete definition
Tools for patterns
class LabelPatVars a b i | b -> i 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
Methods
labelPatVars :: a -> State [i] 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)))
Instances
| LabelPatVars Pattern DeBruijnPattern Int Source # | |
| LabelPatVars a b i => LabelPatVars [a] [b] i Source # | |
| LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i Source # | |
| LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source # | |
numberPatVars :: LabelPatVars a b Int => Int -> Permutation -> a -> b Source #
Augment pattern variables with their de Bruijn index.
unnumberPatVars :: LabelPatVars a b i => 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 #