diff options
author | Son Ho | 2022-02-09 11:43:56 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 11:43:56 +0100 |
commit | 2ec238154350c6ed8b2129828292b81752d4d750 (patch) | |
tree | 90622cbf59819d9a413c8d6917e79db9359e98aa /src/ExtractToFStar.ml | |
parent | 56b17df2da3fa60d6c20de7288cc870767576827 (diff) |
Improve a bit the quality of the generated code by adjusting the
function suffixes depending on whether forward/backward translations
have been filtered
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0c77f48b..a28d8c6d 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -264,12 +264,12 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) in let fun_name (_fid : A.fun_id) (fname : name) (num_rgs : int) - (rg : region_group_info option) : string = + (rg : region_group_info option) (filter_info : bool * int) : string = let fname = get_fun_name fname in (* Converting to snake case should be a no-op, but it doesn't cost much *) let fname = to_snake_case fname in (* Compute the suffix *) - let suffix = default_fun_suffix num_rgs rg in + let suffix = default_fun_suffix num_rgs rg filter_info in (* Concatenate *) fname ^ suffix in @@ -632,14 +632,16 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (** Compute the names for all the pure functions generated from a rust function (forward function and backward functions). *) -let extract_fun_def_register_names (ctx : extraction_ctx) +let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool) (def : pure_fun_translation) : extraction_ctx = let fwd, back_ls = def in (* Register the forward function name *) - let ctx = ctx_add_fun_def fwd ctx in + let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in (* Register the backward functions' names *) let ctx = - List.fold_left (fun ctx back -> ctx_add_fun_def back ctx) ctx back_ls + List.fold_left + (fun ctx back -> ctx_add_fun_def (keep_fwd, def) back ctx) + ctx back_ls in (* Return *) ctx |