Update TranslateCore.pure_fun_translation

5 files changed, 33 insertions, 34 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 73a081a7..5c0a08ad 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2329,7 +2329,8 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
 let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
     (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) :
     extraction_ctx =
-  let { f = fwd; loops = loop_fwds }, back_ls = def in
+  let { f = fwd; loops = loop_fwds } = def.fwd in
+  let back_ls = def.backs in
   (* Register the decrease clauses, if necessary *)
   let register_decreases ctx def =
     if has_decreases_clause def then
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 26940c0c..7a21d42d 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -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, (_, 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/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 72e3d05e..e97a9cd7 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1461,12 +1461,12 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
     altogether.
   *)
 let keep_forward (trans : pure_fun_translation) : bool =
-  let { f = fwd; _ }, backs = trans in
+  let { fwd; backs } = trans in
   (* Note that at this point, the output types are no longer seen as tuples:
    * they should be lists of length 1. *)
   if
     !Config.filter_useless_functions
-    && fwd.signature.output = mk_result_ty mk_unit_ty
+    && fwd.f.signature.output = mk_result_ty mk_unit_ty
     && backs <> []
   then false
   else true
@@ -1996,8 +1996,8 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
       (List.concat
          (List.concat
             (List.map
-               (fun (_, ({ f = fwd; loops = loops_fwd }, backs)) ->
-                 [ fwd :: loops_fwd ]
+               (fun (_, { fwd; backs }) ->
+                 [ fwd.f :: fwd.loops ]
                  :: List.map
                       (fun { f = back; loops = loops_back } ->
                         [ back :: loops_back ])
@@ -2246,13 +2246,13 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
   in
   let transl =
     List.map
-      (fun (b, (fwd, backs)) ->
+      (fun (b, { fwd; backs }) ->
         let filter_fun_and_loops f =
           { f = filter_in_one f.f; loops = List.map filter_in_one f.loops }
         in
         let fwd = filter_fun_and_loops fwd in
         let backs = List.map filter_fun_and_loops backs in
-        (b, (fwd, backs)))
+        (b, { fwd; backs }))
       transl
   in
 
@@ -2278,10 +2278,10 @@ let apply_passes_to_pure_fun_translations (ctx : trans_ctx)
   let apply_to_one (trans : fun_decl * fun_decl list) :
       bool * pure_fun_translation =
     (* Apply the passes to the individual functions *)
-    let forward, backwards = trans in
-    let forward = Option.get (apply_passes_to_def ctx forward) in
-    let backwards = List.filter_map (apply_passes_to_def ctx) backwards in
-    let trans = (forward, backwards) in
+    let fwd, backs = trans in
+    let fwd = Option.get (apply_passes_to_def ctx fwd) in
+    let backs = List.filter_map (apply_passes_to_def ctx) backs in
+    let trans = { fwd; backs } in
     (* Compute whether we need to filter the forward function or not *)
     (keep_forward trans, trans)
   in
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2f751693..7122e462 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -439,8 +439,8 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
   in
   let has_opaque_funs =
     A.FunDeclId.Map.exists
-      (fun _ ((_, (fwd, _)) : bool * pure_fun_translation) ->
-        Option.is_none fwd.f.body)
+      (fun _ ((_, trans) : bool * pure_fun_translation) ->
+        Option.is_none trans.fwd.f.body)
       ctx.trans_funs
   in
   (has_opaque_types, has_opaque_funs)
@@ -552,11 +552,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
   let global_decls = ctx.trans_ctx.global_context.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
-  let _, ({ f = body; loops = loop_fwds }, body_backs) =
-    A.FunDeclId.Map.find global.body_id ctx.trans_funs
-  in
-  assert (body_backs = []);
-  assert (loop_fwds = []);
+  let _, trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+  assert (trans.fwd.loops = []);
+  assert (trans.backs = []);
+  let body = trans.fwd.f in
 
   let is_opaque = Option.is_none body.Pure.body in
   if
@@ -676,7 +675,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Extract the decrease clauses template bodies *)
   if config.extract_template_decreases_clauses then
     List.iter
-      (fun (_, (fwd, _)) ->
+      (fun (_, { fwd; _ }) ->
         (* We only generate decreases clauses for the forward functions, because
            the termination argument should only depend on the forward inputs.
            The backward functions thus use the same decreases clauses as the
@@ -711,15 +710,13 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   let decls =
     List.concat
       (List.map
-         (fun (keep_fwd, (fwd, (back_ls : fun_and_loops list))) ->
+         (fun (keep_fwd, { fwd; backs }) ->
            let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
-           let back : Pure.fun_decl list =
+           let backs : Pure.fun_decl list =
              List.concat
-               (List.map
-                  (fun back -> List.append back.loops [ back.f ])
-                  back_ls)
+               (List.map (fun back -> List.append back.loops [ back.f ]) backs)
            in
-           List.append fwd back)
+           List.append fwd backs)
          pure_ls)
   in
 
@@ -737,8 +734,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Insert unit tests if necessary *)
   if config.test_trans_unit_functions then
     List.iter
-      (fun (keep_fwd, (fwd, _)) ->
-        if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd.f)
+      (fun (keep_fwd, trans) ->
+        if keep_fwd then
+          Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
       pure_ls
 
 (** Export a trait declaration. *)
@@ -790,7 +788,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match (fst (snd pure_fun)).f.Pure.kind with
+        match (snd pure_fun).fwd.f.Pure.kind with
         | TraitMethodDecl _ -> ()
         | _ ->
             (* Translate *)
@@ -995,7 +993,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
     List.map
-      (fun (_, (fwd, _)) ->
+      (fun (_, { fwd; _ }) ->
         let fwd_f =
           if fwd.f.Pure.signature.info.effect_info.is_rec then
             [ (fwd.f.def_id, None) ]
@@ -1022,8 +1020,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t =
     A.FunDeclId.Map.of_list
       (List.map
-         (fun ((keep_fwd, (fwd, bdl)) : bool * pure_fun_translation) ->
-           (fwd.f.def_id, (keep_fwd, (fwd, bdl))))
+         (fun ((keep_fwd, { fwd; backs }) : bool * pure_fun_translation) ->
+           (fwd.f.def_id, (keep_fwd, { fwd; backs })))
          trans_funs)
   in
 
@@ -1077,7 +1075,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       (fun ctx ((keep_fwd, defs) : bool * pure_fun_translation) ->
         (* If requested by the user, register termination measures and decreases
            proofs for all the recursive functions *)
-        let fwd_def = (fst defs).f in
+        let fwd_def = defs.fwd.f in
         let gen_decr_clause (def : Pure.fun_decl) =
           !Config.extract_decreases_clauses
           && PureUtils.FunLoopIdSet.mem
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 9694c95e..9fd27c59 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -33,7 +33,7 @@ type trans_ctx = {
 
 type fun_and_loops = { f : Pure.fun_decl; loops : Pure.fun_decl list }
 type pure_fun_translation_no_loops = Pure.fun_decl * Pure.fun_decl list
-type pure_fun_translation = fun_and_loops * fun_and_loops list
+type pure_fun_translation = { fwd : fun_and_loops; backs : fun_and_loops list }
 
 let trans_ctx_to_type_formatter (ctx : trans_ctx)
     (type_params : Pure.type_var list)