summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/SymbolicToPure.ml51
1 files changed, 26 insertions, 25 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3d955061..ef0a0bde 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1137,39 +1137,30 @@ let compute_back_tys (dsg : Pure.decomposed_fun_sig) : ty list =
mk_arrows inputs output)
(RegionGroupId.Map.values dsg.back_sg)
-(** Return the pure signature of a backward function, in the case the
- forward/backward functions are merged (i.e., the forward functions
+(** Return the instantiated pure signature of a backward function, in the
+ case the forward/backward functions are merged (i.e., the forward functions
return the backward functions).
-
- TODO: merge with {!translate_fun_sig_from_decomposed}
*)
-let translate_ret_back_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
- (gid : RegionGroupId.id) : fun_sig =
+let translate_ret_back_inst_fun_sig_from_decomposed
+ (dsg : Pure.decomposed_fun_sig) (generics : generic_args)
+ (gid : RegionGroupId.id) : inst_fun_sig =
assert !Config.return_back_funs;
-
- let generics = dsg.generics in
- let llbc_generics = dsg.llbc_generics in
- let preds = dsg.preds in
- (* Compute the effects info *)
- let fwd_info = dsg.fwd_info in
- let back_effect_info =
- RegionGroupId.Map.of_list
- (List.map
- (fun ((gid, info) : RegionGroupId.id * back_sg_info) ->
- (gid, info.effect_info))
- (RegionGroupId.Map.bindings dsg.back_sg))
- in
- (* Two cases depending on whether we split the forward/backward functions
- or not *)
let mk_output_ty = mk_output_ty_from_effect_info in
-
+ (* Lookup the signature information *)
let back_sg = RegionGroupId.Map.find gid dsg.back_sg in
let effect_info = back_sg.effect_info in
(* Do not prepend the forward inputs *)
let inputs = List.map snd back_sg.inputs in
let output = mk_simpl_tuple_ty back_sg.outputs in
let output = mk_output_ty effect_info output in
- { generics; llbc_generics; preds; inputs; output; fwd_info; back_effect_info }
+ (* Substitute the types *)
+ let tr_self = UnknownTrait __FUNCTION__ in
+ let subst = make_subst_from_generics dsg.generics generics tr_self in
+ let subst = ty_substitute subst in
+ let inputs = List.map subst inputs in
+ let output = subst output in
+ (* Return *)
+ { inputs; output }
let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
(gid : RegionGroupId.id option) : fun_sig =
@@ -1898,12 +1889,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
call.regions_hierarchy
in
let back_sgs =
- List.map (translate_ret_back_fun_sig_from_decomposed dsg) gids
+ List.map
+ (translate_ret_back_inst_fun_sig_from_decomposed dsg generics)
+ gids
in
(* Introduce variables for the backward functions *)
let back_tys =
List.map
- (fun (sg : fun_sig) -> mk_arrows sg.inputs sg.output)
+ (fun (sg : inst_fun_sig) -> mk_arrows sg.inputs sg.output)
back_sgs
in
(* Compute a proper basename for the variables *)
@@ -2216,6 +2209,14 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
(fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
(List.combine inputs args_mplaces)
in
+ log#ldebug
+ (lazy
+ (let args = List.map (texpression_to_string ctx) args in
+ "func: "
+ ^ texpression_to_string ctx func
+ ^ "\nfunc type: "
+ ^ pure_ty_to_string ctx func.ty
+ ^ "\n\nargs:\n" ^ String.concat "\n" args));
let call = mk_apps func args in
(* **Optimization**:
=================