type-safe-avl-1.0.0.1: 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.Intern.Balance

Description

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).

Synopsis

Documentation

class Balanceable (t :: Tree) where Source #

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

Methods

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

Instances

Instances details
(us ~ UnbalancedState (Height l) (Height r), Balanceable' ('ForkTree l (Node n a) r) us) => Balanceable ('ForkTree l (Node n a) r) Source # 
Instance details

Defined in Data.Tree.AVL.Intern.Balance

Associated Types

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Instances

Instances details
(us ~ UnbalancedState (Height l) (Height r), ProofLtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofLtNBalance ('ForkTree l (Node n1 a) r) n Source # 
Instance details

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

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

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

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

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

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

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

Instances

Instances details
(us ~ UnbalancedState (Height l) (Height r), ProofGtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofGtNBalance ('ForkTree l (Node n1 a) r) n Source # 
Instance details

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

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

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

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

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