diff --git a/src/core/CCList.ml b/src/core/CCList.ml index 20e9c77d..7ee178c1 100644 --- a/src/core/CCList.ml +++ b/src/core/CCList.ml @@ -1259,7 +1259,7 @@ let replicate i x = *) (*$Q - Q.(pair small_int (list int)) (fun (n,l) -> \ + Q.(pair small_int (small_list int)) (fun (n,l) -> \ if n>0 then repeat n l = flat_map (fun _ -> l) (1--n) \ else Q.assume_fail()) *) diff --git a/src/data/CCRAL.ml b/src/data/CCRAL.ml index 351e687b..3126cf22 100644 --- a/src/data/CCRAL.ml +++ b/src/data/CCRAL.ml @@ -257,6 +257,13 @@ let flat_map f l = append l acc ) +(*$Q + Q.(pair (fun1 Observable.int (list int)) (list int)) (fun (f,l) -> \ + let f x = Q.Fn.apply f x in \ + let f' x = f x |> of_list in \ + of_list l |> flat_map f' |> to_list = CCList.(flat_map f l)) + *) + let flatten l = fold_rev ~f:(fun acc l -> append l acc) ~x:empty l (*$T @@ -264,6 +271,11 @@ let flatten l = fold_rev ~f:(fun acc l -> append l acc) ~x:empty l of_list [1;2;3;] *) +(*$Q + Q.(small_list (small_list int)) (fun l -> \ + of_list l |> map ~f:of_list |> flatten |> to_list = CCList.flatten l) + *) + let app funs l = fold_rev ~x:empty funs ~f:(fun acc f -> @@ -307,6 +319,11 @@ and take_tree_ ~size n t = match t with take 0 (of_list CCList.(1--10)) |> to_list = [] *) +(*$Q + Q.(pair small_int (list int)) (fun (n,l) -> \ + of_list l |> take n |> to_list = CCList.take n l) +*) + let take_while ~f l = (* st: stack of subtrees *) let rec aux p st = match st with @@ -323,6 +340,9 @@ let take_while ~f l = Q.(list int) (fun l -> \ let f x = x mod 7 <> 0 in \ of_list l |> take_while ~f |> to_list = CCList.take_while f l) + Q.(pair (fun1 Observable.int bool) (list int)) (fun (f,l) -> \ + let f x = Q.Fn.apply f x in \ + of_list l |> take_while ~f |> to_list = CCList.take_while f l) *) let rec drop n l = match l with @@ -346,6 +366,11 @@ and drop_tree_ ~size n t tail = match t with of_list [1;2;3] |> drop 2 |> length = 1 *) +(*$Q + Q.(pair small_int (list int)) (fun (n,l) -> \ + of_list l |> drop n |> to_list = CCList.drop n l) +*) + let drop_while ~f l = let rec aux p st = match st with | St_nil -> Nil @@ -410,6 +435,12 @@ let repeat n l = in aux n l empty + +(*$Q + Q.(pair small_int (list int)) (fun (n,l) -> \ + of_list l |> repeat n |> to_list = CCList.(repeat n l)) + *) + let range i j = let rec aux i j acc = if i=j then cons i acc