33
33
* modify it under the terms of the GNU Lesser General Public
34
34
* License as published by the Free Software Foundation,
35
35
* version 2.1 of the License.
36
- *
36
+ *
37
37
* This library is distributed in the hope that it will be useful,
38
38
* but WITHOUT ANY WARRANTY; without even the implied warranty of
39
39
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
40
40
* Lesser General Public License for more details.
41
- *
41
+ *
42
42
* You should have received a copy of the GNU Lesser General Public
43
43
* License along with this library; if not, write to the Free Software
44
44
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
45
- *
45
+ *
46
46
* Additional permission is given to link this library with the
47
47
* OpenSSL project's "OpenSSL" library, and with the OCaml runtime,
48
48
* and you may distribute the linked executables. See the file
@@ -1022,6 +1022,47 @@ struct
1022
1022
let max_depth = pred (log2 1 (succ length)) in
1023
1023
of_sorted_array 0 max_depth elements 0 length
1024
1024
1025
+ (*
1026
+ * Following treeify function are taken from Appel's Efficient Verified Red-Black Trees
1027
+ *)
1028
+ let rec treeify_f n l =
1029
+ if n = 1 then
1030
+ match l with
1031
+ x :: l -> Red (x, Leaf , Leaf , 1 ), l
1032
+ | _ -> raise (invalid_arg " treeify" )
1033
+ else
1034
+ let h = n lsr 1 in
1035
+ let f = if n mod 2 = 0 then
1036
+ treeify_g
1037
+ else
1038
+ treeify_f
1039
+ in
1040
+ match treeify_f h l with
1041
+ (left , x :: l ) -> let right, l' = f h l
1042
+ in new_black x left right, l'
1043
+ | _ -> raise (invalid_arg " treeify" )
1044
+
1045
+ and treeify_g n l =
1046
+ if n = 1 then
1047
+ Leaf , l
1048
+ else
1049
+ let h = n lsr 1 in
1050
+ let f = if n mod 2 = 0 then
1051
+ treeify_g
1052
+ else
1053
+ treeify_f
1054
+ in
1055
+ match f h l with
1056
+ (left , x :: l ) -> let right, l' = treeify_g h l
1057
+ in new_black x left right, l'
1058
+ | _ -> raise (invalid_arg " treeify" )
1059
+
1060
+ (*
1061
+ * Build a tree directly from ordered list,
1062
+ * take length + 1 of the list.
1063
+ *)
1064
+ let treeify n l = (fst (treeify_g n l))
1065
+
1025
1066
(*
1026
1067
* Convert to a list.
1027
1068
*)
@@ -1046,6 +1087,7 @@ struct
1046
1087
| Leaf ->
1047
1088
s1
1048
1089
1090
+ (* TODO: LDB: implement linear union *)
1049
1091
let union s1 s2 =
1050
1092
let size1 = cardinality s1 in
1051
1093
let size2 = cardinality s2 in
@@ -1154,6 +1196,19 @@ struct
1154
1196
| Leaf ->
1155
1197
arg
1156
1198
1199
+ (*
1200
+ * Fold in reverse direction, useful for define
1201
+ * other operations.
1202
+ *)
1203
+ let rec fold_r f arg = function
1204
+ Black (key , left , right , _ )
1205
+ | Red (key , left , right , _ ) ->
1206
+ let arg = fold_r f arg right in
1207
+ let arg = f arg key in
1208
+ fold_r f arg left
1209
+ | Leaf ->
1210
+ arg
1211
+
1157
1212
(*
1158
1213
* Equality of sets.
1159
1214
*)
@@ -1166,15 +1221,17 @@ struct
1166
1221
false
1167
1222
1168
1223
(*
1169
- * BUG: these functions are too slow!
1170
- * Could be much more optimized.
1224
+ * Optimization by construct the tree directly.
1171
1225
*)
1226
+ let add_item i (n , l ) = (succ n, i :: l)
1227
+
1172
1228
let filter pred s =
1173
- fold (fun s' x ->
1174
- if pred x then
1175
- add s' x
1176
- else
1177
- s') empty s
1229
+ let n, l = fold_r (fun s x ->
1230
+ if pred x then
1231
+ add_item x s
1232
+ else
1233
+ s) (1 , [] ) s
1234
+ in treeify n l
1178
1235
1179
1236
let inter s1 s2 =
1180
1237
let size1 = cardinality s1 in
@@ -1183,20 +1240,23 @@ struct
1183
1240
if size1 < size2 then
1184
1241
s1, s2
1185
1242
else
1186
- s2, s1
1187
- in
1188
- fold ( fun s3 x ->
1189
- if mem s2 x then
1190
- add s3 x
1191
- else
1192
- s3) empty s1
1243
+ s2, s1 in
1244
+ let n, l = fold_r ( fun s3 x ->
1245
+ if mem s2 x then
1246
+ add_item x s3
1247
+ else
1248
+ s3) ( 1 , [] ) s1
1249
+ in treeify n l
1193
1250
1194
1251
let partition pred s =
1195
- fold (fun (s1 , s2 ) x ->
1196
- if pred x then
1197
- add s1 x, s2
1198
- else
1199
- s1, add s2 x) (empty, empty) s
1252
+ let (n1, l1), l2 =
1253
+ fold_r (fun (s1 , s2 ) x ->
1254
+ if pred x then
1255
+ add_item x s1, s2
1256
+ else
1257
+ s1, x :: s2) ((1 , [] ), [] ) s in
1258
+ let n2 = cardinality s - n1 + 2
1259
+ in treeify n1 l1, treeify n2 l2
1200
1260
1201
1261
let rec diff s = function
1202
1262
Black (key , left , right , _ )
@@ -1219,9 +1279,9 @@ struct
1219
1279
1220
1280
let compare s1 s2 =
1221
1281
let rec compare s1 s2 =
1222
- match s1, s2 with
1223
- x1 :: s1 , x2 :: s2 ->
1224
- let cmp = Ord. compare x1 x2 in
1282
+ match s1, s2 with
1283
+ x1 :: s1 , x2 :: s2 ->
1284
+ let cmp = Ord. compare x1 x2 in
1225
1285
if cmp = 0 then
1226
1286
compare s1 s2
1227
1287
else
@@ -1357,28 +1417,6 @@ struct
1357
1417
let print = pp_print
1358
1418
end
1359
1419
1360
- module Make (Ord : OrderedType ) : S with type elt = Ord. t =
1361
- struct
1362
- module XSet = LmMake (Ord )
1363
-
1364
- include XSet
1365
-
1366
- let mem x s =
1367
- XSet. mem s x
1368
-
1369
- let add x s =
1370
- XSet. add s x
1371
-
1372
- let remove x s =
1373
- XSet. remove s x
1374
-
1375
- let fold f s x =
1376
- XSet. fold (fun x y -> f y x) x s
1377
-
1378
- let partition f s =
1379
- fst (XSet. partition f s)
1380
- end
1381
-
1382
1420
(*
1383
1421
* -*-
1384
1422
* Local Variables:
0 commit comments