Safe Haskell | None |
---|---|
Language | Haskell98 |
- clauseArgs :: Clause -> Args
- clauseElims :: Clause -> Elims
- class FunArity a where
- class LabelPatVars a b i | b -> i where
- labelPatVars :: a -> State [i] b
- numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
- patternsToElims :: Permutation -> [NamedArg Pattern] -> [Elim]
- data OneHolePatterns = OHPats [NamedArg Pattern] (NamedArg OneHolePattern) [NamedArg Pattern]
- data OneHolePattern
- plugHole :: Pattern -> OneHolePatterns -> [NamedArg Pattern]
- allHoles :: [NamedArg Pattern] -> [OneHolePatterns]
- allHolesWithContents :: [NamedArg Pattern] -> [(Pattern, OneHolePatterns)]
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.
Arity of a function, computed from clauses.
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.
labelPatVars :: a -> State [i] b Source
Intended, but unpractical due to the absence of type-level lambda, is:
labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))
LabelPatVars a b i => LabelPatVars [a] [b] i Source | |
LabelPatVars (Pattern' x) (Pattern' (i, x)) i Source | |
LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source | |
LabelPatVars a b i => LabelPatVars (Arg c a) (Arg c b) i Source |
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b Source
Augment pattern variables with their de Bruijn index.
patternsToElims :: Permutation -> [NamedArg Pattern] -> [Elim] Source
One hole patterns
data OneHolePatterns Source
A OneholePattern
is a linear pattern context P
such that for
any non-projection pattern p
, inserting p
into the single hole P[p]
,
yields again a non-projection pattern.
data OneHolePattern Source
Hole | |
OHCon ConHead ConPatternInfo OneHolePatterns | The type in TODO: If a hole is plugged this type may have to be updated in some way. |
allHoles :: [NamedArg Pattern] -> [OneHolePatterns] Source
allHoles ps
returns for each pattern variable x
in ps
a
context P
such P[x]
is one of the patterns of ps
.
The Ps
are returned in the left-to-right order of the
pattern variables in ps
.
allHolesWithContents :: [NamedArg Pattern] -> [(Pattern, OneHolePatterns)] Source