Safe Haskell	Safe-Inferred
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

data WithArity c = WithArity {
- arity :: Int
- content :: c
}
data Case c = Branches {
- projPatterns :: Bool
- conBranches :: Map QName (WithArity c)
- etaBranch :: Maybe (ConHead, WithArity c)
- litBranches :: Map Literal c
- catchAllBranch :: Maybe c
- fallThrough :: Maybe Bool
- lazyMatch :: Bool
}
data CompiledClauses' a
- = Case (Arg Int) (Case (CompiledClauses' a))
- | Done [Arg ArgName] a
- | Fail [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
hasCatchAll :: CompiledClauses -> Bool
hasProjectionPatterns :: CompiledClauses -> Bool
prettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc]

Documentation

data WithArity c Source #

Constructors

WithArity
Fields arity :: Int content :: c

Instances

Instances details

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)
Functor WithArity Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> WithArity a -> WithArity b (<$) :: a -> WithArity b -> WithArity a #
Pretty a => Pretty (WithArity a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: WithArity a -> Doc Source # prettyPrec :: Int -> WithArity a -> Doc Source # prettyList :: [WithArity a] -> Doc Source #
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 #
NamesIn a => NamesIn (WithArity a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> WithArity a -> m Source #
KillRange c => KillRange (WithArity c) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source #
InstantiateFull t => InstantiateFull (WithArity t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity t -> ReduceM (WithArity t) Source #
EmbPrj a => EmbPrj (WithArity a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Int32 Source # icod_ :: WithArity a -> S Int32 Source # value :: Int32 -> R (WithArity a) Source #
Abstract a => Abstract (WithArity a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
Apply a => Apply (WithArity a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
(Semigroup c, Monoid c) => Monoid (WithArity c) Source #
Instance details 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) 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
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
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
NFData c => NFData (WithArity c) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: WithArity c -> ()
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.3.20230930-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

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)
Functor Case Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> Case a -> Case b (<$) :: a -> Case b -> 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 #
(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) :: Type -> Type 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
NFData a => NFData (Case a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: Case a -> ()
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.3.20230930-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 #
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)
Functor CompiledClauses' Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b (<$) :: a -> CompiledClauses' b -> 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 #
Generic (CompiledClauses' a) Source #
Instance details 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) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> CompiledClauses' a -> ShowS show :: CompiledClauses' a -> String showList :: [CompiledClauses' a] -> ShowS
NFData a => NFData (CompiledClauses' a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: CompiledClauses' a -> ()
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.3.20230930-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]))))