| 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.FullExtern
Description
Interface for the main functions over type safe AVL trees
implemented with the internalist approach. This module reexports
the functions defined over ITree trees from the modules
Data.Tree.AVL.Extern.Constructors, Data.Tree.AVL.Extern.Delete,
Data.Tree.AVL.Extern.Insert and Data.Tree.AVL.Extern.Lookup.
Synopsis
- data AVL :: Tree -> Type where
- AVL :: ITree t -> IsBSTT t -> IsBalancedT t -> AVL t
- mkAVL :: (IsBSTC t, IsBalancedC t) => ITree t -> AVL 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 AVL :: Tree -> Type where Source #
Constructor of AVL trees. Given an arbitrary ITree, it constructs
a new AVL together with the proof terms IsBSTT, which shows
that the keys are ordered, and IsBalancedT, which shows that the heights are balanced.
Constructors
| AVL :: ITree t -> IsBSTT t -> IsBalancedT t -> AVL t |
mkAVL :: (IsBSTC t, IsBalancedC t) => ITree t -> AVL t Source #
Given an ITree, compute the proof terms IsBSTT and IsBalancedT, through
the type classes IsBSTC and IsBalancedC in order to check if it is an AVL tree.
This is the fully externalist constructor for AVL 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 |
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.