| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.CompiledClause
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 {}
- 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
- 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
Instances
Branches in a case tree.
Constructors
| Branches | |
Fields
| |
Instances
| 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 # | |||||
| Functor 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 # | |||||
| (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 # | |||||
| NFData a => NFData (Case a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause | |||||
| type Rep (Case c) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.6.4.1-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)) |
|
| Done [Arg ArgName] 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
| Pretty CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source # | |||||
| 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 | |||||
| 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 # | |||||
| 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) # | |||||
| Functor CompiledClauses' Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a # | |||||
| 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 # | |||||
| 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 # | |||||
| NFData a => NFData (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods rnf :: CompiledClauses' a -> () # | |||||
| type Rep (CompiledClauses' a) Source # | |||||
Defined in Agda.TypeChecking.CompiledClause type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.6.4.1-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 #
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