Data.Trees

Definitions

data BinTree : Type -> Type -> Type

  Finite binary trees with labels on leaves and nodes

Totality: total
Visibility: public export
Constructors:

Leaf : leafType -> BinTree leafType nodeType

Node : nodeType -> BinTree leafType nodeType -> BinTree leafType nodeType -> BinTree leafType nodeType

Hints:

Bifunctor BinTree

Eq leafType => Eq nodeType => Eq (BinTree leafType nodeType)

Show leafType => Show nodeType => Show (BinTree leafType nodeType)

BinTreeSame : Type -> Type

  Binary trees with the same type of value on both leaves and nodes

Totality: total
Visibility: public export

liftA2BinTreeSame : BinTreeSame a -> BinTreeSame b -> BinTreeSame (a, b)

  Smaller tree expands to the shape of a bigger one
  We can do this for BinTreeSame but not for BinTree precisely
  because we copy the leaf value across to the nodes

Totality: total
Visibility: public export

BinTreeLeaf : Type -> Type

Totality: total
Visibility: public export

Node' : BinTree l () -> BinTree l () -> BinTree l ()

  Helper function to construct a node with a trivial value

Totality: total
Visibility: public export

liftA2BinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf b -> BinTreeLeaf (a, b)

Totality: total
Visibility: public export

BinTreeNode : Type -> Type

Totality: total
Visibility: public export

Leaf' : BinTree () n

  Helper function to construct a leaf with a trivial value

Totality: total
Visibility: public export

inorder : BinTree a b -> List (Either a b)

Totality: total
Visibility: public export

preorder : BinTree a b -> List (Either a b)

Totality: total
Visibility: public export

postorder : BinTree a b -> List (Either a b)

Totality: total
Visibility: public export

fromEitherUnit : List (Either a ()) -> List a

Totality: total
Visibility: public export

fromUnitEither : List (Either () a) -> List a

Totality: total
Visibility: public export

traverseBinTreeLeaf : BinTreeLeaf a -> List a

  For leaf-only trees, inorder=preorder=postorder

Totality: total
Visibility: public export

inorderNode : BinTreeNode a -> List a

Totality: total
Visibility: public export

preorderNode : BinTreeNode a -> List a

Totality: total
Visibility: public export

postorderNode : BinTreeNode a -> List a

Totality: total
Visibility: public export

data RoseTree : Type -> Type -> Type

  This can likely be generalised to work for an arbitrary applicative
  instead of just List

Totality: total
Visibility: public export
Constructors:

Leaf : leafType -> RoseTree leafType nodeType

Node : nodeType -> List (RoseTree leafType nodeType) -> RoseTree leafType nodeType

Hints:

Eq leafType => Eq nodeType => Eq (RoseTree leafType nodeType)

Show leafType => Show nodeType => Show (RoseTree leafType nodeType)

RoseTreeSame : Type -> Type

Totality: total
Visibility: public export

liftA2RoseTreeSame : RoseTreeSame a -> RoseTreeSame b -> RoseTreeSame (a, b)

Visibility: public export