Commit 50d60654 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Fuzz [P.to_seq] and [E.to_seq] as affine sequences. (A more complete test.)

parent b2c93696
......@@ -149,6 +149,9 @@ let length =
let list spec =
list ~length:max_length spec
let aseq_element =
declare_affine_seq ~length:max_length element
(* -------------------------------------------------------------------------- *)
(* A fixed default element. *)
......@@ -466,13 +469,14 @@ let () =
if testing EToArray then
declare "E.to_array" spec R.E.to_array C.E.to_array;
(* TODO harness_to_seq immediately converts the sequence to a list, so does
not verify that sequence is persistent, and does not verify that sequence
remains valid as long as the underlying sequence is not modified *)
let spec = direction ^> esek ^> list element in
(* [to_seq] is expected to produce an affine sequence. This sequence remains
valid as long as the underlying sequence is not modified. This is not
visible in the specification below, but an attempt to use this sequence
after it has been become invalid is detected by [R.E.to_seq], which then
raises [Monolith.PleaseBackOff]. *)
let spec = direction ^> esek ^> aseq_element in
if testing EToSeq then
declare "harness_to_seq E.to_seq" spec
(harness_to_seq R.E.to_seq) (harness_to_seq C.E.to_seq);
declare "E.to_seq" spec R.E.to_seq C.E.to_seq;
let spec_of_list_segment =
rot3 (list element ^>> fun xs -> default ^> le (List.length xs) ^> esek)
......@@ -776,10 +780,10 @@ let () =
if testing PToArray then
declare "P.to_array" spec R.P.to_array C.P.to_array;
let spec = direction ^> psek ^> list element in
(* [to_seq] is expected to produce an affine sequence. *)
let spec = direction ^> psek ^> aseq_element in
if testing PToSeq then
declare "harness_to_seq P.to_seq" spec
(harness_to_seq R.P.to_seq) (harness_to_seq C.P.to_seq);
declare "P.to_seq" spec R.P.to_seq C.P.to_seq;
let spec_of_list_segment =
rot3 (list element ^>> fun xs -> default ^> le (List.length xs) ^> psek)
......
......@@ -110,9 +110,6 @@ let harness_iteri iteri direction s =
iteri direction (fun i x -> accu := (i, x) :: !accu) s;
List.rev !accu
let harness_to_seq to_seq direction s =
List.of_seq (to_seq direction s)
let harness_of_seq_segment of_seq_segment default n xs =
let xs = once (List.to_seq xs) in
of_seq_segment default n xs
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment