diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 15:24:56 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 16:02:48 +0200 |
| commit | 6aac2c78ad5dec79c6ed16a50accde57c37398a9 (patch) | |
| tree | 53968b5035fd9b70d4431130cf12621f314cb187 /lib | |
| parent | a452e436af72ccc1b8342ac6b666f0ff202cc20a (diff) | |
| parent | 791f3254cba602672b834ec3484d308db074b684 (diff) | |
Merge 'pr/191' into trunk
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cList.ml | 11 | ||||
| -rw-r--r-- | lib/cList.mli | 1 |
2 files changed, 12 insertions, 0 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index ba592d13f..3a792d416 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 9c7b815c1..b19d1a80f 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 |