1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the AVL tree module can be used
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module README.Data.Tree.AVL where
------------------------------------------------------------------------
-- Setup
-- AVL trees are defined in Data.Tree.AVL.
import Data.Tree.AVL
-- This module is parametrised by keys, which have to form a (strict)
-- total order, and values, which are indexed by keys. Let us use
-- natural numbers as keys and vectors of strings as values.
open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product.Base as Product using (_,_; _,′_)
open import Data.String.Base using (String)
open import Data.Vec.Base using (Vec; _∷_; [])
open import Relation.Binary.PropositionalEquality
open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)
Tree = Tree′ (MkValue (Vec String) (subst (Vec String)))
------------------------------------------------------------------------
-- Construction of trees
-- Some values.
v₁ = "cepa" ∷ []
v₁′ = "depa" ∷ []
v₂ = "apa" ∷ "bepa" ∷ []
-- Empty and singleton trees.
t₀ : Tree
t₀ = empty
t₁ : Tree
t₁ = singleton 2 v₂
-- Insertion of a key-value pair into a tree.
t₂ = insert 1 v₁ t₁
-- If you insert a key-value pair and the key already exists in the
-- tree, then the old value is thrown away.
t₂′ = insert 1 v₁′ t₂
-- Deletion of the mapping for a certain key.
t₃ = delete 2 t₂
-- Conversion of a list of key-value mappings to a tree.
open import Data.List.Base using (_∷_; [])
t₄ : Tree
t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])
------------------------------------------------------------------------
-- Queries
-- Let us formulate queries as unit tests.
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-- Searching for a key.
open import Data.Bool.Base using (true; false)
open import Data.Maybe.Base as Maybe using (just; nothing)
q₀ : lookup t₂ 2 ≡ just v₂
q₀ = refl
q₁ : lookup t₃ 2 ≡ nothing
q₁ = refl
q₂ : (3 ∈? t₂) ≡ false
q₂ = refl
q₃ : (1 ∈? t₄) ≡ true
q₃ = refl
-- Turning a tree into a sorted list of key-value pairs.
q₄ : toList t₁ ≡ (2 , v₂) ∷ []
q₄ = refl
q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
q₅ = refl
q₅′ : toList t₂′ ≡ (1 , v₁′) ∷ (2 , v₂) ∷ []
q₅′ = refl
------------------------------------------------------------------------
-- Views
-- Partitioning a tree into the smallest element plus the rest, or the
-- largest element plus the rest.
open import Function.Base using (id)
v₆ : headTail t₀ ≡ nothing
v₆ = refl
v₇ : Maybe.map (Product.map₂ toList) (headTail t₂) ≡
just ((1 , v₁) , ((2 , v₂) ∷ []))
v₇ = refl
v₈ : initLast t₀ ≡ nothing
v₈ = refl
v₉ : Maybe.map (Product.map₁ toList) (initLast t₄) ≡
just (((1 , v₁) ∷ []) ,′ (2 , v₂))
v₉ = refl
------------------------------------------------------------------------
-- Further reading
-- Variations of the AVL tree module are available:
-- • Finite maps with indexed keys and values.
import Data.Tree.AVL.IndexedMap
-- • Finite sets.
import Data.Tree.AVL.Sets
|
