From 4a46fa4d710e5df00920da337d4c209ab0746dd3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 9 Apr 2023 14:59:39 -0400 Subject: [PATCH] add a op test for Fun_vec --- containers-data.opam | 2 +- src/data/CCFun_vec.ml | 2 +- src/data/CCFun_vec.mli | 3 +- tests/data/t_fun_vec.ml | 174 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 178 insertions(+), 3 deletions(-) diff --git a/containers-data.opam b/containers-data.opam index 241fad92..815665fd 100644 --- a/containers-data.opam +++ b/containers-data.opam @@ -14,7 +14,7 @@ depends: [ "dune" { >= "2.0" } "containers" { = version } "seq" - (("ocaml" {with-test & < "4.08"} & "qcheck-core" {>= "0.17" & with-test}) + (("ocaml" {with-test & < "4.08"} & "qcheck-core" {>= "0.20" & with-test}) | ("ocaml" {with-test & >= "4.08"} & "qcheck-core" {>= "0.18" & with-test})) "iter" { with-test } "gen" { with-test } diff --git a/src/data/CCFun_vec.ml b/src/data/CCFun_vec.ml index 5a9b980a..54148133 100644 --- a/src/data/CCFun_vec.ml +++ b/src/data/CCFun_vec.ml @@ -213,7 +213,7 @@ let pop_ i (m : 'a t) : 'a * 'a t = aux (split_idx i) m let pop_exn (v : 'a t) : 'a * 'a t = - if v.size = 0 then failwith "Fun_vec.pop_exn"; + if v.size = 0 then invalid_arg "Fun_vec.pop_exn"; pop_ (v.size - 1) v let pop (v : 'a t) : ('a * 'a t) option = diff --git a/src/data/CCFun_vec.mli b/src/data/CCFun_vec.mli index 5821fc72..06ce752f 100644 --- a/src/data/CCFun_vec.mli +++ b/src/data/CCFun_vec.mli @@ -67,7 +67,8 @@ val get_exn : int -> 'a t -> 'a (** @raise Not_found if key not present. *) val pop_exn : 'a t -> 'a * 'a t -(** Pop last element. *) +(** Pop last element. + @raise Invalid_argument in case the vec is empty. *) val pop : 'a t -> ('a * 'a t) option (** Pop last element. diff --git a/tests/data/t_fun_vec.ml b/tests/data/t_fun_vec.ml index 803d1e93..cd5d181b 100644 --- a/tests/data/t_fun_vec.ml +++ b/tests/data/t_fun_vec.ml @@ -2,6 +2,8 @@ module Test = (val Containers_testlib.make ~__FILE__ ()) open Test open CCFun_vec +let spf = Printf.sprintf + let _listuniq = let g = Q.(small_list (pair small_int small_int)) in Q.map_same_type @@ -70,3 +72,175 @@ q _listuniq (fun l -> t @@ fun () -> choose empty = None;; t @@ fun () -> choose (of_list [ 1, 1; 2, 2 ]) <> None + +module Ref_impl = struct + type +'a t = 'a list + + let empty : _ t = [] + let length = List.length + let push x l : _ t = l @ [ x ] + let get i l = List.nth l i + let to_list l = l + let to_gen = Gen.of_list + let add_list l l2 : _ t = List.append l l2 + + let pop_exn l = + match List.rev l with + | x :: tl -> x, List.rev tl + | [] -> invalid_arg "empty" + + let is_empty l = l = [] + + let choose l = + match l with + | [] -> None + | x :: _ -> Some x +end + +module Op = struct + type 'a t = + | Push of 'a + | Pop + (* TODO: set *) + | Add_list of 'a list + | Check_get of int + | Check_choose + | Check_is_empty + | Check_len + | Check_to_list + | Check_to_gen + + let well_formed ops : bool = + let rec loop size = function + | [] -> true + | Push _ :: tl -> loop (size + 1) tl + | Pop :: tl -> size >= 0 && loop (size - 1) tl + | Add_list l :: tl -> loop (size + List.length l) tl + | Check_get x :: tl -> x < size && loop size tl + | Check_choose :: tl + | Check_is_empty :: tl + | Check_len :: tl + | Check_to_list :: tl + | Check_to_gen :: tl -> + loop size tl + in + loop 0 ops + + let show show_x (self : _ t) : string = + match self with + | Push x -> spf "push %s" (show_x x) + | Pop -> "pop" + | Add_list l -> spf "add_list [%s]" (String.concat ";" @@ List.map show_x l) + | Check_get i -> spf "check_get %d" i + | Check_choose -> "check_choose" + | Check_is_empty -> "check_is_empty" + | Check_len -> "check_len" + | Check_to_list -> "check_to_list" + | Check_to_gen -> "check_to_gen" + + let shrink shrink_x (op : _ t) : _ Q.Iter.t = + let open Q.Shrink in + let open Q.Iter in + match op with + | Push x -> shrink_x x >|= fun x -> Push x + | Pop -> empty + | Add_list l -> list ~shrink:shrink_x l >|= fun x -> Add_list x + | Check_get _ | Check_choose | Check_is_empty | Check_len | Check_to_list + | Check_to_gen -> + empty + + let shrink_l shrink_x : _ t list Q.Shrink.t = + Q.Shrink.list ~shrink:(shrink shrink_x) |> Q.Shrink.filter well_formed + + type 'a op = 'a t + + (* generate list of length [n] *) + let gen (gen_x : 'a Q.Gen.t) n : 'a t list Q.Gen.t = + let open Q.Gen in + let rec loop size n : 'a op list Q.Gen.t = + if n = 0 then + return [] + else ( + let op = + frequency + @@ List.flatten + [ + [ + (3, gen_x >|= fun x -> Push x, size + 1); + 1, return (Check_choose, size); + 1, return (Check_is_empty, size); + 1, return (Check_to_list, size); + 1, return (Check_to_gen, size); + ]; + (if size > 0 then + [ + 1, return (Pop, size - 1); + (1, 0 -- (size - 1) >|= fun x -> Check_get x, size); + ] + else + []); + [ + ( 1, + small_list gen_x >|= fun l -> + Add_list l, size + List.length l ); + ]; + ] + in + + op >>= fun (op, size) -> + loop size (n - 1) >>= fun tl -> return (op :: tl) + ) + in + loop 0 n +end + +let arb_ops_int : int Op.t list Q.arbitrary = + Q.make + ~print:(fun o -> + spf "[%s]" @@ String.concat ";" @@ List.map (Op.show @@ spf "%d") o) + ~shrink:(Op.shrink_l Q.Shrink.int) + Q.Gen.(0 -- 40 >>= fun len -> Op.gen small_int len) + +let check_ops ~show_x (ops : 'a Op.t list) : unit = + let fail () = + Q.Test.fail_reportf "on list [%s]" + (String.concat ";" @@ List.map (Op.show show_x) ops) + in + let cur = ref empty in + let cur_ref = ref Ref_impl.empty in + List.iter + (fun (op : _ Op.t) -> + match op with + | Op.Push x -> + cur := push x !cur; + cur_ref := Ref_impl.push x !cur_ref + | Op.Pop -> + let x1, cur' = pop_exn !cur in + cur := cur'; + let x2, cur_ref' = Ref_impl.pop_exn !cur_ref in + cur_ref := cur_ref'; + if x1 <> x2 then fail () + | Op.Add_list l -> + cur := add_list !cur l; + cur_ref := Ref_impl.add_list !cur_ref l + | Op.Check_get i -> + if get_exn i !cur <> Ref_impl.get i !cur_ref then fail () + | Op.Check_is_empty -> + if is_empty !cur <> Ref_impl.is_empty !cur_ref then fail () + | Op.Check_len -> if length !cur <> Ref_impl.length !cur_ref then fail () + | Op.Check_to_list -> + if to_list !cur <> Ref_impl.to_list !cur_ref then fail () + | Op.Check_choose -> + if choose !cur <> Ref_impl.choose !cur_ref then fail () + | Op.Check_to_gen -> + if + to_gen !cur |> Gen.to_list <> (Ref_impl.to_gen !cur_ref |> Gen.to_list) + then + fail ()) + ops; + () + +let () = + q arb_ops_int (fun ops -> + check_ops ~show_x:(spf "%d") ops; + true)