Data.Tree.AVL.Intern.Delete

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.

Documentation

class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where

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.

Methods

proofLtNDelete' :: (CmpNat x n ~ 'LT, LtN t n ~ 'True) => Proxy x -> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True

class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where

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.

Methods

proofGtNDelete' :: (CmpNat x n ~ 'GT, GtN t n ~ 'True) => Proxy x -> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True

class ProofGTMaxKey (t :: Tree) (n :: Nat) where

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.

Methods

proofGTMaxKey :: GtN t n ~ 'True => AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT

class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that GtN t n ~ 'True, the tree resulting from the removal of the maximum key of t preserves the GtN invariant. This proof is needed for the delete operation.

Methods

proofGtNMaxKeyDelete :: GtN t n ~ 'True => AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True

class ProofLTMaxKey (t :: Tree) (n :: Nat) where

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.

Methods

proofLTMaxKey :: LtN t n ~ 'True => AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT

class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where

Prove that in a tree t which verifies that LtN t n ~ 'True, the tree resulting from the removal of the maximum key of t preserves the LtN invariant. This proof is needed for the delete operation.

Methods

proofLtNMaxKeyDelete :: LtN t n ~ 'True => AVL t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True

class MaxKeyDeletable (t :: Tree) where

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

Methods

maxKeyDelete :: t ~ 'ForkTree l (Node n a1) r => AVL t -> AVL (MaxKeyDelete t)

class Maxable (t :: Tree) where

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.

Associated Types

type MaxKey (t :: Tree) :: Nat

type MaxValue (t :: Tree) :: Type

Methods

maxValue :: t ~ 'ForkTree l (Node n a1) r => AVL t -> MaxValue t

class Deletable (x :: Nat) (t :: Tree) where

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.

Associated Types

type Delete (x :: Nat) (t :: Tree) :: Tree

Methods

delete :: Proxy x -> AVL t -> AVL (Delete x t)

Instances

Deletable x 'EmptyTree

Defined in Data.Tree.AVL.Intern.Delete

Associated Types

type Delete x 'EmptyTree :: Tree

Methods

delete :: Proxy x -> AVL 'EmptyTree -> AVL (Delete x 'EmptyTree)

(o ~ CmpNat x n, Deletable' x ('ForkTree l (Node n a1) r) o) => Deletable x ('ForkTree l (Node n a1) r)

Defined in Data.Tree.AVL.Intern.Delete

Associated Types

type Delete x ('ForkTree l (Node n a1) r) :: Tree

Methods

delete :: Proxy x -> AVL ('ForkTree l (Node n a1) r) -> AVL (Delete x ('ForkTree l (Node n a1) r))

class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where

This type class provides the functionality to delete a node with key x in a non empty AVL t. It's only used by the Deletable class and it has one extra parameter o, which is the type level comparison of x with the key value of the root node. The o parameter guides the insertion.

Associated Types

type Delete' (x :: Nat) (t :: Tree) (o :: Ordering) :: Tree

Methods

delete' :: Proxy x -> AVL t -> Proxy o -> AVL (Delete' x t o)