Data.Tree.AVL.Extern.Delete

Implementation of the deletion algorithm over ITree trees for externalist AVL trees.

Documentation

class MaxKeyDeletable (t :: Tree) where

This type class provides the functionality to delete the node with maximum key value in a tree t without checking any structural invariant (key ordering or height balance). The deletion is defined at the value level and the type level, and is performed as if the tree is an AVL; the verification of the AVL restrictions is performed after the deletion.

Associated Types

type MaxKeyDelete (t :: Tree) :: Tree

Methods

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

Instances

MaxKeyDeletable 'EmptyTree

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type MaxKeyDelete 'EmptyTree :: Tree

Methods

maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree). 'EmptyTree ~ 'ForkTree l (Node n a1) r => ITree 'EmptyTree -> ITree (MaxKeyDelete 'EmptyTree)

(r ~ 'ForkTree rl (Node rn ra) rr, MaxKeyDeletable r, Balanceable ('ForkTree l (Node n a1) (MaxKeyDelete r))) => MaxKeyDeletable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type MaxKeyDelete ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) :: Tree

Methods

maxKeyDelete :: forall (l0 :: Tree) (n0 :: Nat) a10 (r :: Tree). 'ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr) ~ 'ForkTree l0 (Node n0 a10) r => ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) -> ITree (MaxKeyDelete ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)))

MaxKeyDeletable ('ForkTree l (Node n a1) 'EmptyTree)

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree) :: Tree

Methods

maxKeyDelete :: forall (l0 :: Tree) (n0 :: Nat) a10 (r :: Tree). 'ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l0 (Node n0 a10) r => ITree ('ForkTree l (Node n a1) 'EmptyTree) -> ITree (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))

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

This type class provides the functionality to delete the node with key x in a tree t without checking any structural invariant (key ordering or height balance). The deletion is defined at the value level and the type level, and is performed as if the tree is a AVL; the verification of the AVL restrictions is performed after the deletion.

Associated Types

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

Methods

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

Delete the node with the given key. If the key is not in the tree, return the same tree.

Instances

Deletable x 'EmptyTree

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete x 'EmptyTree :: Tree

Methods

delete :: Proxy x -> ITree 'EmptyTree -> ITree (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.Extern.Delete

Associated Types

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

Methods

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

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

This type class provides the functionality to delete a node with key x in a non empty tree t without checking any structural invariant (key ordering or height balance). It's only used by the Deletable type 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 deletion.

Minimal complete definition

delete'

Associated Types

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

Instances

(o ~ CmpNat x rn, r ~ 'ForkTree rl (Node rn ra) rr, Deletable' x r o, Balanceable ('ForkTree l (Node n a1) (Delete' x r o))) => Deletable' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) -> Proxy 'GT -> ITree (Delete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)

Deletable' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

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

Methods

delete' :: Proxy x -> ITree ('ForkTree l (Node n a1) 'EmptyTree) -> Proxy 'GT -> ITree (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)

(l ~ 'ForkTree ll (Node ln la) lr, o ~ CmpNat x ln, Deletable' x l o, Balanceable ('ForkTree (Delete' x l (CmpNat x ln)) (Node n a1) r)) => Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) -> Proxy 'LT -> ITree (Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)

Deletable' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

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

Methods

delete' :: Proxy x -> ITree ('ForkTree 'EmptyTree (Node n a1) r) -> Proxy 'LT -> ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)

(l ~ 'ForkTree ll (Node ln la) lr, r ~ 'ForkTree rl (Node rn ra) rr, Show (MaxValue l), MaxKeyDeletable l, Maxable l, Balanceable ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r)) => Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) -> Proxy 'EQ -> ITree (Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ)

Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) -> Proxy 'EQ -> ITree (Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ)

Deletable' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) -> Proxy 'EQ -> ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ)

Deletable' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ

Defined in Data.Tree.AVL.Extern.Delete

Associated Types

type Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ :: Tree

Methods

delete' :: Proxy x -> ITree ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) -> Proxy 'EQ -> ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)