From b4425ee9085caaadd7bd4d3749e9f9d58731f7b8 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 15:10:21 +0200
Subject: [PATCH 01/14] Move code internally in Reserr

---
 plugins/qcheck-stm/src/reserr.ml | 74 ++++++++++++++++----------------
 1 file changed, 37 insertions(+), 37 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 3ecc9554..f0c9ca47 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -60,43 +60,6 @@ let level kind =
       W.Error
   | _ -> W.level kind
 
-type 'a reserr = ('a, W.t list) result * W.t list
-
-let ok x = (Result.ok x, [])
-let error e = (Result.error [ e ], [])
-let warns ws = (Result.ok (), ws)
-let warn w = warns [ w ]
-
-let ( let* ) x f =
-  match x with
-  | Ok v, warns1 ->
-      let res, warns2 = f v in
-      (res, warns1 @ warns2)
-  | (Error _, _) as x -> x
-
-let ( >>= ) = ( let* )
-
-let ( and* ) (a, aw) (b, bw) =
-  let r =
-    match (a, b) with
-    | Error e0, Error e1 -> Error (e0 @ e1)
-    | Error e, _ | _, Error e -> Error e
-    | Ok a, Ok b -> Ok (a, b)
-  in
-  (r, aw @ bw)
-
-let fmap f r =
-  let* r = r in
-  ok (f r)
-
-let ( <$> ) = fmap
-
-let app f r =
-  let* f = f and* r = r in
-  ok (f r)
-
-let ( <*> ) = app
-
 let pp_kind ppf kind =
   let open Fmt in
   match kind with
@@ -270,6 +233,43 @@ let pp quiet pp_ok ppf r =
         match warns with [] -> () | warns -> pf stderr "%a@." pp_errors warns)
   | Error errs, warns -> pf stderr "%a@." pp_errors (errs @ warns)
 
+type 'a reserr = ('a, W.t list) result * W.t list
+
+let ok x = (Result.ok x, [])
+let error e = (Result.error [ e ], [])
+let warns ws = (Result.ok (), ws)
+let warn w = warns [ w ]
+
+let ( let* ) x f =
+  match x with
+  | Ok v, warns1 ->
+      let res, warns2 = f v in
+      (res, warns1 @ warns2)
+  | (Error _, _) as x -> x
+
+let ( >>= ) = ( let* )
+
+let ( and* ) (a, aw) (b, bw) =
+  let r =
+    match (a, b) with
+    | Error e0, Error e1 -> Error (e0 @ e1)
+    | Error e, _ | _, Error e -> Error e
+    | Ok a, Ok b -> Ok (a, b)
+  in
+  (r, aw @ bw)
+
+let fmap f r =
+  let* r = r in
+  ok (f r)
+
+let ( <$> ) = fmap
+
+let app f r =
+  let* f = f and* r = r in
+  ok (f r)
+
+let ( <*> ) = app
+
 let sequence r =
   let rec aux = function
     | [] -> ok []

From 2f4d7ffaefe2f6ec0a08b5ee88c5f00f9bc3a1fc Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 2 Oct 2024 09:40:18 +0200
Subject: [PATCH 02/14] Remove unsused `Warnings.kind`

---
 plugins/qcheck-stm/src/reserr.ml  | 20 ++++----------------
 plugins/qcheck-stm/src/reserr.mli |  3 ---
 2 files changed, 4 insertions(+), 19 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index f0c9ca47..33f12265 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -15,7 +15,6 @@ type W.kind +=
   | Ensures_not_found_for_ret_sut of (string * string list)
   | Functional_argument of string
   | Ghost_values of (string * [ `Arg | `Ret ])
