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

Safe Haskell | None

Agda.TypeChecking.Coverage.SplitTree

Contents

- Printing a split tree
- Generating random split trees for testing
- Testing the printer

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

- type SplitTree = SplitTree' QName
- type SplitTrees = SplitTrees' QName
- data SplitTree' a
  - = SplittingDone {
    - splitBindings :: Int
    }
  - | SplitAt {
    - splitArg :: Int
    - splitTrees :: SplitTrees' a
    }
- type SplitTrees' a = [(a, SplitTree' a)]
- data SplitTreeLabel a = SplitTreeLabel {
  - lblConstructorName :: Maybe a
  - lblSplitArg :: Maybe Int
  - lblBindings :: Maybe Int
  }
- toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
- toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
- newtype CName = CName String
- testSplitTreePrinting :: IO ()

# 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 :: Int

  Arg. no to split at.

splitTrees :: SplitTrees' a

  Sub split trees.

Instances

Eq a => Eq (SplitTree' a) |
Show a => Show (SplitTree' a) |
Arbitrary a => Arbitrary (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 Int
lblBindings :: Maybe Int

Instances

Show a => Show (SplitTreeLabel a) |

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 |
Arbitrary CName |

testSplitTreePrinting :: IO ()