Add support for tuples

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Add support for testing functions with tuple arguments/return values
+  [\#237](https://github.com/ocaml-gospel/ortac/pull/237)
 - Add support for testing functions without a sut argument
   [\#235](https://github.com/ocaml-gospel/ortac/pull/235)
 - Add error for empty command type 

plugins/qcheck-stm/doc/example_limitations.mli

@@ -8,6 +8,10 @@ val make : int -> 'a -> 'a t
     ensures t.size = i
     ensures t.contents = List.init i (fun j -> a) *)
 
+val dummy : 'a t -> int
+(*@ l = dummy t
+    ensures l = t.size *)
+
 (* $MDX part-begin=fun-decl *)
 
 val compare : 'a t -> 'a t -> bool
@@ -16,11 +20,8 @@ val compare : 'a t -> 'a t -> bool
 val of_list : 'a list -> 'a t
 (*@ t = of_list xs *)
 
-val g : int * int -> 'a t -> bool
-(*@ b = g x t *)
-
-val h : 'a t -> 'a * 'a
-(*@ (l, r) = h t *)
+val g : 'a t -> 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a -> bool
+(*@ b = g t x *)
 
 val for_all : ('a -> bool) -> 'a t -> bool
 (*@ b = for_all p t *)

plugins/qcheck-stm/doc/index.mld

@@ -446,8 +446,8 @@ 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 at most one [SUT] argument in its signature, we don't support tuples and
-we only support first-order functions.
+with at most one [SUT] argument in its signature, tuples with less than 10
+elements and we only support first-order functions.
 
 If we add the following declarations to our example file,
 
@@ -458,11 +458,8 @@ val compare : 'a t -> 'a t -> bool
 val of_list : 'a list -> 'a t
 (*@ t = of_list xs *)
 
-val g : int * int -> 'a t -> bool
-(*@ b = g x t *)
-
-val h : 'a t -> 'a * 'a
-(*@ (l, r) = h t *)
+val g : 'a t -> 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a -> bool
+(*@ b = g t x *)
 
 val for_all : ('a -> bool) -> 'a t -> bool
 (*@ b = for_all p t *)
@@ -472,29 +469,21 @@ 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 14-34:
-13 | val compare : 'a t -> 'a t -> bool
+File "example_limitations.mli", line 17, characters 14-34:
+17 | val compare : 'a t -> 'a t -> bool
                    ^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping compare: functions with multiple SUT arguments cannot be
          tested.
-File "example_limitations.mli", line 16, characters 25-29:
-16 | val of_list : 'a list -> 'a t
+File "example_limitations.mli", line 20, characters 25-29:
+20 | val of_list : 'a list -> 'a t
                               ^^^^
 Warning: Skipping of_list: functions returning a SUT value cannot be tested.
-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 25, characters 15-25:
-25 | val for_all : ('a -> bool) -> 'a t -> bool
+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 15-25:
+26 | val for_all : ('a -> bool) -> 'a t -> bool
                     ^^^^^^^^^^
 Warning: Skipping for_all: functions are not supported yet as arguments.
-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 19, characters 8-17:
-19 | val g : int * int -> 'a t -> bool
-             ^^^^^^^^^
-Warning: Type (int * int) not supported.
 ]}

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -10,13 +10,15 @@ 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 =
     match ty.ptyp_desc with
     | Ptyp_arrow (_, _, _) ->
         error (Functional_argument vd.vd_name.id_str, ty.ptyp_loc)
+    | Ptyp_tuple xs when List.length xs > 9 ->
+        error (Tuple_arity vd.vd_name.id_str, ty.ptyp_loc)
     | Ptyp_tuple xs | Ptyp_constr (_, xs) ->
         let* _ = List.map contains_arrow xs |> sequence in
         ok ()
@@ -27,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
@@ -215,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/reserr.ml

@@ -35,6 +35,7 @@ type W.kind +=
   | Sut_type_not_specified of string
   | Sut_type_not_supported of string
   | Syntax_error_in_config_module of string
+  | Tuple_arity of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string
   | Type_parameter_not_instantiated of string
@@ -45,7 +46,7 @@ let level kind =
   | Functional_argument _ | Ghost_values _ | Ignored_modifies
   | Impossible_term_substitution _ | Incompatible_type _
   | Incomplete_ret_val_computation _ | Multiple_sut_arguments _ | No_spec _
-  | Returned_tuple _ | Returning_sut _ | Type_not_supported _ ->
+  | Returned_tuple _ | Returning_sut _ | Tuple_arity _ | Type_not_supported _ ->
       W.Warning
   | Empty_cmd_type | Impossible_init_state_generation _ | Incompatible_sut _
   | Incomplete_configuration_module _ | No_configuration_file _
@@ -157,6 +158,8 @@ let pp_kind ppf kind =
              next_state function"
       in
       pf ppf "Skipping clause:@ %a" text msg
+  | Tuple_arity fct ->
+      pf ppf "Skipping %s:@ %a" fct text "Can only test tuples with arity < 10"
   (* This following message is broad and used in seemingly different contexts
      but in fact we support all the types that the Gospel type-checker supports,
      so that error message should never get reported to the end user *)

plugins/qcheck-stm/src/reserr.mli

@@ -35,6 +35,7 @@ type W.kind +=
   | Sut_type_not_specified of string
   | Sut_type_not_supported of string
   | Syntax_error_in_config_module of string
+  | Tuple_arity of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string
   | Type_parameter_not_instantiated of string

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),
@@ -226,6 +232,12 @@ let exp_of_core_type inst typ =
             pexp_apply
             <$> constr_str
             <*> (List.map (fun e -> (Nolabel, e)) <$> map aux xs))
+    | Ptyp_tuple xs ->
+        let tup_constr =
+          pexp_ident (lident ("tup" ^ string_of_int (List.length xs)))
+        in
+        pexp_apply tup_constr
+        <$> (List.map (fun e -> (Nolabel, e)) <$> map aux xs)
     | _ ->
         error
           ( Type_not_supported (Fmt.str "%a" Pprintast.core_type typ),
@@ -440,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)
@@ -518,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),
@@ -537,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")
@@ -576,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
@@ -738,9 +743,10 @@ let pp_cmd_case config value =
   let open Reserr in
   let rec pp_of_ty ty : expression reserr =
     match ty.ptyp_desc with
