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

Description

Interface for the main functions over type safe AVL trees implemented with the externalist approach.

Synopsis

emptyAVL :: AVL 'EmptyTree
insertAVL :: (Insertable x a t, ProofIsBSTInsert x a t, ProofIsBalancedInsert x a t) => Proxy x -> a -> AVL t -> AVL (Insert x a t)
lookupAVL :: (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True, Lookupable x a t) => Proxy x -> AVL t -> a
deleteAVL :: (Deletable x t, ProofIsBSTDelete x t, ProofIsBalancedDelete x t) => Proxy x -> AVL t -> AVL (Delete x t)

Documentation

emptyAVL :: AVL 'EmptyTree Source #

Empty AVL tree with the externalist implementation.

insertAVL :: (Insertable x a t, ProofIsBSTInsert x a t, ProofIsBalancedInsert x a t) => Proxy x -> a -> AVL t -> AVL (Insert x a t) Source #

Interface for the insertion algorithm in the externalist implementation. It calls insert over ITree, and proofIsBSTInsert and proofIsBalancedInsert for constructing the evidence that the new tree remains AVL.

lookupAVL :: (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True, Lookupable x a t) => Proxy x -> AVL t -> a Source #

Interface for the lookup algorithm in the externalist implementation of AVL.

deleteAVL :: (Deletable x t, ProofIsBSTDelete x t, ProofIsBalancedDelete x t) => Proxy x -> AVL t -> AVL (Delete x t) Source #

Interface for the deletion algorithm in the externalist implementation. It calls delete over ITree, and proofIsBSTDelete and proofIsBalancedDelete for constructing the evidence that the new tree remains AVL.