summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/ExtractToFStar.ml12
-rw-r--r--src/PureToExtract.ml63
-rw-r--r--src/Translate.ml4
3 files changed, 34 insertions, 45 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
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 04d65423..c61338b9 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -65,12 +65,18 @@ type formatter = {
- type name
*)
type_name : name -> string; (** Provided a basename, compute a type name. *)
- fun_name : A.fun_id -> name -> int -> region_group_info option -> string;
+ fun_name :
+ A.fun_id -> name -> int -> region_group_info option -> bool * int -> string;
(** Inputs:
- function id: this is especially useful to identify whether the
function is an assumed function or a local function
- function basename
- number of region groups
+ - pair:
+ - do we generate the forward function (it may have been filtered)?
+ - the number of extracted backward functions (not necessarily equal
+ to the number of region groups, because we may have filtered
+ some of them)
- region group information in case of a backward function
(`None` if forward function)
*)
@@ -497,12 +503,15 @@ let ctx_add_struct (def : type_def) (ctx : extraction_ctx) :
let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
(ctx, name)
-let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
+ (ctx : extraction_ctx) : extraction_ctx =
(* Lookup the CFIM def to compute the region group information *)
let def_id = def.def_id in
let cfim_def = FunDefId.Map.find def_id ctx.trans_ctx.fun_context.fun_defs in
let sg = cfim_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
+ let keep_fwd, (_, backs) = trans_group in
+ let num_backs = List.length backs in
let rg_info =
match def.back_id with
| None -> None
@@ -519,7 +528,9 @@ let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx =
Some { id = rg_id; region_names }
in
let def_id = A.Local def_id in
- let name = ctx.fmt.fun_name def_id def.basename num_rgs rg_info in
+ let name =
+ ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
+ in
let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
ctx
@@ -588,13 +599,17 @@ let compute_type_def_name (fmt : formatter) (def : type_def) : string =
TODO: move all those helpers.
*)
let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
- : string =
+ ((keep_fwd, num_backs) : bool * int) : string =
(* There are several cases:
- [rg] is `Some`: this is a forward function:
- we add "_fwd"
- [rg] is `None`: this is a backward function:
- - this function has one region group: we add "_back"
- - this function has several backward function: we add "_back" and an
+ - this function has one extracted backward function:
+ - if the forward function has been filtered, we add "_fwd_back":
+ the forward function is useless, so the unique backward function
+ takes its place, in a way
+ - otherwise we add "_back"
+ - this function has several backward functions: we add "_back" and an
additional suffix to identify the precise backward function
Note that we always add a suffix (in case there are no region groups,
we could not add the "_fwd" suffix) to prevent name clashes between
@@ -603,9 +618,10 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
match rg with
| None -> "_fwd"
| Some rg ->
- assert (num_region_groups > 0);
- if num_region_groups = 1 then (* Exactly one backward function *)
- "_back"
+ assert (num_region_groups > 0 && num_backs > 0);
+ if num_backs = 1 then
+ (* Exactly one backward function *)
+ if not keep_fwd then "_fwd_back" else "_back"
else if
(* Several region groups/backward functions:
- if all the regions in the group have names, we use those names
@@ -617,32 +633,3 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
"_back" ^ String.concat "" (List.map Option.get rg.region_names)
else (* Use the region index *)
"_back" ^ RegionGroupId.to_string rg.id
-
-(** Extract information from a function, and give this information to a
- [formatter] to generate a function's name.
-
- Note that we need region information coming from CFIM (when generating
- the name for a backward function, we try to use the names of the regions
- to
- *)
-let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
- (rg_id : RegionGroupId.id option) : string =
- (* Lookup the function CFIM signature (we need the region information) *)
- let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
- let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
- (* Compute the regions information *)
- let num_region_groups = List.length sg.regions_hierarchy in
- let rg_info =
- match rg_id with
- | None -> None
- | Some rg_id ->
- let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
- let regions =
- List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
- in
- let region_names =
- List.map (fun (r : T.region_var) -> r.name) regions
- in
- Some { id = rg.id; region_names }
- in
- fmt.fun_name fun_id basename num_region_groups rg_info
diff --git a/src/Translate.ml b/src/Translate.ml
index 8084dc38..f86ef438 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -314,8 +314,8 @@ let translate_module (filename : string) (dest_dir : string)
let extract_ctx =
List.fold_left
- (fun extract_ctx (_, def) ->
- ExtractToFStar.extract_fun_def_register_names extract_ctx def)
+ (fun extract_ctx (keep_fwd, def) ->
+ ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd def)
extract_ctx trans_funs
in