Add support for tuples as return values

This adds functionality to test functions which return tuples.
This is conceptually different from having tuples in argument positions
as we need to extend the STM.ty type and provide a constructor so that
Res values can be created for it.

plugins/qcheck-stm/doc/index.mld

@@ -485,12 +485,12 @@ File "example_limitations.mli", line 23, characters 16-63:
 23 | val g : 'a t -> 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a -> bool
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping g: Can only test tuples with arity < 10.
-File "example_limitations.mli", line 26, characters 16-23:
-26 | val h : 'a t -> 'a * 'a
-                     ^^^^^^^
-Warning: Skipping h: functions returning tuples are not supported yet.
 File "example_limitations.mli", line 29, characters 15-25:
 29 | val for_all : ('a -> bool) -> 'a t -> bool
                     ^^^^^^^^^^
 Warning: Skipping for_all: functions are not supported yet as arguments.
+File "example_limitations.mli", line 26, characters 0-43:
+26 | val h : 'a t -> 'a * 'a
+27 | (*@ (l, r) = h t *)
+Warning: Incomplete computation of the returned value in the specification of h. Failure message won't be able to display the expected returned value.
 ]}

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -10,7 +10,7 @@ let constant_test vd =
       (Constant_value (Fmt.str "%a" Ident.pp vd.vd_name), vd.vd_loc) |> error
   | _ -> ok ()
 
-let no_functional_arg_or_returned_tuple vd =
+let no_functional_arg_or_big_tuple vd =
   let open Reserr in
   let open Ppxlib in
   let rec contains_arrow ty =
@@ -29,7 +29,6 @@ let no_functional_arg_or_returned_tuple vd =
     | Ptyp_arrow (_, l, r) ->
         let* _ = contains_arrow l in
         aux r
-    | Ptyp_tuple _ -> error (Returned_tuple vd.vd_name.id_str, ty.ptyp_loc)
     | _ -> ok ()
   in
   aux vd.vd_type
@@ -217,7 +216,7 @@ let postcond spec =
 
 let val_desc config state vd =
   let open Reserr in
-  let* () = constant_test vd and* () = no_functional_arg_or_returned_tuple vd in
+  let* () = constant_test vd and* () = no_functional_arg_or_big_tuple vd in
   let* inst = ty_var_substitution config vd
   and* spec =
     of_option ~default:(No_spec vd.vd_name.id_str, vd.vd_loc) vd.vd_spec

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -202,6 +202,12 @@ let pat_of_core_type inst typ =
           | xs -> (fun xs -> Some (ppat_tuple xs)) <$> map aux xs
         in
         ppat_construct <$> constr_str <*> pat_arg
