Merge pull request #517 from ocaml-multicore/lin-dynarray-tweaks

Lin Dynarray tweaks + add `Lin.{seq_small, array_small, list_small}`

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
 

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

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. *)
 

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);