Data.Tree.AVL.Intern.Insert

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

Documentation

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 an AVL 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 -> AVL 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 an AVL 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 -> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True

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 an AVL t. The insertion is defined at the value level and the type level. The returned tree verifies the BST/AVL restrictions.

Associated Types

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

Methods

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

Instances

Show a => Insertable x a 'EmptyTree

Defined in Data.Tree.AVL.Intern.Insert

Associated Types

type Insert x a 'EmptyTree :: Tree

Methods

insert :: Node x a -> AVL 'EmptyTree -> AVL (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.AVL.Intern.Insert

Associated Types

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

Methods

insert :: Node x a -> AVL ('ForkTree l (Node n a1) r) -> AVL (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 AVL 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 -> AVL t -> Proxy o -> AVL (Insert' x a t o)