| 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.Delete
Description
Implementation of the deletion algorithm over internalist AVL trees, along with the necessary proofs to ensure (at compile time) that the key ordering and height balancing still holds.
Synopsis
- class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- class ProofGTMaxKey (t :: Tree) (n :: Nat) where
- class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofGtNMaxKeyDelete :: GtN t n ~ 'True => AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
- class ProofLTMaxKey (t :: Tree) (n :: Nat) where
- class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofLtNMaxKeyDelete :: LtN t n ~ 'True => AVL t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
- class MaxKeyDeletable (t :: Tree) where
- type MaxKeyDelete (t :: Tree) :: Tree
- maxKeyDelete :: t ~ 'ForkTree l (Node n a1) r => AVL t -> AVL (MaxKeyDelete t)
- class Maxable (t :: Tree) where
- class Deletable (x :: Nat) (t :: Tree) where
- class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where
Documentation
class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #
Prove that deleting a node with key x (lower than n)
in a tree t which verifies LtN t n ~ 'True preserves the LtN invariant,
given that the comparison between x and the root key of the tree equals o.
The o parameter guides the proof.
class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #
Prove that deleting a node with key x (greater than n)
in a tree t which verifies GtN t n ~ 'True preserves the GtN invariant,
given that the comparison between x and the root key of the tree equals o.
The o parameter guides the proof.
class ProofGTMaxKey (t :: Tree) (n :: Nat) where Source #
Prove that in a tree t which verifies that GtN t n ~ 'True,
the maximum key of t is also greater than n.
This proof is needed for the delete operation.
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where Source #
class ProofLTMaxKey (t :: Tree) (n :: Nat) where Source #
Prove that in a tree t which verifies that LtN t n ~ 'True,
the maximum key of t is also less than n.
This proof is needed for the delete operation.
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where Source #
class MaxKeyDeletable (t :: Tree) where Source #
This type class provides the functionality to delete the node with maximum key value
in an AVL t.
The deletion is defined at the value level and the type level.
Associated Types
type MaxKeyDelete (t :: Tree) :: Tree Source #
Methods
maxKeyDelete :: t ~ 'ForkTree l (Node n a1) r => AVL t -> AVL (MaxKeyDelete t) Source #
class Maxable (t :: Tree) where Source #
This type class provides the functionality to get the key, type and value of the node with maximum key value
in an AVL t.
The lookup is defined at the value level and the type level.
Since the keys are only kept at the type level, there's no value level getter of the maximum key.
class Deletable (x :: Nat) (t :: Tree) where Source #
This type class provides the functionality to delete the node with key x
in an AVL t.
The deletion is defined at the value level and the type level,
and both return AVL trees.
class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where Source #