summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/ExtractBase.ml')
-rw-r--r--compiler/ExtractBase.ml161
1 files changed, 22 insertions, 139 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 04686705..591e8aab 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -167,11 +167,7 @@ type id =
| TraitImplId of TraitImplId.id
| LocalTraitClauseId of TraitClauseId.id
| TraitDeclConstructorId of TraitDeclId.id
- | TraitMethodId of TraitDeclId.id * string * T.RegionGroupId.id option
- (** Something peculiar with trait methods: because we have to take into
- account forward/backward functions, we may need to generate fields
- items per method.
- *)
+ | TraitMethodId of TraitDeclId.id * string
| TraitItemId of TraitDeclId.id * string
(** A trait associated item which is not a method *)
| TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
@@ -353,8 +349,6 @@ let basename_to_unique (names_set : StringSet.t)
in
if StringSet.mem basename names_set then gen 1 else basename
-type fun_name_info = { keep_fwd : bool; num_backs : int }
-
type names_maps = {
names_map : names_map;
(** The map for id to names, where we forbid name collisions
@@ -384,7 +378,7 @@ let allow_collisions (id : id) : bool =
| FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
| TraitMethodId _ ->
!Config.record_fields_short_names
- | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _, _)) ->
+ | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) ->
(* We map several assumed functions to the same id *)
true
| _ -> false
@@ -549,15 +543,6 @@ type extraction_ctx = {
-- makes the if then else dependent
]}
*)
- fun_name_info : fun_name_info PureUtils.RegularFunIdMap.t;
- (** Information used to filter and name functions - we use it
- to print comments in the generated code, to help link
- the generated code to the original code (information such
- as: "this function is the backward function of ...", or
- "this function is the merged forward/backward function of ..."
- in case a Rust function only has one backward translation
- and we filter the forward function because it returns unit.
- *)
trait_decl_id : trait_decl_id option;
(** If we are extracting a trait declaration, identifies it *)
is_provided_method : bool;
@@ -668,14 +653,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
^ TraitClauseId.to_string clause_id
| TraitItemId (id, name) ->
"trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
- | TraitMethodId (trait_decl_id, fun_name, rg_id) ->
- let fwd_back_kind =
- match rg_id with
- | None -> "forward"
- | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
- in
- trait_decl_id_to_string trait_decl_id
- ^ ", method name (" ^ fwd_back_kind ^ "): " ^ fun_name
+ | TraitMethodId (trait_decl_id, fun_name) ->
+ trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name
| TraitSelfClauseId -> "trait_self_clause"
let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
@@ -694,8 +673,8 @@ let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
ctx_get (FunId id) ctx
let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
- (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string =
- ctx_get_function (FromLlbc (FunId (FRegular id), lp, rg)) ctx
+ (ctx : extraction_ctx) : string =
+ ctx_get_function (FromLlbc (FunId (FRegular id), lp)) ctx
let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
assert (id <> TTuple);
@@ -733,8 +712,8 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
ctx_get_trait_item id item_name ctx
let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
- (rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string =
- ctx_get (TraitMethodId (id, item_name, rg_id)) ctx
+ (ctx : extraction_ctx) : string =
+ ctx_get (TraitMethodId (id, item_name)) ctx
let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
@@ -1164,8 +1143,7 @@ let initialize_names_maps () : names_maps =
in
let assumed_functions =
List.map
- (fun (fid, rg, name) ->
- (FromLlbc (Pure.FunId (FAssumed fid), None, rg), name))
+ (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
init.assumed_llbc_functions
@ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
in
@@ -1408,61 +1386,12 @@ let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
If this function admits only one loop, we omit it. *)
if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
-(** A helper function: generates a function suffix from a region group
- information.
+(** A helper function: generates a function suffix.
TODO: move all those helpers.
*)
-let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
- (num_region_groups : int) (rg : region_group_info option)
- ((keep_fwd, num_backs) : bool * int) : string =
- let lp_suff = default_fun_loop_suffix num_loops loop_id in
-
- (* 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 extracted backward function:
- - if the forward function has been filtered, we add nothing:
- the forward function is useless, so the unique backward function
- takes its place, in a way (in effect, we "merge" the forward
- and the backward functions).
- - 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
- definitions (in particular between type and function definitions).
- *)
- let rg_suff =
- (* TODO: make all the backends match what is done for Lean *)
- match rg with
- | None ->
- if
- (* In order to avoid name conflicts:
- * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
- * - otherwise, no suffix (because the backward functions will have a suffix)
- *)
- num_backs = 1 && not keep_fwd
- then "_fwd"
- else ""
- | Some rg ->
- assert (num_region_groups > 0 && num_backs > 0);
- if num_backs = 1 then
- (* Exactly one backward function *)
- if not keep_fwd then "" else "_back"
- else if
- (* Several region groups/backward functions:
- - if all the regions in the group have names, we use those names
- - otherwise we use an index
- *)
- List.for_all Option.is_some rg.region_names
- then
- (* Concatenate the region names *)
- "_back" ^ String.concat "" (List.map Option.get rg.region_names)
- else (* Use the region index *)
- "_back" ^ RegionGroupId.to_string rg.id
- in
- lp_suff ^ rg_suff
+let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string =
+ (* We only generate a suffix for the functions we generate from the loops *)
+ default_fun_loop_suffix num_loops loop_id
(** Compute the name of a regular (non-assumed) function.
@@ -1472,24 +1401,13 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
indices to derive unique names for the loops for instance - if there is
exactly one loop, we don't need to use indices)
- loop id (if pertinent)
- - number of region groups
- - region group information in case of a backward function
- ([None] if forward function)
- - pair:
- - do we generate the forward function (it may have been filtered)?
- - the number of *extracted backward functions* (same comment as for
- the number of loops)
- The number of extracted backward functions if not necessarily
- equal to the number of region groups, because we may have
- filtered some of them.
TODO: use the fun id for the assumed functions.
*)
let ctx_compute_fun_name (ctx : extraction_ctx) (fname : llbc_name)
- (num_loops : int) (loop_id : LoopId.id option) (num_rgs : int)
- (rg : region_group_info option) (filter_info : bool * int) : string =
+ (num_loops : int) (loop_id : LoopId.id option) : string =
let fname = ctx_compute_fun_name_no_suffix ctx fname in
(* Compute the suffix *)
- let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
+ let suffix = default_fun_suffix num_loops loop_id in
(* Concatenate *)
fname ^ suffix
@@ -1963,61 +1881,26 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
| None ->
(* Not the case: "standard" registration *)
let name = ctx_compute_global_name ctx def.name in
- let body = FunId (FromLlbc (FunId (FRegular def.body), None, None)) in
+ let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
let ctx = ctx_add decl (name ^ "_c") ctx in
let ctx = ctx_add body (name ^ "_body") ctx in
ctx
-let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
- (ctx : extraction_ctx) : string =
- (* Lookup the LLBC def to compute the region group information *)
- let def_id = def.def_id in
- let llbc_def = A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_ctx.fun_decls in
- let sg = llbc_def.signature in
- let regions_hierarchy =
- LlbcAstUtils.FunIdMap.find (FRegular def_id)
- ctx.trans_ctx.fun_ctx.regions_hierarchies
- in
- let num_rgs = List.length regions_hierarchy in
- let { keep_fwd; fwd = _; backs } = trans_group in
- let num_backs = List.length backs in
- let rg_info =
- match def.back_id with
- | None -> None
- | Some rg_id ->
- let rg = T.RegionGroupId.nth regions_hierarchy rg_id in
- let region_names =
- List.map
- (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
- rg.regions
- in
- Some { id = rg_id; region_names }
- in
+let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
(* Add the function name *)
- ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id num_rgs
- rg_info (keep_fwd, num_backs)
+ ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id
(* TODO: move to Extract *)
-let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
- (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
(* Sanity check: the function should not be a global body - those are handled
* separately *)
assert (not def.is_global_decl_body);
(* Lookup the LLBC def to compute the region group information *)
let def_id = def.def_id in
- let { keep_fwd; fwd = _; backs } = trans_group in
- let num_backs = List.length backs in
(* Add the function name *)
- let def_name = ctx_compute_fun_name trans_group def ctx in
- let fun_id = (Pure.FunId (FRegular def_id), def.loop_id, def.back_id) in
- let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in
- (* Add the name info *)
- {
- ctx with
- fun_name_info =
- PureUtils.RegularFunIdMap.add fun_id { keep_fwd; num_backs }
- ctx.fun_name_info;
- }
+ let def_name = ctx_compute_fun_name def ctx in
+ let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in
+ ctx_add (FunId (FromLlbc fun_id)) def_name ctx
let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
=