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

Description

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

Synopsis

emptyBST :: BST 'EmptyTree
insertBST :: (Insertable x a t, ProofIsBSTInsert x a t) => Proxy x -> a -> BST t -> BST (Insert x a t)
lookupBST :: (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True, Lookupable x a t) => Proxy x -> BST t -> a
deleteBST :: (Deletable x t, ProofIsBSTDelete x t) => Proxy x -> BST t -> BST (Delete x t)

Documentation

emptyBST :: BST 'EmptyTree Source #

Empty BST tree with the externalist implementation.

insertBST :: (Insertable x a t, ProofIsBSTInsert x a t) => Proxy x -> a -> BST t -> BST (Insert x a t) Source #

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

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

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

deleteBST :: (Deletable x t, ProofIsBSTDelete x t) => Proxy x -> BST t -> BST (Delete x t) Source #

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