Data.Tree.BST.FullExtern

Interface for the main functions over type safe BST trees implemented with the internalist approach. This module reexports the functions defined over ITree trees from the modules Data.Tree.BST.Extern.Constructors, Data.Tree.BST.Extern.Delete, Data.Tree.BST.Extern.Insert and Data.Tree.BST.Extern.Lookup.

Documentation

data BST :: Tree -> Type where

Constructor of BST trees. Given an arbitrary ITree, it constructs a new BST together with the proof term IsBSTT which shows that the keys are ordered.

Constructors

BST :: ITree t -> IsBSTT t -> BST t

Instances

Show (BST t)

Instance definition for the Show type class. It relies on the instance for ITree.

Defined in Data.Tree.BST.Extern.Constructors

Methods

showsPrec :: Int -> BST t -> ShowS

show :: BST t -> String

showList :: [BST t] -> ShowS

mkBST :: IsBSTC t => ITree t -> BST t

Given an ITree, compute the proof term IsBSTT, through the type class IsBSTC, in order to check if it is a BST tree. This is the fully externalist constructor for BST trees.

data ITree :: Tree -> Type where

Value level trees indexed by trees of kind `Tree. The tree structure from the value level is replicated at the type level.

Constructors

EmptyITree :: ITree 'EmptyTree

Instances

Show (ITree t)

Show instance for ITree.

Defined in Data.Tree.ITree

Methods

showsPrec :: Int -> ITree t -> ShowS

show :: ITree t -> String

showList :: [ITree t] -> ShowS

insert :: Insertable x a t => 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.

lookup :: (Lookupable x a t, t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True) => Proxy x -> ITree t -> a

Lookup the given key in the tree.

delete :: Deletable x t => Proxy x -> ITree t -> ITree (Delete x t)

Delete the node with the given key. If the key is not in the tree, return the same tree.