Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.CompiledClause

Contents

Pretty instances.
KillRange instances.
TermLike instances

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 arity :: Int content :: c

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) #
Data c => Data (WithArity c) #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithArity c -> c (WithArity c) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithArity c) # toConstr :: WithArity c -> Constr # dataTypeOf :: WithArity c -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (WithArity c)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithArity c)) # gmapT :: (forall b. Data b => b -> b) -> WithArity c -> WithArity c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithArity c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithArity c -> r # gmapQ :: (forall d. Data d => d -> u) -> WithArity c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WithArity c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) #
Show c => Show (WithArity c) #
Methods showsPrec :: Int -> WithArity c -> ShowS # show :: WithArity c -> String # showList :: [WithArity c] -> ShowS #
Semigroup 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 #
(Semigroup c, Monoid c) => Monoid (WithArity c) #
Methods mempty :: WithArity c # mappend :: WithArity c -> WithArity c -> WithArity c # mconcat :: [WithArity c] -> WithArity c #
Pretty a => Pretty (WithArity a) #
Methods pretty :: WithArity a -> Doc # prettyPrec :: Int -> WithArity a -> Doc # prettyList :: [WithArity a] -> Doc #
KillRange c => KillRange (WithArity c) #
Methods killRange :: KillRangeT (WithArity c) #
TermLike a => TermLike (WithArity a) #
Methods traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a) # foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m #
NamesIn a => NamesIn (WithArity a) #
Methods namesIn :: WithArity a -> Set QName #
InstantiateFull a => InstantiateFull (WithArity a) #
Methods instantiateFull' :: WithArity a -> ReduceM (WithArity a) #

data Case c #

Branches in a case tree.

Constructors

Branches
Fields projPatterns :: Bool We 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 c Map from literal to case subtree. catchAllBranch :: Maybe c (Possibly additional) catch-all clause.

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) #
Data c => Data (Case c) #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Case c -> c (Case c) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Case c) # toConstr :: Case c -> Constr # dataTypeOf :: Case c -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Case c)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c)) # gmapT :: (forall b. Data b => b -> b) -> Case c -> Case c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r # gmapQ :: (forall d. Data d => d -> u) -> Case c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Case c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) #
Show c => Show (Case c) #
Methods showsPrec :: Int -> Case c -> ShowS # show :: Case c -> String # showList :: [Case c] -> ShowS #
Semigroup 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 #
(Semigroup m, Monoid m) => Monoid (Case m) #
Methods mempty :: Case m # mappend :: Case m -> Case m -> Case m # mconcat :: [Case m] -> Case m #
Null (Case m) #
Methods empty :: Case m # null :: Case m -> Bool #
Pretty a => Pretty (Case a) #
Methods pretty :: Case a -> Doc # prettyPrec :: Int -> Case a -> Doc # prettyList :: [Case a] -> Doc #
KillRange c => KillRange (Case c) #
Methods killRange :: KillRangeT (Case c) #
TermLike a => TermLike (Case a) #
Methods traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a) # foldTerm :: Monoid m => (Term -> m) -> Case a -> m #
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' a #

Case tree with bodies.

Constructors

Case (Arg Int) (Case (CompiledClauses' a))	`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] a	`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

Functor CompiledClauses' #
Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a #
Foldable CompiledClauses' #
Methods fold :: Monoid m => CompiledClauses' m -> m # foldMap :: Monoid m => (a -> m) -> CompiledClauses' a -> m # foldr :: (a -> b -> b) -> b -> CompiledClauses' a -> b # foldr' :: (a -> b -> b) -> b -> CompiledClauses' a -> b # foldl :: (b -> a -> b) -> b -> CompiledClauses' a -> b # foldl' :: (b -> a -> b) -> b -> CompiledClauses' a -> b # foldr1 :: (a -> a -> a) -> CompiledClauses' a -> a # foldl1 :: (a -> a -> a) -> CompiledClauses' a -> a # toList :: CompiledClauses' a -> [a] # null :: CompiledClauses' a -> Bool # length :: CompiledClauses' a -> Int # elem :: Eq a => a -> CompiledClauses' a -> Bool # maximum :: Ord a => CompiledClauses' a -> a # minimum :: Ord a => CompiledClauses' a -> a # sum :: Num a => CompiledClauses' a -> a # product :: Num a => CompiledClauses' a -> a #
Traversable CompiledClauses' #
Methods traverse :: Applicative f => (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b) # sequenceA :: Applicative f => CompiledClauses' (f a) -> f (CompiledClauses' a) # mapM :: Monad m => (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b) # sequence :: Monad m => CompiledClauses' (m a) -> m (CompiledClauses' a) #
Pretty CompiledClauses #
Methods pretty :: CompiledClauses -> Doc # prettyPrec :: Int -> CompiledClauses -> Doc # prettyList :: [CompiledClauses] -> Doc #
KillRange CompiledClauses #
Methods killRange :: KillRangeT CompiledClauses #
NamesIn CompiledClauses #
Methods namesIn :: CompiledClauses -> Set QName #
InstantiateFull CompiledClauses #
Methods instantiateFull' :: CompiledClauses -> ReduceM 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.
Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses #
Data a => Data (CompiledClauses' a) #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompiledClauses' a -> c (CompiledClauses' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a) # toConstr :: CompiledClauses' a -> Constr # dataTypeOf :: CompiledClauses' a -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CompiledClauses' a)) # gmapT :: (forall b. Data b => b -> b) -> CompiledClauses' a -> CompiledClauses' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r # gmapQ :: (forall d. Data d => d -> u) -> CompiledClauses' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) #
Show a => Show (CompiledClauses' a) #
Methods showsPrec :: Int -> CompiledClauses' a -> ShowS # show :: CompiledClauses' a -> String # showList :: [CompiledClauses' a] -> ShowS #
TermLike a => TermLike (CompiledClauses' a) #
Methods traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a) # foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m #

type CompiledClauses = CompiledClauses' Term #

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

conCase :: QName -> WithArity 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 :: (Pretty k, Pretty v) => Map k v -> [Doc] #

Documentation

Pretty instances.

KillRange instances.

TermLike instances