| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.CompiledClause
Contents
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
- type ClauseNumber = Int
- data WithArity c = WithArity {}
- 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
- type CompiledClauses = CompiledClauses' Term
- data CompiledClauses' a
- data CCDone a = CCDone {}
- pattern Done :: ClauseNumber -> ClauseRecursive -> [Arg ArgName] -> a -> CompiledClauses' a
- 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
- class MapDone (f :: Type -> Type) where
- prettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc]
Documentation
type ClauseNumber = Int Source #
The number of a Clause (starting with 0) in the clause list of a FunctionData.
Instances
Branches in a case tree.
Constructors
| Branches | |
Fields
| |
Instances
| Functor Case Source # | |||||
| Foldable Case Source # | |||||
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 # elem :: Eq a => a -> Case a -> Bool # maximum :: Ord a => Case a -> a # | |||||
| Traversable Case Source # | |||||
| Pretty a => Pretty (Case a) Source # | |||||
| TermLike a => TermLike (Case a) Source # | |||||
| NamesIn a => NamesIn (Case a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| KillRange c => KillRange (Case c) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source # | |||||
| InstantiateFull a => InstantiateFull (Case a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| EmbPrj a => EmbPrj (Case a) Source # | |||||
| Abstract a => Abstract (Case a) Source # | |||||
| Apply a => Apply (Case a) Source # | |||||
| Null (Case m) Source # | |||||
| NFData a => NFData (Case a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause | |||||
| (Semigroup m, Monoid m) => Monoid (Case m) Source # | |||||
| Semigroup m => Semigroup (Case m) Source # | |||||
| Generic (Case c) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Associated Types
| |||||
| Show c => Show (Case c) Source # | |||||
| type Rep (Case c) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.9.0-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))))) | |||||
type CompiledClauses = CompiledClauses' Term Source #
data CompiledClauses' a Source #
Case tree with bodies.
Constructors
| Case (Arg Int) (Case (CompiledClauses' a)) |
|
| Done_ (CCDone a) | |
| 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
| NamesIn CompiledClauses Source # | |||||
Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source # | |||||
| KillRange CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods | |||||
| MapDone CompiledClauses' Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods mapDone :: (CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b Source # | |||||
| DropArgs CompiledClauses Source # | To drop the first | ||||
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source # | |||||
| InstantiateFull CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source # | |||||
| EmbPrj CompiledClauses Source # | |||||
| Abstract CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source # | |||||
| Apply CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source # | |||||
| Functor CompiledClauses' Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a # | |||||
| Foldable CompiledClauses' Source # | |||||
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 # | |||||
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 a => Pretty (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses' a -> Doc Source # prettyPrec :: Int -> CompiledClauses' a -> Doc Source # prettyList :: [CompiledClauses' a] -> Doc Source # | |||||
| TermLike a => TermLike (CompiledClauses' a) Source # | |||||
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 # | |||||
Defined in Agda.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source # | |||||
| NFData a => NFData (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods rnf :: CompiledClauses' a -> () # | |||||
| Generic (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Associated Types
Methods from :: CompiledClauses' a -> Rep (CompiledClauses' a) x # to :: Rep (CompiledClauses' a) x -> CompiledClauses' a # | |||||
| Show a => Show (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> CompiledClauses' a -> ShowS # show :: CompiledClauses' a -> String # showList :: [CompiledClauses' a] -> ShowS # | |||||
| type Rep (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.9.0-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 (CCDone a))) :+: C1 ('MetaCons "Fail" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName])))) | |||||
Data stored in Done nodes of the case tree.
CCDone no mr 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.
The no is the number of the original Clause this case tree leaf comes from.
mr tells whether this body contains calls to the mutually recursive functions.
Constructors
| CCDone | |
Fields
| |
Instances
| Functor CCDone Source # | |||||
| Foldable CCDone Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods fold :: Monoid m => CCDone m -> m # foldMap :: Monoid m => (a -> m) -> CCDone a -> m # foldMap' :: Monoid m => (a -> m) -> CCDone a -> m # foldr :: (a -> b -> b) -> b -> CCDone a -> b # foldr' :: (a -> b -> b) -> b -> CCDone a -> b # foldl :: (b -> a -> b) -> b -> CCDone a -> b # foldl' :: (b -> a -> b) -> b -> CCDone a -> b # foldr1 :: (a -> a -> a) -> CCDone a -> a # foldl1 :: (a -> a -> a) -> CCDone a -> a # elem :: Eq a => a -> CCDone a -> Bool # maximum :: Ord a => CCDone a -> a # minimum :: Ord a => CCDone a -> a # | |||||
| Traversable CCDone Source # | |||||
| Pretty a => Pretty (CCDone a) Source # | |||||
| TermLike a => TermLike (CCDone a) Source # | |||||
| NFData a => NFData (CCDone a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause | |||||
| Generic (CCDone a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Associated Types
| |||||
| Show a => Show (CCDone a) Source # | |||||
| type Rep (CCDone a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause type Rep (CCDone a) = D1 ('MetaData "CCDone" "Agda.TypeChecking.CompiledClause" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "CCDone" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ccClauseNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClauseNumber) :*: S1 ('MetaSel ('Just "ccClauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClauseRecursive)) :*: (S1 ('MetaSel ('Just "ccBoundVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName]) :*: S1 ('MetaSel ('Just "ccBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) | |||||
pattern Done :: ClauseNumber -> ClauseRecursive -> [Arg ArgName] -> a -> CompiledClauses' a 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
Traversing the Done leaves
class MapDone (f :: Type -> Type) where Source #
Instances
| MapDone CompiledClauses' Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods mapDone :: (CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b Source # | |