-
Notifications
You must be signed in to change notification settings - Fork 4
/
redblack.mli
101 lines (63 loc) · 1.7 KB
/
redblack.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
90
91
92
93
94
95
96
97
98
99
100
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 color =
| Red
| Black
type rbtree =
| Leaf
| Node of color * rbtree * a * rbtree
type findResult =
| Found
| NotFound
val find : a -> rbtree -> findResult
val cof : rbtree -> color
val midRedCombine : rbtree -> a -> rbtree -> a -> rbtree -> rbtree
val red2black : rbtree -> rbtree
type iChanged =
| ISameIndx
| IReddened
| IBlackInc
val rebalRight : rbtree -> a -> rbtree -> ( * )
val rebalLeft : rbtree -> a -> rbtree -> ( * )
val color2change : color -> iChanged
type insertResult =
| FoundByInsert
| Inserted of iChanged * rbtree
val insert : a -> rbtree -> insertResult
type dChanged =
| StillFits
| Rebalance
val dRotateLeft : rbtree -> a -> rbtree -> rbtree
val dRotateRight : rbtree -> a -> rbtree -> rbtree
val color2dchange : color -> dChanged
val colorAs : color -> rbtree -> rbtree
val dRebalRight : color -> rbtree -> a -> rbtree -> ( * )
val dRebalLeft : color -> rbtree -> a -> rbtree -> ( * )
val dFitLeft : color -> ( * ) -> a -> rbtree -> ( * )
val dFitRight : color -> rbtree -> a -> ( * ) -> ( * )
val colorFit : color -> rbtree -> ( * )
type delminResult =
| NoMin
| MinDeleted of a * ( * )
val delmin : rbtree -> delminResult
type deleteResult =
| DelNotFound
| Deleted of ( * )
val delete : a -> rbtree -> deleteResult