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

Description

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

Synopsis

class ProofIsBSTInsert (x :: Nat) (a :: Type) (t :: Tree) where
- proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
class ProofIsBSTInsert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
- proofIsBSTInsert' :: Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)
class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
- proofLtNInsert' :: (CmpNat x n ~ 'LT, LtN t n ~ 'True) => Proxy (Node x a) -> IsBSTT t -> Proxy n -> Proxy o -> LtN (Insert' x a t o) n :~: 'True
class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
- proofGtNInsert' :: (CmpNat x n ~ 'GT, GtN t n ~ 'True) => Proxy (Node x a) -> IsBSTT t -> Proxy n -> Proxy o -> GtN (Insert' x a t o) n :~: 'True

Documentation

class ProofIsBSTInsert (x :: Nat) (a :: Type) (t :: Tree) where Source #

Prove that inserting a node with key x and element value a in a BST tree preserves the BST condition.

Methods

proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t) Source #

Instances

Instances details

ProofIsBSTInsert x a 'EmptyTree Source #
Instance details Defined in Data.Tree.BST.Extern.InsertProofs Methods proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT 'EmptyTree -> IsBSTT (Insert x a 'EmptyTree) Source #
(o ~ CmpNat x n, ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) o) => ProofIsBSTInsert x a ('ForkTree l (Node n a1) r) Source #
Instance details Defined in Data.Tree.BST.Extern.InsertProofs Methods proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT ('ForkTree l (Node n a1) r) -> IsBSTT (Insert x a ('ForkTree l (Node n a1) r)) Source #

class ProofIsBSTInsert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where Source #

Prove that inserting a node with key x and element value a in a BST tree preserves the BST condition, given that the comparison between x and the root key of the tree equals o. The BST condition was already checked when proofIsBSTInsert was called before. The o parameter guides the proof.

Methods

proofIsBSTInsert' :: Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o) Source #

class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #

Prove that inserting a node with key x (lower than n) and element value a 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

proofLtNInsert' :: (CmpNat x n ~ 'LT, LtN t n ~ 'True) => Proxy (Node x a) -> IsBSTT t -> Proxy n -> Proxy o -> LtN (Insert' x a t o) n :~: 'True Source #

class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #

Prove that inserting a node with key x (greater than n) and element value a 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

proofGtNInsert' :: (CmpNat x n ~ 'GT, GtN t n ~ 'True) => Proxy (Node x a) -> IsBSTT t -> Proxy n -> Proxy o -> GtN (Insert' x a t o) n :~: 'True Source #