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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.CompiledClause

Contents

Description

Case trees.

After coverage checking, pattern matching is translated to case trees, i.e., a tree of successive case splits on one variable at a time.

Synopsis

Documentation

data WithArity c #

Constructors

WithArity 

Fields

Instances

Functor WithArity # 

Methods

fmap :: (a -> b) -> WithArity a -> WithArity b #

(<$) :: a -> WithArity b -> WithArity a #

Foldable WithArity # 

Methods

fold :: Monoid m => WithArity m -> m #

foldMap :: Monoid m => (a -> m) -> WithArity a -> m #

foldr :: (a -> b -> b) -> b -> WithArity a -> b #

foldr' :: (a -> b -> b) -> b -> WithArity a -> b #

foldl :: (b -> a -> b) -> b -> WithArity a -> b #

foldl' :: (b -> a -> b) -> b -> WithArity a -> b #

foldr1 :: (a -> a -> a) -> WithArity a -> a #

foldl1 :: (a -> a -> a) -> WithArity a -> a #

toList :: WithArity a -> [a] #

null :: WithArity a -> Bool #

length :: WithArity a -> Int #

elem :: Eq a => a -> WithArity a -> Bool #

maximum :: Ord a => WithArity a -> a #

minimum :: Ord a => WithArity a -> a #

sum :: Num a => WithArity a -> a #

product :: Num a => WithArity a -> a #

Traversable WithArity # 

Methods

traverse :: Applicative f => (a -> f b) -> WithArity a -> f (WithArity b) #

sequenceA :: Applicative f => WithArity (f a) -> f (WithArity a) #

mapM :: Monad m => (a -> m b) -> WithArity a -> m (WithArity b) #

sequence :: Monad m => WithArity (m a) -> m (WithArity a) #

Monoid c => Semigroup (WithArity c) # 

Methods

(<>) :: WithArity c -> WithArity c -> WithArity c #

sconcat :: NonEmpty (WithArity c) -> WithArity c #

stimes :: Integral b => b -> WithArity c -> WithArity c #

Monoid c => Monoid (WithArity c) # 
Pretty a => Pretty (WithArity a) # 

Methods

pretty :: WithArity a -> Doc #

prettyPrec :: Int -> WithArity a -> Doc #

KillRange c => KillRange (WithArity c) # 
NamesIn a => NamesIn (WithArity a) # 

Methods

namesIn :: WithArity a -> Set QName #

InstantiateFull a => InstantiateFull (WithArity a) # 

data Case c #

Branches in a case tree.

Constructors

Branches 

Fields

Instances

Functor Case # 

Methods

fmap :: (a -> b) -> Case a -> Case b #

(<$) :: a -> Case b -> Case a #

Foldable Case # 

Methods

fold :: Monoid m => Case m -> m #

foldMap :: Monoid m => (a -> m) -> Case a -> m #

foldr :: (a -> b -> b) -> b -> Case a -> b #

foldr' :: (a -> b -> b) -> b -> Case a -> b #

foldl :: (b -> a -> b) -> b -> Case a -> b #

foldl' :: (b -> a -> b) -> b -> Case a -> b #

foldr1 :: (a -> a -> a) -> Case a -> a #

foldl1 :: (a -> a -> a) -> Case a -> a #

toList :: Case a -> [a] #

null :: Case a -> Bool #

length :: Case a -> Int #

elem :: Eq a => a -> Case a -> Bool #

maximum :: Ord a => Case a -> a #

minimum :: Ord a => Case a -> a #

sum :: Num a => Case a -> a #

product :: Num a => Case a -> a #

Traversable Case # 

Methods

traverse :: Applicative f => (a -> f b) -> Case a -> f (Case b) #

sequenceA :: Applicative f => Case (f a) -> f (Case a) #

mapM :: Monad m => (a -> m b) -> Case a -> m (Case b) #

sequence :: Monad m => Case (m a) -> m (Case a) #

Pretty a => Show (Case a) # 

Methods

showsPrec :: Int -> Case a -> ShowS #

show :: Case a -> String #

showList :: [Case a] -> ShowS #

Monoid m => Semigroup (Case m) # 

Methods

(<>) :: Case m -> Case m -> Case m #

sconcat :: NonEmpty (Case m) -> Case m #

stimes :: Integral b => b -> Case m -> Case m #

Monoid m => Monoid (Case m) # 

Methods

mempty :: Case m #

mappend :: Case m -> Case m -> Case m #

mconcat :: [Case m] -> Case m #

Pretty a => Pretty (Case a) # 

Methods

pretty :: Case a -> Doc #

prettyPrec :: Int -> Case a -> Doc #

Null (Case m) # 

Methods

empty :: Case m #

null :: Case m -> Bool #

KillRange c => KillRange (Case c) # 

Methods

killRange :: KillRangeT (Case c) #

NamesIn a => NamesIn (Case a) # 

Methods

namesIn :: Case a -> Set QName #

InstantiateFull a => InstantiateFull (Case a) # 

Methods

instantiateFull' :: Case a -> ReduceM (Case a) #

data CompiledClauses #

Case tree with bodies.

Constructors

Case (Arg Int) (Case CompiledClauses)

Case n bs stands for a match on the n-th argument (counting from zero) with bs as the case branches. If the n-th argument is a projection, we have only conBranches with arity 0.

Done [Arg ArgName] Term

Done xs b stands for the body b where the xs contains hiding and name suggestions for the free variables. This is needed to build lambdas on the right hand side for partial applications which can still reduce.

Fail

Absurd case.

Instances

Show CompiledClauses # 
Pretty CompiledClauses # 
KillRange CompiledClauses # 
NamesIn CompiledClauses # 
DropArgs CompiledClauses #

To drop the first n arguments in a compiled clause, we reduce the split argument indices by n and drop n arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.

InstantiateFull CompiledClauses # 

litCase :: Literal -> c -> Case c #

projCase :: QName -> c -> Case c #

catchAll :: c -> Case c #

hasCatchAll :: CompiledClauses -> Bool #

Check whether a case tree has a catch-all clause.

Pretty instances.

prettyMap :: (Show k, Pretty v) => Map k v -> [Doc] #

KillRange instances.