-  | Ignored_modifies
   | Impossible_init_state_generation of init_state_error
   | Impossible_term_substitution of
       [ `Never | `New | `Old | `NotModel | `OutOfScope ]
@@ -23,14 +22,12 @@ type W.kind +=
   | Incompatible_type of (string * string)
   | Incomplete_ret_val_computation of string
   | Incomplete_configuration_module of [ `Init_sut | `Sut ]
-  | Multiple_sut_arguments of string
   | No_configuration_file of string
   | No_init_function of string
   | No_models of string
   | No_spec of string
   | No_sut_type of string
   | Not_a_structure of string
-  | Returned_tuple of string
   | Returning_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string
@@ -46,10 +43,10 @@ let level kind =
   match kind with
   | Constant_value _ | Ensures_not_found_for_next_state _
   | Ensures_not_found_for_ret_sut _ | Functional_argument _ | Ghost_values _
-  | Ignored_modifies | Impossible_term_substitution _ | Incompatible_type _
-  | Incomplete_ret_val_computation _ | Multiple_sut_arguments _ | No_spec _
-  | Returned_tuple _ | Returning_sut _ | Sut_as_type_inst _ | Sut_in_tuple _
-  | Tuple_arity _ | Type_not_supported _ ->
+  | Impossible_term_substitution _ | Incompatible_type _
+  | Incomplete_ret_val_computation _ | No_spec _ | Returning_sut _
+  | Sut_as_type_inst _ | Sut_in_tuple _ | Tuple_arity _ | Type_not_supported _
+    ->
       W.Warning
   | Impossible_init_state_generation _ | Incompatible_sut _
   | Incomplete_configuration_module _ | No_configuration_file _
@@ -89,23 +86,14 @@ let pp_kind ppf kind =
       pf ppf "Skipping %s:@ %a%a%a" id text "functions with a ghost " text
         (match k with `Arg -> "argument" | `Ret -> "returned value")
         text " are not supported"
-  | Ignored_modifies ->
-      pf ppf "Skipping unsupported modifies clause:@ %a" text
-        "expected \"modifies x\" or \"modifies x.model\" where x is the SUT"
   | Incompatible_type (v, t) ->
       pf ppf "Skipping %s:@ %a%s" v text
         "the type of its SUT-type argument is incompatible with the configured \
          SUT type: "
         t
-  | Multiple_sut_arguments id ->
-      pf ppf "Skipping %s:@ %a" id text
-        "functions with multiple SUT arguments cannot be tested"
   | No_spec fct ->
       pf ppf "Skipping %s:@ %a" fct text
         "functions without specifications cannot be tested"
-  | Returned_tuple f ->
-      pf ppf "Skipping %s:@ %a" f text
-        "functions returning tuples are not supported yet"
   | Returning_sut id ->
       pf ppf "Skipping %s:@ %a" id text
         "functions returning a SUT nested inside another type cannot be tested"
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 0d8114cc..e6a44752 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -15,7 +15,6 @@ type W.kind +=
   | Ensures_not_found_for_ret_sut of (string * string list)
   | Functional_argument of string
   | Ghost_values of (string * [ `Arg | `Ret ])
-  | Ignored_modifies
   | Impossible_init_state_generation of init_state_error
   | Impossible_term_substitution of
       [ `Never | `New | `Old | `NotModel | `OutOfScope ]
@@ -23,14 +22,12 @@ type W.kind +=
   | Incompatible_type of (string * string)
   | Incomplete_configuration_module of [ `Init_sut | `Sut ]
   | Incomplete_ret_val_computation of string
-  | Multiple_sut_arguments of string
   | No_configuration_file of string
   | No_init_function of string
   | No_models of string
   | No_spec of string
   | No_sut_type of string
   | Not_a_structure of string
-  | Returned_tuple of string
   | Returning_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string

From c12abd48df7bda3bd056bee8042b6c7c1eb718b4 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 2 Oct 2024 09:44:24 +0200
Subject: [PATCH 03/14] Rename `Returning_sut` to `Returning_nested_sut`

---
 plugins/qcheck-stm/src/ir_of_gospel.ml | 4 ++--
 plugins/qcheck-stm/src/reserr.ml       | 6 +++---
 plugins/qcheck-stm/src/reserr.mli      | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml
index cc8946ed..d26a7b00 100644
--- a/plugins/qcheck-stm/src/ir_of_gospel.ml
+++ b/plugins/qcheck-stm/src/ir_of_gospel.ml
@@ -84,7 +84,7 @@ let ty_var_substitution config (vd : val_description) =
         | Some _ -> (
             match pos with
             | `Left -> error (Sut_as_type_inst value_name, ty.ptyp_loc)
-            | `Right -> error (Returning_sut value_name, ty.ptyp_loc))
+            | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
         | None ->
             let* _ = List.map (check pos) args |> sequence in
             ok ())
@@ -93,7 +93,7 @@ let ty_var_substitution config (vd : val_description) =
         | Some _ -> (
             match pos with
             | `Left -> error (Sut_in_tuple value_name, ty.ptyp_loc)
-            | `Right -> error (Returning_sut value_name, ty.ptyp_loc))
+            | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
         | None ->
             let* _ = List.map (check pos) elems |> sequence in
             ok ())
diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 33f12265..502a0a31 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -28,7 +28,7 @@ type W.kind +=
   | No_spec of string
   | No_sut_type of string
   | Not_a_structure of string
-  | Returning_sut of string
+  | Returning_nested_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string
   | Sut_type_not_specified of string
@@ -44,7 +44,7 @@ let level kind =
   | Constant_value _ | Ensures_not_found_for_next_state _
   | Ensures_not_found_for_ret_sut _ | Functional_argument _ | Ghost_values _
   | Impossible_term_substitution _ | Incompatible_type _
