Data.Tree.AVL.Extern.Constructors

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

Documentation

data AVL :: Tree -> Type where

Constructor of AVL trees. Given an arbitrary ITree, it constructs a new AVL together with the proof terms IsBSTT, which shows that the keys are ordered, and IsBalancedT, which shows that the heights are balanced.

Constructors

AVL :: ITree t -> IsBSTT t -> IsBalancedT t -> AVL t

Instances

Show (AVL t)

Instance definition for the Show type class. It relies on the instance for ITree.

Defined in Data.Tree.AVL.Extern.Constructors

Methods

showsPrec :: Int -> AVL t -> ShowS

show :: AVL t -> String

showList :: [AVL t] -> ShowS

mkAVL :: (IsBSTC t, IsBalancedC t) => ITree t -> AVL t

Given an ITree, compute the proof terms IsBSTT and IsBalancedT, through the type classes IsBSTC and IsBalancedC in order to check if it is an AVL tree. This is the fully externalist constructor for AVL trees.

data IsBalancedT :: Tree -> Type where

Proof term which shows that t is an AVL. The restrictions on the constructor ForkIsBalancedT are verified at compile time. Given two proofs of AVL and an arbitrary node, it tests wether the heights of the sub trees are balanced. Notice that this is all that's needed to assert that the new tree is a AVL, since, both left and right proofs are evidence of height balance in both left and right sub trees.

Constructors

EmptyIsBalancedT :: IsBalancedT 'EmptyTree

ForkIsBalancedT :: BalancedHeights (Height l) (Height r) n ~ 'True => IsBalancedT l -> Proxy (Node n a) -> IsBalancedT r -> IsBalancedT ('ForkTree l (Node n a) r)

class IsBalancedC (t :: Tree) where

Type class for automatically constructing the proof term IsBalancedT.

Methods

isBalancedT :: IsBalancedT t

Instances

IsBalancedC 'EmptyTree

Instances for the type class IsBalancedC.

Defined in Data.Tree.AVL.Extern.Constructors

Methods

isBalancedT :: IsBalancedT 'EmptyTree

(IsBalancedC l, IsBalancedC r, BalancedHeights (Height l) (Height r) n ~ 'True) => IsBalancedC ('ForkTree l (Node n a) r)

Defined in Data.Tree.AVL.Extern.Constructors

Methods

isBalancedT :: IsBalancedT ('ForkTree l (Node n a) r)

data IsAlmostBalancedT :: Tree -> Type where

Proof term which shows that t is an Almost AVL.

Constructors

ForkIsAlmostBalancedT :: IsBalancedT l -> Proxy (Node n a) -> IsBalancedT r -> IsAlmostBalancedT ('ForkTree l (Node n a) r)