From 1fa1231ef37644cfdfff360d7b526cebb0e9f54b Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Thu, 28 Mar 2024 16:30:59 +0100 Subject: [PATCH] Update examples to new interface --- examples/README.md | 13 ++++++------- examples/dune.lwt_dllist.inc | 16 ++++++---------- examples/dune.varray.inc | 16 ++++++---------- examples/dune.varray_circular.inc | 16 ++++++---------- examples/lwt_dllist_config.ml | 13 +++++++++++++ examples/lwt_dllist_incl.ml | 8 -------- examples/lwt_dllist_tests.ml | 6 +++++- examples/varray_circular_config.ml | 26 ++++++++++++++++++++++++++ examples/varray_circular_incl.ml | 27 --------------------------- examples/varray_circular_tests.ml | 24 +++++++++++++++++++++++- examples/varray_config.ml | 26 ++++++++++++++++++++++++++ examples/varray_incl.ml | 27 --------------------------- examples/varray_tests.ml | 24 +++++++++++++++++++++++- 13 files changed, 140 insertions(+), 102 deletions(-) create mode 100644 examples/lwt_dllist_config.ml delete mode 100644 examples/lwt_dllist_incl.ml create mode 100644 examples/varray_circular_config.ml delete mode 100644 examples/varray_circular_incl.ml create mode 100644 examples/varray_config.ml delete mode 100644 examples/varray_incl.ml diff --git a/examples/README.md b/examples/README.md index 24239c70..cbeb3819 100644 --- a/examples/README.md +++ b/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 moduel 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 ``` diff --git a/examples/dune.lwt_dllist.inc b/examples/dune.lwt_dllist.inc index 881c3650..9f461598 100644 --- a/examples/dune.lwt_dllist.inc +++ b/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 diff --git a/examples/dune.varray.inc b/examples/dune.varray.inc index 163756c9..ae10cbfe 100644 --- a/examples/dune.varray.inc +++ b/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 diff --git a/examples/dune.varray_circular.inc b/examples/dune.varray_circular.inc index 7b73c2f4..16a07cda 100644 --- a/examples/dune.varray_circular.inc +++ b/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 diff --git a/examples/lwt_dllist_config.ml b/examples/lwt_dllist_config.ml new file mode 100644 index 00000000..a0ca5dd5 --- /dev/null +++ b/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 diff --git a/examples/lwt_dllist_incl.ml b/examples/lwt_dllist_incl.ml deleted file mode 100644 index 0afe0995..00000000 --- a/examples/lwt_dllist_incl.ml +++ /dev/null @@ -1,8 +0,0 @@ -open Lwt_dllist_spec -open STM - -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))) diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml index 099ae07b..29b04ef5 100644 --- a/examples/lwt_dllist_tests.ml +++ b/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 diff --git a/examples/varray_circular_config.ml b/examples/varray_circular_config.ml new file mode 100644 index 00000000..726fe416 --- /dev/null +++ b/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 diff --git a/examples/varray_circular_incl.ml b/examples/varray_circular_incl.ml deleted file mode 100644 index cfe35125..00000000 --- a/examples/varray_circular_incl.ml +++ /dev/null @@ -1,27 +0,0 @@ -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_circular_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)) diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index c7937aff..80d98460 100644 --- a/examples/varray_circular_tests.ml +++ b/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 diff --git a/examples/varray_config.ml b/examples/varray_config.ml new file mode 100644 index 00000000..726fe416 --- /dev/null +++ b/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 diff --git a/examples/varray_incl.ml b/examples/varray_incl.ml deleted file mode 100644 index 1fe4712e..00000000 --- a/examples/varray_incl.ml +++ /dev/null @@ -1,27 +0,0 @@ -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)) diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml index 5afd33ac..538ad0e0 100644 --- a/examples/varray_tests.ml +++ b/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