-  | Incomplete_ret_val_computation _ | No_spec _ | Returning_sut _
+  | Incomplete_ret_val_computation _ | No_spec _ | Returning_nested_sut _
   | Sut_as_type_inst _ | Sut_in_tuple _ | Tuple_arity _ | Type_not_supported _
     ->
       W.Warning
@@ -94,7 +94,7 @@ let pp_kind ppf kind =
   | No_spec fct ->
       pf ppf "Skipping %s:@ %a" fct text
         "functions without specifications cannot be tested"
-  | Returning_sut id ->
+  | Returning_nested_sut id ->
       pf ppf "Skipping %s:@ %a" id text
         "functions returning a SUT nested inside another type cannot be tested"
   | Impossible_term_substitution why ->
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index e6a44752..c0e06be0 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -28,7 +28,7 @@ type W.kind +=
   | No_spec of string
   | No_sut_type of string
   | Not_a_structure of string
-  | Returning_sut of string
+  | Returning_nested_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string
   | Sut_type_not_specified of string

From a681d8705d2dc9357f9fef17c269018ff88be7bb Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 15:15:33 +0200
Subject: [PATCH 04/14] Add `Reserr.traverse`

---
 plugins/qcheck-stm/src/reserr.ml  | 4 ++++
 plugins/qcheck-stm/src/reserr.mli | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 502a0a31..01675468 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -258,6 +258,10 @@ let app f r =
 
 let ( <*> ) = app
 
+let traverse f xs =
+  let cons_f x xs = List.cons <$> f x <*> xs in
+  List.fold_right cons_f xs (ok [])
+
 let sequence r =
   let rec aux = function
     | [] -> ok []
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index c0e06be0..f101ac97 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -49,6 +49,10 @@ val ( let* ) : 'a reserr -> ('a -> 'b reserr) -> 'b reserr
 val ( >>= ) : 'a reserr -> ('a -> 'b reserr) -> 'b reserr
 val ( and* ) : 'a reserr -> 'b reserr -> ('a * 'b) reserr
 
+val traverse : ('a -> 'b reserr) -> 'a list -> 'b list reserr
+(** [traverse f xs] maps [f] over [xs] and returns [ok] of the resulting list
+    iff it contains no [error] *)
+
 val sequence : 'a reserr list -> 'a list reserr
 (** [sequence rs] returns [ok] of the list of ['a] iff there is no [error] in
     [rs] *)

From ee0f919c41650f991a7e0a8af73da6d1a60a5adf Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 15:22:39 +0200
Subject: [PATCH 05/14] Add `Reserr.traverse_`

---
 plugins/qcheck-stm/src/reserr.ml  | 4 ++++
 plugins/qcheck-stm/src/reserr.mli | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 01675468..7f9f75fc 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -262,6 +262,10 @@ let traverse f xs =
   let cons_f x xs = List.cons <$> f x <*> xs in
   List.fold_right cons_f xs (ok [])
 
+let traverse_ f xs =
+  let f x u = f x >>= Fun.const u in
+  List.fold_right f xs (ok ())
+
 let sequence r =
   let rec aux = function
     | [] -> ok []
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index f101ac97..7850d544 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -53,6 +53,9 @@ val traverse : ('a -> 'b reserr) -> 'a list -> 'b list reserr
 (** [traverse f xs] maps [f] over [xs] and returns [ok] of the resulting list
     iff it contains no [error] *)
 
+val traverse_ : ('a -> 'b reserr) -> 'a list -> unit reserr
+(** [traverse_ f xs] is [traverse f xs] ignoring the returned list *)
+
 val sequence : 'a reserr list -> 'a list reserr
 (** [sequence rs] returns [ok] of the list of ['a] iff there is no [error] in
     [rs] *)

From 0945c1560f776ccda13f2bc820539889be20edd7 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Fri, 2 Aug 2024 16:18:16 +0200
Subject: [PATCH 06/14] Use `traverse` and `traverse_` when appropriate

---
 plugins/qcheck-stm/src/ir_of_gospel.ml | 14 ++++----------
 plugins/qcheck-stm/src/stm_of_ir.ml    |  4 ++--
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml
index d26a7b00..9c5d20c2 100644
--- a/plugins/qcheck-stm/src/ir_of_gospel.ml
+++ b/plugins/qcheck-stm/src/ir_of_gospel.ml
@@ -19,9 +19,7 @@ let no_functional_arg_or_big_tuple vd =
         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 ()
+    | Ptyp_tuple xs | Ptyp_constr (_, xs) -> traverse_ contains_arrow xs
     | _ -> ok ()
   in
   let rec aux ty =
@@ -85,18 +83,14 @@ let ty_var_substitution config (vd : val_description) =
             match pos with
             | `Left -> error (Sut_as_type_inst value_name, ty.ptyp_loc)
             | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
-        | None ->
-            let* _ = List.map (check pos) args |> sequence in
-            ok ())
+        | None -> traverse_ (check pos) args)
     | Ptyp_tuple elems -> (
         match List.find_opt (Cfg.is_sut config) elems with
         | Some _ -> (
             match pos with
             | `Left -> error (Sut_in_tuple value_name, ty.ptyp_loc)
             | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
-        | None ->
-            let* _ = List.map (check pos) elems |> sequence in
-            ok ())
+        | None -> traverse_ (check pos) elems)
     | _ -> ok ()
   in
   let rec aux insts ty =
