Agda.Syntax.Internal.Pattern

Tools for clauses

clauseArgs :: Clause -> Args

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

Precondition: no projection patterns.

clauseElims :: Clause -> Elims

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

class FunArity a where

Arity of a function, computed from clauses.

Methods

funArity :: a -> Int

Instances

FunArity Clause

Get the number of initial Apply patterns in a clause.

IsProjP p => FunArity [p]

Get the number of initial Apply patterns.

FunArity [Clause]

Get the number of common initial Apply patterns in a list of clauses.

Tools for patterns

class LabelPatVars a b i | b -> i where

Label the pattern variables from left to right using one label for each variable pattern and one for each dot pattern.

Methods

labelPatVars :: a -> State [i] b

Intended, but unpractical due to the absence of type-level lambda, is: labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))

Instances

LabelPatVars a b i => LabelPatVars [a] [b] i

LabelPatVars (Pattern' x) (Pattern' (i, x)) i

LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i

LabelPatVars a b i => LabelPatVars (Arg c a) (Arg c b) i

numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b

Augment pattern variables with their de Bruijn index.

patternsToElims :: Permutation -> [NamedArg Pattern] -> [Elim]

One hole patterns

data OneHolePatterns

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.

Constructors

OHPats [NamedArg Pattern] (NamedArg OneHolePattern) [NamedArg Pattern]

Instances

Show OneHolePatterns

data OneHolePattern

Constructors

Hole

OHCon ConHead ConPatternInfo OneHolePatterns

The type in ConPatternInfo serves the same role as in ConP.

TODO: If a hole is plugged this type may have to be updated in some way.

Instances

Show OneHolePattern

plugHole :: Pattern -> OneHolePatterns -> [NamedArg Pattern]

allHoles :: [NamedArg Pattern] -> [OneHolePatterns]

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)]