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

Safe HaskellNone
LanguageHaskell2010

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

Documentation

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
DropArgs SplitTree Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> SplitTree -> SplitTree 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 :: (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)

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

Pretty a => Pretty (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

KillRange a => KillRange (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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 #

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).

Instances
Eq SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

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

(/=) :: SplitTag -> SplitTag -> Bool

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 :: (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

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

Show SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

showsPrec :: Int -> SplitTag -> ShowS

show :: SplitTag -> String

showList :: [SplitTag] -> ShowS

Pretty SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

KillRange SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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 #

PrettyTCM SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

DropArgs SplitTree Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> SplitTree -> SplitTree Source #

Printing a split tree

data SplitTreeLabel a Source #

Constructors

SplitTreeLabel 

Fields

toTree :: SplitTree' a -> Tree (SplitTreeLabel a) Source #

Convert a split tree into a Tree (for printing).