@@ -295,7 +289,7 @@ let val_desc config state vd =
           failwith
             "shouldn't happen (only non labelled and ghost value are returned)"
     in
-    List.map p spec.sp_ret |> sequence
+    traverse p spec.sp_ret
   in
   let ret_values = List.map (returned_value_description spec) ret in
   let next_states = next_states suts state spec in
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index be1e6d51..82c0f5a8 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -272,12 +272,12 @@ let arb_cmd_case config value =
   in
   let gen_args =
     (* XXX TODO: use `requires` clauses to build smarter generators *)
-    List.map
+    traverse
       (fun (ty, _) -> exp_of_core_type ~use_small:is_create value.inst ty)
       value.args
   in
   let app l r = pexp_apply (evar "( <*> )") [ (Nolabel, l); (Nolabel, r) ] in
-  List.fold_left app fun_cstr <$> sequence gen_args
+  List.fold_left app fun_cstr <$> gen_args
 
 let arb_cmd config ir =
   let open Reserr in

From 243420ec88b190c89317ede1bdd63fadb9d18f66 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 15:25:43 +0200
Subject: [PATCH 07/14] Rewrite `Reserr.sequence` using `Reserr.traverse`

---
 plugins/qcheck-stm/src/reserr.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 7f9f75fc..6cdbe7e0 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -266,15 +266,7 @@ let traverse_ f xs =
   let f x u = f x >>= Fun.const u in
   List.fold_right f xs (ok ())
 
-let sequence r =
-  let rec aux = function
-    | [] -> ok []
-    | ((Ok _, _) as x) :: xs ->
-        let* y = x and* ys = aux xs in
-        ok (y :: ys)
-    | ((Error _, _) as x) :: _ -> x
-  in
-  aux r
+let sequence xs = traverse Fun.id xs
 
 let rec filter_errs = function
   | [] -> ok ()

From 912c3f244a8325a58e459fe219b819623856358f Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:32:24 +0200
Subject: [PATCH 08/14] Add `Reserr.promote_mapi`

---
 plugins/qcheck-stm/src/reserr.ml  | 14 ++++++++++++++
 plugins/qcheck-stm/src/reserr.mli |  3 +++
 2 files changed, 17 insertions(+)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 6cdbe7e0..0e50d394 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -286,6 +286,20 @@ let rec promote = function
       let* _ = warns ws and* _ = filter_errs errs in
       promote xs
 
+let promote_mapi f =
+  let rec aux i = function
+    | [] -> ok []
+    | x :: xs -> (
+        match f i x with
+        | (Ok _, _) as x ->
+            let* y = x and* ys = aux (i + 1) xs in
+            ok (y :: ys)
+        | Error errs, ws ->
+            let* _ = warns ws and* _ = filter_errs errs in
+            aux (i + 1) xs)
+  in
+  aux 0
+
 let promote_opt r =
   match r with
   | (Ok _, _) as x ->
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 7850d544..e41598b8 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -65,6 +65,9 @@ val promote : 'a reserr list -> 'a list reserr
     no [errors] of level [Error] in [rs] and store the [errors] of level
     [Warning] in the warnings list *)
 
+val promote_mapi : (int -> 'a -> 'b reserr) -> 'a list -> 'b list reserr
+(** [promote_mapi f xs] is [List.mapi f xs |> promote] with only one traversal *)
+
 val promote_opt : 'a reserr -> 'a option reserr
 (** [promote_opt r] is [promote] for a unique value *)
 

From 4320e577619225de56d0fb82a1f80b60781b5134 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:32:48 +0200
Subject: [PATCH 09/14] Use `Reserr.promote_mapi`

---
 plugins/qcheck-stm/src/stm_of_ir.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 82c0f5a8..549d5252 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -769,13 +769,12 @@ let postcond_case config state invariants idx state_ident new_state_ident value
               ret_id :: value.sut_vars
             else value.sut_vars
           in
-          List.mapi
+          promote_mapi
             (fun idx sut ->
               map
                 (fun t -> wrap_check t <$> translate_invariants idx sut id t)
                 xs)
             suts
