summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-09 00:36:14 +0100
committerSon Ho2022-02-09 00:36:14 +0100
commitdeb16c3f1407db876d2493ab61cd65010dac4c71 (patch)
treec93120fdac6187f93380d3025adc8a452fb6b2d0
parent03ffaf947ae7810c0c0928616ee0aaea7c258e4f (diff)
Add a check to detect if forward/backward translations are mutually
recursive
-rw-r--r--src/Translate.ml11
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 =