Add/Move to a module-based configuration

[n-osborne]

I open this issue to keep track of our thoughts about a module-based configuration for ortac qcheck-stm.

In the current version, the command-line is asking for:

1. the name of the specified interface file
2. the value to evaluate for init_sut
3. the type (and how to instantiate type parameters if there is any) of the system under test

There is a first choice to make: whether to put 2. and 3. in the configuration module. I'm thinking something like:

let init_sut = Array.make 16 'a'
type sut = char array

We'll then have to parse the module in order to retrieve the information as we also use them for the value init_state and the type state.

One thing that would be facilitated is the process of extending the STM.ty type. In the current version, the user has to edit the generated file (which seems incompatible with an integration in a dune workflow). With a module-based configuration, the user could just write the type extension in the module and we'll inject them in the generated file.

Once we have a configuration module, it is easy to add some (optional) extra configuration like the values for count and name with which to run the STM tests.

[n-osborne]

(Discussed offline with @shym)

The configuration module could contain an implementation of init_state for the cases where it is not possible to generate it from the specifications. We should have a clear idea of some use cases though.

[n-osborne]

More thoughs about what the configuration module should look like.

The idea i snow to completely get rid of passing information other than this module's name through the command-line: that way, any future change of the API will be transparent to the dune rules. User will be able to upgrade their ortac without having to rewrite dune rules (amending the configuration modules is necessary though). Flags like the --quiet one should still be provided on the command-line though, same for output filename I believe.

The user may want to provide multiple configuration modules (testing with different instanciation of the type parameters).

We could imagine a user interface like:

$ ortac qcheck-stm module_under_test.mli configuration_module.ml

What kind of information the configuration should contain?

A good start would be (the equivalent of the information we can give Ortac/QCheckSTM today)

1. an init_sut value
2. the sut type, with proper instanciation of the type parameters
3. pp_* values, QCheck generators and STM.ty type extension and functional constructor for custom types introduced by the module under test

Now there is the question of the organisation of the configuration module. For now, we give the information for [3] in the included module like that (taken from examples/varray_incl.ml):

module Util = struct
  module Pp = struct
    include Util.Pp

    let pp_elt pp = pp
  end
end

module QCheck = struct
  include QCheck

  module Gen = struct
    include QCheck.Gen

    let int = small_signed_int
    let elt gen = gen
  end
end

open STM
open Varray_spec

type _ ty += Elt : 'a ty -> 'a elt ty

let elt spec =
  let ty, show = spec in
  (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x))

This is a bit heavy with all the nested modules. I believe we can have something slightly lighter as we know that the Pp module should end up in the Util one and the Gen in the QCheck one.

I would be comfortable proposing something like:

open Module_under_test
type sut = int t
let init_sut = create ()
(* for now, let's keep the constraint that `init_sut` is a function call so
that we can look up this function's specification to build `init_state` *)

module Pp = struct
  (* define here your custom printers *)
end

module Gen = struct
  (* define here your custom generators *)
end

module Ty = struct
(* type extension and functional `ty` constructors *)
end