From 9e40a64bc3f50fa6ec2b42b988b09bc5168eb7a0 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 23 Jan 2009 14:47:07 +0000
Subject: 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
---
 lib/util.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

(limited to 'lib/util.ml')

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
   | [] -> ([], [], [])
-- 
cgit v1.2.3