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

Agda.TypeChecking.CompiledClause

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 Source #

Constructors

 WithArity Fieldsarity :: Int content :: c

Instances

 Source # Methodsfmap :: (a -> b) -> WithArity a -> WithArity b #(<$) :: a -> WithArity b -> WithArity a # Source # Methodsfold :: 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 # Source # Methodstraverse :: 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 => Monoid (WithArity c) Source # Methodsmappend :: WithArity c -> WithArity c -> WithArity c #mconcat :: [WithArity c] -> WithArity c # Pretty a => Pretty (WithArity a) Source # MethodsprettyPrec :: Int -> WithArity a -> Doc Source # KillRange c => KillRange (WithArity c) Source # Methods NamesIn a => NamesIn (WithArity a) Source # Methods Abstract a => Abstract (WithArity a) Source # Methods Apply a => Apply (WithArity a) Source # Methodsapply :: WithArity a -> Args -> WithArity a Source #applyE :: WithArity a -> Elims -> WithArity a Source # Source # Methods data Case c Source # Branches in a case tree. Constructors  Branches FieldsprojPatterns :: BoolWe are constructing a record here (copatterns). conBranches lists projections.conBranches :: Map QName (WithArity c)Map from constructor (or projection) names to their arity and the case subtree. (Projections have arity 0.)litBranches :: Map Literal cMap from literal to case subtree.catchAllBranch :: Maybe c(Possibly additional) catch-all clause. Instances  Source # Methodsfmap :: (a -> b) -> Case a -> Case b #(<$) :: a -> Case b -> Case a # Source # Methodsfold :: 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 # Source # Methodstraverse :: 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) Source # MethodsshowsPrec :: Int -> Case a -> ShowS #show :: Case a -> String #showList :: [Case a] -> ShowS # Monoid m => Monoid (Case m) Source # Methodsmempty :: Case m #mappend :: Case m -> Case m -> Case m #mconcat :: [Case m] -> Case m # Pretty a => Pretty (Case a) Source # Methodspretty :: Case a -> Doc Source #prettyPrec :: Int -> Case a -> Doc Source # Null (Case m) Source # Methodsnull :: Case m -> Bool Source # KillRange c => KillRange (Case c) Source # Methods NamesIn a => NamesIn (Case a) Source # Methods Abstract a => Abstract (Case a) Source # Methodsabstract :: Telescope -> Case a -> Case a Source # Apply a => Apply (Case a) Source # Methodsapply :: Case a -> Args -> Case a Source #applyE :: Case a -> Elims -> Case a Source # Source # Methods

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

 Source # MethodsshowList :: [CompiledClauses] -> ShowS # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # 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. Methods Source # Methods

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

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

catchAll :: c -> Case c Source #

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

# Pretty instances.

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