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 #
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 #
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 #
Data a => Data (SplitTree' a) Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SplitTree' a -> c (SplitTree' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SplitTree' a) # toConstr :: SplitTree' a -> Constr # dataTypeOf :: SplitTree' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SplitTree' a)) # gmapT :: (forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r # gmapQ :: (forall d. Data d => d -> u) -> SplitTree' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) #
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.2.1.20220320-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 #
Data LazySplit Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LazySplit -> c LazySplit # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LazySplit # toConstr :: LazySplit -> Constr # dataTypeOf :: LazySplit -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LazySplit) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LazySplit) # gmapT :: (forall b. Data b => b -> b) -> LazySplit -> LazySplit # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LazySplit -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LazySplit -> r # gmapQ :: (forall d. Data d => d -> u) -> LazySplit -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LazySplit -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit #
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.2.1.20220320-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

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 #
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 #
Data SplitTag Source #
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SplitTag -> c SplitTag # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SplitTag # toConstr :: SplitTag -> Constr # dataTypeOf :: SplitTag -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SplitTag) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SplitTag) # gmapT :: (forall b. Data b => b -> b) -> SplitTag -> SplitTag # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SplitTag -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SplitTag -> r # gmapQ :: (forall d. Data d => d -> u) -> SplitTag -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SplitTag -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag #
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.2.1.20220320-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 #