Util: remove list_split_at which is a clone of list_chop

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

6 files changed, 21 insertions, 27 deletions

diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index 39e8155d3f..cadb5941e4 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -18,14 +18,14 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#append_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_split_at real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 (* XXX - Temporary hack to compile with archaic lablgtk
   method insert_term ?(build=default_build) ?pos (term:'a) =
     let tab_label,menu_label,page = build term in
     let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Util.list_split_at real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -34,7 +34,7 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#prepend_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_split_at real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
diff --git a/lib/util.ml b/lib/util.ml
index a2c6c7899d..ba3d2c6d28 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -396,14 +396,6 @@ let list_subtract l1 l2 =
 let list_subtractq l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
 
-let list_chop n l =
-  let rec chop_aux acc = function
-    | (0, l2) -> (List.rev acc, l2)
-    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
-    | (_, []) -> failwith "list_chop"
-  in
-  chop_aux [] (n,l)
-
 let list_tabulate f len =
   let rec tabrec n =
     if n = len then [] else (f n)::(tabrec (n+1))
@@ -655,15 +647,17 @@ let list_subset l1 l2 =
   in
   look l1
 
-(* [list_split_at 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_split_at index l =
-  let rec aux i acc = function
-      tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
+(* [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].
diff --git a/lib/util.mli b/lib/util.mli
index ddf32e7623..f900e9bf71 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -116,7 +116,6 @@ val list_union : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
 val list_subtract : 'a list -> 'a list -> 'a list
 val list_subtractq : 'a list -> 'a list -> 'a list
-val list_chop : int -> 'a list -> 'a list * 'a list
 (* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_make : int -> 'a -> 'a list
@@ -164,7 +163,8 @@ val list_uniquize : 'a list -> 'a list
 (* merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
-val list_split_at : int -> 'a list -> 'a list*'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+(* former [list_split_at] was a duplicate of [list_chop] *)
 val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
diff --git a/library/impargs.ml b/library/impargs.ml
index fead921a55..b53b2a89d1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -415,9 +415,9 @@ let compute_global_implicits flags manual = function
 let merge_impls oldimpls newimpls =
   let (before, news), olds =
     let len = List.length newimpls - List.length oldimpls in
-      if len >= 0 then list_split_at len newimpls, oldimpls
+      if len >= 0 then list_chop len newimpls, oldimpls
       else
-	let before, after = list_split_at (-len) oldimpls in
+	let before, after = list_chop (-len) oldimpls in
 	  (before, newimpls), after
   in
     before @ (List.map2 (fun orig ni ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 8353379522..667f2e91a0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -830,7 +830,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_split_at 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
@@ -838,7 +838,7 @@ let extract_std_constant env kn body typ =
   in
   let n = List.length rels in
   let s = list_firstn n s in
-  let l,l' = list_split_at n l 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/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5275d04c7c..4c58edf595 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -452,7 +452,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 	  let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in
 	  let v' s' pfs' : proof_tree =
 	    let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) ->
-	      let before, after = list_split_at (List.length gls) pfs' in
+	      let before, after = list_chop (List.length gls) pfs' in
 		(v s' before :: newpfs, after))
 	      ([], pfs') res
 	    in assert(rest = []); v s' (List.rev newpfs)