aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--lib/util.ml21
-rw-r--r--lib/util.mli2
2 files changed, 23 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 48de0387e..1014a6545 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -490,6 +490,16 @@ let lowercase_first_char_utf8 s =
(* Lists *)
+let rec list_compare cmp l1 l2 =
+ match l1,l2 with
+ [], [] -> 0
+ | _::_, [] -> 1
+ | [], _::_ -> -1
+ | x1::l1, x2::l2 ->
+ (match cmp x1 x2 with
+ | 0 -> list_compare cmp l1 l2
+ | c -> c)
+
let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1
@@ -934,6 +944,17 @@ let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl
(* Arrays *)
+let array_compare item_cmp v1 v2 =
+ let c = compare (Array.length v1) (Array.length v2) in
+ if c<>0 then c else
+ let rec cmp = function
+ -1 -> 0
+ | i ->
+ let c' = item_cmp v1.(i) v2.(i) in
+ if c'<>0 then c'
+ else cmp (i-1) in
+ cmp (Array.length v1 - 1)
+
let array_exists f v =
let rec exrec = function
| -1 -> false
diff --git a/lib/util.mli b/lib/util.mli
index 23fdd7670..0acff599d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -99,6 +99,7 @@ val lowercase_first_char_utf8 : string -> string
(*s Lists. *)
+val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
val list_add_set : 'a -> 'a list -> 'a list
val list_eq_set : 'a list -> 'a list -> bool
val list_intersect : 'a list -> 'a list -> 'a list
@@ -196,6 +197,7 @@ val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
(*s Arrays. *)
+val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
val array_exists : ('a -> bool) -> 'a array -> bool
val array_for_all : ('a -> bool) -> 'a array -> bool
val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool