diff options
| -rw-r--r-- | src/PureUtils.ml | 18 |
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 |