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

Description

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

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' :: (CmpNat x n ~ 'LT, 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' :: (CmpNat x n ~ 'GT, 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 :: (MaxKeyDeletable t, 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
class ProofMaxKeyDeleteIsBalanced (t :: Tree) where
- proofMaxKeyDeleteIsBalanced :: IsBalancedT t -> IsBalancedT (MaxKeyDelete t)
class ProofIsBalancedDelete (x :: Nat) (t :: Tree) where
- proofIsBalancedDelete :: Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)
class ProofIsBalancedDelete' (x :: Nat) (t :: Tree) (o :: Ordering) where
- proofIsBalancedDelete' :: Proxy x -> IsBalancedT t -> Proxy o -> IsBalancedT (Delete' x t o)

Documentation

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

Prove that deleting a node with key x | in an AVL tree preserves the AVL 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.AVL.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.AVL.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 inserting a node with key x and element value a in an AVL tree preserves the AVL restrictions, given that the comparison between x and the root key of the tree equals o. The AVL restrictions were already checked when proofIsBSTInsert 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 (lower than n) 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' :: (CmpNat x n ~ 'LT, 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 (greater than n) 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' :: (CmpNat x n ~ 'GT, 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 :: (MaxKeyDeletable t, 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 #

class ProofMaxKeyDeleteIsBalanced (t :: Tree) where Source #

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

Methods

proofMaxKeyDeleteIsBalanced :: IsBalancedT t -> IsBalancedT (MaxKeyDelete t) Source #

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

Prove that deleting a node with key x in an AVL tree preserves the AVL condition.

Methods

proofIsBalancedDelete :: Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t) Source #

Instances

Instances details

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

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

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

Methods

proofIsBalancedDelete' :: Proxy x -> IsBalancedT t -> Proxy o -> IsBalancedT (Delete' x t o) Source #