diff options
| author | Son Ho | 2024-04-04 11:56:09 +0200 |
|---|---|---|
| committer | Son Ho | 2024-04-04 11:56:09 +0200 |
| commit | 795e2107e305d425efdf6071b29f186cae83656b (patch) | |
| tree | 8f1cf29f3a25d6e36b323045a1108aef5b50a917 | |
| parent | 88cb18c614819f4abba1e0dfdb80c455d334d595 (diff) | |
Update the names of the synthesized backward functions
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 6 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 9 |
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} *) |