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, 20 insertions, 19 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 9e6b63537..5b58dc9ba 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,20 +149,20 @@ let canonical_path_name p =
 
 let find_logical_path phys_dir =
   let phys_dir = canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
+  match List.filter2 (fun p d -> p = phys_dir) !load_paths with
   | _,[dir] -> dir
   | _,[] -> default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let remove_load_path dir =
-  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+  load_paths := List.filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
     ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
-    match list_filter2 (fun p d -> p = phys_path) !load_paths with
+    match List.filter2 (fun p d -> p = phys_path) !load_paths with
       | _,[dir] ->
 	  if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let load_paths_of_dir_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_paths)
+  fst (List.filter2 (fun p d -> d = dir) !load_paths)
 
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
diff --git a/checker/check.mllib b/checker/check.mllib
index 15d7df1d3..b7e196d4b 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -7,6 +7,7 @@ Loc
 Segmenttree
 Unicodetable
 Errors
+CList
 Util
 Option
 Hashcons
diff --git a/checker/closure.ml b/checker/closure.ml
index 7f23ed201..c3351cea1 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -370,7 +370,7 @@ let rec compact_constr (lg, subs as s) c k =
   match c with
       Rel i ->
         if i < k then c,s else
-          (try Rel (k + lg - list_index (i-k+1) subs), (lg,subs)
+          (try Rel (k + lg - List.index (i-k+1) subs), (lg,subs)
           with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
     | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
     | Evar(ev,v) ->
@@ -648,7 +648,7 @@ let rec get_args n tys f e stk =
           let eargs = Array.sub l n (na-n) in
           (Inl (subs_cons(args,e)), Zapp eargs :: s)
         else (* more lambdas *)
-          let etys = list_skipn na tys in
+          let etys = List.skipn na tys in
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index ba56c243f..ad14a3bbe 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -546,7 +546,7 @@ let subst_rel_declaration sub (id,copt,t as x) =
   let t' = subst_mps sub t in
   if copt == copt' & t == t' then x else (id,copt',t')
 
-let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
 type recarg =
   | Norec
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index b11b79d1a..6d936796a 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -331,7 +331,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     recursive parameters *)
 
 let check_rec_par (env,n,_,_) hyps nrecp largs =
-  let (lpar,_) = list_chop nrecp largs in
+  let (lpar,_) = List.chop nrecp largs in
   let rec find index =
     function
       | ([],_) -> ()
@@ -355,7 +355,7 @@ let abstract_mind_lc env ntyps npars lc =
     lc
   else
     let make_abs =
-      list_tabulate
+      List.tabulate
 	(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
     in
     Array.map (substl make_abs) lc
@@ -432,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
     let auxnpar = mib.mind_nparams_rec in
     let nonrecpar = mib.mind_nparams - auxnpar in
     let (lpar,auxlargs) =
-      try list_chop auxnpar largs
+      try List.chop auxnpar largs
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
       (* If the inductive appears in the args (non params) then the
 	 definition is not positive. *)
@@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds =
   let lparams = rel_context_length params in
   let check_one i mip =
     let ra_env =
-      list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+      List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
       check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 6e87fb365..f35d68ad1 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 let ind_subst mind mib =
   let ntypes = mib.mind_ntypes in
   let make_Ik k = Ind (mind,ntypes-k-1) in
-  list_tabulate make_Ik ntypes
+  List.tabulate make_Ik ntypes
 
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind mib c =
@@ -255,7 +255,7 @@ let extended_rel_list n hyps =
   reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist
     (Ind ind,
        List.map (lift mip.mind_nrealargs_ctxt) params
@@ -309,7 +309,7 @@ let build_branches_type ind (_,mip as specif) params dep p =
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop (inductive_params specif) allargs in
+    let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       if dep then
         let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -331,7 +331,7 @@ let build_case_type dep p c realargs =
 let type_case_branches env (ind,largs) (p,pj) c =
   let specif = lookup_mind_specif env ind in
   let nparams = inductive_params specif in
-  let (params,realargs) = list_chop nparams largs in
+  let (params,realargs) = List.chop nparams largs in
   let dep = is_correct_arity env c (p,pj) ind specif params in
   let lc = build_branches_type ind specif params dep p in
   let ty = build_case_type dep p c realargs in
@@ -444,7 +444,7 @@ let push_var renv (x,ty,spec) =
     genv = spec:: renv.genv }
 
 let assign_var_spec renv (i,spec) =
-  { renv with genv = list_assign renv.genv (i-1) spec }
+  { renv with genv = List.assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
   push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
@@ -527,7 +527,7 @@ let branches_specif renv c_spec ci =
 		    vra
 	      | Dead_code -> Array.create nca Dead_code
 	      | _ -> Array.create nca Not_subterm) in
-	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+	 List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
       car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
@@ -871,7 +871,7 @@ let check_one_cofix env nbfix def deftype =
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
-            let realargs = list_skipn mib.mind_nparams args in
+            let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
                   if rar = mk_norec then
diff --git a/checker/term.ml b/checker/term.ml
index 955a61c14..a7fc0a8b8 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -346,7 +346,7 @@ let map_context f l =
       if body_o' == body_o && typ' == typ then decl else
 	(n, body_o', typ')
   in
-    list_smartmap map_decl l
+    List.smartmap map_decl l
 
 let map_rel_context = map_context