I have had several times to generate dependent pairs in my property checks: for instance, pairs formed of an array and a valid index.
To do that, I used the function
let dep_pair a f = a >>= fun x -> tup2 (pure x) (f x)
(where QGheck2.Gen is open), rather than first generating all pairs and then discarding the unwanted ones using assume.
The above example can then be obtained with:
let array_index =
dep_pair
(array_size (int_range 1 100) nat_small)
(fun t -> int_bound (pred (Array.length t)))
My use cases included more complex pairs of structures bound by relations, but I think the above example shows the basic idea.
A function like dep_pair may be worth adding to QCheck2.Gen.
I have had several times to generate dependent pairs in my property checks: for instance, pairs formed of an array and a valid index.
To do that, I used the function
(where
QGheck2.Genis open), rather than first generating all pairs and then discarding the unwanted ones usingassume.The above example can then be obtained with:
My use cases included more complex pairs of structures bound by relations, but I think the above example shows the basic idea.
A function like
dep_pairmay be worth adding toQCheck2.Gen.