diff --git a/CHANGES.md b/CHANGES.md index db30ac429..3b1d9faf2 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,6 +4,7 @@ - #509: Change/Fix to use a symmetric barrier to synchronize domains - #511: Introduce extended specs to allow wrapping command sequences +- #517: Add `Lin` combinators `seq_small`, `array_small`, and `list_small` ## 0.6 diff --git a/lib/lin.ml b/lib/lin.ml index 4285b14ac..aa68e58cb 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -191,12 +191,24 @@ let list : type a c s. (a, c, s, combinable) ty -> (a list, c, s, combinable) ty | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.list arb, QCheck.Print.list print, List.equal eq) | Deconstr (print, eq) -> Deconstr (QCheck.Print.list print, List.equal eq) +let list_small : type a c s. (a, c, s, combinable) ty -> (a list, c, s, combinable) ty = + fun ty -> match ty with + | Gen (arb, print) -> Gen (QCheck.small_list arb, QCheck.Print.list print) + | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.small_list arb, QCheck.Print.list print, List.equal eq) + | Deconstr (print, eq) -> Deconstr (QCheck.Print.list print, List.equal eq) + let array : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable) ty = fun ty -> match ty with | Gen (arb, print) -> Gen (QCheck.array arb, QCheck.Print.array print) | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.array arb, QCheck.Print.array print, Array.for_all2 eq) | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq) +let array_small : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable) ty = + fun ty -> match ty with + | Gen (arb, print) -> Gen (QCheck.array_of_size QCheck.Gen.small_nat arb, QCheck.Print.array print) + | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.array_of_size QCheck.Gen.small_nat arb, QCheck.Print.array print, Array.for_all2 eq) + | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq) + let seq_iteri f s = let (_:int) = Seq.fold_left (fun i x -> f i x; i + 1) 0 s in () @@ -210,11 +222,11 @@ let print_seq pp s = Buffer.add_char b '>'; Buffer.contents b -let arb_seq a = +let arb_seq size_gen a = let open QCheck in let print = match a.print with None -> None | Some ap -> Some (print_seq ap) in let shrink s = Iter.map List.to_seq (Shrink.list ?shrink:a.shrink (List.of_seq s)) in - let gen = Gen.map List.to_seq (Gen.list a.gen) in + let gen = Gen.map List.to_seq (Gen.list_size size_gen a.gen) in QCheck.make ?print ~shrink gen let rec seq_equal eq s1 s2 = @@ -226,8 +238,14 @@ let rec seq_equal eq s1 s2 = let seq : type a c s. (a, c, s, combinable) ty -> (a Seq.t, c, s, combinable) ty = fun ty -> match ty with - | Gen (arb, print) -> Gen (arb_seq arb, print_seq print) - | GenDeconstr (arb, print, eq) -> GenDeconstr (arb_seq arb, print_seq print, seq_equal eq) + | Gen (arb, print) -> Gen (arb_seq QCheck.Gen.nat arb, print_seq print) + | GenDeconstr (arb, print, eq) -> GenDeconstr (arb_seq QCheck.Gen.nat arb, print_seq print, seq_equal eq) + | Deconstr (print, eq) -> Deconstr (print_seq print, seq_equal eq) + +let seq_small : type a c s. (a, c, s, combinable) ty -> (a Seq.t, c, s, combinable) ty = + fun ty -> match ty with + | Gen (arb, print) -> Gen (arb_seq QCheck.Gen.small_nat arb, print_seq print) + | GenDeconstr (arb, print, eq) -> GenDeconstr (arb_seq QCheck.Gen.small_nat arb, print_seq print, seq_equal eq) | Deconstr (print, eq) -> Deconstr (print_seq print, seq_equal eq) let state = State diff --git a/lib/lin.mli b/lib/lin.mli index a22288116..47f91ac6b 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -207,17 +207,34 @@ val list : ('a, 'c, 's, combinable) ty -> ('a list, 'c, 's, combinable) ty and have their elements generated by the [t] combinator. It is based on {!QCheck.list}. *) +val list_small : ('a, 'c, 's, combinable) ty -> ('a list, 'c, 's, combinable) ty +(** The [list_small] combinator represents the {{!Stdlib.List.t}[list]} type. + The generated lists from [list_small t] have a length resulting from {!QCheck.Gen.small_nat} + and have their elements generated by the [t] combinator. + It is based on {!QCheck.small_list}. *) + val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty (** The [array] combinator represents the {{!Stdlib.Array.t}[array]} type. The generated arrays from [array t] have a length resulting from {!QCheck.Gen.nat} and have their elements generated by the [t] combinator. It is based on {!QCheck.array}. *) +val array_small : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty +(** The [array_small] combinator represents the {{!Stdlib.Array.t}[array]} type. + The generated arrays from [array_small t] have a length resulting from {!QCheck.Gen.small_nat} + and have their elements generated by the [t] combinator. + It is based on {!QCheck.array_of_size}. *) + val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty (** The [seq] combinator represents the {!Stdlib.Seq.t} type. The generated sequences from [seq t] have a length resulting from {!QCheck.Gen.nat} and have their elements generated by the [t] combinator. *) +val seq_small : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty +(** The [seq_small] combinator represents the {!Stdlib.Seq.t} type. + The generated sequences from [seq_small t] have a length resulting from {!QCheck.Gen.small_nat} + and have their elements generated by the [t] combinator. *) + val t : ('a, constructible, 'a, noncombinable) ty (** The [t] combinator represents the type {!Spec.t} of the system under test. *) diff --git a/src/dynarray/lin_tests.ml b/src/dynarray/lin_tests.ml index 69d5d1940..33680a0b1 100644 --- a/src/dynarray/lin_tests.ml +++ b/src/dynarray/lin_tests.ml @@ -18,7 +18,7 @@ module Dynarray_api = struct val_ "set" Dynarray.set (t @-> int @-> elem @-> returning_or_exc unit); val_ "length" Dynarray.length (t @-> returning int); val_freq 3 "add_last" Dynarray.add_last (t @-> elem @-> returning_or_exc unit); - val_ "append_seq" Dynarray.append_seq (t @-> seq elem @-> returning_or_exc unit); + val_ "append_seq" Dynarray.append_seq (t @-> seq_small elem @-> returning_or_exc unit); val_ "get_last" Dynarray.get_last (t @-> returning_or_exc elem); val_ "pop_last" Dynarray.pop_last (t @-> returning_or_exc elem); val_freq 2 "remove_last" Dynarray.remove_last (t @-> returning_or_exc unit);