Data.Tree.BST.Intern.Insert

Implementation of the insertion algorithm over internalist BST trees, along with the necessary proofs to ensure (at compile time) that the key ordering still holds.

Documentation

class Insertable (x :: Nat) (a :: Type) (t :: Tree) where

This type class provides the functionality to insert a node with key x and value type a in a BST t. The insertion is defined at the value level and the type level. The returned tree verifies the BST restrictions.

Associated Types

type Insert (x :: Nat) (a :: Type) (t :: Tree) :: Tree

Methods

insert :: Node x a -> BST t -> BST (Insert x a t)

Instances

Show a => Insertable x a 'EmptyTree

Defined in Data.Tree.BST.Intern.Insert

Associated Types

type Insert x a 'EmptyTree :: Tree

Methods

insert :: Node x a -> BST 'EmptyTree -> BST (Insert x a 'EmptyTree)

(o ~ CmpNat x n, Insertable' x a ('ForkTree l (Node n a1) r) o) => Insertable x a ('ForkTree l (Node n a1) r)

Defined in Data.Tree.BST.Intern.Insert

Associated Types

type Insert x a ('ForkTree l (Node n a1) r) :: Tree

Methods

insert :: Node x a -> BST ('ForkTree l (Node n a1) r) -> BST (Insert x a ('ForkTree l (Node n a1) r))

class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where

This type class provides the functionality to insert a node with key x and value type a in a non empty BST t. It's only used by the Insertable class and it has one extra parameter o, which is the type level comparison of x with the key value of the root node. The o parameter guides the insertion.

Associated Types

type Insert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) :: Tree

Methods

insert' :: Node x a -> BST t -> Proxy o -> BST (Insert' x a t o)

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

Prove that inserting a node with key x (lower than n) and element value a in a BST 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) => Node x a -> BST t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True

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

Prove that inserting a node with key x (greater than n) and element value a in a BST 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) => Node x a -> BST t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True