summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml
diff options
context:
space:
mode:
authorSon Ho2023-12-18 10:11:44 +0100
committerSon Ho2023-12-18 10:11:44 +0100
commit2fb4ca72b112f6181d74d1ca37ed6d54c65f43cd (patch)
tree3be605c79e34a271f7d1785f07546c4ab61ac4f3 /compiler/Extract.ml
parent58b838594777b1489b31db40bba27b5fca355a73 (diff)
Do not register the names of the back funs if they are merged with the fwd funs
Diffstat (limited to 'compiler/Extract.ml')
-rw-r--r--compiler/Extract.ml11
1 files changed, 8 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 7e2efd8a..3429cd11 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -43,8 +43,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
}
| _ -> ctx
in
- let backs = List.map (fun f -> f.f) def.backs in
- let funs = if def.keep_fwd then def.fwd.f :: backs else backs in
+ let funs =
+ if !Config.return_back_funs then [ def.fwd.f ]
+ else
+ let backs = List.map (fun f -> f.f) def.backs in
+ if def.keep_fwd then def.fwd.f :: backs else backs
+ in
List.fold_left
(fun ctx (f : fun_decl) ->
let open ExtractBuiltin in
@@ -1988,7 +1992,8 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* We add one field per required forward/backward function *)
let get_funs_for_id (id : fun_decl_id) : fun_decl list =
let trans : pure_fun_translation = FunDeclId.Map.find id ctx.trans_funs in
- List.map (fun f -> f.f) (trans.fwd :: trans.backs)
+ if !Config.return_back_funs then [ trans.fwd.f ]
+ else List.map (fun f -> f.f) (trans.fwd :: trans.backs)
in
match builtin_info with
| None ->