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.Extern.DeleteProofs

Description

Implementation of the necessary proofs to ensure (at compile time) that the deletion algorithm defined in Data.Tree.BST.Extern.Delete respects the key ordering.

Synopsis

class ProofIsBSTDelete (x :: Nat) (t :: Tree) where
- proofIsBSTDelete :: Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
class ProofIsBSTDelete' (x :: Nat) (t :: Tree) (o :: Ordering) where
- proofIsBSTDelete' :: Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)
class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- proofLtNDelete' :: LtN t n ~ 'True => Proxy x -> IsBSTT 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 -> IsBSTT t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
class ProofMaxKeyDeleteIsBST (t :: Tree) where
- proofMaxKeyDeleteIsBST :: IsBSTT t -> IsBSTT (MaxKeyDelete t)
class ProofGTMaxKey (t :: Tree) (n :: Nat) where
- proofGTMaxKey :: GtN t n ~ 'True => IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofGtNMaxKeyDelete :: GtN t n ~ 'True => IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
class ProofLTMaxKey (t :: Tree) (n :: Nat) where
- proofLTMaxKey :: LtN t n ~ 'True => IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
- proofLtNMaxKeyDelete :: LtN t n ~ 'True => IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True

Documentation

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

Prove that deleting a node with key x in a BST tree preserves BST restrictions.

Methods

proofIsBSTDelete :: Proxy x -> IsBSTT t -> IsBSTT (Delete x t) Source #

Instances

Instances details

ProofIsBSTDelete x 'EmptyTree Source #
Instance details Defined in Data.Tree.BST.Extern.DeleteProofs Methods proofIsBSTDelete :: Proxy x -> IsBSTT 'EmptyTree -> IsBSTT (Delete x 'EmptyTree) Source #
(o ~ CmpNat x n, ProofIsBSTDelete' x ('ForkTree l (Node n a1) r) o) => ProofIsBSTDelete x ('ForkTree l (Node n a1) r) Source #
Instance details Defined in Data.Tree.BST.Extern.DeleteProofs Methods proofIsBSTDelete :: Proxy x -> IsBSTT ('ForkTree l (Node n a1) r) -> IsBSTT (Delete x ('ForkTree l (Node n a1) r)) Source #

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

Prove that deleting a node with key x in a BST tree preserves BST restrictions, given that the comparison between x and the root key of the tree equals o. The BST restrictions were already checked when proofIsBSTDelete was called before. The o parameter guides the proof.

Methods

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

class ProofMaxKeyDeleteIsBST (t :: Tree) where Source #

Prove that deleting the node with maximum key value in a BST t preserves the BST restrictions. This proof is needed for the delete operation.

Methods

proofMaxKeyDeleteIsBST :: IsBSTT t -> IsBSTT (MaxKeyDelete t) Source #

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.

Methods

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

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

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 => IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True 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.

Methods

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

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

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 => IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True Source #