Petit nettoyage faisant suite au commit #11847 .

Quelques modifications autour (géographiquement) de Util.list_split_at

Util.list_split_at devient Util.list_split_when (dénomination inventée
arbitrairement par moi-même, mais qui ne devrait pas déranger grand
monde vu qu'il semble n'y avoir que deux occurences de cette fonction).
Pour laisser la place à la fonction suivante :

Introduction de Util.list_split_at: qui sépare la liste à une position
donnée (alors que la nouvellement nommé list_split_when sépare à la 
première occurence "vrai" d'un prédicat).                            

Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux 
fonctions.

Suppression de Impargs.list_split_at (appel à Util).   

Suppression de Subtac_pretyping.list_split_at (qui était du code mort de 
toute façon).

Suppression Util.list_split_by qui n'est utilisé nulle part et est une 
réimplémentation de List.partition (qui est probablement meilleure, en 
particulier tail-recursive)



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

2 files changed, 19 insertions, 14 deletions

diff --git a/lib/util.ml b/lib/util.ml
index c685ee2268..172d8d9113 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -770,21 +770,26 @@ let list_subset l1 l2 =
   in 
   look l1
 
-let list_split_at p = 
-  let rec split_at_loop x y = 
+(* [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_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 
       | []      -> ([],[])
-      | (a::l)  -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l
+      | (a::l)  -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
   in 
-  split_at_loop []
-
-let list_split_by p = 
-  let rec split_loop = function
-  | []      -> ([],[])
-  | (a::l)  ->
-      let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2)
-  in 
-  split_loop
+  split_when_loop []
 
 let rec list_split3 = function
   | [] -> ([], [], [])
diff --git a/lib/util.mli b/lib/util.mli
index 7af5816ea2..023b8a15ee 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -150,8 +150,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 : ('a -> bool) -> 'a list -> 'a list * 'a list
-val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_at : int -> 'a list -> 'a list*'a list
+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
 val list_firstn : int -> 'a list -> 'a list