Add a check to detect if forward/backward translations are mutually

recursive

1 files changed, 10 insertions, 1 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index 913c5cf8..3781fc33 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -371,10 +371,19 @@ let translate_module (filename : string) (dest_dir : string)
   let export_functions (is_rec : bool) (pure_ls : pure_fun_translation list) :
       unit =
     (* Generate the function definitions *)
-    let is_mut_rec = is_rec && pure_ls <> [] in
     let fls =
       List.concat (List.map (fun (fwd, back_ls) -> fwd :: back_ls) pure_ls)
     in
+    (* Check if the functions are mutually recursive - this really works
+     * to check if the forward and backward translations of a single
+     * recursive function are mutually recursive *)
+    let is_mut_rec =
+      if is_rec then
+        if List.length pure_ls <= 1 then
+          not (PureUtils.functions_not_mutually_recursive fls)
+        else true
+      else false
+    in
     List.iteri
       (fun i def ->
         let qualif =