Add function generation support

[jmid]

This (draft) PR add function generation, fixing #270

The core commit is 7a9df34 describing the change as:
- building a generator with QCheck.fun1-4 of arbitrary.t type
that takes Observables and an arbitrary.t result
and finally selecting its .gen field to get a resulting Gen.t
- quantifying arbitrary.t generators with QCheck to not pick up Gen.t ones
- emitting the special (_ -> _) fun_ type for an arrow type
- invoking functions f with QCheck.Fn.apply f in both run_cmd and next_state
- validating the fragment of functions we support, i.e., second-order and arity<=4

The PR is good enough shape to share and get feedback on at this point, since I'm starting to hit issues that are getting further from function generation itself.

One remaining issue is warnings about incomplete computations, which shows up in two places, despite both representing a complete model computation, that just happens to involve a function AFAICS:

+File "all_warnings.mli", line 39, characters 0-89:
+39 | val functional_argument : ('a -> bool) -> 'a t -> bool
+40 | (*@ b = functional_argument p t *)
+Warning: Incomplete computation of the returned value in the specification of functional_argument. Failure message won't be able to display the expected returned value.

and

-File "example_limitations.mli", line 23, characters 15-25:
+File "example_limitations.mli", line 23, characters 0-65:
 23 | val for_all : ('a -> bool) -> 'a t -> bool
-                    ^^^^^^^^^^
-Warning: Skipping for_all: functions are not supported yet as arguments.
+24 | (*@ b = for_all p t *)
+Warning: Incomplete computation of the returned value in the specification of for_all. Failure message won't be able to display the expected returned value.

Another issue which took some time to diagnose is a mixture of List and Sequence in the hashtbl specification.
In filter_map_inplace Ortac fails to parse the specification correctly, which results in next_state modeling a state change, despite the modifies h specification.
The issue is that h.contents = Sequence.filter_map is parsed as

TApp ( "infix =", [ TApp ( "Sequence.of_list", [...] ),  ... ] )

i.e., with nested applications on the left-hand-side of the equality sign =.

Commit 2d0ce5a adds a fix attempt for it, which makes Ortac output a next_state function honoring the modify h clause, however the produced code then fails to type-check because of the mixture of List and Sequence:

$ git checkout 2d0ce5a
$ dune build @launchtests plugins/qcheck-stm/
File "plugins/qcheck-stm/test/hashtbl_stm_tests.ml", lines 389-395, characters 21-46:
389 | .....................Ortac_runtime.Gospelstdlib.Sequence.filter_map
390 |                        (fun (x_1, y) ->
391 |                           match QCheck.Fn.apply f x_1 y with
392 |                           | None -> None
393 |                           | Some b' -> Some (x_1, b'))
394 |                        (Ortac_runtime.Gospelstdlib.List.to_seq
395 |                           h_10__028_.contents)
Error: This expression has type
         (char * int) Ortac_runtime.Gospelstdlib.sequence
       but an expression was expected of type (char * int) list
random seed: 380065948                           
generated error fail pass / total     time test name
[✓] 1000    0    0 1000 / 1000     0.1s Test_cleanup STM tests (generating)
================================================================================
success (ran 1 tests)
random seed: 66238626                            
generated error fail pass / total     time test name
[✓] 1000    0    0 1000 / 1000     0.1s Sequence_model STM tests (generating)
================================================================================
[...]

As an illustration,the last two commits 63109c8 and 93ea93a adds a quick-and-dirty List.filter_map to the runtime and
adjusts the hashtbl specification to use Lists exclusively, which is sufficient to make dune build @launchtests plugins/qcheck-stm/ pass.

These commits only serve as an illustration and should of course be dropped. I seem to recall something about List being removed from the Stdlib revision, which may also help solve this problem.

[jmid]

Oh, I forgot: The PR requires qcheck-multicoretests-util from ocaml-multicore/multicoretests#486 which has been merged to main, but not released on opam yet.

[jmid]

As part of the yak-shaving that this PR triggered, I've opened 2 QCheck PRs: c-cube/qcheck#296 and c-cube/qcheck#297 which will help printing nicer counterexample functions involving chars and strings. Feel free to chip in on which QCheck.Print behaviour you prefer... 🙏 🙂

[jmid]

Just an quick update:

With the following patch, inserting a manual List coercion as we discussed off-line, dune build @launchtests passes without 2d0ce5a (and 63109c8 and 93ea93a):

diff --git a/plugins/qcheck-stm/test/hashtbl.mli b/plugins/qcheck-stm/test/hashtbl.mli
index 8b10a51..45525ae 100644
--- a/plugins/qcheck-stm/test/hashtbl.mli
+++ b/plugins/qcheck-stm/test/hashtbl.mli
@@ -64,11 +64,11 @@ val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
 val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit
 (*@ filter_map_inplace f h
     modifies h
-    ensures h.contents = Sequence.filter_map
+    ensures h.contents = List.of_seq (Sequence.filter_map
                             (fun (x,y) -> match f x y with
                                           | None -> None
                                           | Some b' -> Some (x, b'))
-                            (old h.contents) *)
+                            (old h.contents)) *)
 
 val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
 val length : ('a, 'b) t -> int

[n-osborne]

Excellent!
I'm confident the new Gospel standard library will soon be merged, so we should rewrite those tests using sequences anyway as it won't contain a List module anymore.

[jmid]

I've just removed REMOVE ME commits 63109c8 and 93ea93a again.

Looking more at the first errors described above, e.g., in all_warnings.mli:

