diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 15 |
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 |
