| 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
- class Balanceable' (t :: Tree) (us :: US) where
- class Rotateable (t :: Tree) (us :: US) (bs :: BS) where
- class ProofLtNBalance (t :: Tree) (n :: Nat) where
- class ProofLtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- class ProofLtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where
- class ProofGtNBalance (t :: Tree) (n :: Nat) where
- class ProofGtNBalance' (t :: Tree) (n :: Nat) (us :: US) where
- class ProofGtNRotate (t :: Tree) (n :: Nat) (us :: US) (bs :: BS) where
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.
Instances
| (us ~ UnbalancedState (Height l) (Height r), Balanceable' ('ForkTree l (Node n a) r) us) => Balanceable ('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.
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.
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
| (us ~ UnbalancedState (Height l) (Height r), ProofLtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofLtNBalance ('ForkTree l (Node n1 a) r) n 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.
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.
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
| (us ~ UnbalancedState (Height l) (Height r), ProofGtNBalance' ('ForkTree l (Node n1 a) r) n us) => ProofGtNBalance ('ForkTree l (Node n1 a) r) n 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.