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

Safe HaskellNone
LanguageHaskell98

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

Show a => Show (SplitTree' a) Source # 
Arbitrary a => Arbitrary (SplitTree' a) Source # 

Methods

arbitrary :: Gen (SplitTree' a)

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

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.

Printing a split tree

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

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

Generating random split trees for testing

Testing the printer

newtype CName Source #

Constructors

CName String 

Instances

Show CName Source # 

Methods

showsPrec :: Int -> CName -> ShowS #

show :: CName -> String #

showList :: [CName] -> ShowS #

Arbitrary CName Source # 

Methods

arbitrary :: Gen CName

shrink :: CName -> [CName]