comparison functions on lists and arrays

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12091 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 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