Update PureUtils.functions_not_mutually_recursive

1 files changed, 9 insertions, 9 deletions

diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index e0703d30..dfa8c1a3 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -147,11 +147,10 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
 (** Return true if a list of functions are *not* mutually recursive, false otherwise.
     This function is meant to be applied on a set of (forward, backwards) functions
     generated for one recursive function.
-    The way we do the test is very simple: if any function body references another
-    function from the set, we consider the whole set is mutually recursive. Otherwise,
-    we consider it is not the case. Note that this check is conservative, making
-    it sound (also note that if the test is wrong, the code generated by the synthesis
-    will not be valid anyway...)
+    The way we do the test is very simple:
+    - we explore the functions one by one, in the order
+    - if all functions only call functions we already explored, they are not
+      mutually recursive
  *)
 let functions_not_mutually_recursive (funs : fun_def list) : bool =
   (* Compute the set of function identifiers in the group *)
@@ -161,18 +160,19 @@ let functions_not_mutually_recursive (funs : fun_def list) : bool =
          (fun (f : fun_def) -> Regular (A.Local f.def_id, f.back_id))
          funs)
   in
+  let ids = ref ids in
   (* Explore every body *)
   let body_only_calls_itself (fdef : fun_def) : bool =
-    let other_ids =
-      FunIdSet.remove (Regular (A.Local fdef.def_id, fdef.back_id)) ids
-    in
+    (* Remove the current id from the id set *)
+    ids := FunIdSet.remove (Regular (A.Local fdef.def_id, fdef.back_id)) !ids;
 
+    (* Check if we call functions from the updated id set *)
     let obj =
       object
         inherit [_] iter_expression as super
 
         method! visit_call env call =
-          if FunIdSet.mem call.func other_ids then raise Utils.Found
+          if FunIdSet.mem call.func !ids then raise Utils.Found
           else super#visit_call env call
       end
     in