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' QName

type SplitTrees = SplitTrees' QName

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.

• splitTrees :: SplitTrees' a

  Sub split trees.

Instances

Show a => Show (SplitTree' a)

Methods

showsPrec :: Int -> SplitTree' a -> ShowS

show :: SplitTree' a -> String

showList :: [SplitTree' a] -> ShowS

Arbitrary a => Arbitrary (SplitTree' a)

Methods

arbitrary :: Gen (SplitTree' a)

shrink :: SplitTree' a -> [SplitTree' a]

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.

Printing a split tree

data SplitTreeLabel a

Constructors

SplitTreeLabel

Fields

• lblConstructorName :: Maybe a

  Nothing for root of split tree

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

Instances

Show a => Show (SplitTreeLabel a)

Methods

showsPrec :: Int -> SplitTreeLabel a -> ShowS

show :: SplitTreeLabel a -> String

showList :: [SplitTreeLabel a] -> ShowS

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

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

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

Generating random split trees for testing

Testing the printer

newtype CName

Constructors

CName String

Instances

Show CName

Methods

showsPrec :: Int -> CName -> ShowS

show :: CName -> String

showList :: [CName] -> ShowS

Arbitrary CName

Methods

arbitrary :: Gen CName

shrink :: CName -> [CName]

testSplitTreePrinting :: IO ()