Add a [CList.partitioni] function.

3 files changed, 14 insertions, 4 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index d1970abc9a..2b8fc00574 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -409,10 +409,8 @@ let tclFOCUSLIST l t =
       | [] -> tclZERO (NoSuchGoals 0)
       | (mi, _) :: _ ->
           let left, sub_right = CList.goto (mi-1) comb in
-          let p x = CList.exists (fun (i, j) -> i <= x && x <= j) l in
-          (* Since there is no [CList.partitioni], we do it manually. *)
-          let sub = CList.filteri (fun x _ -> p (x + mi)) sub_right in
-          let right = CList.filteri (fun x _ -> not (p (x + mi))) sub_right in
+          let p x _ = CList.exists (fun (i, j) -> i <= x +mi && x + mi <= j) l in
+          let sub, right = CList.partitioni p sub_right in
           let mj = mi - 1 + CList.length sub in
             Comb.set (CList.rev_append left (sub @ right)) >>
             tclFOCUS mi mj t
diff --git a/lib/cList.ml b/lib/cList.ml
index ba592d13f3..3a792d4168 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -47,6 +47,8 @@ sig
     ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
+  val partitioni :
+    (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
@@ -486,6 +488,15 @@ let filteri p =
   in
   filter_i_rec 0
 
+let partitioni p =
+  let rec aux i = function
+    | [] -> [], []
+    | x :: l ->
+        let (l1, l2) = aux (succ i) l in
+        if p i x then (x :: l1, l2)
+        else (l1, x :: l2)
+  in aux 0
+
 let rec sep_last = function
   | [] -> failwith "sep_last"
   | hd::[] -> (hd,[])
diff --git a/lib/cList.mli b/lib/cList.mli
index 9c7b815c15..b19d1a80fc 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -89,6 +89,7 @@ sig
   val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
     'd list -> 'e list
   val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+  val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
 
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i