+    | Ptyp_tuple xs ->
+        let* pat_arg = ppat_tuple <$> map aux xs in
+        ppat_construct
+          (lident ("Tup" ^ string_of_int (List.length xs)))
+          (Some pat_arg)
+        |> ok
     | _ ->
         error
           ( Type_not_supported (Fmt.str "%a" Pprintast.core_type typ),
@@ -446,10 +452,6 @@ let expected_returned_value translate_postcond value =
   let ret_val =
     match (ty_ret.ptyp_desc, value.ret_values) with
     | Ptyp_constr ({ txt = Lident "unit"; _ }, _), _ -> Some eunit
-    | Ptyp_tuple _, _ ->
-        failwith
-          "shouldn't happen (functions returning tuples are filtered out \
-           before)"
     | _, [ xs ] ->
         Option.bind
           (to_option @@ map translate_postcond xs)
@@ -524,7 +526,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
     let* ret_ty =
       let open Ppxlib in
       match ret_ty.ptyp_desc with
-      | Ptyp_var _ | Ptyp_constr _ -> ok ret_ty
+      | Ptyp_var _ | Ptyp_constr _ | Ptyp_tuple _ -> ok ret_ty
       | _ ->
           error
             ( Type_not_supported (Fmt.str "%a" Pprintast.core_type ret_ty),
@@ -543,10 +545,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
           if may_raise_exception value then pvar (str_of_ident res_default)
           else ppat_any
       | [ id ] -> pvar (str_of_ident id)
-      | _ ->
-          failwith
-            "shouldn't happen (functions returning tuples are filtered out \
-             before)"
+      | xs -> ppat_tuple (List.map (fun x -> pvar @@ str_of_ident x) xs)
     in
     ok
       (ppat_construct (lident "Res")
@@ -582,10 +581,10 @@ let postcond_case config state invariants idx state_ident new_state_ident value
     | [ id ] ->
         let id = str_of_ident id in
         (evar id, pvar id)
-    | _ ->
-        failwith
-          "shouldn't happen (functions returning tuples are filtered out \
-           before)"
+    | xs ->
+        let evars = List.map (fun x -> evar @@ str_of_ident x) xs in
+        let pvars = List.map (fun x -> pvar @@ str_of_ident x) xs in
+        (pexp_tuple evars, ppat_tuple pvars)
   in
   let* rhs =
     if may_raise_exception value then
@@ -985,6 +984,95 @@ let util config =
       let name = noloc (Some "Util") and expr = pmod_structure structure in
       [ pstr_module (module_binding ~name ~expr) ]
 
+let gen_tuple_ty arities =
+  let constructors =
+    List.map
+      (fun ar ->
+        let name = Located.mk ("Tup" ^ string_of_int ar) in
+        let idxs =
+          List.init ar (fun x -> "a" ^ string_of_int (x + 1) |> ptyp_var)
+        in
+        let args = List.map (fun c -> ptyp_constr (lident "ty") [ c ]) idxs in
+        let ret = ptyp_constr (lident "ty") [ ptyp_tuple idxs ] in
+        let kind = Pext_decl ([], Pcstr_tuple args, Some ret) in
+        extension_constructor ~name ~kind)
+      arities
+  in
+  let path = lident "ty" in
+  let params = [ (ptyp_any, (NoVariance, NoInjectivity)) ] in
+  let private_ = Public in
+  pstr_typext (type_extension ~path ~params ~constructors ~private_)
+
+let gen_tuple_constr arities =
+  let range idx = List.init idx (fun x -> x + 1) in
+  let gen_vb arity =
+    let arity_str = string_of_int arity in
+    let idxs = range arity in
+    let pat = pvar ("tup" ^ arity_str) in
+    let last_e =
+      pexp_tuple
+        [
+          pexp_construct
+            (lident ("Tup" ^ arity_str))
+            (Some
+               (pexp_tuple
+                  (List.map (fun i -> evar ("ty" ^ string_of_int i)) idxs)));
+          pexp_apply
+            (evar ("QCheck.Print.tup" ^ string_of_int arity))
+            (List.map
+               (fun i -> (Nolabel, evar ("show" ^ string_of_int i)))
+               idxs);
+        ]
+    in
+    let body =
+      pexp_let Nonrecursive
+        (List.map
+           (fun i ->
+             let pat =
+               ppat_tuple
+                 [
+                   pvar ("ty" ^ string_of_int i); pvar ("show" ^ string_of_int i);
+                 ]
+             in
+             let expr = evar ("spec" ^ string_of_int i) in
+             value_binding ~pat ~expr)
+           idxs)
+        last_e
+    in
+    let expr =
+      List.fold_left
+        (fun acc i ->
+          pexp_fun Nolabel None (pvar ("spec" ^ string_of_int i)) acc)
+        body (List.rev idxs)
+    in
+    value_binding ~pat ~expr
+  in
+  let vbs = List.map gen_vb arities in
+  pstr_value Nonrecursive vbs
+
+(* This function creates type extensions for STM.ty and smart constructors for
+   them. It looks up all required tuple arities from the return types of
+   IR values
+*)
+let tuple_types ir =
+  let ret_tys =
+    List.map (fun v -> (Ir.get_return_type v).ptyp_desc) ir.values
+  in
+  (* We use a set as we only need each tuple arity once *)
+  let module IntS = Set.Make (Int) in
+  let rec aux acc = function
+    | Ptyp_tuple xs ->
+        let acc' =
+          (* Tuples might be nested *)
+          List.fold_left aux acc (List.map (fun x -> x.ptyp_desc) xs)
+        in
+        IntS.union (IntS.singleton (List.length xs)) acc'
+    | _ -> acc
+  in
+  let arities = List.fold_left aux IntS.empty ret_tys |> IntS.elements in
+  if List.length arities = 0 then []
+  else [ gen_tuple_ty arities; gen_tuple_constr arities ]
+
 let stm config ir =
   let open Reserr in
   let* ghost_types = ghost_types config ir.ghost_types in
@@ -1017,6 +1105,7 @@ let stm config ir =
       ((open_mod "STM" :: qcheck config)
       @ util config
       @ Option.value config.ty_mod ~default:[]
+      @ tuple_types ir
       @ [
           sut;
           cmd;

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -42,11 +42,6 @@ File "all_warnings.mli", line 46, characters 6-7:
            ^
 Warning: Skipping ghost_returned_value: functions with a ghost returned value
          are not supported.
-File "all_warnings.mli", line 56, characters 27-36:
-56 | val return_tuple : 'a t -> 'a * bool
-                                ^^^^^^^^^
-Warning: Skipping return_tuple: functions returning tuples are not supported
-         yet.
 File "all_warnings.mli", line 34, characters 13-23:
 34 |     modifies t.contents *)
                   ^^^^^^^^^^
@@ -81,6 +76,10 @@ File "all_warnings.mli", line 52, characters 0-111:
 53 | (*@ b = record_not_model_field t
 54 |     requires Array.length t.v > 0 *)
 Warning: Incomplete computation of the returned value in the specification of record_not_model_field. Failure message won't be able to display the expected returned value.
+File "all_warnings.mli", line 56, characters 0-67:
+56 | val return_tuple : 'a t -> 'a * bool
+57 | (*@ (a, b) = return_tuple t *)
+Warning: Incomplete computation of the returned value in the specification of return_tuple. Failure message won't be able to display the expected returned value.
 File "all_warnings.mli", line 59, characters 0-278:
 59 | val term_refer_to_returned_value_next_state : 'a t -> 'a option
 60 | (*@ o = term_refer_to_returned_value_next_state t

plugins/qcheck-stm/test/tuples.mli

@@ -13,7 +13,7 @@ val clear : ('a, 'b) t -> unit
 val add : ('a, 'b) t -> 'a * 'b -> unit
 (*@ add h tup
     modifies h
-    ensures h.contents = match tup with a, b -> old h.contents *)
+    ensures h.contents = match tup with a, b -> (a, b) :: old h.contents *)
 
 val add' : ('a, 'b) t -> bool * 'a * 'b -> unit
 (*@ add' h tup

plugins/qcheck-stm/test/tuples_errors.expected

@@ -1,4 +1,6 @@
-File "tuples.mli", line 25, characters 29-38:
+File "tuples.mli", line 25, characters 0-141:
 25 | val size_tup : ('a, 'b) t -> int * int
-                                  ^^^^^^^^^
-Warning: Skipping size_tup: functions returning tuples are not supported yet.
+26 | (*@ x, y = size_tup t
+27 |     ensures x = List.length t.contents
+28 |     ensures y = List.length t.contents *)
+Warning: Incomplete computation of the returned value in the specification of size_tup. Failure message won't be able to display the expected returned value.