val functional_argument : ('a -> bool) -> 'a t -> bool
(*@ b = functional_argument p t *)

I realize now that this is a genuine warning, because it is missing an ensures clause describing what value of b is expected. The for_all warning from example_limitations happens for the same reason.

I've thus updated plugins/qcheck-stm/test/function_args.mli with tests of the arity-warning and function order,
which revealed a problem with the arity-check, so I enclude a fix for it.

I've also updated all_warnings.mli with these two new warnings, and updated example_limitations - and plugins/qcheck-stm/doc/index.mld accordingly.

[n-osborne]

Oh, I forgot: The PR requires qcheck-multicoretests-util from ocaml-multicore/multicoretests#486 which has been merged to main, but not released on opam yet.

In the meantime, I'm ok to pin the right version so that CI has a bit more meaning.

As opam files are generated, the pin should be added in a ortac-qcheck-stm.opam.template file.

[jmid]

OK. I've rebased on main following the merge of #279.
I've also dropped commit 2d0ce5a FIXME: Handle nested TApp case with inserted to_seq in get_state_desc…
With these two changes dune runtest plugins/qcheck-stm/ and dune build @launchtests are all green for me... 🤞

[n-osborne]

Thanks again for this nice PR. This is a really good enhancement of Ortac/QCheck-STM!

Maybe it would be cleaner to run ocamlformat on each of the commits rather than at the end with a separate one?

Regarding the new error constructors in Reserr:

• Type_not_supported_in_function_argument could be made more specific as it is only used to avoid third-order functions (e.g. Third_order_function_argument)
• At some point in the past we've (lexicographically) ordered the constructors in Reserr. Could you add them so that the order is preserved?

Now a more in-depth remark: In Stm_of_ir.subst_core_type you can get rid of the insert_prefix extra-argument.

This argument is only set to false in pp_ortac_cmd_case to build a type that is then fed to pp_of_ty that will run munge_longident to get rid of the qualification in the identifier. In the current state, this wouldn't work because you are building the qualified name using lident directly which build Lident "QCheck.fun_", and munge_longident can't do its job. But if you build Ldot (Lident "QCheck", "fun_"), then you don't need to rely on insert_prefix flag.

I've pushed a way to do it on the fun-gen-review branch on my repo.

Two last small remarks:

There are some leftovers next to Stm_of_ir.prefix_identifier definition.

I would have written the checks in Ir_of_gospel.no_third_order_arg_or_big_typle in a more monadic way, but the code is already pretty clear and easy to follow as it is, so no need to change :-)

[jmid]

Thanks for the review Nicolas!

Maybe it would be cleaner to run ocamlformat on each of the commits rather than at the end with a separate one?

Good idea, I've now done so using git rebase -i origin/main --exec "dune fmt"

Regarding the new error constructors in Reserr:

• Type_not_supported_in_function_argument could be made more specific as it is only used to avoid third-order functions (e.g. Third_order_function_argument)
• At some point in the past we've (lexicographically) ordered the constructors in Reserr. Could you add them so that the order is preserved?

Ah, of course. I've restored order to the contructor names in the type declaration in 0b8f9cf.
I then started doing something similar for the cases in the following functions in db85fbb, but realized that some existing ones were already out of order (e.g., listing Sut_as_type_inst and Sut_in_tuple under errors even though they are warnings). I therefore decided this was a digression and stopped.

Now a more in-depth remark: In Stm_of_ir.subst_core_type you can get rid of the insert_prefix extra-argument.

This argument is only set to false in pp_ortac_cmd_case to build a type that is then fed to pp_of_ty that will run munge_longident to get rid of the qualification in the identifier. In the current state, this wouldn't work because you are building the qualified name using lident directly which build Lident "QCheck.fun_", and munge_longident can't do its job. But if you build Ldot (Lident "QCheck", "fun_"), then you don't need to rely on insert_prefix flag.

I've pushed a way to do it on the fun-gen-review branch on my repo.

Ah great. Thanks - I've merged your commit 👍

Two last small remarks:

There are some leftovers next to Stm_of_ir.prefix_identifier definition.

Oops, sorry. Fixed in 4ab0701

I would have written the checks in Ir_of_gospel.no_third_order_arg_or_big_typle in a more monadic way, but the code is already pretty clear and easy to follow as it is, so no need to change :-)

I started writing these in monadic style, but then realized that the check-functions could be pure, and thus ended up with the current version, that calls the pure ones from the monadic-error-merging code 🤷

Let me know how much squashing you want me to do...
...actually, it would probably be good to wait with merging until we can get rid of 9777563 🤔

[n-osborne]

Excellent! Thank you!

Let me know how much squashing you want me to do...

I would say if it is not too much hassle, it would be cleaner to have every commit after the Changelog update (54a21d3) squashed at the appropriate place.

...actually, it would probably be good to wait with merging until we can get rid of 9777563 🤔

I agree, let's do releases in the right order :-)

[jmid]

I would say if it is not too much hassle, it would be cleaner to have every commit after the Changelog update (54a21d3) squashed at the appropriate place.

Ack!

...actually, it would probably be good to wait with merging until we can get rid of 9777563 🤔

I agree, let's do releases in the right order :-)

Things are falling into place: After rolling qcheck.0.23 I've rolled ocaml/opam-repository#27114
which should allow us to do that. I'm now just waiting for the change to propagate to the ocaml.org opam-repo mirror 🚀

[jmid]

I would say if it is not too much hassle, it would be cleaner to have every commit after the Changelog update (54a21d3) squashed at the appropriate place.

I've now done so (and learning some nice features of git rebase in the process...) 😃

...actually, it would probably be good to wait with merging until we can get rid of 9777563 🤔

I agree, let's do releases in the right order :-)

0.5 is now available fromthe caml.org opam-repo mirror, so I've added an initial commit 104c2e8 bumping the required version, and dropped the pin commit.

If the CI is green (tests are green locally), I believe this should be good to go.

[n-osborne]

Excellent!
I'm merging now 🚀

Thanks again for this nice PR 😃