Merge pull request #111 from AeneasVerif/son/names

Improve the names used for the variables in the generated code

3 files changed, 38 insertions, 14 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..0a7c8df2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1662,9 +1662,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
   in
   (* If there is a basename, we use it *)
   match basename with
-  | Some basename ->
+  | Some basename -> (
       (* This should be a no-op *)
-      to_snake_case basename
+      match !Config.backend with
+      | Lean -> basename
+      | FStar | Coq | HOL4 -> to_snake_case basename)
   | None -> (
       (* No basename: we use the first letter of the type *)
       match ty with
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..6f44bb74 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
 
+let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
+  match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None
+
+let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
+
 let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
-  match ty with
-  | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
-  | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+  match opt_dest_arrow_ty ty with
+  | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+  | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
 
 let compute_literal_type (cv : literal) : literal_type =
   match cv with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..5cd13072 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1499,9 +1499,27 @@ 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"
+     (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 (name, ty) -> (Option.map (fun _ -> "back") name, 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} *)
@@ -2240,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)