Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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 

Fields

Instances

Instances details
Functor WithArity Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

Foldable WithArity Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

foldMap :: Monoid m => (a -> m) -> WithArity a -> 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 Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> WithArity c -> c0 (WithArity c) #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (WithArity c) #

toConstr :: WithArity c -> Constr #

dataTypeOf :: WithArity c -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (WithArity c)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (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 :: forall r r'. (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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Generic (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (WithArity c) :: Type -> Type #

Methods

from :: WithArity c -> Rep (WithArity c) x #

to :: Rep (WithArity c) x -> WithArity c #

Semigroup c => Semigroup (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

NFData c => NFData (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: WithArity c -> () #

Pretty a => Pretty (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange c => KillRange (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Abstract a => Abstract (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply a => Apply (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

TermLike a => TermLike (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a) Source #

foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m Source #

EmbPrj a => EmbPrj (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn a => NamesIn (WithArity a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> WithArity a -> m Source #

InstantiateFull t => InstantiateFull (WithArity t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type Rep (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (WithArity c) = D1 ('MetaData "WithArity" "Agda.TypeChecking.CompiledClause" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "WithArity" 'PrefixI 'True) (S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c)))

data Case c Source #

Branches in a case tree.

Constructors

Branches 

Fields

Instances

Instances details
Functor Case Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

Foldable Case Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

foldMap :: Monoid m => (a -> m) -> Case a -> 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 Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> Case c -> c0 (Case c) #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (Case c) #

toConstr :: Case c -> Constr #

dataTypeOf :: Case c -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (Case c)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (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 :: forall r r'. (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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

show :: Case c -> String #

showList :: [Case c] -> ShowS #

Generic (Case c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (Case c) :: Type -> Type #

Methods

from :: Case c -> Rep (Case c) x #

to :: Rep (Case c) x -> Case c #

Semigroup m => Semigroup (Case m) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

mempty :: Case m #

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

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

NFData a => NFData (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: Case a -> () #

Null (Case m) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m Source #

null :: Case m -> Bool Source #

Pretty a => Pretty (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: Case a -> Doc Source #

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

prettyList :: [Case a] -> Doc Source #

KillRange c => KillRange (Case c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Abstract a => Abstract (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Case a -> Case a Source #

Apply a => Apply (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Case a -> Args -> Case a Source #

applyE :: Case a -> Elims -> Case a Source #

TermLike a => TermLike (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a) Source #

foldTerm :: Monoid m => (Term -> m) -> Case a -> m Source #

EmbPrj a => EmbPrj (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32 Source #

icod_ :: Case a -> S Int32 Source #

value :: Int32 -> R (Case a) Source #

NamesIn a => NamesIn (Case a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Case a -> m Source #

InstantiateFull a => InstantiateFull (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type Rep (Case c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "Branches" 'PrefixI 'True) ((S1 ('MetaSel ('Just "projPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conBranches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (WithArity c))) :*: S1 ('MetaSel ('Just "etaBranch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (ConHead, WithArity c))))) :*: ((S1 ('MetaSel ('Just "litBranches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Literal c)) :*: S1 ('MetaSel ('Just "catchAllBranch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe c))) :*: (S1 ('MetaSel ('Just "fallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "lazyMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data CompiledClauses' a Source #

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 [Arg ArgName]

Absurd case. Add the free variables here as well so we can build correct number of lambdas for strict backends. (#4280)

Instances

Instances details
Functor CompiledClauses' Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b #

(<$) :: a -> CompiledClauses' b -> CompiledClauses' a #

Foldable CompiledClauses' Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => CompiledClauses' m -> m #

foldMap :: Monoid m => (a -> m) -> CompiledClauses' a -> 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' Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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

Defined in Agda.TypeChecking.CompiledClause

KillRange CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Abstract CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn CompiledClauses Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> CompiledClauses -> m Source #

DropArgs CompiledClauses 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.

Instance details

Defined in Agda.TypeChecking.DropArgs

InstantiateFull CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Data a => Data (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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 :: forall r r'. (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) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Generic (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (CompiledClauses' a) :: Type -> Type #

NFData a => NFData (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: CompiledClauses' a -> () #

PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause.Compile

TermLike a => TermLike (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a) Source #

foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m Source #

type Rep (CompiledClauses' a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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

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

catchAll :: c -> Case c Source #

checkLazyMatch :: Case c -> Case c Source #

Check that the requirements on lazy matching (single inductive case) are met, and set lazy to False otherwise.

hasCatchAll :: CompiledClauses -> Bool Source #

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

hasProjectionPatterns :: CompiledClauses -> Bool Source #

Check whether a case tree has any projection patterns

Pretty instances.

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

KillRange instances.

TermLike instances