ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Coverage.SplitTree
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.
- 7 types
- 2 values
- PackageAgda-2.7.0.1
- Exports9
- LanguageHaskell2010
- LicenceMIT
- SourceSplitTree.hs
Abstract case tree shape.
Constructors
SplittingDoneNo more splits coming. We are at a single, all-variable clause.
splitBindings :: IntThe number of variables bound in the clause
SplitAtA split is necessary.
splitArg :: Arg IntArg. no to split at.
splitLazy :: LazySplitsplitTrees :: SplitTrees' aSub split trees.
Instances10DropArgs, Show, Generic, NFData, Pretty, KillRange, …
DropArgs SplitTreeDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgsShow a => Show (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeGeneric (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeNFData a => NFData (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreePretty a => Pretty (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeKillRange a => KillRange (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeDropFrom (SplitTree' c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.RecordPatternsEmbPrj a => EmbPrj (SplitTree' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphanDropFrom (c, SplitTree' c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.RecordPatternstype Rep (SplitTree' a) = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTree"SplitTree'"
"Agda.TypeChecking.Coverage.SplitTree"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'False) (C1 ('MetaCons"SplittingDone"
'PrefixI 'True) (S1 ('MetaSel ('Just"splitBindings"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons"SplitAt"
'PrefixI 'True) (S1 ('MetaSel ('Just"splitArg"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Int)) :*: (S1 ('MetaSel ('Just"splitLazy"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LazySplit) :*: S1 ('MetaSel ('Just"splitTrees"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SplitTrees' a)))))
Instances7Eq, Ord, Show, Generic, NFData, EmbPrj, …
Eq LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeOrd LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeShow LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeGeneric LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeNFData LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeEmbPrj LazySplitDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphantype Rep LazySplit = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTree"LazySplit"
"Agda.TypeChecking.Coverage.SplitTree"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'False) (C1 ('MetaCons"LazySplit"
'PrefixI 'False) U1 :+: C1 ('MetaCons"StrictSplit"
'PrefixI 'False) U1)
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
Instances11Eq, Ord, Show, Generic, NFData, Pretty, …
Eq SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeOrd SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeShow SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeGeneric SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeNFData SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreePretty SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreePrettyTCM SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.PrettyKillRange SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTreeDropArgs SplitTreeDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgsEmbPrj SplitTagDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphantype Rep SplitTag = D1 ('MetaDataDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTree"SplitTag"
"Agda.TypeChecking.Coverage.SplitTree"
"Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8"
'False) (C1 ('MetaCons"SplitCon"
'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons"SplitLit"
'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons"SplitCatchall"
'PrefixI 'False) U1))
Printing a split tree
3 declarationsConstructors
SplitTreeLabellblConstructorName :: Maybe aNothing for root of split tree
lblSplitArg :: Maybe (Arg Int)lblLazy :: LazySplitlblBindings :: Maybe Int
Instances1Pretty
Pretty a => Pretty (SplitTreeLabel a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.SplitTree
Convert a split tree into a Data.Tree (for printing).