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