summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-09-03 19:44:39 +0200
committerSon Ho2023-09-03 19:44:39 +0200
commite090e09725e3fd5c7f2a92813955ce2d81560227 (patch)
tree6fc4957c0295dce7c02ea5f87892dc5917e75709
parentdfcbfab4030be2f03b159a4b298ed75ac2f236ae (diff)
Do more cleanup
-rw-r--r--compiler/Extract.ml8
-rw-r--r--compiler/ExtractBase.ml6
-rw-r--r--compiler/Translate.ml4
3 files changed, 9 insertions, 9 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 5c0a08ad..204fee04 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2326,7 +2326,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
(** Compute the names for all the pure functions generated from a rust function
(forward function and backward functions).
*)
-let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
+let extract_fun_decl_register_names (ctx : extraction_ctx)
(has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) :
extraction_ctx =
let { f = fwd; loops = loop_fwds } = def.fwd in
@@ -2344,7 +2344,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
else ctx
in
let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
- let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in
+ let register_fun ctx f = ctx_add_fun_decl def f ctx in
let register_funs ctx fl = List.fold_left register_fun ctx fl in
(* Register the forward functions' names *)
let ctx = register_funs ctx (fwd :: loop_fwds) in
@@ -3971,7 +3971,9 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
(* TODO: for the methods, we need to add fields for the forward/backward functions *)
raise (Failure "TODO");
List.fold_left
- (fun ctx (name, id) -> ctx_add_trait_method trait_decl name ctx)
+ (fun ctx (name, id) ->
+ (* We add one field per required forward/backward function *)
+ ctx_add_trait_method trait_decl name ctx)
ctx required_methods
(** Similar to {!extract_type_decl_register_names} *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 885467c2..17f5b693 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1185,8 +1185,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
ctx
-let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
- (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_fun_decl (trans_group : pure_fun_translation) (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);
@@ -1197,7 +1197,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
in
let sg = llbc_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
- let keep_fwd, { fwd = _; backs } = trans_group in
+ let { keep_fwd; fwd = _; backs } = trans_group in
let num_backs = List.length backs in
let rg_info =
match def.back_id with
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 835edd46..a4041751 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1084,9 +1084,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
* those are handled later *)
let is_global = fwd_def.Pure.is_global_decl_body in
if is_global then ctx
- else
- Extract.extract_fun_decl_register_names ctx trans.keep_fwd
- gen_decr_clause trans)
+ else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans)
ctx
(A.FunDeclId.Map.values trans_funs)
in