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.

Minimal complete definition

funArity

Methods

funArity :: a -> Int

Instances

FunArity Clause

Get the number of initial Apply patterns in a clause.

Methods

funArity :: Clause -> Int

IsProjP p => FunArity [p]

Get the number of initial Apply patterns.

Methods

funArity :: [p] -> Int

FunArity [Clause]

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

Methods

funArity :: [Clause] -> Int

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.

Minimal complete definition

labelPatVars, unlabelPatVars

Methods

labelPatVars :: a -> State [i] b

unlabelPatVars :: b -> a

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

Methods

labelPatVars :: [a] -> State [i] [b]

unlabelPatVars :: [b] -> [a]

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

Methods

labelPatVars :: Arg a -> State [i] (Arg b)

unlabelPatVars :: Arg b -> Arg a

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

Methods

labelPatVars :: Pattern' x -> State [i] (Pattern' (i, x))

unlabelPatVars :: Pattern' (i, x) -> Pattern' x

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

Methods

labelPatVars :: Named x a -> State [i] (Named x b)

unlabelPatVars :: Named x b -> Named x a

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

Augment pattern variables with their de Bruijn index.

unnumberPatVars :: LabelPatVars a b i => b -> a

dbPatPerm :: [NamedArg DeBruijnPattern] -> Permutation

clausePerm :: Clause -> Permutation

patternToElim :: Arg DeBruijnPattern -> Elim

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

patternToTerm :: DeBruijnPattern -> Term