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

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 Methods showsPrec :: Int -> WithArity c -> ShowS # show :: WithArity c -> String # showList :: [WithArity c] -> ShowS #
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 Methods mempty :: WithArity c # mappend :: WithArity c -> WithArity c -> WithArity c # mconcat :: [WithArity c] -> WithArity c #
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 #
KillRange c => KillRange (WithArity c) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) 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 #
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 Methods icode :: WithArity a -> S Int32 Source # icod_ :: WithArity a -> S Int32 Source # value :: Int32 -> R (WithArity a) Source #
NamesIn a => NamesIn (WithArity a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: WithArity a -> Set QName Source #
InstantiateFull t => InstantiateFull (WithArity t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity t -> ReduceM (WithArity t) Source #

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) #
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 #
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 #
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 Methods killRange :: KillRangeT (Case c) 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 #
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 :: Case a -> Set QName Source #
InstantiateFull a => InstantiateFull (Case a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Case a -> ReduceM (Case a) Source #

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	Absurd case.

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 Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
KillRange CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT 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 #
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 #
NamesIn CompiledClauses Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName 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 #
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 Methods showsPrec :: Int -> CompiledClauses' a -> ShowS # show :: CompiledClauses' a -> String # showList :: [CompiledClauses' a] -> ShowS #
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source #
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 #