Data.Tree.BST.Extern.Delete

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

Documentation

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 a tree t without checking any structural invariant (key ordering). The lookup is defined at the value level and the type level, and is performed as if the tree is a BST. 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 => ITree t -> MaxValue t

Instances

Maxable ('ForkTree rl (Node rn ra) rr) => Maxable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))

Defined in Data.Tree.BST.Extern.Delete

Associated Types

type MaxKey ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) :: Nat

type MaxValue ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))

Methods

maxValue :: 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)) -> MaxValue ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))

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

Defined in Data.Tree.BST.Extern.Delete

Associated Types

type MaxKey ('ForkTree l (Node n a1) 'EmptyTree) :: Nat

type MaxValue ('ForkTree l (Node n a1) 'EmptyTree)

Methods

maxValue :: 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) -> MaxValue ('ForkTree l (Node n a1) 'EmptyTree)

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). The deletion is defined at the value level and the type level, and is performed as if the tree is a BST; the verification of the BST 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.BST.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)

MaxKeyDeletable ('ForkTree rl (Node rn ra) rr) => MaxKeyDeletable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))

Defined in Data.Tree.BST.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.BST.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). The deletion is defined at the value level and the type level, and is performed as if the tree is a BST; the key ordering is verified 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.BST.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.BST.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) where

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

Associated Types

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

Methods

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

Instances

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

Defined in Data.Tree.BST.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.BST.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)

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

Defined in Data.Tree.BST.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.BST.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, Show (MaxValue l), MaxKeyDeletable l, Maxable l) => Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ

Defined in Data.Tree.BST.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.BST.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.BST.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.BST.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)