-
Notifications
You must be signed in to change notification settings - Fork 4
/
avl.mli
90 lines (57 loc) · 1.64 KB
/
avl.mli
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
type comparison =
| Eq
| Lt
| Gt
type compareSpecT =
| CompEqT
| CompLtT
| CompGtT
type 'a sig0 =
'a
(* singleton inductive, whose constructor was exist *)
type sumbool =
| Left
| Right
type 'a eqDec = 'a -> 'a -> sumbool
type 'a ordered = { eq_dec : 'a eqDec; compare : ('a -> 'a -> comparison); compare_spec : ('a -> 'a -> compareSpecT) }
val compare_spec : 'a1 ordered -> 'a1 -> 'a1 -> compareSpecT
type a (* AXIOM TO BE REALIZED *)
val ordA : a ordered
type balanceFactor =
| HiLeft
| Flat
| HiRight
| NoSubs
type avltree =
| Leaf
| Node of balanceFactor * avltree * a * avltree
type findResult =
| Found
| NotFound
val find : a -> avltree -> findResult
val bof : avltree -> balanceFactor
val rotateRight : avltree -> a -> avltree -> avltree
val rotateLeft : avltree -> a -> avltree -> avltree
val raised : avltree -> avltree -> bool
type insertResult =
| FoundByInsert
| Inserted of avltree
val ifitl : balanceFactor -> avltree -> a -> avltree -> insertResult
val ifitr : balanceFactor -> avltree -> a -> avltree -> insertResult
val insert : a -> avltree -> insertResult
type delout =
avltree
(* singleton inductive, whose constructor was Delout *)
val lowered : avltree -> avltree -> bool
val dRotateRight : avltree -> a -> avltree -> delout
val dRotateLeft : avltree -> a -> avltree -> delout
val dFitLeft : balanceFactor -> delout -> avltree -> a -> avltree -> delout
val dFitRight : balanceFactor -> delout -> avltree -> a -> avltree -> delout
type delminResult =
| NoMin
| MinDeleted of a * delout
val delmin : avltree -> delminResult
type deleteResult =
| DelNotFound
| Deleted of delout
val delete : a -> avltree -> deleteResult