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.BST.Intern.Delete

Description

Implementation of the deletion algorithm over internalist BST trees, along with the necessary proofs to ensure (at compile time) that the key ordering still holds.

Synopsis

class MaxKeyDeletable (t :: Tree) where
- type MaxKeyDelete (t :: Tree) :: Tree
- maxKeyDelete :: t ~ 'ForkTree l (Node n a1) r => BST t -> BST (MaxKeyDelete t)
class Maxable (t :: Tree) where
- type MaxKey (t :: Tree) :: Nat
- type MaxValue (t :: Tree) :: Type
- maxValue :: t ~ 'ForkTree l (Node n a1) r => BST t -> MaxValue t
class Deletable (x :: Nat) (t :: Tree) where
- type Delete (x :: Nat) (t :: Tree) :: Tree
- delete :: Proxy x -> BST t -> BST (Delete x t)
class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where
- type Delete' (x :: Nat) (t :: Tree) (o :: Ordering) :: Tree
- delete' :: Proxy x -> BST t -> Proxy o -> BST (Delete' x t o)
class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- proofLtNDelete' :: LtN t n ~ 'True => Proxy x -> BST t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- proofGtNDelete' :: GtN t n ~ 'True => Proxy x -> BST t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
class ProofGTMaxKey (t :: Tree) (n :: Nat) where
- proofGTMaxKey :: GtN t n ~ 'True => BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofGtNMaxKeyDelete :: GtN t n ~ 'True => BST t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
class ProofLTMaxKey (t :: Tree) (n :: Nat) where
- proofLTMaxKey :: LtN t n ~ 'True => BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofLtNMaxKeyDelete :: LtN t n ~ 'True => BST t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True

Documentation

class MaxKeyDeletable (t :: Tree) where Source #

This type class provides the functionality to delete the node with maximum key value in a BST 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 => BST t -> BST (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 a BST 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 Source #

type MaxValue (t :: Tree) :: Type Source #

Methods

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

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

This type class provides the functionality to delete a node with key x in a BST t. The deletion is defined at the value level and the type level. The returned tree verifies the BST invariant.

Associated Types

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

Methods

delete :: Proxy x -> BST t -> BST (Delete x t) Source #

Instances

Instances details

Deletable x 'EmptyTree Source #
Instance details Defined in Data.Tree.BST.Intern.Delete Associated Types type Delete x 'EmptyTree :: Tree Source # Methods delete :: Proxy x -> BST 'EmptyTree -> BST (Delete x 'EmptyTree) Source #
(o ~ CmpNat x n, Deletable' x ('ForkTree l (Node n a1) r) o) => Deletable x ('ForkTree l (Node n a1) r) Source #
Instance details Defined in Data.Tree.BST.Intern.Delete Associated Types type Delete x ('ForkTree l (Node n a1) r) :: Tree Source # Methods delete :: Proxy x -> BST ('ForkTree l (Node n a1) r) -> BST (Delete x ('ForkTree l (Node n a1) r)) Source #

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

This type class provides the functionality to delete a node with key x in a non empty BST 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 Source #

Methods

delete' :: Proxy x -> BST t -> Proxy o -> BST (Delete' x t o) Source #

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 BST 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' :: LtN t n ~ 'True => Proxy x -> BST t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True Source #

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 BST 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' :: GtN t n ~ 'True => Proxy x -> BST t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True Source #

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

Prove that in a BST 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 => BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT Source #

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

Prove that in a BST 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 => BST t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True Source #

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

Prove that in a BST 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 => BST t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT Source #

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

Prove that in a BST 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 => BST t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True Source #