diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Main.ml | 3 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 19 |
2 files changed, 15 insertions, 7 deletions
diff --git a/compiler/Main.ml b/compiler/Main.ml index 835b9088..abc27b46 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -120,6 +120,9 @@ let () = " Generate a default lakefile.lean (Lean only)" ); ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC"); ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error"); + ( "-split-fwd-back", + Arg.Clear return_back_funs, + " Split the forward and backward functions." ); ] in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 41922cb5..4674b61c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1076,16 +1076,20 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let inputs_no_state = List.map (fun ty -> (Some "ret", ty)) inputs_no_state in - (* We consider the backward function as stateful and potentially failing + (* In case we merge the forward/backward functions: + we consider the backward function as stateful and potentially failing **only if it has inputs** (for the "potentially failing": if it has not inputs, we directly evaluate it in the body of the forward function). *) let back_effect_info = - { - back_effect_info with - stateful = back_effect_info.stateful && inputs_no_state <> []; - can_fail = back_effect_info.can_fail && inputs_no_state <> []; - } + if !Config.return_back_funs then + let b = inputs_no_state <> [] in + { + back_effect_info with + stateful = back_effect_info.stateful && b; + can_fail = back_effect_info.can_fail && b; + } + else back_effect_info in let state = if back_effect_info.stateful then [ (None, mk_state_ty) ] else [] @@ -1093,7 +1097,8 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let inputs = inputs_no_state @ state in let output_names, outputs = compute_back_outputs_for_gid gid in let filter = - !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] + !Config.simplify_merged_fwd_backs + && !Config.return_back_funs && inputs = [] && outputs = [] in let info = { |