-
Notifications
You must be signed in to change notification settings - Fork 4
/
gaptree.mli
130 lines (85 loc) · 2.21 KB
/
gaptree.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
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
type 'a option =
| Some of 'a
| None
type comparison =
| Eq
| Lt
| Gt
type compareSpecT =
| CompEqT
| CompLtT
| CompGtT
type 'a sig0 =
'a
(* singleton inductive, whose constructor was exist *)
type 'a eqDec = 'a -> 'a -> bool
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 gap =
| G1
| G0
type gaptree =
| Leaf
| Node of gap * gaptree * a * gaptree
type findResult =
| Found
| NotFound
val find : a -> gaptree -> findResult
val gof : gaptree -> gap option
val isLeaf : gaptree -> bool
val setGap : gap -> gaptree -> gaptree
type regapR =
gaptree
(* singleton inductive, whose constructor was regapR *)
val regapAs : gaptree -> gaptree -> regapR
val gofis : gaptree -> gap -> bool
type gapnode =
gaptree
(* singleton inductive, whose constructor was Gapnode *)
type ires =
| ISameH
| Higher
type insertResult =
| FoundByInsert
| Inserted of gaptree * ires
val rotateRight : gaptree -> a -> gaptree -> gap -> gapnode
val rotateLeft : gaptree -> a -> gaptree -> gap -> gapnode
val iFitLeft : gap -> gaptree -> gaptree -> a -> gaptree -> insertResult
val iFitRight : gap -> gaptree -> a -> gaptree -> gaptree -> insertResult
val insert : a -> gaptree -> insertResult
type dres =
| DSameH
| Lower
type tryLowerResult =
| Lowered of gaptree
| LowerFailed
val tryLowering : gaptree -> tryLowerResult
val dRotateLeft : gaptree -> a -> gaptree -> gap -> gapnode
type delminResult =
| NoMin
| MinDeleted of a * ( * )
val dFitLeft : gap -> gaptree -> gaptree -> a -> gaptree -> ( * )
val delmin : gaptree -> delminResult
val dRotateRight : gaptree -> a -> gaptree -> gap -> gapnode
val dFitRight : gap -> gaptree -> a -> gaptree -> gaptree -> ( * )
type delmaxResult =
| NoMax
| MaxDeleted of a * ( * )
val delmax : gaptree -> delmaxResult
type deleteResult =
| DelNotFound
| Deleted of ( * )
type twoGaps =
| NoneNone
| G0G0
| G1G1
| NoneG0
| G1G0
| G0None
| G0G1
val gof2 : gaptree -> gaptree -> twoGaps
val delMinOrMax : gap -> gaptree -> a -> gaptree -> ( * )
val delete : a -> gaptree -> deleteResult