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

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