aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 2ac913607a..46969ec831 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1145,7 +1145,21 @@ let array_fold_map2' f v1 v2 e =
in
(v',!e')
+(* N.logN *)
let array_distinct v =
+ let visited = Hashtbl.create 23 in
+ try
+ Array.iter
+ (fun x ->
+ if Hashtbl.mem visited h then raise Exit
+ else Hashtbl.add visited h h)
+ v;
+ true
+ with Exit -> false
+
+
+(* quadratic *)
+(*let array_distinct v =
try
for i=0 to Array.length v-1 do
for j=i+1 to Array.length v-1 do
@@ -1155,6 +1169,7 @@ let array_distinct v =
true
with Exit ->
false
+*)
let array_union_map f a acc =
Array.fold_left