balanced-binary-search-tree-1.0.0.0: Type safe BST and AVL trees
Copyright(c) Nicolás Rodríguez 2021
LicenseGPL-3
MaintainerNicolás Rodríguez
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

Data.Tree.AVL.Extern.Constructors

Description

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

Synopsis

Documentation

data AVL :: Tree -> Type where Source #

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

Instances details
Show (AVL t) Source #

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

Instance details

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 Source #

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 Source #

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.

class IsBalancedC (t :: Tree) where Source #

Type class for automatically constructing the proof term IsBalancedT.

Instances

Instances details
IsBalancedC 'EmptyTree Source #

Instances for the type class IsBalancedC.

Instance details

Defined in Data.Tree.AVL.Extern.Constructors

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

Defined in Data.Tree.AVL.Extern.Constructors

Methods

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

data IsAlmostBalancedT :: Tree -> Type where Source #

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)