Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

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

1 files changed, 3 insertions, 532 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 1365f53ce..8916400ac 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -363,536 +363,7 @@ let ascii_of_ident s =
     done with End_of_input -> () end;
     !out
 
-(* Lists *)
-
-let rec list_compare cmp l1 l2 =
-  if l1 == l2 then 0 else
-  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 rec list_equal cmp l1 l2 =
-  l1 == l2 ||
-  match l1, l2 with
-    | [], [] -> true
-    | x1 :: l1, x2 :: l2 ->
-      cmp x1 x2 && list_equal cmp l1 l2
-    | _ -> false
-
-let list_intersect l1 l2 =
-  List.filter (fun x -> List.mem x l2) l1
-
-let list_union l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if List.mem a l2 then urec l else a::urec l
-  in
-  urec l1
-
-let list_unionq l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if List.memq a l2 then urec l else a::urec l
-  in
-  urec l1
-
-let list_subtract l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
-
-let list_subtractq l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
-
-let list_tabulate f len =
-  let rec tabrec n =
-    if n = len then [] else (f n)::(tabrec (n+1))
-  in
-  tabrec 0
-
-let list_addn n v =
-  let rec aux n l =
-    if n = 0 then l
-    else aux (pred n) (v::l)
-  in
-    if n < 0 then invalid_arg "list_addn"
-    else aux n
-
-let list_make n v = list_addn n v []
-
-let list_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)
-    | ([], _) -> failwith "list_assign"
-  in
-  assrec [] (l,n)
-
-let rec list_smartmap f l = match l with
-    [] -> l
-  | h::tl ->
-      let h' = f h and tl' = list_smartmap f tl in
-	if h'==h && tl'==tl then l
-	else h'::tl'
-
-let list_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 list_map_i f =
-  let rec map_i_rec i = function
-    | [] -> []
-    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
-  in
-  map_i_rec
-
-let list_map2_i f i l1 l2 =
-  let rec map_i i = function
-    | ([], []) -> []
-    | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2)
-    | (_, _) -> invalid_arg "map2_i"
-  in
-  map_i i (l1,l2)
-
-let list_map3 f l1 l2 l3 =
-  let rec map = function
-    | ([], [], []) -> []
-    | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3)
-    | (_, _, _) -> invalid_arg "map3"
-  in
-  map (l1,l2,l3)
-
-let list_map4 f l1 l2 l3 l4 =
-  let rec map = function
-    | ([], [], [], []) -> []
-    | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4)
-    | (_, _, _, _) -> invalid_arg "map4"
-  in
-  map (l1,l2,l3,l4)
-
-let list_map_to_array f l =
-  Array.of_list (List.map f l)
-
-let rec list_smartfilter f l = match l with
-    [] -> l
-  | h::tl ->
-      let tl' = list_smartfilter f tl in
-	if f h then
-	  if tl' == tl then l
-	  else h :: tl'
-	else tl'
-	  
-let list_index_f f x =
-  let rec index_x n = function
-    | y::l -> if f x y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
-
-let list_index0_f f x l = list_index_f f x l - 1
-
-let list_index x =
-  let rec index_x n = function
-    | y::l -> if x = y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
-
-let list_index0 x l = list_index x l - 1
-
-let list_unique_index x =
-  let rec index_x n = function
-    | y::l ->
-	if x = y then
-	  if List.mem x l then raise Not_found
-	  else n
-	else index_x (succ n) l
-    | [] -> raise Not_found
-  in index_x 1
-
-let list_fold_right_i f i l =
-  let rec it_list_f i l a = match l with
-    | [] -> a
-    | b::l -> f (i-1) b (it_list_f (i-1) l a)
-  in
-  it_list_f (List.length l + i) l
-
-let list_fold_left_i f =
-  let rec it_list_f i a = function
-    | [] -> a
-    | b::l -> it_list_f (i+1) (f i a b) l
-  in
-  it_list_f
-
-let rec list_fold_left3 f accu l1 l2 l3 =
-  match (l1, l2, l3) with
-    ([], [], []) -> accu
-  | (a1::l1, a2::l2, a3::l3) -> list_fold_left3 f (f accu a1 a2 a3) l1 l2 l3
-  | (_, _, _) -> invalid_arg "list_fold_left3"
-
-(* [list_fold_right_and_left f [a1;...;an] hd =
-   f (f (... (f (f hd
-                   an
-                   [an-1;...;a1])
-              an-1
-              [an-2;...;a1])
-         ...)
-        a2
-        [a1])
-     a1
-     []] *)
-
-let list_fold_right_and_left f l hd =
-  let rec aux tl = function
-    | [] -> hd
-    | a::l -> let hd = aux (a::tl) l in f hd a tl
-   in aux [] l
-
-let list_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 list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
-
-let list_for_all_i p =
-  let rec for_all_p i = function
-    | [] -> true
-    | a::l -> p i a && for_all_p (i+1) l
-  in
-  for_all_p
-
-let list_except x l = List.filter (fun y -> not (x = y)) l
-
-let list_remove = list_except (* Alias *)
-
-let rec list_remove_first a = function
-  | b::l when a = b -> l
-  | b::l -> b::list_remove_first a l
-  | [] -> raise Not_found
-
-let rec list_remove_assoc_in_triple x = function
-  | [] -> []
-  | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
-
-let rec list_assoc_snd_in_triple x = function
-    [] -> raise Not_found
-  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_snd_in_triple x l
-
-let list_add_set x l = if List.mem x l then l else x::l
-
-let list_eq_set l1 l2 =
-  let rec aux l1 = function
-  | [] -> l1 = []
-  | a::l2 -> aux (list_remove_first a l1) l2 in
-  try aux l1 l2 with Not_found -> false
-
-let list_for_all2eq f l1 l2 =
-  try List.for_all2 f l1 l2 with Invalid_argument _ -> false
-
-let list_filter_i 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'
-  in
-  filter_i_rec 0
-
-let rec list_sep_last = function
-  | [] -> failwith "sep_last"
-  | hd::[] -> (hd,[])
-  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
-
-let list_try_find_i f =
-  let rec try_find_f n = function
-    | [] -> failwith "try_find_i"
-    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
-  in
-  try_find_f
-
-let list_try_find f =
-  let rec try_find_f = function
-    | [] -> failwith "try_find"
-    | h::t -> try f h with Failure _ -> try_find_f t
-  in
-  try_find_f
-
-let list_uniquize l =
-  let visited = Hashtbl.create 23 in
-  let rec aux acc = function
-    | h::t -> if Hashtbl.mem visited h then aux acc t else
-	  begin
-	    Hashtbl.add visited h h;
-	    aux (h::acc) t
-	  end
-    | [] -> List.rev acc
-  in aux [] l
-
-let list_distinct l =
-  let visited = Hashtbl.create 23 in
-  let rec loop = function
-    | h::t ->
-	if Hashtbl.mem visited h then false
-	else
-	  begin
-	    Hashtbl.add visited h h;
-	    loop t
-	  end
-    | [] -> true
-  in loop l
-
-let rec list_merge_uniq cmp l1 l2 =
-  match l1, l2 with
-  | [], l2 -> l2
-  | l1, [] -> l1
-  | h1 :: t1, h2 :: t2 ->
-      let c = cmp h1 h2 in
-      if c = 0
-      then h1 :: list_merge_uniq cmp t1 t2
-      else if c <= 0
-      then h1 :: list_merge_uniq cmp t1 l2
-      else h2 :: list_merge_uniq cmp l1 t2
-
-let rec list_duplicates = function
-  | [] -> []
-  | x::l ->
-      let l' = list_duplicates l in
-      if List.mem x l then list_add_set x l' else l'
-
-let rec list_filter2 f = function
-  | [], [] as p -> p
-  | d::dp, l::lp ->
-     let (dp',lp' as p) = list_filter2 f (dp,lp) in
-      if f d l then d::dp', l::lp' else p
-  | _ -> invalid_arg "list_filter2"
-
-let rec list_map_filter f = function
-  | [] -> []
-  | x::l ->
-      let l' = list_map_filter f l in
-      match f x with None -> l' | Some y -> y::l'
-
-let list_map_filter_i f =
-  let rec aux i = function
-    | [] -> []
-    | x::l ->
-      let l' = aux (succ i) l in
-	match f i x with None -> l' | Some y -> y::l'
-  in aux 0
-
-let list_filter_along f filter l =
-  snd (list_filter2 (fun b c -> f b) (filter,l))
-
-let list_filter_with filter l =
-  list_filter_along (fun x -> x) filter l
-
-let list_subset l1 l2 =
-  let t2 = Hashtbl.create 151 in
-  List.iter (fun x -> Hashtbl.add t2 x ()) l2;
-  let rec look = function
-    | [] -> true
-    | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
-  in
-  look l1
-
-(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
-   [l1++l2=l] and [l1] has length [i].
-   It raises [Failure] when [i] is negative or greater than the length of [l]  *)
-
-let list_chop n l =
-  let rec chop_aux i acc = function
-    | tl when i=0 -> (List.rev acc, tl)
-    | h::t -> chop_aux (pred i) (h::acc) t
-    | [] -> failwith "list_chop"
-  in
-  chop_aux n [] l
-
-(* [list_split_when p l] splits [l] into two lists [(l1,a::l2)] such that
-    [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
-    If there is no such [a], then it returns [(l,[])] instead *)
-let list_split_when p =
-  let rec split_when_loop x y =
-    match y with
-      | []      -> (List.rev x,[])
-      | (a::l)  -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
-  in
-  split_when_loop []
-
-(* [list_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 list_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 list_split3 = function
-  | [] -> ([], [], [])
-  | (x,y,z)::l ->
-      let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
-
-let rec list_insert_in_class f a = function
-  | [] -> [[a]]
-  | (b::_ as l)::classes when f a b -> (a::l)::classes
-  | l::classes -> l :: list_insert_in_class f a classes
-
-let list_partition_by f l =
-  List.fold_right (list_insert_in_class f) l []
-
-let list_firstn n l =
-  let rec aux acc = function
-    | (0, l) -> List.rev acc
-    | (n, (h::t)) -> aux (h::acc) (pred n, t)
-    | _ -> failwith "firstn"
-  in
-  aux [] (n,l)
-
-let rec list_last = function
-  | [] -> failwith "list_last"
-  | [x] -> x
-  | _ :: l -> list_last l
-
-let list_lastn n l =
-  let len = List.length l in
-  let rec aux m l =
-    if m = n then l else aux (m - 1) (List.tl l)
-  in
-  if len < n then failwith "lastn" else aux len l
-
-let rec list_skipn n l = match n,l with
-  | 0, _ -> l
-  | _, [] -> failwith "list_skipn"
-  | n, _::l -> list_skipn (pred n) l
-
-let list_skipn_at_least n l =
-  try list_skipn n l with Failure _ -> []
-
-let list_prefix_of prefl l =
-  let rec prefrec = function
-    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
-    | ([], _) -> true
-    | (_, _) -> false
-  in
-    prefrec (prefl,l)
-
-let list_drop_prefix p l =
-(* if l=p++t then return t else l *)
-  let rec list_drop_prefix_rec = function
-    | ([], tl) -> Some tl
-    | (_, []) -> None
-    | (h1::tp, h2::tl) ->
-	if h1 = h2 then list_drop_prefix_rec (tp,tl) else None
-  in
-    match list_drop_prefix_rec (p,l) with
-      | Some r -> r
-      | None -> l
-
-let list_map_append f l = List.flatten (List.map f l)
-let list_join_map = list_map_append   (* Alias *)
-
-let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
-
-let list_share_tails l1 l2 =
-  let rec shr_rev acc = function
-    | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
-    | (l1,l2) -> (List.rev l1, List.rev l2, acc)
-  in
-  shr_rev [] (List.rev l1, List.rev l2)
-
-let rec list_fold_map f e = function
-  |  []  -> (e,[])
-  |  h::t ->
-       let e',h' = f e h in
-       let e'',t' = list_fold_map f e' t in
-         e'',h'::t'
-
-(* (* tail-recursive version of the above function *)
-let list_fold_map f e l =
-  let g (e,b') h =
-    let (e',h') = f e h in
-      (e',h'::b')
-  in
-  let (e',lrev) = List.fold_left g (e,[]) l in
-    (e',List.rev lrev)
-*)
-
-(* The same, based on fold_right, with the effect accumulated on the right *)
-let list_fold_map' f l e =
-  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
-
-let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
-
-let rec list_assoc_f f a = function
-  | (x, e) :: xs -> if f a x then e else list_assoc_f f a xs
-  | [] -> raise Not_found
-
-(* Specification:
-   - =p= is set equality (double inclusion)
-   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
-   - let g = fun x -> f x [] in
-   - union_map f l acc =p= append (flatten (map g l)) acc
- *)
-let list_union_map f l acc =
-  List.fold_left
-    (fun x y -> f y x)
-    acc
-    l
-
-(* A generic cartesian product: for any operator (**),
-   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
-   and so on if there are more elements in the lists. *)
-
-let list_cartesian op l1 l2 =
-  list_map_append (fun x -> List.map (op x) l2) l1
-
-(* [list_cartesians] is an n-ary cartesian product: it iterates
-   [list_cartesian] over a list of lists.  *)
-
-let list_cartesians op init ll =
-  List.fold_right (list_cartesian op) ll [init]
-
-(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
-
-let list_combinations l = list_cartesians (fun x l -> x::l) [] l
-
-let rec list_combine3 x y z = 
-  match x, y, z with
-  | [], [], [] -> []
-  | (x :: xs), (y :: ys), (z :: zs) ->
-      (x, y, z) :: list_combine3 xs ys zs
-  | _, _, _ -> raise (Invalid_argument "list_combine3")
-  
-(* Keep only those products that do not return None *)
-
-let list_cartesian_filter op l1 l2 =
-  list_map_append (fun x -> list_map_filter (op x) l2) l1
-
-(* Keep only those products that do not return None *)
-
-let list_cartesians_filter op init ll =
-  List.fold_right (list_cartesian_filter op) ll [init]
-
-(* Drop the last element of a list *)
-
-let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
-
-(* Factorize lists of pairs according to the left argument *)
-let rec list_factorize_left = function
-  | (a,b)::l ->
-      let al,l' = list_split_by (fun (a',b) -> a=a') l in
-      (a,(b::List.map snd al)) :: list_factorize_left l'
-  | [] ->
-      []
+module List : CList.ExtS = CList
 
 (* Arrays *)
 
@@ -1212,10 +683,10 @@ let array_rev_to_list a =
   tolist 0 []
 
 let array_filter_along f filter v =
-  Array.of_list (list_filter_along f filter (Array.to_list v))
+  Array.of_list (CList.filter_along f filter (Array.to_list v))
 
 let array_filter_with filter v =
-  Array.of_list (list_filter_with filter (Array.to_list v))
+  Array.of_list (CList.filter_with filter (Array.to_list v))
 
 (* Matrices *)