More cleaning in CArray...

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

4 files changed, 48 insertions, 54 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index 7f25bb10c7..bdc084f44b 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -50,7 +50,7 @@ sig
   val for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
     'a array -> 'b array -> 'c array -> 'd array -> bool
   val for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
-  val find_i : (int -> 'a -> bool) -> 'a array -> int option
+  val findi : (int -> 'a -> bool) -> 'a array -> int option
   val hd : 'a array -> 'a
   val tl : 'a array -> 'a array
   val last : 'a array -> 'a
@@ -68,9 +68,6 @@ sig
   val fold_left2_i :
     (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
-  val fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
-  val app_tl : 'a array -> 'a list -> 'a list
-  val list_of_tl : 'a array -> 'a list
   val map_to_list : ('a -> 'b) -> 'a array -> 'b list
   val chop : int -> 'a array -> 'a array * 'a array
   val smartmap : ('a -> 'a) -> 'a array -> 'a array
@@ -79,17 +76,13 @@ sig
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
   val map_left : ('a -> 'b) -> 'a array -> 'b array
-  val map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
-    'b array * 'd array
   val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
   val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   val fold_map2' :
     ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
   val distinct : 'a array -> bool
-  val union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
   val rev_to_list : 'a array -> 'a list
-  val filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
   val filter_with : bool list -> 'a array -> 'a array
 end
 
@@ -161,7 +154,7 @@ let for_all_i f i v =
 
 exception Found of int
 
-let find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option =
+let findi (pred: int -> 'a -> bool) (arr: 'a array) : int option =
   try
     for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
     None
@@ -249,20 +242,6 @@ let fold_left_from n f a v =
   in
   fold a n
 
-let fold_right_from n f v a =
-  let rec fold n =
-    if n >= Array.length v then a else f v.(n) (fold (succ n))
-  in
-  fold n
-
-let app_tl v l =
-  if Array.length v = 0 then invalid_arg "Array.app_tl";
-  fold_right_from 1 (fun e l -> e::l) v l
-
-let list_of_tl v =
-  if Array.length v = 0 then invalid_arg "Array.list_of_tl";
-  fold_right_from 1 (fun e l -> e::l) v []
-
 let map_to_list f v =
   List.map f (Array.to_list v)
 
@@ -347,18 +326,6 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
     r
   end
 
-let map_left_pair f a g b =
-  let l = Array.length a in
-  if l = 0 then [||],[||] else begin
-    let r = Array.create l (f a.(0)) in
-    let s = Array.create l (g b.(0)) in
-    for i = 1 to l - 1 do
-      r.(i) <- f a.(i);
-      s.(i) <- g b.(i)
-    done;
-    r, s
-  end
-
 let iter2 f v1 v2 =
   let n = Array.length v1 in
   if Array.length v2 <> n then invalid_arg "Array.iter2"
@@ -390,6 +357,7 @@ let fold_map2' f v1 v2 e =
   in
   (v',!e')
 
+
 let distinct v =
   let visited = Hashtbl.create 23 in
   try
@@ -401,20 +369,11 @@ let distinct v =
     true
   with Exit -> false
 
-let union_map f a acc =
-  Array.fold_left
-    (fun x y -> f y x)
-    acc
-    a
-
 let rev_to_list a =
   let rec tolist i res =
     if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
   tolist 0 []
 
-let filter_along f filter v =
-  Array.of_list (CList.filter_along f filter (Array.to_list v))
-
 let filter_with filter v =
   Array.of_list (CList.filter_with filter (Array.to_list v))
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index bf5648881c..1738bb6184 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -43,8 +43,14 @@ module type ExtS =
 sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
+  (** First size comparison, then lexicographic order. *)
+
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Lift equality to array type. *)
+
   val exists : ('a -> bool) -> 'a array -> bool
+  (** As [List.exists] but on arrays. *)
+
   val for_all : ('a -> bool) -> 'a array -> bool
   val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
   val for_all3 : ('a -> 'b -> 'c -> bool) ->
@@ -52,12 +58,24 @@ sig
   val for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
     'a array -> 'b array -> 'c array -> 'd array -> bool
   val for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
-  val find_i : (int -> 'a -> bool) -> 'a array -> int option
+
+  val findi : (int -> 'a -> bool) -> 'a array -> int option
+
   val hd : 'a array -> 'a
+  (** First element of an array, or [Failure "Array.hd"] if empty. *)
+
   val tl : 'a array -> 'a array
+  (** Remaining part of [hd], or [Failure "Array.tl"] if empty. *)
+
   val last : 'a array -> 'a
+  (** Last element of an array, or [Failure "Array.last"] if empty. *)
+
   val cons : 'a -> 'a array -> 'a array
+  (** Append an element on the left. *)
+
   val rev : 'a array -> unit
+  (** In place reversal. *)
+
   val fold_right_i :
     (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
   val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -70,29 +88,45 @@ sig
   val fold_left2_i :
     (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
-  val fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
-  val app_tl : 'a array -> 'a list -> 'a list
-  val list_of_tl : 'a array -> 'a list
+
   val map_to_list : ('a -> 'b) -> 'a array -> 'b list
+  (** Composition of [map] and [to_list]. *)
+
   val chop : int -> 'a array -> 'a array * 'a array
+  (** [chop i a] returns [(a1, a2)] s.t. [a = a1 + a2] and [length a1 = n].
+      Raise [Failure "Array.chop"] if [i] is not a valid index. *)
+
   val smartmap : ('a -> 'a) -> 'a array -> 'a array
+  (** [smartmap f a] behaves as [map f a] but returns [a] instead of a copy when
+      [f x == x] for all [x] in [a]. *)
+
   val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+
   val map_left : ('a -> 'b) -> 'a array -> 'b array
-  val map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
-    'b array * 'd array
+  (** As [map] but guaranteed to be left-to-right. *)
+
   val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
+  (** Iter on two arrays. Raise [Invalid_argument "Array.iter2" if sizes differ. *)
+
   val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   val fold_map2' :
     ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
+
   val distinct : 'a array -> bool
-  val union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+  (** Return [true] if every element of the array is unique (for default 
+      equality). *)
+
   val rev_to_list : 'a array -> 'a list
-  val filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
+  (** [rev_to_list a] is equivalent to [List.rev (List.of_array a)]. *)
+
   val filter_with : bool list -> 'a array -> 'a array
+  (** [filter_with b a] selects elements of [a] whose corresponding element in
+      [b] is [true].  Raise [Invalid_argument _] when sizes differ. *)
+
 end
 
 include ExtS
diff --git a/lib/cList.ml b/lib/cList.ml
index 3a4a2f5669..2bf8d3597b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -75,7 +75,6 @@ sig
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
   val filter_with : bool list -> 'a list -> 'a list
-  val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
 
   (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
     [ f ai == ai], then [smartmap f l==l] *)
diff --git a/lib/cList.mli b/lib/cList.mli
index 20b63dcd61..fbc87f301e 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -100,8 +100,10 @@ sig
   val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+
   val filter_with : bool list -> 'a list -> 'a list
-  val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
+  (** [filter_with b a] selects elements of [a] whose corresponding element in
+      [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
 
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
   (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i