Data.Tree.AVL.Intern.Balance

Implementation of the balancing algorithm over internalist AlmostAVL trees, along with the necessary proofs to ensure (at compile time) that the new tree is AVL (the balance is restored).

Documentation

class Balanceable (t :: Tree) where

This type class provides the functionality to balance an AlmostAVL t (a tree that came up from an insertion or deletion on an AVL). The insertion is defined at the value level and the type level.

Associated Types

type Balance (t :: Tree) :: Tree

Methods

balance :: AlmostAVL t -> AVL (Balance t)

Instances

(us ~ UnbalancedState (Height l) (Height r), Balanceable' ('ForkTree l (Node n a) r) us) => Balanceable ('ForkTree l (Node n a) r)

Defined in Data.Tree.AVL.Intern.Balance

Associated Types

type Balance ('ForkTree l (Node n a) r) :: Tree

Methods

balance :: AlmostAVL ('ForkTree l (Node n a) r) -> AVL (Balance ('ForkTree l (Node n a) r))

class Balanceable' (t :: Tree) (us :: US) where

This type class provides the functionality to balance an AlmostAVL t. It's only used by the Balanceable class and it has one extra parameter us, which is the UnbalancedState of the two sub trees of t.

Associated Types

type Balance' (t :: Tree) (us :: US) :: Tree

Methods

balance' :: AlmostAVL t -> Proxy us -> AVL (Balance' t us)

class Rotateable (t :: Tree) (us :: US) (bs :: BS) where

This type class provides the functionality to apply a rotation to an AlmostAVL tree t. The rotation is defined at the value level and the type level.

Associated Types

type Rotate (t :: Tree) (us :: US) (bs :: BS) :: Tree

Methods

rotate :: AlmostAVL t -> Proxy us -> Proxy bs -> AVL (Rotate t us bs)

class ProofLtNBalance (t :: Tree) (n :: Nat) where

Prove that rebalancing a tree t which verifies LtN t n ~ 'True preserves the LtN invariant.

Methods

proofLtNBalance :: LtN t n ~ 'True => AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True

Instances

(us ~ UnbalancedState (Height l) (Height r), ProofLtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofLtNBalance ('ForkTree l (Node n1 a) r) n

Defined in Data.Tree.AVL.Intern.Balance

Methods

proofLtNBalance :: AlmostAVL ('ForkTree l (Node n1 a) r) -> Proxy n -> LtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True

class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where

Prove that rebalancing a tree t which verifies LtN t n ~ 'True preserves the LtN invariant, given the UnbalancedState us of the tree. The us parameter guides the proof.

Methods

proofLtNBalance' :: LtN t n ~ 'True => AlmostAVL t -> Proxy n -> Proxy us -> LtN (Balance' t us) n :~: 'True

class ProofLtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where

Prove that applying a rotation to a tree t which verifies LtN t n ~ 'True preserves the LtN invariant.

Methods

proofLtNRotate :: LtN t n ~ 'True => AlmostAVL t -> Proxy n -> Proxy us -> Proxy bs -> LtN (Rotate t us bs) n :~: 'True

class ProofGtNBalance (t :: Tree) (n :: Nat) where

Prove that rebalancing a tree t which verifies GtN t n ~ 'True preserves the GtN invariant.

Methods

proofGtNBalance :: GtN t n ~ 'True => AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True

Instances

(us ~ UnbalancedState (Height l) (Height r), ProofGtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofGtNBalance ('ForkTree l (Node n1 a) r) n

Defined in Data.Tree.AVL.Intern.Balance

Methods

proofGtNBalance :: AlmostAVL ('ForkTree l (Node n1 a) r) -> Proxy n -> GtN (Balance ('ForkTree l (Node n1 a) r)) n :~: 'True

class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where

Prove that rebalancing a tree t which verifies GtN t n ~ 'True preserves the GtN invariant, given the UnbalancedState us of the tree. The us parameter guides the proof.

Methods

proofGtNBalance' :: GtN t n ~ 'True => AlmostAVL t -> Proxy n -> Proxy us -> GtN (Balance' t us) n :~: 'True

class ProofGtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where

Prove that applying a rotation to a tree t which verifies GtN t n ~ 'True preserves the GtN invariant.

Methods

proofGtNRotate :: GtN t n ~ 'True => AlmostAVL t -> Proxy n -> Proxy us -> Proxy bs -> GtN (Rotate t us bs) n :~: 'True