| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Coverage.SplitTree
Contents
Description
Split tree for transforming pattern clauses into case trees.
The coverage checker generates a split tree from the clauses. The clause compiler uses it to transform clauses to case trees.
The initial problem is a set of clauses. The root node designates on which argument to split and has subtrees for all the constructors. Splitting continues until there is only a single clause left at each leaf of the split tree.
Synopsis
- type SplitTree = SplitTree' SplitTag
- type SplitTrees = SplitTrees' SplitTag
- data SplitTree' a
- = SplittingDone {
- splitBindings :: Int
- | SplitAt {
- splitArg :: Arg Int
- splitLazy :: LazySplit
- splitTrees :: SplitTrees' a
- = SplittingDone {
- data LazySplit
- type SplitTrees' a = [(a, SplitTree' a)]
- data SplitTag
- data SplitTreeLabel a = SplitTreeLabel {
- lblConstructorName :: Maybe a
- lblSplitArg :: Maybe (Arg Int)
- lblLazy :: LazySplit
- lblBindings :: Maybe Int
- toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
- toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
Documentation
type SplitTree = SplitTree' SplitTag Source #
type SplitTrees = SplitTrees' SplitTag Source #
data SplitTree' a Source #
Abstract case tree shape.
Constructors
| SplittingDone | No more splits coming. We are at a single, all-variable clause. |
Fields
| |
| SplitAt | A split is necessary. |
Fields
| |
Instances
Constructors
| LazySplit | |
| StrictSplit |
Instances
| EmbPrj LazySplit Source # | |
| Generic LazySplit Source # | |
| Show LazySplit Source # | |
| NFData LazySplit Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree | |
| Eq LazySplit Source # | |
| Ord LazySplit Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree | |
| type Rep LazySplit Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree | |
type SplitTrees' a = [(a, SplitTree' a)] Source #
Split tree branching. A finite map from constructor names to splittrees A list representation seems appropriate, since we are expecting not so many constructors per data type, and there is no need for random access.
Tag for labeling branches of a split tree. Each branch is associated to either a constructor or a literal, or is a catchall branch (currently only used for splitting on a literal type).
Constructors
| SplitCon QName | |
| SplitLit Literal | |
| SplitCatchall |
Instances
Printing a split tree
data SplitTreeLabel a Source #
Constructors
| SplitTreeLabel | |
Fields
| |
Instances
| Pretty a => Pretty (SplitTreeLabel a) Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTreeLabel a -> Doc Source # prettyPrec :: Int -> SplitTreeLabel a -> Doc Source # prettyList :: [SplitTreeLabel a] -> Doc Source # | |
toTree :: SplitTree' a -> Tree (SplitTreeLabel a) Source #
Convert a split tree into a Tree (for printing).
toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a) Source #