Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 [Arg ArgName]
- 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 Source # (<$) :: a -> WithArity b -> WithArity a Source #
Foldable WithArity Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => WithArity m -> m Source #

foldMap :: Monoid m => (a -> m) -> WithArity a -> m Source #

foldMap' :: Monoid m => (a -> m) -> WithArity a -> m Source #

foldr :: (a -> b -> b) -> b -> WithArity a -> b Source #

foldr' :: (a -> b -> b) -> b -> WithArity a -> b Source #

foldl :: (b -> a -> b) -> b -> WithArity a -> b Source #

foldl' :: (b -> a -> b) -> b -> WithArity a -> b Source #

foldr1 :: (a -> a -> a) -> WithArity a -> a Source #

foldl1 :: (a -> a -> a) -> WithArity a -> a Source #

toList :: WithArity a -> [a] Source #

null :: WithArity a -> Bool Source #

length :: WithArity a -> Int Source #

elem :: Eq a => a -> WithArity a -> Bool Source #

maximum :: Ord a => WithArity a -> a Source #

minimum :: Ord a => WithArity a -> a Source #

sum :: Num a => WithArity a -> a Source #

product :: Num a => WithArity a -> a Source #

Traversable WithArity Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverse :: Applicative f => (a -> f b) -> WithArity a -> f (WithArity b) Source # sequenceA :: Applicative f => WithArity (f a) -> f (WithArity a) Source # mapM :: Monad m => (a -> m b) -> WithArity a -> m (WithArity b) Source # sequence :: Monad m => WithArity (m a) -> m (WithArity a) Source #
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 #
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 #
NamesIn a => NamesIn (WithArity a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> WithArity a -> m Source #
KillRange c => KillRange (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source #
InstantiateFull t => InstantiateFull (WithArity t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity t -> ReduceM (WithArity t) Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Word32 Source # icod_ :: WithArity a -> S Word32 Source # value :: Word32 -> R (WithArity a) 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 #
NFData c => NFData (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: WithArity c -> () Source #
(Semigroup c, Monoid c) => Monoid (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods mempty :: WithArity c Source # mappend :: WithArity c -> WithArity c -> WithArity c Source # mconcat :: [WithArity c] -> WithArity c Source #
Semigroup c => Semigroup (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: WithArity c -> WithArity c -> WithArity c Source # sconcat :: NonEmpty (WithArity c) -> WithArity c Source # stimes :: Integral b => b -> WithArity c -> WithArity c Source #
Generic (WithArity c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (WithArity c) |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (WithArity c) = D1 ('MetaData "WithArity" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "WithArity" 'PrefixI 'True) (S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c)))

Methods

from :: WithArity c -> Rep (WithArity c) x Source #

to :: Rep (WithArity c) x -> WithArity c Source #

Show c => Show (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> WithArity c -> ShowS Source # show :: WithArity c -> String Source # showList :: [WithArity c] -> ShowS Source #
type Rep (WithArity c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (WithArity c) = D1 ('MetaData "WithArity" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "WithArity" 'PrefixI 'True) (S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c)))

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 Source # (<$) :: a -> Case b -> Case a Source #
Foldable Case Source # |

Instance details

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 #

sum :: Num a => Case a -> a Source #

product :: Num a => Case a -> a Source #

Traversable Case Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverse :: Applicative f => (a -> f b) -> Case a -> f (Case b) Source # sequenceA :: Applicative f => Case (f a) -> f (Case a) Source # mapM :: Monad m => (a -> m b) -> Case a -> m (Case b) Source # sequence :: Monad m => Case (m a) -> m (Case a) 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 #
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 #
NamesIn a => NamesIn (Case a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Case a -> m Source #
KillRange c => KillRange (Case c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source #
InstantiateFull a => InstantiateFull (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Case a -> ReduceM (Case a) Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Word32 Source # icod_ :: Case a -> S Word32 Source # value :: Word32 -> R (Case a) 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 #
Null (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods empty :: Case m Source # null :: Case m -> Bool Source #
NFData a => NFData (Case a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: Case a -> () Source #
(Semigroup m, Monoid m) => Monoid (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods mempty :: Case m Source # mappend :: Case m -> Case m -> Case m Source # mconcat :: [Case m] -> Case m Source #
Semigroup m => Semigroup (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: Case m -> Case m -> Case m Source # sconcat :: NonEmpty (Case m) -> Case m Source # stimes :: Integral b => b -> Case m -> Case m Source #
Generic (Case c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (Case c) |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: Case c -> Rep (Case c) x Source #

to :: Rep (Case c) x -> Case c Source #

Show c => Show (Case c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> Case c -> ShowS Source # show :: Case c -> String Source # showList :: [Case c] -> ShowS Source #
type Rep (Case c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)) | `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 [Arg ArgName] | Absurd case. Add the free variables here as well so we can build correct number of lambdas for strict backends. (#4280)

#### Instances

Instances details

Pretty CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source #
KillRange CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses 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 #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Word32 Source # icod_ :: CompiledClauses -> S Word32 Source # value :: Word32 -> R 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 #
Functor CompiledClauses' Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b Source # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a Source #
Foldable CompiledClauses' Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => CompiledClauses' m -> m Source #

foldMap :: Monoid m => (a -> m) -> CompiledClauses' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> CompiledClauses' a -> m Source #

foldr :: (a -> b -> b) -> b -> CompiledClauses' a -> b Source #

foldr' :: (a -> b -> b) -> b -> CompiledClauses' a -> b Source #

foldl :: (b -> a -> b) -> b -> CompiledClauses' a -> b Source #

foldl' :: (b -> a -> b) -> b -> CompiledClauses' a -> b Source #

foldr1 :: (a -> a -> a) -> CompiledClauses' a -> a Source #

foldl1 :: (a -> a -> a) -> CompiledClauses' a -> a Source #

toList :: CompiledClauses' a -> [a] Source #

null :: CompiledClauses' a -> Bool Source #

length :: CompiledClauses' a -> Int Source #

elem :: Eq a => a -> CompiledClauses' a -> Bool Source #

maximum :: Ord a => CompiledClauses' a -> a Source #

minimum :: Ord a => CompiledClauses' a -> a Source #

sum :: Num a => CompiledClauses' a -> a Source #

product :: Num a => CompiledClauses' a -> a Source #

Traversable CompiledClauses' Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

traverse :: Applicative f => (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b) Source #

sequenceA :: Applicative f => CompiledClauses' (f a) -> f (CompiledClauses' a) Source #

mapM :: Monad m => (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b) Source #

sequence :: Monad m => CompiledClauses' (m a) -> m (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 #
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source #
NFData a => NFData (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods rnf :: CompiledClauses' a -> () Source #
Generic (CompiledClauses' a) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Associated Types

type Rep (CompiledClauses' a) |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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]))))

Methods

from :: CompiledClauses' a -> Rep (CompiledClauses' a) x Source #

to :: Rep (CompiledClauses' a) x -> CompiledClauses' a Source #

Show a => Show (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> CompiledClauses' a -> ShowS Source # show :: CompiledClauses' a -> String Source # showList :: [CompiledClauses' a] -> ShowS Source #
type Rep (CompiledClauses' a) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #

litCase :: Literal -> c -> Case c Source #

conCase :: QName -> Bool -> WithArity c -> Case c Source #

etaCase :: ConHead -> WithArity c -> Case c Source #

projCase :: QName -> c -> Case c Source #

catchall :: c -> Case c 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

# Pretty instances.

prettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc] Source #

# KillRange instances.

# TermLike instances