-          |> promote
     in
     list_append (postcond @ List.concat invariants) |> ok
   in

From 82a2edd9eedd8a954045b1b1d715276a87c6eeb1 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:39:12 +0200
Subject: [PATCH 10/14] Rename map to promote_map

Make it clearer how errors are treated compared to traverse
---
 plugins/qcheck-stm/src/config.ml    |  6 +--
 plugins/qcheck-stm/src/reserr.ml    |  5 ++-
 plugins/qcheck-stm/src/reserr.mli   |  3 +-
 plugins/qcheck-stm/src/stm_of_ir.ml | 68 ++++++++++++++++-------------
 4 files changed, 46 insertions(+), 36 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index ac234a42..f60dada1 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -96,10 +96,10 @@ let rec acceptable_type_parameter param =
   let str = Fmt.str "%a" Ppxlib_ast.Pprintast.core_type param in
   match param.ptyp_desc with
   | Ptyp_constr (_, cts) ->
-      let* _ = map acceptable_type_parameter cts in
+      let* _ = promote_map acceptable_type_parameter cts in
       ok ()
   | Ptyp_tuple args ->
-      let* _ = map acceptable_type_parameter args in
+      let* _ = promote_map acceptable_type_parameter args in
       ok ()
   | Ptyp_var _ | Ptyp_any ->
       error (Type_parameter_not_instantiated str, Location.none)
@@ -110,7 +110,7 @@ let core_type_is_a_well_formed_sut (core_type : Ppxlib.core_type) =
   let open Reserr in
   match core_type.ptyp_desc with
   | Ptyp_constr (_lid, cts) ->
-      let* _ = map acceptable_type_parameter cts in
+      let* _ = promote_map acceptable_type_parameter cts in
       ok ()
   | _ ->
       let str = Fmt.str "%a" Ppxlib_ast.Pprintast.core_type core_type in
diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 0e50d394..eed6fdc4 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -286,6 +286,8 @@ let rec promote = function
       let* _ = warns ws and* _ = filter_errs errs in
       promote xs
 
+let promote_map f l = List.map f l |> promote
+
 let promote_mapi f =
   let rec aux i = function
     | [] -> ok []
@@ -323,5 +325,4 @@ let rec fold_left (f : 'a -> 'b -> 'a reserr) (acc : 'a) : 'b list -> 'a reserr
 
 let of_option ~default = Option.fold ~none:(error default) ~some:ok
 let to_option = function Ok x, _ -> Some x | _ -> None
-let map f l = List.map f l |> promote
-let concat_map f l = fmap List.concat (map f l)
+let concat_map f l = fmap List.concat (promote_map f l)
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index e41598b8..48cd18c9 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -65,6 +65,8 @@ val promote : 'a reserr list -> 'a list reserr
     no [errors] of level [Error] in [rs] and store the [errors] of level
     [Warning] in the warnings list *)
 
+val promote_map : ('a -> 'b reserr) -> 'a list -> 'b list reserr
+
 val promote_mapi : (int -> 'a -> 'b reserr) -> 'a list -> 'b list reserr
 (** [promote_mapi f xs] is [List.mapi f xs |> promote] with only one traversal *)
 
