diff --git a/src/core/CCList.ml b/src/core/CCList.ml index 5d84d136..1a0ab160 100644 --- a/src/core/CCList.ml +++ b/src/core/CCList.ml @@ -366,6 +366,25 @@ let combine l1 l2 = else Q.assume_fail() ) *) +let combine_gen l1 l2 = + let l1 = ref l1 in + let l2 = ref l2 in + fun () -> match !l1, !l2 with + | [], _ + | _, [] -> None + | x1 :: tail1, x2 :: tail2 -> + l1 := tail1; + l2 := tail2; + Some (x1,x2) + +(*$Q + Q.(let p = small_list int in pair p p)(fun (l1,l2) -> \ + let n = min (List.length l1) (List.length l2) in \ + let res1 = combine (take n l1) (take n l2) in \ + let res2 = combine_gen l1 l2 |> of_gen in \ + res1 = res2) + *) + let return x = [x] let (>>=) l f = flat_map f l diff --git a/src/core/CCList.mli b/src/core/CCList.mli index df85ca5f..46fbeff4 100644 --- a/src/core/CCList.mli +++ b/src/core/CCList.mli @@ -83,6 +83,13 @@ val combine : 'a list -> 'b list -> ('a * 'b) list @raise Invalid_argument if the lists have distinct lengths. @since NEXT_RELEASE *) +val combine_gen : 'a list -> 'b list -> ('a * 'b) gen +(** Lazy version of {!combine}. + Unlike {!combine}, it does not fail if the lists have different + lengths; + instead, the output has as many pairs as the smallest input list. + @since NEXT_RELEASE *) + val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool