Copyright	(c) Nicolás Rodríguez 2021
License	GPL-3
Maintainer	Nicolás Rodríguez
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

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

data AVL :: Tree -> Type where
- AVL :: ITree t -> IsBSTT t -> IsBalancedT t -> AVL t
mkAVL :: (IsBSTC t, IsBalancedC t) => ITree t -> AVL t
data IsBalancedT :: Tree -> Type where
- 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
- isBalancedT :: IsBalancedT t
data IsAlmostBalancedT :: Tree -> Type where
- ForkIsAlmostBalancedT :: IsBalancedT l -> Proxy (Node n a) -> IsBalancedT r -> IsAlmostBalancedT ('ForkTree l (Node n a) r)

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.

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

Type class for automatically constructing the proof term IsBalancedT.

Methods

isBalancedT :: IsBalancedT t Source #

Instances

Instances details

IsBalancedC 'EmptyTree Source #	Instances for the type class `IsBalancedC`.
Instance details Defined in Data.Tree.AVL.Extern.Constructors Methods isBalancedT :: IsBalancedT 'EmptyTree Source #
(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)