@@ -74,7 +76,6 @@ val promote_opt : 'a reserr -> 'a option reserr
 val fold_left : ('a -> 'b -> 'a reserr) -> 'a -> 'b list -> 'a reserr
 val of_option : default:W.t -> 'a option -> 'a reserr
 val to_option : 'a reserr -> 'a option
-val map : ('a -> 'b reserr) -> 'a list -> 'b list reserr
 val concat_map : ('a -> 'b list reserr) -> 'a list -> 'b list reserr
 val fmap : ('a -> 'b) -> 'a reserr -> 'b reserr
 val ( <$> ) : ('a -> 'b) -> 'a reserr -> 'b reserr
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 549d5252..9178ed07 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -196,11 +196,11 @@ let pat_of_core_type inst typ =
         and pat_arg =
           match xs with
           | [] -> ok None
-          | xs -> (fun xs -> Some (ppat_tuple xs)) <$> map aux xs
+          | xs -> (fun xs -> Some (ppat_tuple xs)) <$> promote_map aux xs
         in
         ppat_construct <$> constr_str <*> pat_arg
     | Ptyp_tuple xs ->
-        let* pat_arg = ppat_tuple <$> map aux xs in
+        let* pat_arg = ppat_tuple <$> promote_map aux xs in
         ppat_construct
           (lident ("Tup" ^ string_of_int (List.length xs)))
           (Some pat_arg)
@@ -230,13 +230,13 @@ let exp_of_core_type ?(use_small = false) inst typ =
             else constr_str |> ok
         | xs ->
             pexp_apply constr_str
-            <$> (List.map (fun e -> (Nolabel, e)) <$> map aux xs))
+            <$> (List.map (fun e -> (Nolabel, e)) <$> promote_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)
+        <$> (List.map (fun e -> (Nolabel, e)) <$> promote_map aux xs)
     | _ ->
         error
           ( Type_not_supported (Fmt.str "%a" Pprintast.core_type typ),
@@ -281,7 +281,7 @@ let arb_cmd_case config value =
 
 let arb_cmd config ir =
   let open Reserr in
-  let* cmds = elist <$> map (arb_cmd_case config) ir.values in
+  let* cmds = elist <$> promote_map (arb_cmd_case config) ir.values in
   let open Ppxlib in
   let let_open str e =
     pexp_open Ast_helper.(Opn.mk (Mod.ident (lident str |> noloc))) e
@@ -377,7 +377,7 @@ let run config ir =
   let cmd_name = gen_symbol ~prefix:"cmd" () in
   let sut_name = gen_symbol ~prefix:"sut" () in
   let open Reserr in
-  let* cases = map (run_case config sut_name) ir.values in
+  let* cases = promote_map (run_case config sut_name) ir.values in
   let body = pexp_match (evar cmd_name) cases in
   let pat = pvar "run" in
   let expr = efun [ (Nolabel, pvar cmd_name); (Nolabel, pvar sut_name) ] body in
@@ -421,7 +421,7 @@ let next_state_case state config state_ident nb_models value =
         List.filter (fun (id, _) -> List.mem id modified_suts) sut_map
       in
       let* next_states =
-        map
+        promote_map
           (fun (sut, next_state) ->
             (* substitute state variable when under `old` operator and translate description into ocaml *)
             let descriptions =
@@ -439,7 +439,7 @@ let next_state_case state config state_ident nb_models value =
               List.find_opt (fun (_, m, _) -> Ident.equal id m) descriptions
             in
             let* descriptions =
-              map
+              promote_map
                 (fun (id, loc) ->
                   of_option
                     ~default:
@@ -506,7 +506,7 @@ let next_state_case state config state_ident nb_models value =
       let new_state = pexp_let Nonrecursive vbs_next_states push_expr in
       let idx = List.fold_left (fun acc (i, _, _) -> i @ acc) [] next_states in
       let translate_checks = translate_checks config state value sut_map in
-      let* checks = map translate_checks value.postcond.checks in
+      let* checks = promote_map translate_checks value.postcond.checks in
       match checks with
       | [] -> ok (idx, wrap new_state)
       | _ ->
@@ -525,7 +525,7 @@ let next_state config ir =
   let nb_models = List.length ir.state in
   let open Reserr in
   let* idx_cases =
-    map
+    promote_map
       (fun v ->
         let* i, c = next_state_case ir.state config state_ident nb_models v in
         ok ((v.id, i), c))
@@ -546,7 +546,7 @@ let precond_case config state state_ident value =
     let vbs, sut_map = pop_states state_ident value in
     let wrap e = (if vbs <> [] then pexp_let Nonrecursive vbs e else e) |> ok in
     list_and
-    <$> map
+    <$> promote_map
           (fun t ->
             subst_term state ~gos_t:value.sut_vars ~old_t:[] ~new_t:sut_map t
             >>= ocaml_of_term config)
@@ -560,7 +560,9 @@ let precond config ir =
   let state_name = gen_symbol ~prefix:"state" () in
   let state_ident = Ident.create ~loc:Location.none state_name in
   let open Reserr in
-  let* cases = map (precond_case config ir.state state_ident) ir.values in
+  let* cases =
+    promote_map (precond_case config ir.state state_ident) ir.values
+  in
   let body = pexp_match (evar cmd_name) cases in
   let pat = pvar "precond" in
   let expr =
@@ -585,12 +587,12 @@ let expected_returned_value translate_postcond value =
   | Ptyp_constr ({ txt = Lident "unit"; _ }, _), _ -> ret_res ty_show eunit
   | Ptyp_constr ({ txt = Lident "int"; _ }, _), [ (t :: _ as xs) ]
     when t.term.t_ty = Some Gospel.Ttypes.ty_integer ->
-      map translate_postcond xs
+      promote_map translate_postcond xs
       |> to_option
       >>= Fun.flip List.nth_opt 0
       >>= ret_res (Some ty_show_integer)
   | _, [ xs ] ->
-      map translate_postcond xs
+      promote_map translate_postcond xs
       |> to_option
       >>= Fun.flip List.nth_opt 0
       >>= ret_res ty_show
@@ -753,7 +755,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
     in
     (* [postcond] and [invariants] are specification of normal behaviour *)
     let* postcond =
-      map (fun t -> wrap_check t <$> translate_postcond t) normal
+      promote_map (fun t -> wrap_check t <$> translate_postcond t) normal
       (* only functions that do not return a sut can have postconditions
          referring to the returned value, therefore no shifting is needed *)
     and* invariants =
@@ -771,7 +773,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
           in
           promote_mapi
             (fun idx sut ->
-              map
+              promote_map
                 (fun t -> wrap_check t <$> translate_invariants idx sut id t)
                 xs)
             suts
@@ -796,7 +798,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
       in
       let* cases_error =
         Fun.flip ( @ ) [ case ~lhs:ppat_any ~guard:None ~rhs:enone ]
-        <$> map
+        <$> promote_map
               (fun (x, p, t) ->
                 let xstr = Fmt.str "%a" Ident.pp x.Gospel.Ttypes.xs_ident in
                 let lhs =
@@ -836,7 +838,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value
       fun t -> wrap <$> translate_checks config state value sut_map t
     in
     let* checks =
-      map
+      promote_map
         (fun t ->
           wrap_check ~exn:(Some "Invalid_argument") t <$> translate_checks t)
         value.postcond.checks
@@ -889,7 +891,7 @@ let postcond config idx ir =
   let open Reserr in
   let* cases =
     (Fun.flip ( @ )) [ case ~lhs:ppat_any ~guard:None ~rhs:enone ]
-    <$> map
+    <$> promote_map
           (fun v ->
             postcond_case config ir.state ir.invariants (List.assoc v.id idx)
               state_ident new_state_ident v)
@@ -948,11 +950,12 @@ let pp_cmd_case config value =
   let rec pp_of_ty ty : expression reserr =
     match ty.ptyp_desc with
     | Ptyp_tuple xs ->
-        let* pps = map pp_of_ty xs in
+        let* pps = promote_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* xs = promote_map pp_of_ty xs
+        and* s = munge_longident false ty lid in
         let pp = qualify_pp ("pp_" ^ s) in
         ok
           (match xs with
@@ -997,7 +1000,7 @@ let pp_cmd_case config value =
 let cmd_show config ir =
   let cmd_name = gen_symbol ~prefix:"cmd" () in
   let open Reserr in
-  let* cases = map (pp_cmd_case config) ir.values in
+  let* cases = promote_map (pp_cmd_case config) ir.values in
   let body = pexp_match (evar cmd_name) cases in
   let pat = pvar "show_cmd" in
   let expr = efun [ (Nolabel, pvar cmd_name) ] body in
@@ -1064,9 +1067,11 @@ let init_state config ir =
     in
     ok (model, desc)
   in
-  let* fields = map translate_field_desc ir.Ir.init_state.descriptions in
   let* fields =
-    map
+    promote_map translate_field_desc ir.Ir.init_state.descriptions
+  in
+  let* fields =
+    promote_map
       (fun (id, _) ->
         (fun d -> (longident_loc_of_ident id, d))
         <$> (List.assoc_opt id fields
@@ -1139,7 +1144,7 @@ let check_init_state config ir =
             [ value_binding ~pat:state_pat ~expr:init_state ]
             (pexp_ifthenelse (list_or xs) msg None))
     <$> Option.fold ~none:(ok [])
-          ~some:(fun (id, xs) -> map (translate_invariants id) xs)
+          ~some:(fun (id, xs) -> promote_map (translate_invariants id) xs)
           ir.invariants
   in
   let pat = pvar "check_init_state" and expr = efun [ (Nolabel, punit) ] expr in
@@ -1195,7 +1200,7 @@ let ghost_types config =
       | Gospel.Tast.Recursive -> Recursive
     in
     let* tds =
-      map
+      promote_map
         (fun td ->
           try
             ok
@@ -1206,7 +1211,7 @@ let ghost_types config =
     in
     ok (pstr_type rec_flag tds)
   in
-  map aux
+  promote_map aux
 
 let agree_prop =
   [%stri
@@ -1389,11 +1394,12 @@ let pp_ortac_cmd_case config suts last value =
   let rec pp_of_ty ty : expression reserr =
     match ty.ptyp_desc with
     | Ptyp_tuple xs ->
-        let* pps = map pp_of_ty xs in
+        let* pps = promote_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* xs = promote_map pp_of_ty xs
+        and* s = munge_longident false ty lid in
         let pp = qualify_pp ("pp_" ^ s) in
         ok
           (match xs with
@@ -1494,7 +1500,9 @@ let ortac_cmd_show config ir =
   let res_name = gen_symbol ~prefix:"res" () in
   let last_name = gen_symbol ~prefix:"last" () in
   let open Reserr in
-  let* cases = map (pp_ortac_cmd_case config suts_name last_name) ir.values in
+  let* cases =
+    promote_map (pp_ortac_cmd_case config suts_name last_name) ir.values
+  in
   let default_case =
     case ~lhs:ppat_any ~guard:None ~rhs:(eapply (evar "assert") [ ebool false ])
   in

From 1e0631b5ddfa5c154b7e229d1057256f493b9689 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:46:15 +0200
Subject: [PATCH 11/14] Improve `promote_map` implementation

---
 plugins/qcheck-stm/src/reserr.ml  | 14 +++++++++++++-
 plugins/qcheck-stm/src/reserr.mli |  1 +
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index eed6fdc4..d0fc7ccb 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -286,7 +286,19 @@ let rec promote = function
       let* _ = warns ws and* _ = filter_errs errs in
       promote xs
 
-let promote_map f l = List.map f l |> promote
+let promote_map f =
+  let rec aux = function
+    | [] -> ok []
+    | x :: xs -> (
+        match f x with
+        | (Ok _, _) as x ->
+            let* y = x and* ys = aux xs in
+            ok (y :: ys)
+        | Error errs, ws ->
+            let* _ = warns ws and* _ = filter_errs errs in
+            aux xs)
+  in
+  aux
 
 let promote_mapi f =
   let rec aux i = function
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 48cd18c9..d62277f5 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -66,6 +66,7 @@ val promote : 'a reserr list -> 'a list reserr
     [Warning] in the warnings list *)
 
 val promote_map : ('a -> 'b reserr) -> 'a list -> 'b list reserr
+(** [promote_map f xs] is [List.map f xs |> promote] with only one traversal *)
 
 val promote_mapi : (int -> 'a -> 'b reserr) -> 'a list -> 'b list reserr
 (** [promote_mapi f xs] is [List.mapi f xs |> promote] with only one traversal *)

From d8fe270b86933cb4e17f8db4c856b5d077daf124 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:50:30 +0200
Subject: [PATCH 12/14] Remove `Reserr.concat_map`

It wasn't used and its implementation was not particularly clever
---
 plugins/qcheck-stm/src/reserr.ml  | 1 -
 plugins/qcheck-stm/src/reserr.mli | 1 -
 2 files changed, 2 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index d0fc7ccb..a2c44cb3 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -337,4 +337,3 @@ let rec fold_left (f : 'a -> 'b -> 'a reserr) (acc : 'a) : 'b list -> 'a reserr
 
 let of_option ~default = Option.fold ~none:(error default) ~some:ok
 let to_option = function Ok x, _ -> Some x | _ -> None
-let concat_map f l = fmap List.concat (promote_map f l)
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index d62277f5..156c3249 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -77,7 +77,6 @@ val promote_opt : 'a reserr -> 'a option reserr
 val fold_left : ('a -> 'b -> 'a reserr) -> 'a -> 'b list -> 'a reserr
 val of_option : default:W.t -> 'a option -> 'a reserr
 val to_option : 'a reserr -> 'a option
-val concat_map : ('a -> 'b list reserr) -> 'a list -> 'b list reserr
 val fmap : ('a -> 'b) -> 'a reserr -> 'b reserr
 val ( <$> ) : ('a -> 'b) -> 'a reserr -> 'b reserr
 val app : ('a -> 'b) reserr -> 'a reserr -> 'b reserr

From 913312106e2c9cc5d47a41125aa9024ca38a802e Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 14:52:26 +0200
Subject: [PATCH 13/14] Remove type signature from `Reserr.fold_left`
 implementation

---
 plugins/qcheck-stm/src/reserr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index a2c44cb3..40217210 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -323,8 +323,7 @@ let promote_opt r =
       let* _ = warns ws and* _ = filter_errs errs in
       ok None
 
-let rec fold_left (f : 'a -> 'b -> 'a reserr) (acc : 'a) : 'b list -> 'a reserr
-    = function
+let rec fold_left f acc = function
   | [] -> ok acc
   | x :: xs -> (
       match f acc x with

From 3575bb65454c755f76fe453cbf93b9a48cf0daca Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 5 Sep 2024 15:57:44 +0200
Subject: [PATCH 14/14] Update Changelog

---
 CHANGES.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index eeff9fb3..84c26032 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,8 @@
 # Unreleased
 
+- Add `Reserr.{traverse,traverse_,promote_mapi}`, rename `Reserr.map` to
+  `Reserr.promote_map` and remove `Reserr.concat_map`
+  [\#250](https://github.com/ocaml-gospel/ortac/pull/250)
 - Fix display of the runnable scenario for protected values
   [\#251](https://github.com/ocaml-gospel/ortac/pull/251)
 - Fix sut as type argument or inside tuple bug