Some documentation and cleaning of CList and Util interfaces.

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

3 files changed, 94 insertions, 83 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index bc2109167..c5845e74c 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -87,8 +87,7 @@ sig
     ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val map4 :
     ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val map_to_array : ('a -> 'b) -> 'a list -> 'b array
-  val filter_i :
+  val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
 
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
@@ -105,8 +104,7 @@ sig
   (** [index0] behaves as [index] except that it starts counting at 0 *)
   val index0 : 'a -> 'a list -> int
   val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
-  val iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
   val fold_right_and_left :
@@ -130,9 +128,7 @@ sig
   val chop : int -> 'a list -> 'a list * 'a list
   (* former [split_at] was a duplicate of [chop] *)
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-  val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
   val firstn : int -> 'a list -> 'a list
   val last : 'a list -> 'a
   val lastn : int -> 'a list -> 'a list
@@ -366,28 +362,34 @@ let subtractq l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
 
 let tabulate f len =
-  let rec tabrec n =
-    if n = len then [] else (f n)::(tabrec (n+1))
+  let rec loop p i =
+    if len <= i then ()
+    else
+      let c = { head = f i; tail = [] } in
+      let () = p.tail <- cast c in
+      loop c (succ i)
   in
-  tabrec 0
+  let dummy = { head = Obj.magic 0; tail = [] } in
+  loop dummy 0;
+  dummy.tail
 
 let addn n v =
   let rec aux n l =
     if n = 0 then l
-    else aux (pred n) (v::l)
+    else aux (pred n) (v :: l)
   in
-    if n < 0 then invalid_arg "List.addn"
-    else aux n
+  if n < 0 then invalid_arg "List.addn"
+  else aux n
 
 let make n v = addn n v []
 
 let assign l n e =
-  let rec assrec stk = function
-    | ((h::t), 0) -> List.rev_append stk (e::t)
-    | ((h::t), n) -> assrec (h::stk) (t, n-1)
+  let rec assrec stk l i = match l, i with
+    | ((h::t), 0) -> List.rev_append stk (e :: t)
+    | ((h::t), n) -> assrec (h :: stk) t (pred n)
     | ([], _) -> failwith "List.assign"
   in
-  assrec [] (l,n)
+  assrec [] l n
 
 let rec smartmap f l = match l with
     [] -> l
@@ -396,12 +398,7 @@ let rec smartmap f l = match l with
         if h'==h && tl'==tl then l
         else h'::tl'
 
-let map_left f = (* ensures the order in case of side-effects *)
-  let rec map_rec = function
-    | [] -> []
-    | x::l -> let v = f x in v :: map_rec l
-  in
-  map_rec
+let map_left = map
 
 let map2_i f i l1 l2 =
   let rec map_i i = function
@@ -427,9 +424,6 @@ let map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
-let map_to_array f l =
-  Array.of_list (List.map f l)
-
 let rec smartfilter f l = match l with
     [] -> l
   | h::tl ->
@@ -505,15 +499,7 @@ let fold_right_and_left f l hd =
     | a::l -> let hd = aux (a::tl) l in f hd a tl
    in aux [] l
 
-let iter3 f l1 l2 l3 =
-  let rec iter = function
-    | ([], [], []) -> ()
-    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
-    | (_, _, _) -> invalid_arg "map3"
-  in
-  iter (l1,l2,l3)
-
-let iter_i f l = fold_left_i (fun i _ x -> f i x) 0 () l
+let iteri f l = fold_left_i (fun i _ x -> f i x) 0 () l
 
 let for_all_i p =
   let rec for_all_p i = function
@@ -539,7 +525,7 @@ let rec assoc_snd_in_triple x = function
     [] -> raise Not_found
   | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l
 
-let add_set x l = if List.mem x l then l else x::l
+let add_set x l = if List.mem x l then l else x :: l
 
 let eq_set l1 l2 =
   let rec aux l1 = function
@@ -550,7 +536,7 @@ let eq_set l1 l2 =
 let for_all2eq f l1 l2 =
   try List.for_all2 f l1 l2 with Invalid_argument _ -> false
 
-let filter_i p =
+let filteri p =
   let rec filter_i_rec i = function
     | [] -> []
     | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
@@ -677,16 +663,6 @@ let split_when p =
   in
   split_when_loop []
 
