| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.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 {
- ccClauseNumber :: !ClauseNumber
- ccClauseRecursive :: !ClauseRecursive
- ccBoundVars :: ![Arg ArgName]
- ccBody :: a
- 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 Mikan.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 Mikan.Syntax.Internal.Names | |||||
| KillRange c => KillRange (Case c) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source # | |||||
| InstantiateFull a => InstantiateFull (Case a) Source # | |||||
Defined in Mikan.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 Mikan.TypeChecking.CompiledClause | |||||
| Monoid m => Monoid (Case m) Source # | |||||
| Semigroup m => Semigroup (Case m) Source # | |||||
| Generic (Case c) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Associated Types
| |||||
| Show c => Show (Case c) Source # | |||||
| type Rep (Case c) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause type Rep (Case c) = D1 ('MetaData "Case" "Mikan.TypeChecking.CompiledClause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Branches" 'PrefixI 'True) ((S1 ('MetaSel ('Just "projPatterns") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conBranches") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map QName (WithArity c))) :*: S1 ('MetaSel ('Just "etaBranch") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (ConHead, WithArity c))))) :*: ((S1 ('MetaSel ('Just "litBranches") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Literal c)) :*: S1 ('MetaSel ('Just "catchallBranch") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe c))) :*: (S1 ('MetaSel ('Just "fallThrough") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "lazyMatch") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (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 Mikan.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source # | |||||
| KillRange CompiledClauses Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Methods | |||||
| MapDone CompiledClauses' Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Methods mapDone :: (CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b Source # | |||||
| DropArgs CompiledClauses Source # | To drop the first | ||||
Defined in Mikan.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source # | |||||
| InstantiateFull CompiledClauses Source # | |||||
Defined in Mikan.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source # | |||||
| EmbPrj CompiledClauses Source # | |||||
| Abstract CompiledClauses Source # | |||||
Defined in Mikan.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source # | |||||
| Apply CompiledClauses Source # | |||||
Defined in Mikan.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source # | |||||
| Functor CompiledClauses' Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a # | |||||
| Foldable CompiledClauses' Source # | |||||
Defined in Mikan.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 Mikan.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 Mikan.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 Mikan.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 Mikan.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source # | |||||
| NFData a => NFData (CompiledClauses' a) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Methods rnf :: CompiledClauses' a -> () # | |||||
| Generic (CompiledClauses' a) Source # | |||||
Defined in Mikan.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 Mikan.TypeChecking.CompiledClause Methods showsPrec :: Int -> CompiledClauses' a -> ShowS # show :: CompiledClauses' a -> String # showList :: [CompiledClauses' a] -> ShowS # | |||||
| type Rep (CompiledClauses' a) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Mikan.TypeChecking.CompiledClause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Case" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Arg Int)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Case (CompiledClauses' a)))) :+: (C1 ('MetaCons "Done_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (CCDone a))) :+: C1 ('MetaCons "Fail" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (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 Mikan.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 Mikan.TypeChecking.CompiledClause | |||||
| Generic (CCDone a) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause Associated Types
| |||||
| Show a => Show (CCDone a) Source # | |||||
| type Rep (CCDone a) Source # | |||||
Defined in Mikan.TypeChecking.CompiledClause type Rep (CCDone a) = D1 ('MetaData "CCDone" "Mikan.TypeChecking.CompiledClause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "CCDone" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ccClauseNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ClauseNumber) :*: S1 ('MetaSel ('Just "ccClauseRecursive") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ClauseRecursive)) :*: (S1 ('MetaSel ('Just "ccBoundVars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (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 Mikan.TypeChecking.CompiledClause Methods mapDone :: (CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b Source # | |