Move to a module based configuration

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Move to a module-based configuration
+  [\#214](https://github.com/ocaml-gospel/ortac/pull/214)
 - Add support for custom ghost types as model
   [\#228](https://github.com/ocaml-gospel/ortac/pull/228)
 

examples/README.md

@@ -28,9 +28,8 @@ need to be visible.
 The STM `postcond` function pattern match on the returned value encapsulated in
 a `STM.ty`. As functions `add_l` and `add_r` both return the node that has been
 added, we need to extend the `STM.ty` type with an encoding for
-`Lwt_dllist.node`. We add this extension in the external module
-`Lwt_dllist_incl` and pass it to the `--include` option of the `ortac
-qcheck-stm` command.
+`Lwt_dllist.node`. We add this extension in the configuration module for
+Ortac/QCheckSTM.
 
 The generated code can be found in `lwt_dllist_tests.ml`. You can run the test
 either with `dune runtest examples/` or by directly running the compiled
@@ -40,7 +39,7 @@ Dune rules have been generated using the `dune-rules` plugin, providing the
 `dune` subcommand:
 
 ```sh
-$ ortac dune qcheck-stm lwt_dllist_spec "create ()" "int t" lwt_dllist_tests --include=lwt_dllist_incl --package=ortac-examples --with-stdout-to=dune.lwt_dllist.inc
+$ ortac dune qcheck-stm lwt_dllist_spec.mli lwt_dllist_config.ml lwt_dllist_tests.ml --package=ortac-examples --with-stdout-to=dune.lwt_dllist.inc
 ```
 
 ## `varray` library
@@ -62,8 +61,8 @@ dune-generated `mli` files hidden in the `_build` folder.
 Here again, as for the previous example, we need to include some code. That is
 the extension of the `STM.ty` type. But also a `QCheck` generator for the `'a
 elt` type, as some functions of the library take arguments of this type. You
-can find these extensions in the `varray_incl.ml` and `varray_circular_incl.ml`
-files.
+can find these extensions in the `varray_config.ml` and
+`varray_circular_config.ml` files.
 
 The generated code can be found in the respective `varray*tests.ml` files. They
 have been promoted in the source tree in order to be easily accessible for
@@ -74,6 +73,6 @@ following command for `varray_spec.mli` and an adapted version for
 `varray_circular_spec.mli`:
 
 ```sh
-$ ortac dune qcheck-stm varray_spec "make 42 'a'" "char t" varray_tests --include=varray_incl --package=ortac-examples --with-stdout-to=dune.varray.inc
+$ ortac dune qcheck-stm varray_spec.mli varray_config.ml varray_tests.ml --package=ortac-examples --with-stdout-to=dune.varray.inc
 ```
 

examples/dune.lwt_dllist.inc

@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for lwt_dllist_spec
+; It contains the rules for generating and running QCheck-STM tests for lwt_dllist_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    lwt_dllist_spec
-    "create ()"
-    "int t"
-    lwt_dllist_tests
-    --include=lwt_dllist_incl
+    lwt_dllist_spec.mli
+    lwt_dllist_config.ml
+    lwt_dllist_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.lwt_dllist.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:lwt_dllist_spec.mli}
-     "create ()"
-     "int t"
-     --include=lwt_dllist_incl
+     %{dep:lwt_dllist_config.ml}
      --quiet)))))
 
 (test
  (name lwt_dllist_tests)
- (modules lwt_dllist_tests lwt_dllist_incl)
+ (modules lwt_dllist_tests)
  (libraries
   lwt_dllist_spec
   qcheck-stm.stm

examples/dune.varray.inc

@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for varray_spec
+; It contains the rules for generating and running QCheck-STM tests for varray_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    varray_spec
-    "make 42 'a'"
-    "char t"
-    varray_tests
-    --include=varray_incl
+    varray_spec.mli
+    varray_config.ml
+    varray_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.varray.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:varray_spec.mli}
-     "make 42 'a'"
-     "char t"
-     --include=varray_incl
+     %{dep:varray_config.ml}
      --quiet)))))
 
 (test
  (name varray_tests)
- (modules varray_tests varray_incl)
+ (modules varray_tests)
  (libraries
   varray_spec
   qcheck-stm.stm

examples/dune.varray_circular.inc

@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for varray_circular_spec
+; It contains the rules for generating and running QCheck-STM tests for varray_circular_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    varray_circular_spec
-    "make 42 'a'"
-    "char t"
-    varray_circular_tests
-    --include=varray_circular_incl
+    varray_circular_spec.mli
+    varray_circular_config.ml
+    varray_circular_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.varray_circular.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:varray_circular_spec.mli}
-     "make 42 'a'"
-     "char t"
-     --include=varray_circular_incl
+     %{dep:varray_circular_config.ml}
      --quiet)))))
 
 (test
  (name varray_circular_tests)
- (modules varray_circular_tests varray_circular_incl)
+ (modules varray_circular_tests)
  (libraries
   varray_circular_spec
   qcheck-stm.stm

examples/lwt_dllist_config.ml

@@ -0,0 +1,13 @@
+open Lwt_dllist_spec
+
+type sut = int t
+
+let init_sut = create ()
+
+module Ty = struct
+  type _ ty += Node : 'a ty -> 'a node ty
+
+  let node spec =
+    let ty, show = spec in
+    (Node ty, fun n -> Printf.sprintf "Node %s" (show (get n)))
+end

examples/lwt_dllist_tests.ml

@@ -6,7 +6,11 @@ module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =
   struct
     open STM
-    include Lwt_dllist_incl
+    type _ ty +=  
+      | Node: 'a ty -> 'a node ty 
+    let node spec =
+      let (ty, show) = spec in
+      ((Node ty), (fun n -> Printf.sprintf "Node %s" (show (get n))))
     type sut = int t
     type cmd =
       | Is_empty 

examples/varray_circular_config.ml

@@ -0,0 +1,26 @@
+open Varray
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Pp = struct
+  include Util.Pp
+
+  let pp_elt pp = pp
+end
+
+module Gen = struct
+  include QCheck.Gen
+
+  let int = small_signed_int
+  let elt gen = gen
+end
+
+module Ty = struct
+  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))
+end

