diff options
| author | Sidney Congard | 2022-06-30 12:22:14 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-06-30 12:22:14 +0200 |
| commit | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (patch) | |
| tree | 06ac570c7f9eee49987d716e043415ae31c681d0 /src/PureToExtract.ml | |
| parent | da118da3e590fbea4e880121837da2ee938837f6 (diff) | |
Traduct globals body separately (WIP)
Diffstat (limited to '')
| -rw-r--r-- | src/PureToExtract.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 195eb879..e58fec2a 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -74,6 +74,7 @@ type formatter = { fun_name : A.fun_id -> fun_name -> + bool -> int -> region_group_info option -> bool * int -> @@ -440,11 +441,13 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found -let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) +let ctx_get_function (id : A.fun_id) + (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get (FunId (id, rg)) ctx -let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option) +let ctx_get_local_function (id : A.FunDeclId.id) + (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get_function (A.Regular id) rg ctx @@ -596,7 +599,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs) in (* Add the function name *) let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in @@ -666,8 +669,12 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = information. TODO: move all those helpers. *) -let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) - ((keep_fwd, num_backs) : bool * int) : string = +let default_fun_suffix + (is_global : bool) + (num_region_groups : int) + (rg : region_group_info option) + ((keep_fwd, num_backs) : bool * int) + : string = (* There are several cases: - [rg] is `Some`: this is a forward function: - we add "_fwd" @@ -683,6 +690,7 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) we could not add the "_fwd" suffix) to prevent name clashes between definitions (in particular between type and function definitions). *) + if is_global then "_c" else match rg with | None -> "_fwd" | Some rg -> |