From e090e09725e3fd5c7f2a92813955ce2d81560227 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 19:44:39 +0200
Subject: Do more cleanup

---
 compiler/Extract.ml     | 8 +++++---
 compiler/ExtractBase.ml | 6 +++---
 compiler/Translate.ml   | 4 +---
 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
-- 
cgit v1.2.3