1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- Some examples showing how the AVL tree module can be used
5
------------------------------------------------------------------------
7
module README.AVL where
9
------------------------------------------------------------------------
12
-- AVL trees are defined in Data.AVL.
16
-- This module is parametrised by keys, which have to form a (strict)
17
-- total order, and values, which are indexed by keys. Let us use
18
-- natural numbers as keys and vectors of strings as values.
20
import Data.Nat.Properties as ℕ
21
open import Data.String using (String)
22
open import Data.Vec using (Vec; _∷_; [])
23
open import Relation.Binary using (module StrictTotalOrder)
25
open Data.AVL (Vec String)
26
(StrictTotalOrder.isStrictTotalOrder ℕ.strictTotalOrder)
28
------------------------------------------------------------------------
29
-- Construction of trees
34
v₂ = "apa" ∷ "bepa" ∷ []
36
-- Empty and singleton trees.
44
-- Insertion of a key-value pair into a tree.
48
-- Deletion of the mapping for a certain key.
52
-- Conversion of a list of key-value mappings to a tree.
54
open import Data.List using (_∷_; [])
55
open import Data.Product as Prod using (_,_; _,′_)
57
t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])
59
------------------------------------------------------------------------
62
-- Let us formulate queries as unit tests.
64
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
66
-- Searching for a key.
68
open import Data.Bool using (true; false)
69
open import Data.Maybe as Maybe using (just; nothing)
71
q₀ : lookup 2 t₂ ≡ just v₂
74
q₁ : lookup 2 t₃ ≡ nothing
83
-- Turning a tree into a sorted list of key-value pairs.
85
q₄ : toList t₁ ≡ (2 , v₂) ∷ []
88
q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
91
------------------------------------------------------------------------
94
-- Partitioning a tree into the smallest element plus the rest, or the
95
-- largest element plus the rest.
97
open import Category.Functor using (module RawFunctor)
98
open import Function using (id)
101
open RawFunctor (Maybe.functor {f = Level.zero}) using (_<$>_)
103
v₆ : headTail t₀ ≡ nothing
106
v₇ : Prod.map id toList <$> headTail t₂ ≡
107
just ((1 , v₁) , ((2 , v₂) ∷ []))
110
v₈ : initLast t₀ ≡ nothing
113
v₉ : Prod.map toList id <$> initLast t₄ ≡
114
just (((1 , v₁) ∷ []) ,′ (2 , v₂))
117
------------------------------------------------------------------------
120
-- Variations of the AVL tree module are available:
122
-- • Finite maps with indexed keys and values.
124
import Data.AVL.IndexedMap
added
removed
README/AVL.agda
