Agda.TypeChecking.Coverage.SplitTree

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.

Documentation

type SplitTree = SplitTree' SplitTag

type SplitTrees = SplitTrees' SplitTag

data SplitTree' a

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

DropArgs SplitTree

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> SplitTree -> SplitTree

KillRange a => KillRange (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT (SplitTree' a)

EmbPrj a => EmbPrj (SplitTree' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTree' a -> S Int32

icod_ :: SplitTree' a -> S Int32

value :: Int32 -> R (SplitTree' a)

Pretty a => Pretty (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTree' a -> Doc

prettyPrec :: Int -> SplitTree' a -> Doc

prettyList :: [SplitTree' a] -> Doc

Generic (SplitTree' a)

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)

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)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

rnf :: SplitTree' a -> ()

type Rep (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

type Rep (SplitTree' a) = D1 ('MetaData "SplitTree'" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.2.2.20230105-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

Constructors

LazySplit

StrictSplit

Instances

EmbPrj LazySplit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32

icod_ :: LazySplit -> S Int32

value :: Int32 -> R LazySplit

Generic LazySplit

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

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

showsPrec :: Int -> LazySplit -> ShowS

show :: LazySplit -> String

showList :: [LazySplit] -> ShowS

NFData LazySplit

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

rnf :: LazySplit -> ()

Eq LazySplit

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

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

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

Ord LazySplit

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

Defined in Agda.TypeChecking.Coverage.SplitTree

type Rep LazySplit = D1 ('MetaData "LazySplit" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "LazySplit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StrictSplit" 'PrefixI 'False) (U1 :: Type -> Type))

type SplitTrees' a = [(a, SplitTree' a)]

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

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

KillRange SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT SplitTag

DropArgs SplitTree

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> SplitTree -> SplitTree

PrettyTCM SplitTag

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => SplitTag -> m Doc

EmbPrj SplitTag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32

icod_ :: SplitTag -> S Int32

value :: Int32 -> R SplitTag

Pretty SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTag -> Doc

prettyPrec :: Int -> SplitTag -> Doc

prettyList :: [SplitTag] -> Doc

Generic SplitTag

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

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

showsPrec :: Int -> SplitTag -> ShowS

show :: SplitTag -> String

showList :: [SplitTag] -> ShowS

NFData SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

rnf :: SplitTag -> ()

Eq SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

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

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

Ord SplitTag

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

Defined in Agda.TypeChecking.Coverage.SplitTree

type Rep SplitTag = D1 ('MetaData "SplitTag" "Agda.TypeChecking.Coverage.SplitTree" "Agda-2.6.2.2.20230105-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

Constructors

SplitTreeLabel

Fields

• lblConstructorName :: Maybe a

  Nothing for root of split tree

• lblSplitArg :: Maybe (Arg Int)
• lblLazy :: LazySplit
• lblBindings :: Maybe Int

Instances

Pretty a => Pretty (SplitTreeLabel a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTreeLabel a -> Doc

prettyPrec :: Int -> SplitTreeLabel a -> Doc

prettyList :: [SplitTreeLabel a] -> Doc

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

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

toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)