Add the merge_returns configuration option

CHANGELOG.md

@@ -1,4 +1,5 @@
 ## [Unreleased]
+* Add the configuration option `merge_returns`.
 * Add the configuration option `merge_types`.
 * Add the configuration options `monadic_lets` (renaming of `monadic_bind`), `monadic_let_returns`, `monadic_rets` and `monadic_ret_lets`.
 * Add a `@coq_plain_module` attribute to force a module to be compiled as a plain module.

doc/docs/configuration.md

@@ -203,6 +203,40 @@ A string to add in the header of each file.
 #### Explanation
 We can use this option to add some default imports, or turn on some notations or flags.
 
+## merge_returns
+#### Example
+```
+"merge_returns": [
+ ["return=", "return?", "return=?"]
+]
+```
+
+#### Value
+A list of triple of strings, with two return operator names which get translated into a third when applied together.
+
+#### Explanation
+We use this configuration option to merge two return operators to a third equivalent one. Note that this only applies to monadic return operators, which are generated by the monadic configuration options. This option does not apply to standard function applications. As an example, we can generate the following code:
+```coq
+let= ctxt :=
+ (|Storage.Contract.Frozen_rewards|).(Storage_sigs.Indexed_data_storage.remove)
+ (ctxt, contract) cycle in
+return=?
+ (ctxt,
+ {| frozen_balance.deposit := deposit; frozen_balance.fees := fees;
+ frozen_balance.rewards := rewards |}).
+```
+instead of:
+```coq
+let= ctxt :=
+ (|Storage.Contract.Frozen_rewards|).(Storage_sigs.Indexed_data_storage.remove)
+ (ctxt, contract) cycle in
+return=
+ (return?
+ (ctxt,
+ {| frozen_balance.deposit := deposit; frozen_balance.fees := fees;
+ frozen_balance.rewards := rewards |})).
+```
+
 ## merge_types
 #### Example
 ```

src/configuration.ml

@@ -60,6 +60,7 @@ type t = {
  file_name : string;
  first_class_module_path_blacklist : string list;
  head_suffix : string;
+ merge_returns : MergeRule.t list;
  merge_types : MergeRule.t list;
  monadic_lets : MonadicOperator.t list;
  monadic_let_returns : MonadicOperators.t list;
@@ -86,6 +87,7 @@ let default (file_name : string) : t = {
  file_name;
  first_class_module_path_blacklist = [];
  head_suffix = "";
+ merge_returns = [];
  merge_types = [];
  monadic_lets = [];
  monadic_let_returns = [];
@@ -140,6 +142,16 @@ let is_in_first_class_module_backlist (configuration : t) (path : Path.t)
  let path = String.concat "." (List.rev path) in
  List.mem path configuration.first_class_module_path_blacklist
 
+let is_in_merge_returns
+ (configuration : t) (source1 : string) (source2 : string) : string option =
+ configuration.merge_returns |> Util.List.find_map
+ (fun (merge_rule : MergeRule.t) ->
+ if source1 = merge_rule.source1 && source2 = merge_rule.source2 then
+ Some merge_rule.target
+ else
+ None
+ )
+
 let is_in_merge_types
  (configuration : t) (source1 : string) (source2 : string) : string option =
  configuration.merge_types |> Util.List.find_map
@@ -308,6 +320,14 @@ let of_json (file_name : string) (json : Yojson.Basic.t) : t =
  | "head_suffix" ->
  let entry = get_string "head_suffix" entry in
  {configuration with head_suffix = entry}
+ | "merge_returns" ->
+ let entry =
+ entry |>
+ get_string_triple_list "merge_returns" |>
+ List.map (fun (source1, source2, target) ->
+ { MergeRule.source1; source2; target }
+ ) in
+ {configuration with merge_returns = entry}
  | "merge_types" ->
  let entry =
  entry |>

src/exp.ml

@@ -224,17 +224,25 @@ let build_module
  ) in
  return (Module (module_typ_params, fields))
 
-let rec smart_return (operator : string) (e : t) : t =
+let rec smart_return (operator : string) (e : t) : t Monad.t =
  match e with
+ | Return (operator2, e2) ->
+ let* configuration = get_configuration in
+ begin match Configuration.is_in_merge_returns configuration operator operator2 with
+ | None -> return (Return (operator, e))
+ | Some target -> return (Return (target, e2))
+ end
  | LetVar (None, x, typ_params, e1, e2) ->
- LetVar (None, x, typ_params, e1, smart_return operator e2)
+ let* e2 = smart_return operator e2 in
+ return (LetVar (None, x, typ_params, e1, e2))
  | Match (e, cases, is_with_default_case) ->
- let cases =
- cases |> List.map (fun (p, existential_cast, e) ->
- (p, existential_cast, smart_return operator e)
+ let* cases =
+ cases |> Monad.List.map (fun (p, existential_cast, e) ->
+ let* e = smart_return operator e in
+ return (p, existential_cast, e)
  ) in
- Match (e, cases, is_with_default_case)
- | _ -> Return (operator, e)
+ return (Match (e, cases, is_with_default_case))
+ | _ -> return (Return (operator, e))
 
 (** Import an OCaml expression. *)
 let rec of_expression (typ_vars : Name.t Name.Map.t) (e : expression)
@@ -329,7 +337,7 @@ let rec of_expression (typ_vars : Name.t Name.Map.t) (e : expression)
  | None -> None
  end
  | _ -> None in
- let apply_with_let_return =
+ let* apply_with_let_return =
  match (e_f, e_xs) with
  | (
  Variable (MixedPath.PathName path_name, []),
@@ -338,25 +346,26 @@ let rec of_expression (typ_vars : Name.t Name.Map.t) (e : expression)
  let name = PathName.to_string path_name in
  begin match Configuration.is_monadic_let_return configuration name with
  | Some (let_symbol, return_notation) ->
- Some (LetVar (
- Some let_symbol, x, [], e1, smart_return return_notation e2
- ))
- | None -> None
+ let* return_e2 = smart_return return_notation e2 in
+ return (Some (LetVar ( Some let_symbol, x, [], e1, return_e2)))
+ | None -> return None
  end
- | _ -> None in
- let apply_with_return =
+ | _ -> return None in
+ let* apply_with_return =
  match (e_f, e_xs) with
  | (
  Variable (MixedPath.PathName path_name, []),
  [e]
  ) ->
  let name = PathName.to_string path_name in
  begin match Configuration.is_monadic_return configuration name with
- | Some return_notation -> Some (smart_return return_notation e)
- | None -> None
+ | Some return_notation ->
+ let* return_e = smart_return return_notation e in
+ return (Some return_e)
+ | None -> return None
  end
- | _ -> None in
- let apply_with_return_let =
+ | _ -> return None in
+ let* apply_with_return_let =
  match (e_f, e_xs) with
  | (
  Variable (MixedPath.PathName path_name, []),
@@ -365,12 +374,13 @@ let rec of_expression (typ_vars : Name.t Name.Map.t) (e : expression)
  let name = PathName.to_string path_name in
  begin match Configuration.is_monadic_return_let configuration name with
  | Some (return_notation, let_symbol) ->
- Some (
- LetVar (Some let_symbol, x, [], smart_return return_notation e1, e2)
- )
- | None -> None
+ let* return_e1 = smart_return return_notation e1 in
+ return (Some (
+ LetVar (Some let_symbol, x, [], return_e1, e2)
+ ))
+ | None -> return None
  end
- | _ -> None in
+ | _ -> return None in
  let applies = [
  apply_with_let;
  apply_with_let_return;