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

Description

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.

Synopsis

data BST :: Tree -> Type where
- BST :: ITree t -> IsBSTT t -> BST t
mkBST :: IsBSTC t => ITree t -> BST t
data ITree :: Tree -> Type where
- EmptyITree :: ITree 'EmptyTree
insert :: Insertable x a t => Node x a -> ITree t -> ITree (Insert x a t)
lookup :: (Lookupable x a t, t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True) => Proxy x -> ITree t -> a
delete :: Deletable x t => Proxy x -> ITree t -> ITree (Delete x t)

Documentation

data BST :: Tree -> Type where Source #

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

Instances details

Show (BST t) Source #	Instance definition for the `Show` type class. It relies on the instance for `ITree`.
Instance details 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 Source #

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

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

Instances details

Show (ITree t) Source #	`Show` instance for `ITree`.
Instance details 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) Source #

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

Lookup the given key in the tree.

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

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