From 8744efaeedc1956948cc4aa2fa9534ecb054346a Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 Jan 2025 14:18:28 +0100 Subject: [PATCH 1/5] Add Lin.seq_small combinator --- lib/lin.ml | 14 ++++++++++---- lib/lin.mli | 5 +++++ 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/lib/lin.ml b/lib/lin.ml index 4285b14ac..079f30788 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -210,11 +210,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 +226,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..ecb304e3d 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -218,6 +218,11 @@ val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty 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. *) From 29f63e29462ada7a997cad5994a6808feb56966b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 Jan 2025 14:19:22 +0100 Subject: [PATCH 2/5] Use new Lin.seq_small combinator in Lin Dynarray test --- src/dynarray/lin_tests.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From 27476156b7879e0cd80d1d2ebe2f9135d599ecd3 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 Jan 2025 14:23:47 +0100 Subject: [PATCH 3/5] Add Lin.array_small combinator --- lib/lin.ml | 6 ++++++ lib/lin.mli | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/lib/lin.ml b/lib/lin.ml index 079f30788..3db33b5e7 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -197,6 +197,12 @@ let array : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable) | 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 () diff --git a/lib/lin.mli b/lib/lin.mli index ecb304e3d..31c442e92 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -213,6 +213,12 @@ val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty 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} From c0d360da2289bd87703763e0d834c3bc5fc8f368 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 Jan 2025 14:29:38 +0100 Subject: [PATCH 4/5] Add Lin.list_small combinator --- lib/lin.ml | 6 ++++++ lib/lin.mli | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/lib/lin.ml b/lib/lin.ml index 3db33b5e7..aa68e58cb 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -191,6 +191,12 @@ 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) diff --git a/lib/lin.mli b/lib/lin.mli index 31c442e92..47f91ac6b 100644 --- a/lib/lin.mli +++ b/lib/lin.mli @@ -207,6 +207,12 @@ 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} From acbbedc72b4cb2e3255a492b56f8db55dfb6055a Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 15 Jan 2025 16:53:45 +0100 Subject: [PATCH 5/5] Add a CHANGES entry --- CHANGES.md | 1 + 1 file changed, 1 insertion(+) 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