Agda.TypeChecking.CompiledClause

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.

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]

KillRange instances.

TermLike instances