From deb16c3f1407db876d2493ab61cd65010dac4c71 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 00:36:14 +0100
Subject: Add a check to detect if forward/backward translations are mutually
 recursive

---
 src/Translate.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src')

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 =
-- 
cgit v1.2.3