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

Description

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.

Synopsis

class ProofIsBSTBalance (t :: Tree) where
- proofIsBSTBalance :: IsBSTT t -> IsBSTT (Balance t)
class ProofIsBSTBalance' (t :: Tree) (us :: US) where
- proofIsBSTBalance' :: IsBSTT t -> Proxy us -> IsBSTT (Balance' t us)
class ProofIsBSTRotate (t :: Tree) (us :: US) (bs :: BS) where
- proofIsBSTRotate :: IsBSTT t -> Proxy us -> Proxy bs -> IsBSTT (Rotate t us bs)
class ProofLtNBalance (t :: Tree) (n :: Nat) where
- proofLtNBalance :: LtN t n ~ 'True => IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- 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
- 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
- proofGtNBalance :: GtN t n ~ 'True => IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- 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
- 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
- proofIsBalancedBalance :: IsAlmostBalancedT t -> IsBalancedT (Balance t)
class ProofIsBalancedBalance' (t :: Tree) (us :: US) where
- 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
- 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)

Documentation

class ProofIsBSTBalance (t :: Tree) where Source #

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

Instances

Instances details

ProofIsBSTBalance 'EmptyTree Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofIsBSTBalance :: IsBSTT 'EmptyTree -> IsBSTT (Balance 'EmptyTree) Source #
(us ~ UnbalancedState (Height l) (Height r), ProofIsBSTBalance' ('ForkTree l (Node n a) r) us) => ProofIsBSTBalance ('ForkTree l (Node n a) r) Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofIsBSTBalance :: IsBSTT ('ForkTree l (Node n a) r) -> IsBSTT (Balance ('ForkTree l (Node n a) r)) Source #

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

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

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

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

Instances

Instances details

ProofLtNBalance 'EmptyTree n Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofLtNBalance :: IsBSTT 'EmptyTree -> Proxy n -> LtN (Balance 'EmptyTree) n :~: 'True Source #
(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.Extern.BalanceProofs Methods proofLtNBalance :: IsBSTT ('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 unbalanced state us of the tree.

Methods

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

Instances

Instances details

ProofGtNBalance 'EmptyTree n Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofGtNBalance :: IsBSTT 'EmptyTree -> Proxy n -> GtN (Balance 'EmptyTree) n :~: 'True Source #
(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.Extern.BalanceProofs Methods proofGtNBalance :: IsBSTT ('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 unbalanced state us of the tree.

Methods

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

class ProofIsBalancedBalance (t :: Tree) where Source #

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

Instances

Instances details

ProofIsBalancedBalance 'EmptyTree Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofIsBalancedBalance :: IsAlmostBalancedT 'EmptyTree -> IsBalancedT (Balance 'EmptyTree) Source #
(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) Source #
Instance details Defined in Data.Tree.AVL.Extern.BalanceProofs Methods proofIsBalancedBalance :: IsAlmostBalancedT ('ForkTree l (Node n a) r) -> IsBalancedT (Balance ('ForkTree l (Node n a) r)) Source #

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

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

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

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