Copyright | (c) Nicolás Rodríguez 2021 |
---|---|
License | GPL-3 |
Maintainer | Nicolás Rodríguez |
Stability | experimental |
Portability | POSIX |
Safe Haskell | Safe |
Language | Haskell2010 |
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
- class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
- class ProofMaxKeyDeleteIsBST (t :: Tree) where
- proofMaxKeyDeleteIsBST :: IsBSTT t -> IsBSTT (MaxKeyDelete t)
- class ProofGTMaxKey (t :: Tree) (n :: Nat) where
- 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
- 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.
Instances
ProofIsBSTDelete x 'EmptyTree Source # | |
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 # | |
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.
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.
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.
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.
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.
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where 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.