diff options
| -rw-r--r-- | engine/proofview.ml | 6 | ||||
| -rw-r--r-- | lib/cList.ml | 11 | ||||
| -rw-r--r-- | lib/cList.mli | 1 |
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 |