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

class Balanceable (t :: Tree) where
- type Balance (t :: Tree) :: Tree
- balance :: AlmostAVL t -> AVL (Balance t)
class Balanceable' (t :: Tree) (us :: US) where
- type Balance' (t :: Tree) (us :: US) :: Tree
- balance' :: AlmostAVL t -> Proxy us -> AVL (Balance' t us)
class Rotateable (t :: Tree) (us :: US) (bs :: BS) where
- type Rotate (t :: Tree) (us :: US) (bs :: BS) :: Tree
- rotate :: AlmostAVL t -> Proxy us -> Proxy bs -> AVL (Rotate t us bs)
class ProofLtNBalance (t :: Tree) (n :: Nat) where
- proofLtNBalance :: LtN t n ~ 'True => AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True
class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- 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
- 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
- proofGtNBalance :: GtN t n ~ 'True => AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True
class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- 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
- proofGtNRotate :: GtN t n ~ 'True => AlmostAVL t -> Proxy n -> Proxy us -> Proxy bs -> GtN (Rotate t us bs) n :~: 'True

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 #