From 795e2107e305d425efdf6071b29f186cae83656b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 11:56:09 +0200 Subject: Update the names of the synthesized backward functions --- compiler/SymbolicToPure.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 0c30f44c..7e970029 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1502,6 +1502,15 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) match ty with None -> None | Some ty -> Some (name, ty)) back_vars in + (* If there is one backward function or less, we use the name "back" + (there is no point in using the lifetime name, and it makes the + code generation more stable) *) + let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in + let back_vars = + if num_back_vars = 1 then + List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars + else back_vars + in fresh_opt_vars back_vars ctx (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *) -- cgit v1.2.3 From bac38f94aacf4a0d621b0b2d2c423db9e0c6f175 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 13:21:08 +0200 Subject: Improve the name of the backward functions further --- compiler/SymbolicToPure.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 7e970029..67fd2c9b 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1499,7 +1499,14 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) let back_vars = List.map (fun (name, ty) -> - match ty with None -> None | Some ty -> Some (name, ty)) + match ty with + | None -> None + | Some ty -> + (* If the type is not an arrow type, don't use the name "back" + (it is a backward function with no inputs, that is to say a + value) *) + let name = if is_arrow_ty ty then name else None in + Some (name, ty)) back_vars in (* If there is one backward function or less, we use the name "back" @@ -1508,7 +1515,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in let back_vars = if num_back_vars = 1 then - List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars + List.map + (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty))) + back_vars else back_vars in fresh_opt_vars back_vars ctx -- cgit v1.2.3 From ec7a1d3c94846a94481a487dd077efb6ddb108fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 13:27:02 +0200 Subject: Make a minor update in SymbolicToPure --- compiler/SymbolicToPure.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 67fd2c9b..5cd13072 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2258,15 +2258,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (fun ty -> match ty with | None -> None - | Some (back_sg, ty) -> - (* We insert a name for the variable only if the function - can fail: if it can fail, it means the call returns a backward - function. Otherwise, it directly returns the value given - back by the backward function, which means we shouldn't - give it a name like "back..." (it doesn't make sense) *) + | Some (_back_sg, ty) -> + (* We insert a name for the variable only if the type + is an arrow type. If it is not, it means the backward + function is degenerate (it takes no inputs) so it is + not a function anymore but a value: it doesn't make + sense to use a name like "back...". *) let name = - if back_sg.effect_info.can_fail then Some back_fun_name - else None + if is_arrow_ty ty then Some back_fun_name else None in Some (name, ty)) back_tys) -- cgit v1.2.3