diff options
Diffstat (limited to 'src/SymbolicToPure.ml')
-rw-r--r-- | src/SymbolicToPure.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index e32e28d6..18e2b873 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1045,10 +1045,12 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (List.combine args args_mplaces) in let dest_v = mk_typed_lvalue_from_var dest dest_mplace in - let call = { func; type_params; args } in - let call = Call call in - let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in - let call = { e = call; ty = call_ty } in + let func = { func; type_params } in + let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in + let ret_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in + let func_ty = mk_arrows input_tys ret_ty in + let func = { e = Func func; ty = func_ty } in + let call = mk_apps func args in (* Translate the next expression *) let next_e = translate_expression config e ctx in (* Put together *) @@ -1177,9 +1179,12 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) (List.combine inputs args_mplaces) in let monadic = fun_is_monadic fun_id in - let call = { func; type_params; args } in - let call_ty = mk_result_ty output.ty in - let call = { e = Call call; ty = call_ty } in + let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in + let ret_ty = if monadic then mk_result_ty output.ty else output.ty in + let func_ty = mk_arrows input_tys ret_ty in + let func = { func; type_params } in + let func = { e = Func func; ty = func_ty } in + let call = mk_apps func args in (* **Optimization**: * ================= * We do a small optimization here: if the backward function doesn't |