Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Coverage.SplitTree

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

Instances details
DropArgs SplitTree Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

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

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

Defined in Agda.TypeChecking.Coverage.SplitTree

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

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

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 #

Show LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Ord LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Instances

Instances details
KillRange SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

DropArgs SplitTree Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

PrettyTCM SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Pretty SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

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

Ord SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Instances

Instances details
Pretty a => Pretty (SplitTreeLabel a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

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