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
Functor Case Source # | |
Foldable Case Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods fold :: Monoid m => Case m -> m Source # foldMap :: Monoid m => (a -> m) -> Case a -> m Source # foldMap' :: Monoid m => (a -> m) -> Case a -> m Source # foldr :: (a -> b -> b) -> b -> Case a -> b Source # foldr' :: (a -> b -> b) -> b -> Case a -> b Source # foldl :: (b -> a -> b) -> b -> Case a -> b Source # foldl' :: (b -> a -> b) -> b -> Case a -> b Source # foldr1 :: (a -> a -> a) -> Case a -> a Source # foldl1 :: (a -> a -> a) -> Case a -> a Source # toList :: Case a -> [a] Source # null :: Case a -> Bool Source # length :: Case a -> Int Source # elem :: Eq a => a -> Case a -> Bool Source # maximum :: Ord a => Case a -> a Source # minimum :: Ord a => Case a -> a Source # | |
Traversable Case Source # | |
Defined in Agda.TypeChecking.CompiledClause | |
Data c => Data (Case c) Source # | |
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) Source # gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (Case c) Source # toConstr :: Case c -> Constr Source # dataTypeOf :: Case c -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (Case c)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (Case c)) Source # gmapT :: (forall b. Data b => b -> b) -> Case c -> Case c Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Case c -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Case c -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source # | |
Show c => Show (Case c) Source # | |
Semigroup m => Semigroup (Case m) Source # | |
(Semigroup m, Monoid m) => Monoid (Case m) Source # | |
Null (Case m) Source # | |
Pretty a => Pretty (Case a) Source # | |
KillRange c => KillRange (Case c) Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source # | |
Abstract a => Abstract (Case a) Source # | |
Apply a => Apply (Case a) Source # | |
TermLike a => TermLike (Case a) Source # | |
EmbPrj a => EmbPrj (Case a) Source # | |
NamesIn a => NamesIn (Case a) Source # | |
InstantiateFull a => InstantiateFull (Case a) Source # | |
Defined in Agda.TypeChecking.Reduce |
data CompiledClauses' a Source #
Case tree with bodies.
Constructors
Case (Arg Int) (Case (CompiledClauses' a)) |
|
Done [Arg ArgName] a |
|
Fail | Absurd case. |
Instances
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