Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 5 commits into from
Jan 15, 2025
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8744efa
Add Lin.seq_small combinator
jmid Jan 15, 2025
29f63e2
Use new Lin.seq_small combinator in Lin Dynarray test
jmid Jan 15, 2025
2747615
Add Lin.array_small combinator
jmid Jan 15, 2025
c0d360d
Add Lin.list_small combinator
jmid Jan 15, 2025
acbbedc
Add a CHANGES entry
jmid Jan 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
26 changes: 22 additions & 4 deletions lib/lin.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()

Expand All @@ -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 =
Expand All @@ -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
Expand Down
17 changes: 17 additions & 0 deletions lib/lin.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)

Expand Down
2 changes: 1 addition & 1 deletion src/dynarray/lin_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
Loading