Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal.Pattern

Contents

Synopsis

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 Pattern DeBruijnPattern Int # 
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 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 => Int -> Permutation -> a -> b #

Augment pattern variables with their de Bruijn index.

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

dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation #

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 #

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 #

Turn a pattern into a term. Projection patterns are turned into projection eliminations, other patterns into apply elimination.

class MapNamedArg f where #

Minimal complete definition

mapNamedArg

Methods

mapNamedArg :: (NamedArg a -> NamedArg b) -> NamedArg (f a) -> NamedArg (f b) #

Instances