1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
5
-- AVL trees are balanced binary search trees. The search tree
6
-- invariant is not statically enforced in the current implementation,
7
-- just the balance invariant.
10
open import Relation.Binary
12
module Data.AVL (OrderedKeySet : StrictTotalOrder zero zero zero)
13
(Value : StrictTotalOrder.Carrier OrderedKeySet → Set)
16
open import Data.Nat hiding (compare)
17
open StrictTotalOrder OrderedKeySet renaming (Carrier to Key)
18
open import Data.Product
19
open import Data.Maybe
21
open import Data.List as List using (List)
22
import Data.DifferenceList as DiffList
23
open import Relation.Binary.PropositionalEquality
25
------------------------------------------------------------------------
26
-- Types and functions which are used to keep track of invariants
28
module Invariants where
30
-- Bits. (I would use Fin 2 instead if Agda had "defined patterns",
31
-- so that I could pattern match on 1# instead of suc zero; the text
32
-- "suc zero" takes up a lot more space.)
46
-- i ⊕ n -1 = pred (i ⊕ n).
54
-- If m ∼ n, then the difference between m and n is at most 1. _∼_
55
-- is used to record the balance factor of the AVL trees, and also
56
-- to ensure that the absolute value of the balance factor is never
59
data _∼_ : ℕ → ℕ → Set where
60
∼+ : ∀ {n} → n ∼ 1 + n
62
∼- : ∀ {n} → 1 + n ∼ n
64
-- The maximum of m and n.
66
max : ∀ {m n} → m ∼ n → ℕ
73
1+ : ∀ {m n} → m ∼ n → 1 + m ∼ 1 + n
78
max∼ : ∀ {i j} (bal : i ∼ j) → max bal ∼ i
83
∼max : ∀ {i j} (bal : i ∼ j) → j ∼ max bal
88
max∼max : ∀ {i j} (bal : i ∼ j) → max (max∼ bal) ∼ max (∼max bal)
93
max-lemma : ∀ {m n} (bal : m ∼ n) →
94
1 + max (1+ (max∼max bal)) ≡ 2 + max bal
99
------------------------------------------------------------------------
111
-- The trees are indexed on their height. (bal is the balance
114
data Tree : ℕ → Set where
117
(l : Tree hˡ) (k : KV) (r : Tree hʳ) (bal : hˡ ∼ hʳ) →
120
-- Various constant-time functions which construct trees out of
121
-- smaller pieces, sometimes using rotation.
124
(∃ λ i → Tree (i ⊕ hˡ)) → KV → Tree hʳ → (bal : hˡ ∼ hʳ) →
125
∃ λ i → Tree (i ⊕ (1 + max bal))
126
joinˡ⁺ (1# , node t₁ k₂
128
∼+) k₆ t₇ ∼- = (0# , subst Tree (max-lemma bal)
129
(node (node t₁ k₂ t₃ (max∼ bal))
131
(node t₅ k₆ t₇ (∼max bal))
133
joinˡ⁺ (1# , node t₁ k₂ t₃ ∼-) k₄ t₅ ∼- = (0# , node t₁ k₂ (node t₃ k₄ t₅ ∼0) ∼0)
134
joinˡ⁺ (1# , node t₁ k₂ t₃ ∼0) k₄ t₅ ∼- = (1# , node t₁ k₂ (node t₃ k₄ t₅ ∼-) ∼+)
135
joinˡ⁺ (1# , t₁) k₂ t₃ ∼0 = (1# , node t₁ k₂ t₃ ∼-)
136
joinˡ⁺ (1# , t₁) k₂ t₃ ∼+ = (0# , node t₁ k₂ t₃ ∼0)
137
joinˡ⁺ (0# , t₁) k₂ t₃ bal = (0# , node t₁ k₂ t₃ bal)
140
Tree hˡ → KV → (∃ λ i → Tree (i ⊕ hʳ)) → (bal : hˡ ∼ hʳ) →
141
∃ λ i → Tree (i ⊕ (1 + max bal))
142
joinʳ⁺ t₁ k₂ (1# , node
144
k₆ t₇ ∼-) ∼+ = (0# , subst Tree (max-lemma bal)
145
(node (node t₁ k₂ t₃ (max∼ bal))
147
(node t₅ k₆ t₇ (∼max bal))
149
joinʳ⁺ t₁ k₂ (1# , node t₃ k₄ t₅ ∼+) ∼+ = (0# , node (node t₁ k₂ t₃ ∼0) k₄ t₅ ∼0)
150
joinʳ⁺ t₁ k₂ (1# , node t₃ k₄ t₅ ∼0) ∼+ = (1# , node (node t₁ k₂ t₃ ∼+) k₄ t₅ ∼-)
151
joinʳ⁺ t₁ k₂ (1# , t₃) ∼0 = (1# , node t₁ k₂ t₃ ∼+)
152
joinʳ⁺ t₁ k₂ (1# , t₃) ∼- = (0# , node t₁ k₂ t₃ ∼0)
153
joinʳ⁺ t₁ k₂ (0# , t₃) bal = (0# , node t₁ k₂ t₃ bal)
156
(∃ λ i → Tree (i ⊕ hˡ -1)) → KV → Tree hʳ → (bal : hˡ ∼ hʳ) →
157
∃ λ i → Tree (i ⊕ max bal)
158
joinˡ⁻ zero (0# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)
159
joinˡ⁻ zero (1# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)
160
joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼+ = joinʳ⁺ t₁ k₂ (1# , t₃) ∼+
161
joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼0 = (1# , node t₁ k₂ t₃ ∼+)
162
joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼- = (0# , node t₁ k₂ t₃ ∼0)
163
joinˡ⁻ (suc _) (1# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)
166
Tree hˡ → KV → (∃ λ i → Tree (i ⊕ hʳ -1)) → (bal : hˡ ∼ hʳ) →
167
∃ λ i → Tree (i ⊕ max bal)
168
joinʳ⁻ zero t₁ k₂ (0# , t₃) bal = (1# , node t₁ k₂ t₃ bal)
169
joinʳ⁻ zero t₁ k₂ (1# , t₃) bal = (1# , node t₁ k₂ t₃ bal)
170
joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼- = joinˡ⁺ (1# , t₁) k₂ t₃ ∼-
171
joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼0 = (1# , node t₁ k₂ t₃ ∼-)
172
joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼+ = (0# , node t₁ k₂ t₃ ∼0)
173
joinʳ⁻ (suc _) t₁ k₂ (1# , t₃) bal = (1# , node t₁ k₂ t₃ bal)
175
-- Extracts the smallest element from the tree, plus the rest.
176
-- Logarithmic in the size of the tree.
178
headTail : ∀ {h} → Tree (1 + h) →
179
KV × ∃ λ i → Tree (i ⊕ h)
180
headTail (node leaf k₁ t₂ ∼+) = (k₁ , 0# , t₂)
181
headTail (node leaf k₁ t₂ ∼0) = (k₁ , 0# , t₂)
182
headTail (node {hˡ = suc _} t₁₂ k₃ t₄ bal) with headTail t₁₂
183
... | (k₁ , t₂) = (k₁ , joinˡ⁻ _ t₂ k₃ t₄ bal)
185
-- Extracts the largest element from the tree, plus the rest.
186
-- Logarithmic in the size of the tree.
188
initLast : ∀ {h} → Tree (1 + h) →
189
∃ (λ i → Tree (i ⊕ h)) × KV
190
initLast (node t₁ k₂ leaf ∼-) = ((0# , t₁) , k₂)
191
initLast (node t₁ k₂ leaf ∼0) = ((0# , t₁) , k₂)
192
initLast (node {hʳ = suc _} t₁ k₂ t₃₄ bal) with initLast t₃₄
193
... | (t₃ , k₄) = (joinʳ⁻ _ t₁ k₂ t₃ bal , k₄)
195
-- Another joining function. Logarithmic in the size of the tree.
198
Tree hˡ → Tree hʳ → (bal : hˡ ∼ hʳ) →
199
∃ λ i → Tree (i ⊕ max bal)
200
join t₁ leaf ∼0 = (0# , t₁)
201
join t₁ leaf ∼- = (0# , t₁)
202
join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
203
... | (k₂ , t₃) = joinʳ⁻ _ t₁ k₂ t₃ bal
212
singleton : (k : Key) → Value k → Tree 1
213
singleton k v = node leaf (k , v) leaf ∼0
215
-- Inserts a key into the tree. If the key already exists, then it
216
-- is replaced. Logarithmic in the size of the tree (assuming
217
-- constant-time comparisons).
219
insert : ∀ {h} → (k : Key) → Value k → Tree h →
221
insert k v leaf = (1# , singleton k v)
222
insert k v (node l p r bal) with compare k (proj₁ p)
223
... | tri< _ _ _ = joinˡ⁺ (insert k v l) p r bal
224
... | tri≈ _ _ _ = (0# , node l (k , v) r bal)
225
... | tri> _ _ _ = joinʳ⁺ l p (insert k v r) bal
227
-- Deletes the key/value pair containing the given key, if any.
228
-- Logarithmic in the size of the tree (assuming constant-time
231
delete : ∀ {h} → Key → Tree h →
232
∃ λ i → Tree (i ⊕ h -1)
233
delete k leaf = (0# , leaf)
234
delete k (node l p r bal) with compare k (proj₁ p)
235
... | tri< _ _ _ = joinˡ⁻ _ (delete k l) p r bal
236
... | tri≈ _ _ _ = join l r bal
237
... | tri> _ _ _ = joinʳ⁻ _ l p (delete k r) bal
239
-- Looks up a key in the tree. Logarithmic in the size of the tree
240
-- (assuming constant-time comparisons).
242
lookup : ∀ {h} → (k : Key) → Tree h →
243
Maybe (∃ λ k′ → Value k′ × k ≈ k′)
244
lookup k leaf = nothing
245
lookup k (node l (k′ , v) r _) with compare k k′
246
... | tri< _ _ _ = lookup k l
247
... | tri≈ _ eq _ = just (k′ , v , eq)
248
... | tri> _ _ _ = lookup k r
250
-- Converts the tree to an ordered list. Linear in the size of the
255
toDiffList : ∀ {h} → Tree h → DiffList KV
257
toDiffList (node l k r _) = toDiffList l ++ [ k ] ++ toDiffList r
259
------------------------------------------------------------------------
260
-- Types and functions with hidden indices
262
data Tree : Set where
263
tree : ∀ {h} → Indexed.Tree h → Tree
266
empty = tree Indexed.empty
268
singleton : (k : Key) → Value k → Tree
269
singleton k v = tree (Indexed.singleton k v)
271
insert : (k : Key) → Value k → Tree → Tree
272
insert k v (tree t) with Indexed.insert k v t
273
... | (_ , t′) = tree t′
275
delete : Key → Tree → Tree
276
delete k (tree t) with Indexed.delete k t
277
... | (_ , t′) = tree t′
279
lookup : (k : Key) → Tree → Maybe (∃ λ k′ → Value k′ × k ≈ k′)
280
lookup k (tree t) = Indexed.lookup k t
282
_∈?_ : Key → Tree → Bool
283
k ∈? t = maybeToBool (lookup k t)
285
headTail : Tree → Maybe (KV × Tree)
286
headTail (tree Indexed.leaf) = nothing
287
headTail (tree {h = suc _} t) with Indexed.headTail t
288
... | (k , _ , t′) = just (k , tree t′)
290
initLast : Tree → Maybe (Tree × KV)
291
initLast (tree Indexed.leaf) = nothing
292
initLast (tree {h = suc _} t) with Indexed.initLast t
293
... | ((_ , t′) , k) = just (tree t′ , k)
295
-- The input does not need to be ordered.
297
fromList : List KV → Tree
298
fromList = List.foldr (uncurry insert) empty
300
-- Returns an ordered list.
302
toList : Tree → List KV
303
toList (tree t) = DiffList.toList (Indexed.toDiffList t)
added
removed
src/Data/AVL.agda
