balanced-binary-search-tree-1.0.0.0: Type safe BST and AVL trees
Copyright(c) Nicolás Rodríguez 2021
LicenseGPL-3
MaintainerNicolás Rodríguez
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

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

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

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

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 #