-(* [split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
-   [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
-let split_by p =
-  let rec split_by_loop = function
-  | []   -> ([],[])
-  | a::l ->
-      let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
-  in
-  split_by_loop
-
 let rec split3 = function
   | [] -> ([], [], [])
   | (x,y,z)::l ->
@@ -697,9 +673,6 @@ let rec insert_in_class f a = function
   | (b::_ as l)::classes when f a b -> (a::l)::classes
   | l::classes -> l :: insert_in_class f a classes
 
-let partition_by f l =
-  List.fold_right (insert_in_class f) l []
-
 let firstn n l =
   let rec aux acc = function
     | (0, l) -> List.rev acc
@@ -840,7 +813,7 @@ let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> h
 (* Factorize lists of pairs according to the left argument *)
 let rec factorize_left = function
   | (a,b)::l ->
-      let al,l' = split_by (fun (a',b) -> a=a') l in
+      let al,l' = partition (fun (a',b) -> a=a') l in
       (a,(b::List.map snd al)) :: factorize_left l'
   | [] ->
       []
diff --git a/lib/cList.mli b/lib/cList.mli
index c530a2081..87eb3aee7 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -8,6 +8,7 @@
 
 (** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
 
+(** Module type [S] is the one from OCaml Stdlib. *)
 module type S =
 sig
   val length : 'a list -> int
@@ -57,58 +58,85 @@ module type ExtS =
 sig
   include S
   val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+  (** Lexicographic order on lists. *)
+
   val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  (** Lifts equality to list type. *)
+
   val add_set : 'a -> 'a list -> 'a list
+  (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
+      otherwise. *)
+
   val eq_set : 'a list -> 'a list -> bool
+  (** Test equality up to permutation. *)
+
   val intersect : 'a list -> 'a list -> 'a list
   val union : 'a list -> 'a list -> 'a list
   val unionq : 'a list -> 'a list -> 'a list
   val subtract : 'a list -> 'a list -> 'a list
   val subtractq : 'a list -> 'a list -> 'a list
 
-  (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
   val tabulate : (int -> 'a) -> int -> 'a list
+  (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+
   val make : int -> 'a -> 'a list
+  (** [make n x] returns a list made of [n] times [x]. Raise
+      [Invalid_argument "List.make"] if [n] is negative. *)
+
   val assign : 'a list -> int -> 'a -> 'a list
+  (** [assign l i x] set the [i]-th element of [l] to [x], starting from [0]. *)
+
   val distinct : 'a list -> bool
+  (** Return [true] if all elements of the list are distinct. *)
+
   val duplicates : 'a list -> 'a list
+  (** Return the list of unique elements which appear at least twice. Elements
+      are kept in the order of their first appearance. *)
+
   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
 
-  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
-    [ f ai == ai], then [smartmap f l==l] *)
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
+  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+    [f ai == ai], then [smartmap f l == l] *)
+
   val map_left : ('a -> 'b) -> 'a list -> 'b list
+  (** As [map] but ensures the left-to-right order of evaluation. *)
+
   val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+  (** As [map] but with the index, which starts from [0]. *)
+
   val map2_i :
     (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
-  val map4 :
-    ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val map_to_array : ('a -> 'b) -> 'a list -> 'b array
-  val filter_i :
-    (int -> 'a -> bool) -> 'a list -> 'a list
+  val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
+    'd list -> 'e list
+  val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
 
-  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
-    [f ai = true], then [smartfilter f l==l] *)
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+    [f ai = true], then [smartfilter f l == l] *)
 
-  (** [index] returns the 1st index of an element in a list (counting from 1) *)
   val index : 'a -> 'a list -> int
+  (** [index] returns the 1st index of an element in a list (counting from 1). *)
+
   val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
 
-  (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
   val unique_index : 'a -> 'a list -> int
+  (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once. *)
 
-  (** [index0] behaves as [index] except that it starts counting at 0 *)
   val index0 : 'a -> 'a list -> int
+  (** [index0] behaves as [index] except that it starts counting at 0. *)
+
   val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
-  val iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+
+  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
+  (** As [iter] but with the index argument (starting from 0). *)
+
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
   val fold_right_and_left :
@@ -124,60 +152,73 @@ sig
   val sep_last : 'a list -> 'a * 'a list
   val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
   val try_find : ('a -> 'b) -> 'a list -> 'b
+
   val uniquize : 'a list -> 'a list
+  (** Return the list of elements without duplicates. *)
 
-  (** merges two sorted lists and preserves the uniqueness property: *)
   val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+  (** Merge two sorted lists and preserves the uniqueness property. *)
+
   val subset : 'a list -> 'a list -> bool
   val chop : int -> 'a list -> 'a list * 'a list
-  (* former [split_at] was a duplicate of [chop] *)
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-  val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
   val firstn : int -> 'a list -> 'a list
   val last : 'a list -> 'a
   val lastn : int -> 'a list -> 'a list
   val skipn : int -> 'a list -> 'a list
   val skipn_at_least : int -> 'a list -> 'a list
+
   val addn : int -> 'a -> 'a list -> 'a list
+  (** [addn n x l] adds [n] times [x] on the left of [l]. *)
+
   val prefix_of : 'a list -> 'a list -> bool
+  (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
+      otherwise. *)
 
-  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
   val drop_prefix : 'a list -> 'a list -> 'a list
+  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *)
+
   val drop_last : 'a list -> 'a list
 
-  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
   val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
+
   val join_map : ('a -> 'b list) -> 'a list -> 'b list
+  (** Alias of [map_append]. *)
 
-  (** raises [Invalid_argument] if the two lists don't have the same length *)
   val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have 
+      the same length. *)
+
   val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 
+  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
   (** [fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
     where [(e_i,k_i)=f e_{i-1} l_i] *)
-  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
   val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
 
+  val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   (** A generic cartesian product: for any operator (**),
     [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
     and so on if there are more elements in the lists. *)
-  val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
 
+  val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
   (** [cartesians] is an n-ary cartesian product: it iterates
     [cartesian] over a list of lists.  *)
-  val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 
-  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
   val combinations : 'a list list -> 'a list list
+  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
 
-  (** Keep only those products that do not return None *)
   val cartesian_filter :
     ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+  (** Keep only those products that do not return None *)
+
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
 
diff --git a/lib/util.ml b/lib/util.ml
index 42ad11ee1..102541731 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -442,12 +442,9 @@ let interval n m =
   interval_n ([],m)
 
 
-let map_succeed f =
-  let rec map_f = function
-    | [] -> []
-    |  h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
-  in
-  map_f
+let map_succeed f l =
+  let filter x = try Some (f x) with Failure _ -> None in
+  List.map_filter filter l 
 
 (*s Memoization *)