Data.Tree.AVL.Intern.Constructors

Implementation of the constructor of type safe internalist AVL trees and instance definition for the Show type class.

Documentation

data AVL :: Tree -> Type where

Constructor of AVL trees. Given two AVL trees and an arbitrary node, it tests at compile time wether the key of the node verifies the LtN and GtN invariants with respect to each tree and if the heights are balanced. Notice that, by inductive reasoning, this is all that's needed to assert that the new tree is a AVL.

Constructors

EmptyAVL :: AVL 'EmptyTree

ForkAVL :: (Show a, LtN l n ~ 'True, GtN r n ~ 'True, BalancedHeights (Height l) (Height r) n ~ 'True) => AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)

Instances

Show (AVL t)

Instance definition for the Show type class.

Defined in Data.Tree.AVL.Intern.Constructors

Methods

showsPrec :: Int -> AVL t -> ShowS

show :: AVL t -> String

showList :: [AVL t] -> ShowS

data AlmostAVL :: Tree -> Type where

Constructor of AlmostAVL tress. This kind of trees arises after an insertion or deletion over an AVL that may leave the tree unbalanced.

Constructors

AlmostAVL :: (Show a, LtN l n ~ 'True, GtN r n ~ 'True) => AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)