Merge pull request ocaml-gospel#235 from nikolaushuber/test-without-sut

Add support for functions without SUT argument

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Add support for testing functions without a sut argument
+  [\#235](https://github.com/ocaml-gospel/ortac/pull/235)
 - Add error for empty command type 
   [\#234](https://github.com/ocaml-gospel/ortac/pull/234)
 - Move to a module-based configuration

examples/lwt_dllist_tests.ml

@@ -1,6 +1,6 @@
 (* This file is generated by ortac qcheck-stm,
    edit how you run the tool instead *)
-[@@@ocaml.warning "-26-27"]
+[@@@ocaml.warning "-26-27-69"]
 open Lwt_dllist_spec
 module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =

examples/varray_circular_tests.ml

@@ -1,6 +1,6 @@
 (* This file is generated by ortac qcheck-stm,
    edit how you run the tool instead *)
-[@@@ocaml.warning "-26-27"]
+[@@@ocaml.warning "-26-27-69"]
 open Varray_circular_spec
 module Ortac_runtime = Ortac_runtime_qcheck_stm
 let inside i s =

examples/varray_tests.ml

@@ -1,6 +1,6 @@
 (* This file is generated by ortac qcheck-stm,
    edit how you run the tool instead *)
-[@@@ocaml.warning "-26-27"]
+[@@@ocaml.warning "-26-27-69"]
 open Varray_spec
 module Ortac_runtime = Ortac_runtime_qcheck_stm
 let inside i s =

plugins/qcheck-stm/doc/example_limitations.mli

@@ -10,9 +10,6 @@ val make : int -> 'a -> 'a t
 
 (* $MDX part-begin=fun-decl *)
 
-val f : int -> int -> bool
-(*@ b = f x y *)
-
 val compare : 'a t -> 'a t -> bool
 (*@ b = compare t1 t2 *)
 

plugins/qcheck-stm/doc/index.mld

@@ -446,15 +446,12 @@ val for_all : 'a t -> bool
 
 Finally, note that this tool is still fairly new and comes with limitations
 that should be lifted in the future. Fow now, we only support testing functions
-with exactly one [SUT] argument in its signature, we don't support tuples and
+with at most one [SUT] argument in its signature, we don't support tuples and
 we only support first-order functions.
 
 If we add the following declarations to our example file,
 
 {@ocaml file=example_limitations.mli,part=fun-decl[
-val f : int -> int -> bool
-(*@ b = f x y *)
-
 val compare : 'a t -> 'a t -> bool
 (*@ b = compare t1 t2 *)
 
@@ -475,33 +472,29 @@ Ortac/QCheck-STM will generate the following warnings:
 
 {@sh[
 $ ortac qcheck-stm example_limitations.mli example_config.ml -o foo.ml
-File "example_limitations.mli", line 13, characters 8-26:
-13 | val f : int -> int -> bool
-             ^^^^^^^^^^^^^^^^^^
-Warning: Skipping f: functions with no SUT argument cannot be tested.
-File "example_limitations.mli", line 16, characters 14-34:
-16 | val compare : 'a t -> 'a t -> bool
+File "example_limitations.mli", line 13, characters 14-34:
+13 | val compare : 'a t -> 'a t -> bool
                    ^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping compare: functions with multiple SUT arguments cannot be
          tested.
-File "example_limitations.mli", line 19, characters 25-29:
-19 | val of_list : 'a list -> 'a t
+File "example_limitations.mli", line 16, characters 25-29:
+16 | val of_list : 'a list -> 'a t
                               ^^^^
 Warning: Skipping of_list: functions returning a SUT value cannot be tested.
-File "example_limitations.mli", line 25, characters 16-23:
-25 | val h : 'a t -> 'a * 'a
+File "example_limitations.mli", line 22, characters 16-23:
+22 | val h : 'a t -> 'a * 'a
                      ^^^^^^^
 Warning: Skipping h: functions returning tuples are not supported yet.
-File "example_limitations.mli", line 28, characters 15-25:
-28 | val for_all : ('a -> bool) -> 'a t -> bool
+File "example_limitations.mli", line 25, characters 15-25:
+25 | val for_all : ('a -> bool) -> 'a t -> bool
                     ^^^^^^^^^^
 Warning: Skipping for_all: functions are not supported yet as arguments.
-File "example_limitations.mli", line 22, characters 0-50:
-22 | val g : int * int -> 'a t -> bool
-23 | (*@ b = g x t *)
+File "example_limitations.mli", line 19, characters 0-50:
+19 | val g : int * int -> 'a t -> bool
+20 | (*@ b = g x t *)
 Warning: Incomplete computation of the returned value in the specification of g. Failure message won't be able to display the expected returned value.
-File "example_limitations.mli", line 22, characters 8-17:
-22 | val g : int * int -> 'a t -> bool
+File "example_limitations.mli", line 19, characters 8-17:
+19 | val g : int * int -> 'a t -> bool
              ^^^^^^^^^
 Warning: Type (int * int) not supported.
 ]}

plugins/qcheck-stm/src/ir.ml

@@ -41,7 +41,7 @@ type value = {
   id : Ident.t;
   ty : Ppxlib.core_type;
   inst : (string * Ppxlib.core_type) list;
-  sut_var : Ident.t;
+  sut_var : Ident.t option;
   args : (Ppxlib.core_type * Ident.t option) list;
       (* arguments of unit types can be nameless *)
   ret : Ident.t list;

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -75,10 +75,7 @@ let ty_var_substitution config (vd : val_description) =
   let value_name, value_type = (vd.vd_name.id_str, vd.vd_type) in
   assert (is_a_function value_type);
   let open Ppxlib in
-  let ret = function
-    | None -> Reserr.(error (No_sut_argument value_name, value_type.ptyp_loc))
-    | Some x -> Reserr.ok x
-  in
+  let ret = function None -> Reserr.ok [] | Some x -> Reserr.ok x in
   let rec aux seen ty =
     match ty.ptyp_desc with
     | Ptyp_any | Ptyp_var _ -> ret seen
@@ -128,8 +125,7 @@ let split_args config vd args =
     | _, _ -> failwith "shouldn't happen (too few parameters)"
   in
   let* sut, args = aux None [] vd.vd_type args in
-  (* sut cannot be none because its presence has already been checked *)
-  ok (Option.get sut, args)
+  ok (sut, args)
 
 let get_state_description_with_index is_t state spec =
   let open Tterm in
@@ -149,8 +145,9 @@ let get_state_description_with_index is_t state spec =
 let next_state sut state spec =
   let open Tterm in
   let is_t vs =
-    let open Symbols in
-    Ident.equal sut vs.vs_name
+    Option.fold
+      ~some:(fun sut -> Ident.equal sut vs.Symbols.vs_name)
+      ~none:false sut
   in
   let formulae = get_state_description_with_index is_t state spec in
   let open Reserr in

plugins/qcheck-stm/src/reserr.ml

@@ -28,7 +28,6 @@ type W.kind +=
   | No_init_function of string
   | No_models of string
   | No_spec of string
-  | No_sut_argument of string
   | No_sut_type of string
   | Not_a_structure of string
   | Returned_tuple of string
@@ -46,8 +45,7 @@ let level kind =
   | Functional_argument _ | Ghost_values _ | Ignored_modifies
   | Impossible_term_substitution _ | Incompatible_type _
   | Incomplete_ret_val_computation _ | Multiple_sut_arguments _ | No_spec _
-  | No_sut_argument _ | Returned_tuple _ | Returning_sut _
-  | Type_not_supported _ ->
+  | Returned_tuple _ | Returning_sut _ | Type_not_supported _ ->
       W.Warning
   | Empty_cmd_type | Impossible_init_state_generation _ | Incompatible_sut _
   | Incomplete_configuration_module _ | No_configuration_file _
@@ -130,9 +128,6 @@ let pp_kind ppf kind =
   | No_spec fct ->
       pf ppf "Skipping %s:@ %a" fct text
         "functions without specifications cannot be tested"
-  | No_sut_argument id ->
-      pf ppf "Skipping %s:@ %a" id text
-        "functions with no SUT argument cannot be tested"
   | Returned_tuple f ->
       pf ppf "Skipping %s:@ %a" f text
         "functions returning tuples are not supported yet"

plugins/qcheck-stm/src/reserr.mli

@@ -28,7 +28,6 @@ type W.kind +=
   | No_init_function of string
   | No_models of string
   | No_spec of string
-  | No_sut_argument of string
   | No_sut_type of string
   | Not_a_structure of string
   | Returned_tuple of string

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -149,9 +149,12 @@ let subst_term state ?(out_of_scope = []) ~gos_t ?(old_lz = false) ~old_t
 
 let translate_checks config state value state_ident t =
   let open Reserr in
-  subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident)
-    ~new_t:(Some state_ident) t.term
-  >>= ocaml_of_term config
+  match value.sut_var with
+  | Some sut_var ->
+      subst_term state ~gos_t:sut_var ~old_t:(Some state_ident)
+        ~new_t:(Some state_ident) t.term
+      >>= ocaml_of_term config
+  | None -> ocaml_of_term config t.term
 
 let str_of_ident = Fmt.str "%a" Ident.pp
 let longident_loc_of_ident id = str_of_ident id |> lident
@@ -330,9 +333,12 @@ let next_state_case state config state_ident nb_models value =
     let descriptions =
       List.filter_map
         (fun (i, { model; description }) ->
-          subst_term ~out_of_scope:value.ret state ~gos_t:value.sut_var
-            ~old_t:(Some state_ident) ~new_t:None description
-          >>= ocaml_of_term config
+          (match value.sut_var with
+          | Some sut_var ->
+              subst_term ~out_of_scope:value.ret state ~gos_t:sut_var
+                ~old_t:(Some state_ident) ~new_t:None description
+              >>= ocaml_of_term config
+          | None -> ocaml_of_term config description)
           |> to_option
           |> Option.map (fun description -> (i, model, description)))
         value.next_state.formulae
@@ -405,9 +411,12 @@ let precond_case config state state_ident value =
     list_and
     <$> map
           (fun t ->
-            subst_term state ~gos_t:value.sut_var ~old_t:None
-              ~new_t:(Some state_ident) t
-            >>= ocaml_of_term config)
+            match value.sut_var with
+            | Some sut_var ->
+                subst_term state ~gos_t:sut_var ~old_t:None
+                  ~new_t:(Some state_ident) t
+                >>= ocaml_of_term config
+            | None -> ocaml_of_term config t)
           value.precond
   in
   ok (case ~lhs ~guard:None ~rhs)
@@ -453,9 +462,12 @@ let postcond_case config state invariants idx state_ident new_state_ident value
     =
   let open Reserr in
   let translate_postcond t =
-    subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident) ~new_lz:true
-      ~new_t:(Some new_state_ident) t.term
-    >>= ocaml_of_term config
+    match value.sut_var with
+    | Some sut_var ->
+        subst_term state ~gos_t:sut_var ~old_t:(Some state_ident) ~new_lz:true
+          ~new_t:(Some new_state_ident) t.term
+        >>= ocaml_of_term config
+    | None -> ocaml_of_term config t.term
   and translate_invariants id t =
     subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident)
       ~new_lz:true t.term
@@ -970,7 +982,7 @@ let stm config ir =
   let open Reserr in
   let* ghost_types = ghost_types config ir.ghost_types in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
-  let warn = [%stri [@@@ocaml.warning "-26-27"]] in
+  let warn = [%stri [@@@ocaml.warning "-26-27-69"]] in
   let sut = sut_type config in
   let* cmd = cmd_type ir in
   let* cmd_show = cmd_show config ir in

plugins/qcheck-stm/test/all_warnings.mli

@@ -16,9 +16,6 @@ val constant : unit
 val returning_sut : 'a -> 'a t
 (*@ t = returning_sut a *)
 
-val no_sut_argument : bool -> bool
-(*@ a = no_sut_argument b *)
-
 val multiple_sut_argument : 'a t -> 'a t -> bool
 (*@ b = multiple_sut_argument x y *)