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

7 files changed, 33 insertions, 33 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index b6b7e5833..8cceb2a11 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -349,7 +349,7 @@ let rec mp_renaming_fun mp = match mp with
   | MPfile _ ->
       assert (modular ()); (* see [at_toplevel] above *)
       assert (get_phase () = Pre);
-      let current_mpfile = (list_last (get_visible ())).mp in
+      let current_mpfile = (List.last (get_visible ())).mp in
       if mp <> current_mpfile then mpfiles_add mp;
       [string_of_modfile mp]
 
@@ -496,7 +496,7 @@ let fstlev_ks k = function
 let pp_ocaml_local k prefix mp rls olab =
   (* what is the largest prefix of [mp] that belongs to [visible]? *)
   assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-  let rls' = list_skipn (mp_length prefix) rls in
+  let rls' = List.skipn (mp_length prefix) rls in
   let k's = fstlev_ks k rls' in
   (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
   if not (visible_clash prefix k's) then dottify rls'
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 588fe0cf2..b5cdec3ec 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -150,9 +150,9 @@ let factor_fix env l cb msb =
   if n = 1 then [|l|], recd, msb
   else begin
     if List.length msb < n-1 then raise Impossible;
-    let msb', msb'' = list_chop (n-1) msb in
+    let msb', msb'' = List.chop (n-1) msb in
     let labels = Array.make n l in
-    list_iter_i
+    List.iter_i
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
@@ -207,7 +207,7 @@ let env_for_mtb_with_def env mp seb idl =
   in
   let l = label_of_id (List.hd idl) in
   let spot = function (l',SFBconst _) -> l = l' | _ -> false in
-  let before = fst (list_split_when spot sig_b) in
+  let before = fst (List.split_when spot sig_b) in
   Modops.add_signature mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0556f6d77..e1bbcf9c7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -193,7 +193,7 @@ let parse_ind_args si args relmax =
 
 let oib_equal o1 o2 =
   id_ord o1.mind_typename o2.mind_typename = 0 &&
-  list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
     Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
@@ -206,10 +206,10 @@ let mib_equal m1 m2 =
   m1.mind_record = m2.mind_record &&
   m1.mind_finite = m2.mind_finite &&
   m1.mind_ntypes = m2.mind_ntypes &&
-  list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
   m1.mind_nparams = m2.mind_nparams &&
   m1.mind_nparams_rec = m2.mind_nparams_rec &&
-  list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
   m1.mind_constraints = m2.mind_constraints
 
 (*S Extraction of a type. *)
@@ -439,7 +439,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in
 	let field_names =
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in
 	let mp,d,_ = repr_mind kn in
@@ -674,7 +674,7 @@ and extract_cst_app env mle mlt kn args =
   let mla =
     if not magic1 then
       try
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
+	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with _ -> mla
@@ -697,7 +697,7 @@ and extract_cst_app env mle mlt kn args =
     (* Partially applied function with some logical arg missing.
        We complete via eta and expunge logical args. *)
     let ls' = ls-la in
-    let s' = list_skipn la s in
+    let s' = List.skipn la s in
     let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
     let e = anonym_or_dummy_lams (mlapp head mla) s' in
     put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
@@ -729,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let la = List.length args in
   assert (la <= ls + params_nb);
   let la' = max 0 (la - params_nb) in
-  let args' = list_lastn la' args in
+  let args' = List.lastn la' args in
   (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in
   (* If stored and expected types differ, then magic! *)
@@ -758,7 +758,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
       let ls' = params_nb + ls - la in
-      let s' = list_lastn ls' s in
+      let s' = List.lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
@@ -847,7 +847,7 @@ let decomp_lams_eta_n n m env c t =
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
-  let rels = (list_firstn d rels) @ rels' in
+  let rels = (List.firstn d rels) @ rels' in
   let eta_args = List.rev_map mkRel (interval 1 d) in
   rels, applist (lift d c,eta_args)
 
@@ -886,7 +886,7 @@ let extract_std_constant env kn body typ =
     and m = nb_lam body in
     if n <= m then decompose_lam_n n body
     else
-      let s,s' = list_chop m s in
+      let s,s' = List.chop m s in
       if List.for_all ((=) Keep) s' &&
 	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
       then decompose_lam_n m body
@@ -895,7 +895,7 @@ let extract_std_constant env kn body typ =
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
     let n = List.length rels in
-    let s,s' = list_chop n s in
+    let s,s' = List.chop n s in
     let k = sign_kind s in
     let empty_s = (k = EmptySig || k = SafeLogicalSig) in
     if lang () = Ocaml && empty_s && not (gentypvar_ok c)
@@ -904,8 +904,8 @@ let extract_std_constant env kn body typ =
     else rels,c
   in
   let n = List.length rels in
-  let s = list_firstn n s in
-  let l,l' = list_chop n l in
+  let s = List.firstn n s in
+  let l,l' = List.chop n l in
   let t' = type_recomp (l',t') in
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3b89386d4..3716695b8 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -534,7 +534,7 @@ let is_regular_match br =
 	match pat with
 	  | Pusual r -> r
 	  | Pcons (r,l) ->
-	    if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+	    if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -636,9 +636,9 @@ let eta_red e =
 	  if m = n then
 	    [], f, a
 	  else if m < n then
-	    list_skipn m ids, f, a
+	    List.skipn m ids, f, a
 	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in
+	    let a1,a2 = List.chop (m-n) a in
 	    [], MLapp (f,a1), a2
 	in
 	let p = List.length args in
@@ -969,7 +969,7 @@ and simpl_case o typ br e =
 	    else ([], Pwild, ast_pop f)
 	  in
 	  let brl = Array.to_list br in
-	  let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+	  let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in
 	  let brl_opt = brl_opt @ [last_br] in
 	  MLcase (typ, e, Array.of_list brl_opt)
 	| None -> MLcase (typ, e, br)
@@ -1022,8 +1022,8 @@ let kill_dummy_lams c =
     | Keep :: bl -> fst_kill (n+1) bl
   in
   let skip = max 0 ((fst_kill 0 bl) - 1) in
-  let ids_skip, ids = list_chop skip ids in
-  let _, bl = list_chop skip bl in
+  let ids_skip, ids = List.chop skip ids in
+  let _, bl = List.chop skip bl in
   let c = named_lams ids_skip c in
   let ids',c = kill_some_lams bl (ids,c) in
   ids, named_lams ids' c
@@ -1051,7 +1051,7 @@ let case_expunge s e =
   let m = List.length s in
   let n = nb_lams e in
   let p = if m <= n then collect_n_lams m e
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+  else eta_expansion_sign (List.skipn n s) (collect_lams e) in
   kill_some_lams (List.rev s) p
 
 (*s [term_expunge] takes a function [fun idn ... id1 -> c]
@@ -1085,7 +1085,7 @@ let kill_dummy_args ids r t =
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
@@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c =
     | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in list_iter_i aux args;
+  in List.iter_i aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 1211bbf17..8659de03e 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -30,7 +30,7 @@ let se_iter do_decl do_spec =
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
-	let l',idl' = list_sep_last idl in
+	let l',idl' = List.sep_last idl in
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
 	in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 34ae1f9ad..951049b7b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -114,7 +114,7 @@ let pp_one_field r i = function
 
 let pp_field r fields i = pp_one_field r i (List.nth fields i)
 
-let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
+let pp_fields r fields = List.map_i (pp_one_field r) 0 fields
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -189,7 +189,7 @@ let rec pp_expr par env args =
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
     | MLglob r ->
 	(try
-	   let args = list_skipn (projection_arity r) args in
+	   let args = List.skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
 	 with _ -> apply (pp_global Term r))
@@ -642,7 +642,7 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
-      let l,idl' = list_sep_last idl in
+      let l,idl' = List.sep_last idl in
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
       in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2dd07b2f2..6151abf6e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -671,7 +671,7 @@ let add_implicits r l =
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try list_index (Name id) names
+	(try List.index (Name id) names
 	 with Not_found ->
 	   err (str "No argument " ++ pr_id id ++ str " for " ++
 		safe_pr_global r))
@@ -877,7 +877,7 @@ let extract_inductive r s l optstr =
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
 	  optstr;
-	list_iter_i
+	List.iter_i
 	  (fun j s ->
 	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));