examples/varray_circular_tests.ml

@@ -62,7 +62,29 @@ let proj e =
 module Spec =
   struct
     open STM
-    include Varray_circular_incl
+    module QCheck =
+      struct
+        include QCheck
+        module Gen =
+          struct
+            include Gen
+            include QCheck.Gen
+            let int = small_signed_int
+            let elt gen = gen
+          end
+      end
+    module Util =
+      struct
+        module Pp =
+          struct include Util.Pp
+                 include Util.Pp
+                 let pp_elt pp = pp end
+      end
+    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)))
     type sut = char t
     type cmd =
       | Push_back of char elt 

examples/varray_config.ml

@@ -0,0 +1,26 @@
+open Varray
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Pp = struct
+  include Util.Pp
+
+  let pp_elt pp = pp
+end
+
+module Gen = struct
+  include QCheck.Gen
+
+  let int = small_signed_int
+  let elt gen = gen
+end
+
+module Ty = struct
+  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))
+end

examples/varray_tests.ml

@@ -62,7 +62,29 @@ let proj e =
 module Spec =
   struct
     open STM
-    include Varray_incl
+    module QCheck =
+      struct
+        include QCheck
+        module Gen =
+          struct
+            include Gen
+            include QCheck.Gen
+            let int = small_signed_int
+            let elt gen = gen
+          end
+      end
+    module Util =
+      struct
+        module Pp =
+          struct include Util.Pp
+                 include Util.Pp
+                 let pp_elt pp = pp end
+      end
+    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)))
     type sut = char t
     type cmd =
       | Push_back of char elt 

plugins/dune-rules/README.md

@@ -20,18 +20,18 @@ plugins (the qcheck-stm plugin for now). You have to give it the option you want
 pass to the other plugins and some more information for dune.
 
 Let's say you want use the [Ortac/QCheck-STM] plugin on a module interface
-`lib.mli` to generate QCheck-STM tests for this module using `make 42 'a'` as
-initial value of type `char t`, including the `Lib_incl` module, in the context
-of the `pack` package.
+`lib.mli` to generate QCheck-STM tests with the `lib_conf.ml` configuration, in
+the context of the `pack` package.
 
 Then you can run:
 
 ```shell
-$ ortac dune qcheck-stm lib "make 42 'a'" "char t" lib_tests --include=lib_incl --package=pack --with-stdout-to=dune.inc
+$ ortac dune qcheck-stm lib.mli lib_conf.ml lib_tests.ml --package=pack --with-stdout-to=dune.inc
 ```
 
-to generate the dune rules to generate and run the tests. Next time you run
-`dune runtest`, your code should be tested using QCheck-STM.
+to generate the dune rules to generate and run the tests. You can then include
+`dune.inc` in the `dune` file and the next time you run `dune runtest`, your
+code should be tested using QCheck-STM.
 
 [Ortac/QCheck-STM]: ../qcheck-stm/README.md