summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-04-04 11:56:09 +0200
committerSon Ho2024-04-04 11:56:09 +0200
commit795e2107e305d425efdf6071b29f186cae83656b (patch)
tree8f1cf29f3a25d6e36b323045a1108aef5b50a917
parent88cb18c614819f4abba1e0dfdb80c455d334d595 (diff)
Update the names of the synthesized backward functions
-rw-r--r--compiler/ExtractBase.ml6
-rw-r--r--compiler/SymbolicToPure.ml9
2 files changed, 13 insertions, 2 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/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} *)