Merge pull request ocaml-gospel#250 from n-osborne/refactor-reserr

Some refactoring of `Reserr`

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

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

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 =
@@ -84,19 +82,15 @@ 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))
-        | None ->
-            let* _ = List.map (check pos) args |> sequence in
-            ok ())
+            | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
+        | 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_sut value_name, ty.ptyp_loc))
-        | None ->
-            let* _ = List.map (check pos) elems |> sequence in
-            ok ())
+            | `Right -> error (Returning_nested_sut value_name, ty.ptyp_loc))
+        | 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

plugins/qcheck-stm/src/reserr.ml

@@ -15,23 +15,20 @@ 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 ]
   | Incompatible_sut of string
   | 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
+  | Returning_nested_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string
   | Sut_type_not_specified 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_nested_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 _
@@ -60,43 +57,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
@@ -126,24 +86,15 @@ 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 ->
+  | 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 ->
@@ -270,15 +221,52 @@ 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)
 
-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
+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
-  aux r
+  (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 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 xs = traverse Fun.id xs
 
 let rec filter_errs = function
   | [] -> ok ()
@@ -298,6 +286,34 @@ let rec promote = function
       let* _ = warns ws and* _ = filter_errs errs in
       promote xs
 
+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
+    | [] -> 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 ->
@@ -307,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
@@ -321,5 +336,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 map f l = List.map f l |> promote
-let concat_map f l = fmap List.concat (map f l)

plugins/qcheck-stm/src/reserr.mli

@@ -15,23 +15,20 @@ 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 ]
   | Incompatible_sut of string
   | 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
+  | Returning_nested_sut of string
   | Sut_as_type_inst of string
   | Sut_in_tuple of string
   | Sut_type_not_specified of string
@@ -52,6 +49,13 @@ 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 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] *)
@@ -61,14 +65,18 @@ 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
+(** [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 *)
+
 val promote_opt : 'a reserr -> 'a option reserr
 (** [promote_opt r] is [promote] for a unique value *)
 
 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
 val app : ('a -> 'b) reserr -> 'a reserr -> 'b reserr