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.AVL.Intern.Insert

Description

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.

Synopsis

class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
- 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
- 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
- type Insert (x :: Nat) (a :: Type) (t :: Tree) :: Tree
- insert :: Node x a -> AVL t -> AVL (Insert x a t)
class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
- type Insert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) :: Tree
- insert' :: Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o)

Documentation

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 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 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 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 Source #

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

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 Source #

Methods

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

Instances

Instances details

Show a => Insertable x a 'EmptyTree Source #
Instance details Defined in Data.Tree.AVL.Intern.Insert Associated Types type Insert x a 'EmptyTree :: Tree Source # Methods insert :: Node x a -> AVL 'EmptyTree -> AVL (Insert x a 'EmptyTree) Source #
(o ~ CmpNat x n, Insertable' x a ('ForkTree l (Node n a1) r) o) => Insertable x a ('ForkTree l (Node n a1) r) Source #
Instance details Defined in Data.Tree.AVL.Intern.Insert Associated Types type Insert x a ('ForkTree l (Node n a1) r) :: Tree Source # Methods insert :: Node x a -> AVL ('ForkTree l (Node n a1) r) -> AVL (Insert x a ('ForkTree l (Node n a1) r)) Source #

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

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 Source #

Methods

insert' :: Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o) Source #