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

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SplitTree' a) Source #

toConstr :: SplitTree' a -> Constr Source #

dataTypeOf :: SplitTree' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SplitTree' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> SplitTree' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a) Source #

Generic (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep (SplitTree' a) :: Type -> Type Source # Methods from :: SplitTree' a -> Rep (SplitTree' a) x Source # to :: Rep (SplitTree' a) x -> SplitTree' a Source #
Show a => Show (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> SplitTree' a -> ShowS Source # show :: SplitTree' a -> String Source # showList :: [SplitTree' a] -> ShowS Source #
NFData a => NFData (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: SplitTree' a -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LazySplit Source #

toConstr :: LazySplit -> Constr Source #

dataTypeOf :: LazySplit -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LazySplit) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LazySplit) Source #

gmapT :: (forall b. Data b => b -> b) -> LazySplit -> LazySplit Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LazySplit -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LazySplit -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LazySplit -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LazySplit -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit Source #

Generic LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep LazySplit :: Type -> Type Source # Methods from :: LazySplit -> Rep LazySplit x Source # to :: Rep LazySplit x -> LazySplit Source #
Show LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> LazySplit -> ShowS Source # show :: LazySplit -> String Source # showList :: [LazySplit] -> ShowS Source #
NFData LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: LazySplit -> () Source #
Eq LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods (==) :: LazySplit -> LazySplit -> Bool Source # (/=) :: LazySplit -> LazySplit -> Bool Source #
Ord LazySplit Source # |

Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

compare :: LazySplit -> LazySplit -> Ordering Source #

(<) :: LazySplit -> LazySplit -> Bool Source #

(<=) :: LazySplit -> LazySplit -> Bool Source #

(>) :: LazySplit -> LazySplit -> Bool Source #

(>=) :: LazySplit -> LazySplit -> Bool Source #

max :: LazySplit -> LazySplit -> LazySplit Source #

min :: LazySplit -> LazySplit -> LazySplit Source #

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.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SplitTag Source #

toConstr :: SplitTag -> Constr Source #

dataTypeOf :: SplitTag -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SplitTag) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SplitTag) Source #

gmapT :: (forall b. Data b => b -> b) -> SplitTag -> SplitTag Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SplitTag -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SplitTag -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> SplitTag -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SplitTag -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag Source #

Generic SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Associated Types type Rep SplitTag :: Type -> Type Source # Methods from :: SplitTag -> Rep SplitTag x Source # to :: Rep SplitTag x -> SplitTag Source #
Show SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods showsPrec :: Int -> SplitTag -> ShowS Source # show :: SplitTag -> String Source # showList :: [SplitTag] -> ShowS Source #
NFData SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods rnf :: SplitTag -> () Source #
Eq SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods (==) :: SplitTag -> SplitTag -> Bool Source # (/=) :: SplitTag -> SplitTag -> Bool Source #
Ord SplitTag Source # |

Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

compare :: SplitTag -> SplitTag -> Ordering Source #

(<) :: SplitTag -> SplitTag -> Bool Source #

(<=) :: SplitTag -> SplitTag -> Bool Source #

(>) :: SplitTag -> SplitTag -> Bool Source #

(>=) :: SplitTag -> SplitTag -> Bool Source #

max :: SplitTag -> SplitTag -> SplitTag Source #

min :: SplitTag -> SplitTag -> SplitTag Source #

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.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #