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

Foldable WithArity

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

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)

Functor WithArity

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

Pretty a => Pretty (WithArity a)

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: WithArity a -> Doc

prettyPrec :: Int -> WithArity a -> Doc

prettyList :: [WithArity a] -> Doc

TermLike a => TermLike (WithArity a)

Defined in Agda.TypeChecking.CompiledClause

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)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> WithArity a -> m

KillRange c => KillRange (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (WithArity c)

InstantiateFull t => InstantiateFull (WithArity t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: WithArity t -> ReduceM (WithArity t)

EmbPrj a => EmbPrj (WithArity a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: WithArity a -> S Int32

icod_ :: WithArity a -> S Int32

value :: Int32 -> R (WithArity a)

Abstract a => Abstract (WithArity a)

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> WithArity a -> WithArity a

Apply a => Apply (WithArity a)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: WithArity a -> Args -> WithArity a

applyE :: WithArity a -> Elims -> WithArity a

(Semigroup c, Monoid c) => Monoid (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

mempty :: WithArity c

mappend :: WithArity c -> WithArity c -> WithArity c

mconcat :: [WithArity c] -> WithArity c

Semigroup c => Semigroup (WithArity c)

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

Generic (WithArity c)

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

Show c => Show (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

showsPrec :: Int -> WithArity c -> ShowS

show :: WithArity c -> String

showList :: [WithArity c] -> ShowS

NFData c => NFData (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: WithArity c -> ()

type Rep (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

type Rep (WithArity c) = D1 ('MetaData "WithArity" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" '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

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.)

• etaBranch :: Maybe (ConHead, WithArity c)

  Eta-expand with the given (eta record) constructor. If this is present, there should not be any conBranches or litBranches.

• litBranches :: Map Literal c

  Map from literal to case subtree.

• catchAllBranch :: Maybe c

  (Possibly additional) catch-all clause.

• fallThrough :: Maybe Bool

  (if True) In case of non-canonical argument use catchAllBranch.

• lazyMatch :: Bool

  Lazy pattern match. Requires single (non-copattern) branch with no lit branches and no catch-all.

Instances

Foldable Case

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

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)

Functor Case

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

Pretty a => Pretty (Case a)

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: Case a -> Doc

prettyPrec :: Int -> Case a -> Doc

prettyList :: [Case a] -> Doc

TermLike a => TermLike (Case a)

Defined in Agda.TypeChecking.CompiledClause

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)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Case a -> m

KillRange c => KillRange (Case c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (Case c)

InstantiateFull a => InstantiateFull (Case a)

Defined in Agda.TypeChecking.Reduce

Methods

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

EmbPrj a => EmbPrj (Case a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32

icod_ :: Case a -> S Int32

value :: Int32 -> R (Case a)

Abstract a => Abstract (Case a)

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Case a -> Case a

Apply a => Apply (Case a)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Case a -> Args -> Case a

applyE :: Case a -> Elims -> Case a

Null (Case m)

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m

null :: Case m -> Bool

(Semigroup m, Monoid m) => Monoid (Case m)

Defined in Agda.TypeChecking.CompiledClause

Methods

mempty :: Case m

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

mconcat :: [Case m] -> Case m

Semigroup m => Semigroup (Case m)

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

Generic (Case c)

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

Show c => Show (Case c)

Defined in Agda.TypeChecking.CompiledClause

Methods

showsPrec :: Int -> Case c -> ShowS

show :: Case c -> String

showList :: [Case c] -> ShowS

NFData a => NFData (Case a)

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: Case a -> ()

type Rep (Case c)

Defined in Agda.TypeChecking.CompiledClause

type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" '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

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

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT 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.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses

InstantiateFull CompiledClauses

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

Abstract CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Apply CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

Foldable CompiledClauses'

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'

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)

Functor CompiledClauses'

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

TermLike a => TermLike (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

Methods

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

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

PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a)

Generic (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

Associated Types

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

Methods

from :: CompiledClauses' a -> Rep (CompiledClauses' a) x

to :: Rep (CompiledClauses' a) x -> CompiledClauses' a

Show a => Show (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

Methods

showsPrec :: Int -> CompiledClauses' a -> ShowS

show :: CompiledClauses' a -> String

showList :: [CompiledClauses' a] -> ShowS

NFData a => NFData (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: CompiledClauses' a -> ()

type Rep (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "Case" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Int)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Case (CompiledClauses' a)))) :+: (C1 ('MetaCons "Done" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "Fail" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName]))))

type CompiledClauses = CompiledClauses' Term

litCase :: Literal -> c -> Case c

conCase :: QName -> Bool -> WithArity c -> Case c

etaCase :: ConHead -> WithArity c -> Case c

projCase :: QName -> c -> Case c

catchAll :: c -> Case c

checkLazyMatch :: Case c -> Case c

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

hasCatchAll :: CompiledClauses -> Bool

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

hasProjectionPatterns :: CompiledClauses -> Bool

Check whether a case tree has any projection patterns

Pretty instances.

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

KillRange instances.

TermLike instances