Data.Tree.AVL.Extern.Insert

Implementation of the insertion algorithm over ITree trees for externalist AVL trees.

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 tree t without checking any structural invariant (key ordering or height balance). The insertion is defined at the value level and the type level, and is performed as if the tree is an AVL; the verification of the AVL restrictions is performed after the insertion.

Associated Types

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

Methods

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

Insert a new node. If the key is already present in the tree, update the value.

Instances

Show a => Insertable x a 'EmptyTree

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

type Insert x a 'EmptyTree :: Tree

Methods

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

Associated Types

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

Methods

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

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

This type class provides the functionality to insert a node with key x and value type a in a non empty tree t without checking any structural invariant (key ordering or height balance). 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.

Minimal complete definition

insert'

Associated Types

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

Instances

(r ~ 'ForkTree rl (Node rn rna) rr, o ~ CmpNat x rn, Insertable' x a r o, Balanceable ('ForkTree l (Node n a1) (Insert' x a r o))) => Insertable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

type Insert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT :: Tree

Methods

insert' :: Node x a -> ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) -> Proxy 'GT -> ITree (Insert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)

(Show a, Balanceable ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))) => Insertable' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

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

Methods

insert' :: Node x a -> ITree ('ForkTree l (Node n a1) 'EmptyTree) -> Proxy 'GT -> ITree (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)

(l ~ 'ForkTree ll (Node ln lna) lr, o ~ CmpNat x ln, Insertable' x a l o, Balanceable ('ForkTree (Insert' x a l o) (Node n a1) r)) => Insertable' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

type Insert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT :: Tree

Methods

insert' :: Node x a -> ITree ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) -> Proxy 'LT -> ITree (Insert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)

(Show a, Balanceable ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)) => Insertable' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

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

Methods

insert' :: Node x a -> ITree ('ForkTree 'EmptyTree (Node n a1) r) -> Proxy 'LT -> ITree (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)

Show a => Insertable' x a ('ForkTree l (Node n a1) r) 'EQ

Defined in Data.Tree.AVL.Extern.Insert

Associated Types

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

Methods

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