Data.Tree.AVL.Extern.BalanceProofs

Implementation of the necessary proofs to ensure (at compile time) that the balance algorithm defined in Data.Tree.AVL.Extern.Balance respects the key ordering and recovers the height balance.

Documentation

class ProofIsBSTBalance (t :: Tree) where

Prove that applying a rebalancing (a composition of rotations) to a BST tree preserves BST condition. The BST invariant was already checked since this proof is called after proofs for insert or delete.

Methods

proofIsBSTBalance :: IsBSTT t -> IsBSTT (Balance t)

Instances

ProofIsBSTBalance 'EmptyTree

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofIsBSTBalance :: IsBSTT 'EmptyTree -> IsBSTT (Balance 'EmptyTree)

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

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofIsBSTBalance :: IsBSTT ('ForkTree l (Node n a) r) -> IsBSTT (Balance ('ForkTree l (Node n a) r))

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

Prove that applying a rebalancing (a composition of rotations) to a BST tree preserves BST condition, given the comparison us of the heights of the left and right sub trees. This is called only from ProofIsBSTBalance. The BST invariant was already checked since this proof is called after proofs for insert or delete.

Methods

proofIsBSTBalance' :: IsBSTT t -> Proxy us -> IsBSTT (Balance' t us)

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

Prove that applying a rotation to a BST tree preserves BST condition. The BST invariant was already checked since this proof is called after proofs for insert or delete.

Methods

proofIsBSTRotate :: IsBSTT t -> Proxy us -> Proxy bs -> IsBSTT (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 => IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True

Instances

ProofLtNBalance 'EmptyTree n

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofLtNBalance :: IsBSTT 'EmptyTree -> Proxy n -> LtN (Balance 'EmptyTree) n :~: 'True

(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.Extern.BalanceProofs

Methods

proofLtNBalance :: IsBSTT ('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 unbalanced state us of the tree.

Methods

proofLtNBalance' :: LtN t n ~ 'True => IsBSTT 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 => IsBSTT 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 => IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True

Instances

ProofGtNBalance 'EmptyTree n

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofGtNBalance :: IsBSTT 'EmptyTree -> Proxy n -> GtN (Balance 'EmptyTree) n :~: 'True

(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.Extern.BalanceProofs

Methods

proofGtNBalance :: IsBSTT ('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 unbalanced state us of the tree.

Methods

proofGtNBalance' :: GtN t n ~ 'True => IsBSTT 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 => IsBSTT t -> Proxy n -> Proxy us -> Proxy bs -> GtN (Rotate t us bs) n :~: 'True

class ProofIsBalancedBalance (t :: Tree) where

Prove that applying a rebalancing (composition of rotations) to an `Almost Balanced` tree returns a `Balanced Tree`.

An `Almost Balanced` tree is a tree t ~ 'ForkTree l (Node n a) r which verifies all the following conditions:

• IsBalanced l ~ 'True

• IsBalanced r ~ 'True

In other words, it's a tree with left and right AVL sub trees that may not be balanced at the root.

Methods

proofIsBalancedBalance :: IsAlmostBalancedT t -> IsBalancedT (Balance t)

Instances

ProofIsBalancedBalance 'EmptyTree

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofIsBalancedBalance :: IsAlmostBalancedT 'EmptyTree -> IsBalancedT (Balance 'EmptyTree)

(us ~ UnbalancedState (Height l) (Height r), LtN l n ~ 'True, GtN r n ~ 'True, ProofIsBalancedBalance' ('ForkTree l (Node n a) r) us) => ProofIsBalancedBalance ('ForkTree l (Node n a) r)

Defined in Data.Tree.AVL.Extern.BalanceProofs

Methods

proofIsBalancedBalance :: IsAlmostBalancedT ('ForkTree l (Node n a) r) -> IsBalancedT (Balance ('ForkTree l (Node n a) r))

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

Prove that applying a rebalancing (a composition of rotations) to an `Almost AVL` tree returns an AVL, given the comparison us of the heights of the left and right sub trees. This is called only from ProofIsBalancedBalance.

Methods

proofIsBalancedBalance' :: (t ~ 'ForkTree l (Node n a) r, LtN l n ~ 'True, GtN r n ~ 'True) => IsAlmostBalancedT t -> Proxy us -> IsBalancedT (Balance' t us)

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

Prove that applying a rotation to an `Almost AVL` tree returns an AVL tree.

Methods

proofIsBalancedRotate :: (t ~ 'ForkTree l (Node n a) r, LtN l n ~ 'True, GtN r n ~ 'True) => IsAlmostBalancedT t -> Proxy us -> Proxy bs -> IsBalancedT (Rotate t us bs)