-    | Ptyp_tuple [ ty0; ty1 ] ->
-        let* pp0 = pp_of_ty ty0 and* pp1 = pp_of_ty ty1 in
-        ok (pexp_apply (evar "pp_pair") [ (Nolabel, pp0); (Nolabel, pp1) ])
+    | Ptyp_tuple xs ->
+        let* pps = map pp_of_ty xs in
+        let func = qualify_pp ("pp_tuple" ^ string_of_int (List.length xs)) in
+        ok (pexp_apply func (List.map (fun e -> (Nolabel, e)) pps))
     | Ptyp_constr (lid, xs) ->
         let* xs = map pp_of_ty xs and* s = munge_longident false ty lid in
         let pp = qualify_pp ("pp_" ^ s) in
@@ -978,6 +984,104 @@ 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 ty_show =
+      pexp_tuple
+        [
+          pexp_construct
+            (lident ("Tup" ^ arity_str))
+            (Some
+               (pexp_tuple
+                  (List.map (fun i -> evar ("ty" ^ string_of_int i)) idxs)));
+          pexp_apply
+            (qualify [ "Util"; "Pp" ] "to_show")
+            [
+              ( Nolabel,
+                pexp_apply
+                  (qualify [ "Util"; "Pp" ] ("pp_tuple" ^ string_of_int arity))
+                  (List.map
+                     (fun i ->
+                       ( Nolabel,
+                         pexp_apply
+                           (qualify [ "Util"; "Pp" ] "of_show")
+                           [ (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)
+        ty_show
+    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
@@ -1010,6 +1114,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