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

Methods

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

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

Show c => Show (WithArity c) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

showsPrec :: Int -> WithArity c -> ShowS

show :: WithArity c -> String

showList :: [WithArity c] -> ShowS

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.20240714-inplace" '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

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

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)

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 #

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 #

NamesIn a => NamesIn (Case a) Source #

Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange c => KillRange (Case c) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (Case c) Source #

InstantiateFull a => InstantiateFull (Case a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Case a -> ReduceM (Case a) 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 #

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 #

Null (Case m) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m Source #

null :: Case m -> Bool Source #

NFData a => NFData (Case a) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: Case a -> ()

(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

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

Generic (Case c) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (Case c)

Instance details

Defined in Agda.TypeChecking.CompiledClause

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

Methods

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

to :: Rep (Case c) x -> 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

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.20240714-inplace" '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

Pretty CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc Source #

prettyPrec :: Int -> CompiledClauses -> Doc Source #

prettyList :: [CompiledClauses] -> Doc Source #

NamesIn CompiledClauses Source #

Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #

InstantiateFull CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #

EmbPrj CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32 Source #

icod_ :: CompiledClauses -> S Int32 Source #

value :: Int32 -> R CompiledClauses Source #

Abstract CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #

Apply CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: CompiledClauses -> Args -> CompiledClauses Source #

applyE :: CompiledClauses -> Elims -> CompiledClauses Source #

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)

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 #

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

Instance details

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

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

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

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

rnf :: CompiledClauses' a -> ()

Generic (CompiledClauses' a) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (CompiledClauses' a)

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.6.20240714-inplace" '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]))))

Methods

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

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

Show a => Show (CompiledClauses' a) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

show :: CompiledClauses' a -> String

showList :: [CompiledClauses' a] -> ShowS

type Rep (CompiledClauses' a) Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.6.20240714-inplace" '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 Source #

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

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

etaCase :: ConHead -> WithArity 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