qcheck icon indicating copy to clipboard operation
qcheck copied to clipboard

Add range_subset, pos_split2, nat_split2, pos_split, nat_split to QCheck2

Open jmid opened this issue 3 years ago • 0 comments

When trying to align the QCheck and QCheck2 expect test suites I noticed a couple of missing tests in QCheck2.

It would be nice to add to QCheck2 the convenience generators from #114

  • range_subset
  • pos_split2
  • nat_split2
  • pos_split
  • nat_split

For a start, here are expect tests translated from QCheck (until I noticed the Check2 generators were missing... 😅):

  let nat_split2_spec =
    Test.make ~name:"nat_split2 spec"
      ~print:Print.(pair int (pair int int))
      Gen.(small_nat >>= fun n -> pair (return n) (nat_split2 n))
      (fun (n, (a, b)) ->
         0 <= a && 0 <= b && a + b = n)

  let pos_split2_spec =
    Test.make ~name:"pos_split2 spec"
      ~print:Print.(pair int (pair int int))
      Gen.(small_nat >>= fun n ->
           (* we need n > 2 *)
           let n = n + 2 in
           pair (return n) (pos_split2 n))
      (fun (n, (a, b)) ->
         (0 < a && 0 < b && a + b = n))

  let range_subset_spec =
    Test.make ~name:"range_subset_spec"
      ~print:Print.(quad int int int (array int))
      Gen.(pair small_nat small_nat >>= fun (m, n) ->
           (* we must guarantee [low <= high]
                 and [size <= high - low + 1] *)
           let low = m and high = m + n in
           int_range 0 (high - low + 1) >>= fun size ->
           quad (return size) (return low) (return high)
             (range_subset ~size low high))
      (fun (size, low, high, arr) ->
         if size = 0 then arr = [||]
         else
           Array.length arr = size
           && low <= arr.(0)
           && Array.for_all (fun (a, b) -> a < b)
               (Array.init (size - 1) (fun k -> arr.(k), arr.(k+1)))
           && arr.(size - 1) <= high)

  let nat_split_n_way =
    Test.make ~name:"nat_split n-way"
      ~print:Print.(pair int (array int))
      Gen.(small_nat >>= fun n ->
           pair (return n) (nat_split ~size:n n))
      (fun (n, arr) ->
         Array.length arr = n
         && Array.for_all (fun k -> 0 <= k) arr
         && Array.fold_left (+) 0 arr = n)

  let nat_split_smaller =
    Test.make ~name:"nat_split smaller"
      ~print:Print.(triple int int (array int))
      Gen.(small_nat >>= fun size ->
           int_bound size >>= fun n ->
           triple (return size) (return n) (nat_split ~size n))
      (fun (m, n, arr) ->
         Array.length arr = m
         && Array.for_all (fun k -> 0 <= k) arr
         && Array.fold_left (+) 0 arr = n)

  let pos_split =
    Test.make ~name:"pos_split"
      ~print:Print.(triple int int (array int))
      Gen.(pair small_nat small_nat >>= fun (m, n) ->
           (* we need both size>0 and n>0 and size <= n *)
           let size = 1 + min m n and n = 1 + max m n in
           triple (return size) (return n) (pos_split ~size n))
      (fun (m, n, arr) ->
         Array.length arr = m
         && Array.for_all (fun k -> 0 < k) arr
         && Array.fold_left (+) 0 arr = n)

jmid avatar Apr 19 '22 09:04 jmid