-
Notifications
You must be signed in to change notification settings - Fork 1
/
avl_tree.gadti.target
58 lines (40 loc) · 1.63 KB
/
avl_tree.gadti.target
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
(** We follow the AVL tree algorithm from OCaml Standard Library, where
the branches of a node are allowed to differ in height by at most 2. *)
datatype Avl : type * num
datacons Empty : ∀a. Avl (a, 0)
datacons Node : ∀k, m, n, a[0 ≤ m ∧ 0 ≤ n ∧ n ≤ m + 2 ∧
m ≤ n + 2 ∧ k=max (m, n)].Avl (a, m) * a * Avl (a, n) * Num (k + 1)
⟶ Avl (a, k + 1)
datatype LinOrder
datacons LT : LinOrder
datacons EQ : LinOrder
datacons GT : LinOrder
external val compare : ∀a. a → a → LinOrder
val height : ∀n, a. Avl (a, n) → Num n
val create :
∀k, n, a[k ≤ n + 2 ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ 0 ≤ n].
Avl (a, k) → a → Avl (a, n) → ∃i[i=max (k + 1, n + 1)].Avl (a, i)
val singleton : ∀a. a → Avl (a, 1)
val rotr :
∀k, n, a[k ≤ n + 3 ∧ n + 2 ≤ k ∧ 0 ≤ n].
Avl (a, k) → a → Avl (a, n) → ∃n[k ≤ n ∧
n ≤ k + 1].Avl (a, n)
val rotl :
∀k, n, a[k + 2 ≤ n ∧ 0 ≤ k ∧ n ≤ k + 3].
Avl (a, k) → a → Avl (a, n) → ∃k[k ≤ n + 1 ∧
n ≤ k].Avl (a, k)
val add :
∀n, a.
a → Avl (a, n) → ∃k[1 ≤ k ∧ n ≤ k ∧ k ≤ n + 1].Avl (a, k)
val mem : ∀n, a. a → Avl (a, n) → Bool
val min_binding : ∀n, a[1 ≤ n]. Avl (a, n) → a
val remove_min_binding :
∀n, a[1 ≤ n].
Avl (a, n) → ∃k[k + 2 ≤ 2 n ∧ k ≤ n ∧ n ≤ k + 1].Avl (a, k)
val merge :
∀k, n, a[k ≤ n + 2 ∧ n ≤ k + 2].
(Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ k ≤ i ∧ i ≤ n + k ∧
i≤max (k + 1, n + 1)].Avl (a, i)
val remove :
∀n, a.
a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ k ≤ n ∧ 0 ≤ k].Avl (a, k)