diff --git a/src/data/CCDeque.ml b/src/data/CCDeque.ml index 840bc958..a9da7861 100644 --- a/src/data/CCDeque.ml +++ b/src/data/CCDeque.ml @@ -411,6 +411,23 @@ let filter_in_place (d:_ t) f : unit = (filter_in_place q f; to_list q) = (List.filter f l)) *) +let filter f q = + let q' = create() in + iter (fun x -> if f x then push_back q' x) q; + q' + +(*$Q + Q.(list small_nat) (fun l -> \ + let f = fun x -> x mod 2=0 in \ + let q = filter f (of_list l) in \ + (to_list q) = (List.filter f l)) + *) + +let filter_map f q = + let q' = create() in + iter (fun x -> match f x with None -> () | Some y -> push_back q' y) q; + q' + let rec gen_iter_ f g = match g() with | None -> () | Some x -> f x; gen_iter_ f g diff --git a/src/data/CCDeque.mli b/src/data/CCDeque.mli index 83a628a0..1fbd54d4 100644 --- a/src/data/CCDeque.mli +++ b/src/data/CCDeque.mli @@ -123,6 +123,14 @@ val to_rev_list : 'a t -> 'a list (** Efficient conversion to list, in reverse order. @since 0.13 *) +val filter : ('a -> bool) -> 'a t -> 'a t +(** Filter into a new copy. + @since NEXT_RELEASE *) + +val filter_map : ('a -> 'b option) -> 'a t -> 'b t +(** Filter map into a new copy + @since NEXT_RELEASE *) + val filter_in_place : 'a t -> ('a -> bool) -> unit (** Keep only elements that satisfy the predicate. @since NEXT_RELEASE *)