Handle tuple as returned value

Replace an internal error by a proper warning.
Still does not generate test for function returning tuple value.

plugins/qcheck-stm/src/ir.ml

@@ -32,7 +32,7 @@ type value = {
   sut_var : Ident.t;
   args : (Ppxlib.core_type * Ident.t option) list;
       (* arguments of unit types can be nameless *)
-  ret : Ident.t option;
+  ret : Ident.t list;
   next_state : next_state;
   precond : Tterm.term list;
   postcond : postcond;

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -193,12 +193,15 @@ let val_desc config state vd =
   in
   let* sut, args = split_args config vd spec.sp_args
   and* ret =
-    match spec.sp_ret with
-    | [ Lnone vs ] -> ok (Some vs.vs_name)
-    | [] -> ok None
-    | Lghost vs :: _ | _ :: Lghost vs :: _ ->
-        error (Ghost_values (vd.vd_name.id_str, `Ret), vs.vs_name.id_loc)
-    | _ -> failwith "shouldn't happen (more than one return OCaml value)"
+    let p = function
+      | Lnone vs -> ok vs.vs_name
+      | Lghost vs ->
+          error (Ghost_values (vd.vd_name.id_str, `Ret), vs.vs_name.id_loc)
+      | _ ->
+          failwith
+            "shouldn't happen (only non labelled and ghost value are returned)"
+    in
+    List.map p spec.sp_ret |> sequence
   in
   let* next_state = next_state sut state spec in
   let postcond = postcond spec in

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -460,10 +460,11 @@ let postcond_case config state idx state_ident new_state_ident value =
     in
     let pat_ret =
       match value.ret with
-      | None ->
+      | [] ->
           if may_raise_exception value then pvar (str_of_ident res_default)
           else ppat_any
-      | Some id -> pvar (str_of_ident id)
+      | [ id ] -> pvar (str_of_ident id)
+      | xs -> ppat_tuple (List.map (fun x -> pvar (str_of_ident x)) xs)
     in
     ok
       (ppat_construct (lident "Res")
@@ -487,10 +488,15 @@ let postcond_case config state idx state_ident new_state_ident value =
   in
   let res, pat_ret =
     match value.ret with
-    | None -> (evar (str_of_ident res_default), ppat_any)
-    | Some id ->
+    | [] -> (evar (str_of_ident res_default), ppat_any)
+    | [ id ] ->
         let id = str_of_ident id in
         (evar id, pvar id)
+    | xs ->
+        let ids = List.map str_of_ident xs in
+        let res = pexp_tuple (List.map evar ids) in
+        let pat_ret = ppat_tuple (List.map pvar ids) in
+        (res, pat_ret)
   in
   let* rhs =
     if may_raise_exception value then

plugins/qcheck-stm/test/all_warnings.mli

@@ -55,3 +55,6 @@ val unsupported_quantification : 'a t -> bool
 val record_not_model_field : 'a t -> bool
 (*@ b = record_not_model_field t
     requires Array.length t.v > 0 *)
+
+val return_tuple : 'a t -> 'a * bool
+(*@ (a, b) = return_tuple t *)

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -57,8 +57,16 @@ File "all_warnings.mli", line 53, characters 16-54:
 53 |     ensures b = forall a. List.mem a t.contents -> p a *)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping clause: unsupported quantification.
+File "all_warnings.mli", line 59, characters 27-36:
+59 | val return_tuple : 'a t -> 'a * bool
+                                ^^^^^^^^^
+Warning: Type ('a * bool) not supported.
 File "all_warnings.mli", line 57, characters 26-29:
 57 |     requires Array.length t.v > 0 *)
                                ^^^
 Warning: Skipping clause: occurrences of the SUT in clauses are only
          supported to access its model fields.
+File "all_warnings.mli", line 59, characters 27-36:
+59 | val return_tuple : 'a t -> 'a * bool
+                                ^^^^^^^^^
+Warning: Type ('a * bool) not supported.