Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Coverage.SplitTree

Contents

Printing a split tree

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
  }
data LazySplit
- = LazySplit
- | StrictSplit
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTag
- = SplitCon QName
- | SplitLit Literal
- | SplitCatchall
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 splitBindings :: Int The number of variables bound in the clause
SplitAt	A split is necessary.
Fields splitArg :: Arg Int Arg. no to split at. splitLazy :: LazySplit splitTrees :: SplitTrees' a Sub split trees.

Instances

Instances details

DropArgs SplitTree Source #
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> SplitTree -> SplitTree Source #
Pretty a => Pretty (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTree' a -> Doc Source # prettyPrec :: Int -> SplitTree' a -> Doc Source # prettyList :: [SplitTree' a] -> Doc Source #
KillRange a => KillRange (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT (SplitTree' a) Source #
EmbPrj a => EmbPrj (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTree' a -> S Int32 Source # icod_ :: SplitTree' a -> S Int32 Source # value :: Int32 -> R (SplitTree' a) Source #
Generic (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep (SplitTree' a) :: Type -> Type Methods from :: SplitTree' a -> Rep (SplitTree' a) x to :: Rep (SplitTree' a) x -> SplitTree' a
Show a => Show (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> SplitTree' a -> ShowS show :: SplitTree' a -> String showList :: [SplitTree' a] -> ShowS
NFData a => NFData (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: SplitTree' a -> ()
type Rep (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree type Rep (SplitTree' a) = D1 ('MetaData "SplitTree'" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.3.20230930-inplace" '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)))))

data LazySplit Source #

Constructors

LazySplit
StrictSplit

Instances

Instances details

EmbPrj LazySplit Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LazySplit -> S Int32 Source # icod_ :: LazySplit -> S Int32 Source # value :: Int32 -> R LazySplit Source #
Generic LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep LazySplit :: Type -> Type Methods from :: LazySplit -> Rep LazySplit x to :: Rep LazySplit x -> LazySplit
Show LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> LazySplit -> ShowS show :: LazySplit -> String showList :: [LazySplit] -> ShowS
NFData LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: LazySplit -> ()
Eq LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods (==) :: LazySplit -> LazySplit -> Bool (/=) :: LazySplit -> LazySplit -> Bool
Ord LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods compare :: LazySplit -> LazySplit -> Ordering (<) :: LazySplit -> LazySplit -> Bool (<=) :: LazySplit -> LazySplit -> Bool (>) :: LazySplit -> LazySplit -> Bool (>=) :: LazySplit -> LazySplit -> Bool max :: LazySplit -> LazySplit -> LazySplit min :: LazySplit -> LazySplit -> LazySplit
type Rep LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree type Rep LazySplit = D1 ('MetaData "LazySplit" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "LazySplit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StrictSplit" 'PrefixI 'False) (U1 :: Type -> Type))

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.

data SplitTag Source #

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

Instances details

Pretty SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTag -> Doc Source # prettyPrec :: Int -> SplitTag -> Doc Source # prettyList :: [SplitTag] -> Doc Source #
KillRange SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT SplitTag Source #
DropArgs SplitTree Source #
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> SplitTree -> SplitTree Source #
PrettyTCM SplitTag Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => SplitTag -> m Doc Source #
EmbPrj SplitTag Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTag -> S Int32 Source # icod_ :: SplitTag -> S Int32 Source # value :: Int32 -> R SplitTag Source #
Generic SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep SplitTag :: Type -> Type Methods from :: SplitTag -> Rep SplitTag x to :: Rep SplitTag x -> SplitTag
Show SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> SplitTag -> ShowS show :: SplitTag -> String showList :: [SplitTag] -> ShowS
NFData SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: SplitTag -> ()
Eq SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods (==) :: SplitTag -> SplitTag -> Bool (/=) :: SplitTag -> SplitTag -> Bool
Ord SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods compare :: SplitTag -> SplitTag -> Ordering (<) :: SplitTag -> SplitTag -> Bool (<=) :: SplitTag -> SplitTag -> Bool (>) :: SplitTag -> SplitTag -> Bool (>=) :: SplitTag -> SplitTag -> Bool max :: SplitTag -> SplitTag -> SplitTag min :: SplitTag -> SplitTag -> SplitTag
type Rep SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree type Rep SplitTag = D1 ('MetaData "SplitTag" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "SplitCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "SplitLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "SplitCatchall" 'PrefixI 'False) (U1 :: Type -> Type)))

Printing a split tree

data SplitTreeLabel a Source #

Constructors

SplitTreeLabel
Fields lblConstructorName :: Maybe a `Nothing` for root of split tree lblSplitArg :: Maybe (Arg Int) lblLazy :: LazySplit lblBindings :: Maybe Int

Instances

Instances details

Pretty a => Pretty (SplitTreeLabel a) Source #
Instance details 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 #