Merge pull request #272 from Nadrieril/remove-llbc_name

9 files changed, 65 insertions, 77 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1fbce7fd..cf632388 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -26,7 +26,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
       let builtin =
         let open ExtractBuiltin in
         let funs_map = builtin_funs_map () in
-        match_name_find_opt ctx.trans_ctx def.f.llbc_name funs_map
+        match_name_find_opt ctx.trans_ctx def.f.item_meta.name funs_map
       in
       (* Use the builtin names if necessary *)
       match builtin with
@@ -214,7 +214,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
         let decl = FunDeclId.Map.find id ctx.trans_funs in
         let err =
           "Ill-formed builtin information for function "
-          ^ name_to_string ctx decl.f.llbc_name
+          ^ name_to_string ctx decl.f.item_meta.name
           ^ ": "
           ^ string_of_int (List.length filter)
           ^ " filtering arguments provided for "
@@ -1158,7 +1158,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params def.item_meta.span def.llbc_name
+    ctx_add_generic_params def.item_meta.span def.item_meta.name
       def.signature.llbc_generics def.signature.generics ctx
   in
   (* Print the generics *)
@@ -1259,11 +1259,11 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
      if !extract_external_name_patterns && not def.item_meta.is_local then
-       Some def.llbc_name
+       Some def.item_meta.name
      else None
    in
    extract_comment_with_raw_span ctx fmt
-     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+     [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases clause" ]
      name def.item_meta.span.span);
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
@@ -1332,7 +1332,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment_with_raw_span ctx fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
+    [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: termination measure" ]
     None def.item_meta.span.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
@@ -1391,7 +1391,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
   extract_comment_with_raw_span ctx fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
+    [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases_by tactic" ]
     None def.item_meta.span.span;
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
@@ -1423,7 +1423,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
 
 let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
-  let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]:" in
+  let comment_pre = "[" ^ name_to_string ctx def.item_meta.name ^ "]:" in
   let comment =
     let loop_comment =
       match def.loop_id with
@@ -1434,7 +1434,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
   in
   let name =
     if !extract_external_name_patterns && not def.item_meta.is_local then
-      Some def.llbc_name
+      Some def.item_meta.name
     else None
   in
   extract_comment_with_raw_span ctx fmt comment name def.item_meta.span.span
@@ -1722,7 +1722,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type/const gen parameters - note that we need those bindings
      only for the generation of the type (they are not top-level) *)
   let ctx, _, _, _ =
-    ctx_add_generic_params def.item_meta.span def.llbc_name
+    ctx_add_generic_params def.item_meta.span def.item_meta.name
       def.signature.llbc_generics def.signature.generics ctx
   in
   (* Add breaks to insert new lines between definitions *)
@@ -1925,11 +1925,11 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   let name =
     if !extract_external_name_patterns && not global.item_meta.is_local then
-      Some global.llbc_name
+      Some global.item_meta.name
     else None
   in
   extract_comment_with_raw_span ctx fmt
-    [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
+    [ "[" ^ name_to_string ctx global.item_meta.name ^ "]" ]
     name global.span.span;
   F.pp_print_space fmt ();
 
@@ -1947,7 +1947,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   in
   (* Add the type parameters *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params span global.llbc_name global.llbc_generics
+    ctx_add_generic_params span global.item_meta.name global.llbc_generics
       global.generics ctx
   in
   match body.body with
@@ -2173,7 +2173,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
           let llbc_name : Types.name =
             [ Types.PeIdent (item_name, Disambiguator.zero) ]
           in
-          let f = { f with llbc_name } in
+          let f =
+            { f with item_meta = { f.item_meta with name = llbc_name } }
+          in
           let name = ctx_compute_fun_name f ctx in
           (* Add a prefix if necessary *)
           let name =
@@ -2208,7 +2210,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
   (* Lookup the information if this is a builtin trait *)
   let open ExtractBuiltin in
   let builtin_info =
-    match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+    match_name_find_opt ctx.trans_ctx trait_decl.item_meta.name
       (builtin_trait_decls_map ())
   in
   let ctx =
@@ -2254,7 +2256,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
       TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
     in
     let decl_ref = trait_impl.impl_trait in
-    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
       decl_ref.decl_generics
       (builtin_trait_impls_map ())
   in
@@ -2360,7 +2362,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
        - we only generate trait clauses for the clauses we find in the
          pure generics *)
     let ctx, type_params, cg_params, trait_clauses =
-      ctx_add_generic_params decl.item_meta.span f.llbc_name
+      ctx_add_generic_params decl.item_meta.span f.item_meta.name
         f.signature.llbc_generics generics ctx
     in
     let backend_uses_forall =
@@ -2390,11 +2392,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
      if !extract_external_name_patterns && not decl.item_meta.is_local then
-       Some decl.llbc_name
+       Some decl.item_meta.name
      else None
    in
    extract_comment_with_raw_span ctx fmt
-     [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+     [ "Trait declaration: [" ^ name_to_string ctx decl.item_meta.name ^ "]" ]
      name decl.item_meta.span.span);
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
@@ -2429,8 +2431,8 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params decl.item_meta.span decl.llbc_name decl.llbc_generics
-      generics ctx
+    ctx_add_generic_params decl.item_meta.span decl.item_meta.name
+      decl.llbc_generics generics ctx
   in
   extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
     generics type_params cg_params trait_clauses;
@@ -2666,7 +2668,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
        - we only generate trait clauses for the clauses we find in the
          pure generics *)
     let ctx, f_tys, f_cgs, f_tcs =
-      ctx_add_generic_params impl.item_meta.span f.llbc_name
+      ctx_add_generic_params impl.item_meta.span f.item_meta.name
         f.signature.llbc_generics f_generics ctx
     in
     let use_forall = f_generics <> empty_generic_params in
@@ -2696,7 +2698,8 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
 (** Extract a trait implementation *)
 let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
-  log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
+  log#ldebug
+    (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.item_meta.name));
   (* Retrieve the impl name *)
   let impl_name = ctx_get_trait_impl impl.item_meta.span impl.def_id ctx in
   (* Add a break before *)
@@ -2707,12 +2710,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
        let decl_id = impl.impl_trait.trait_decl_id in
        let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
        let decl_ref = impl.llbc_impl_trait in
-       ( Some trait_decl.llbc_name,
+       ( Some trait_decl.item_meta.name,
          Some (trait_decl.llbc_generics, decl_ref.decl_generics) )
      else (None, None)
    in
    extract_comment_with_raw_span ctx fmt
-     [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+     [
+       "Trait implementation: [" ^ name_to_string ctx impl.item_meta.name ^ "]";
+     ]
      (* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
      name ?generics:(Some generics) impl.item_meta.span.span);
   F.pp_print_break fmt 0 0;
@@ -2744,8 +2749,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params impl.item_meta.span impl.llbc_name impl.llbc_generics
-      impl.generics ctx
+    ctx_add_generic_params impl.item_meta.span impl.item_meta.name
+      impl.llbc_generics impl.generics ctx
   in
   let all_generics = (type_params, cg_params, trait_clauses) in
   extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
@@ -2913,7 +2918,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_break fmt 0 0;
     (* Print a comment *)
     extract_comment fmt
-      [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ];
+      [ "Unit test for [" ^ name_to_string ctx def.item_meta.name ^ "]" ];
     F.pp_print_space fmt ();
     (* Open a box for the test *)
     F.pp_open_hovbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 57131dad..4d05f0d0 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1467,7 +1467,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
          (some backends don't support collision of variant names) *)
       if !variant_concatenate_type_name then
         StringUtils.capitalize_first_letter
-          (ctx_compute_type_name_no_suffix ctx def.item_meta def.llbc_name
+          (ctx_compute_type_name_no_suffix ctx def.item_meta def.item_meta.name
           ^ "_" ^ variant)
       else variant
   | Lean -> variant
@@ -1549,7 +1549,7 @@ let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
 let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     : string =
   let llbc_name =
-    rename_llbc_name trait_decl.item_meta.attr_info trait_decl.llbc_name
+    rename_llbc_name trait_decl.item_meta.attr_info trait_decl.item_meta.name
   in
   ctx_compute_type_name trait_decl.item_meta ctx llbc_name
 
@@ -1570,7 +1570,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
           let params = trait_impl.llbc_generics in
           let args = trait_impl.llbc_impl_trait.decl_generics in
           let name =
-            ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name
+            ctx_prepare_name trait_impl.item_meta.span ctx
+              trait_decl.item_meta.name
           in
           let name = rename_llbc_name trait_impl.item_meta.attr_info name in
           trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
@@ -1646,7 +1647,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
   *)
   (* We need to lookup the LLBC definitions, to have the original instantiation *)
   let clause =
-    let current_def_name = trait_decl.llbc_name in
+    let current_def_name = trait_decl.item_meta.name in
     let params = trait_decl.llbc_generics in
     ctx_compute_trait_clause_name ctx current_def_name params
       trait_decl.llbc_parent_clauses clause.clause_id
@@ -2009,7 +2010,7 @@ let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
 
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
+  let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
   let name =
     ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name
       def.num_loops def.loop_id
@@ -2020,7 +2021,7 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
 
 let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
+  let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
   let name =
     ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name
       def.num_loops def.loop_id
@@ -2104,7 +2105,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
                     ~default:def.item_meta))
     | _ -> def.item_meta
   in
-  let llbc_name = rename_llbc_name item_meta.attr_info def.llbc_name in
+  let llbc_name = rename_llbc_name item_meta.attr_info def.item_meta.name in
   ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops
     def.loop_id
 
@@ -2123,4 +2124,4 @@ let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
 
 let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
     =
-  ctx_compute_type_name def.item_meta ctx def.llbc_name
+  ctx_compute_type_name def.item_meta ctx def.item_meta.name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 129fdd78..78382179 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -739,7 +739,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
   (* Lookup the builtin information, if there is *)
   let open ExtractBuiltin in
   let info =
-    match_name_find_opt ctx.trans_ctx def.llbc_name (builtin_types_map ())
+    match_name_find_opt ctx.trans_ctx def.item_meta.name (builtin_types_map ())
   in
   (* Register the filtering information, if there is *)
   let ctx =
@@ -783,11 +783,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
                     (fun fid (field : field) ->
                       ( fid,
                         ctx_compute_field_name def field.attr_info ctx
-                          def.llbc_name fid field.field_name ))
+                          def.item_meta.name fid field.field_name ))
                     fields
                 in
                 let cons_name =
-                  ctx_compute_struct_constructor def ctx def.llbc_name
+                  ctx_compute_struct_constructor def ctx def.item_meta.name
                 in
                 (field_names, cons_name)
             | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
@@ -1417,8 +1417,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx_body, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params def.item_meta.span def.llbc_name def.llbc_generics
-      def.generics ctx
+    ctx_add_generic_params def.item_meta.span def.item_meta.name
+      def.llbc_generics def.generics ctx
   in
   (* Add a break before *)
   if backend () <> HOL4 || not (decl_is_first_from_group kind) then
@@ -1426,11 +1426,11 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
      if !Config.extract_external_name_patterns && not def.item_meta.is_local
-     then Some def.llbc_name
+     then Some def.item_meta.name
      else None
    in
    extract_comment_with_raw_span ctx fmt
-     [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+     [ "[" ^ name_to_string ctx def.item_meta.name ^ "]" ]
      name def.item_meta.span.span);
   F.pp_print_break fmt 0 0;
   (* Open a box for the definition, so that whenever possible it gets printed on
@@ -1703,7 +1703,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
       if is_rec then
         (* Add the type params *)
         let ctx, type_params, cg_params, trait_clauses =
-          ctx_add_generic_params decl.item_meta.span decl.llbc_name
+          ctx_add_generic_params decl.item_meta.span decl.item_meta.name
             decl.llbc_generics decl.generics ctx
         in
         (* Record_var will be the ADT argument to the projector *)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index d273546a..2754eaac 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -397,8 +397,6 @@ type predicates = { trait_type_constraints : trait_type_constraint list }
 
 type type_decl = {
   def_id : TypeDeclId.id;
-  llbc_name : llbc_name;
-      (** The original name coming from the LLBC declaration *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
           the name used at extraction time will be derived from the
@@ -1106,7 +1104,6 @@ type fun_decl = {
        *)
   loop_id : LoopId.id option;
       (** [Some] if this definition was generated for a loop *)
-  llbc_name : llbc_name;  (** The original LLBC name. *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
           the name used at extraction time will be derived from the
@@ -1122,7 +1119,6 @@ type global_decl = {
   def_id : GlobalDeclId.id;
   span : span;
   item_meta : T.item_meta;
-  llbc_name : llbc_name;  (** The original LLBC name. *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
           the name used at extraction time will be derived from the
@@ -1140,7 +1136,6 @@ type global_decl = {
 
 type trait_decl = {
   def_id : trait_decl_id;
-  llbc_name : llbc_name;
   name : string;
   item_meta : T.item_meta;
   generics : generic_params;
@@ -1162,7 +1157,6 @@ type trait_decl = {
 
 type trait_impl = {
   def_id : trait_impl_id;
-  llbc_name : llbc_name;
   name : string;
   item_meta : T.item_meta;
   impl_trait : trait_decl_ref;
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index dda6a611..3476df5f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1504,7 +1504,6 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
                 backend_attributes = def.backend_attributes;
                 num_loops;
                 loop_id = Some loop.loop_id;
-                llbc_name = def.llbc_name;
                 name = def.name;
                 signature = loop_sig;
                 is_global_decl_body = def.is_global_decl_body;
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index d38644c1..9673f542 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -690,7 +690,6 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
   let {
     def_id = _;
     name = _;
-    llbc_name = _;
     item_meta = _;
     generics = _;
     llbc_generics = _;
@@ -711,7 +710,6 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
   let {
     def_id = _;
     name = _;
-    llbc_name = _;
     item_meta = _;
     impl_trait = _;
     llbc_impl_trait = _;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 13c94bdf..e829ed30 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -583,7 +583,6 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
        ^ "\n"));
   let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
-  let llbc_name = def.item_meta.name in
   let name = Print.Types.name_to_string env def.item_meta.name in
   (* Can't translate types with regions for now *)
   cassert __FILE__ __LINE__
@@ -596,7 +595,6 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let item_meta = def.item_meta in
   {
     def_id;
-    llbc_name;
     name;
     item_meta;
     generics;
@@ -3772,8 +3770,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
 
   (* Translate the declaration *)
   let def_id = def.def_id in
-  let llbc_name = def.item_meta.name in
-  let name = name_to_string ctx llbc_name in
+  let name = name_to_string ctx def.item_meta.name in
   (* Translate the signature *)
   let signature = translate_fun_sig_from_decomposed ctx.sg in
   (* Translate the body, if there is *)
@@ -3898,7 +3895,6 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
       backend_attributes;
       num_loops;
       loop_id;
-      llbc_name;
       name;
       signature;
       is_global_decl_body = def.is_global_decl_body;
@@ -3943,12 +3939,11 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   } : A.trait_decl =
     trait_decl
   in
-  let llbc_name = item_meta.name in
   let type_infos = ctx.type_ctx.type_infos in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
-      llbc_name
+      item_meta.name
   in
   let generics, preds =
     translate_generic_params trait_decl.item_meta.span llbc_generics
@@ -3978,7 +3973,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   in
   {
     def_id;
-    llbc_name;
     name;
     item_meta;
     generics;
@@ -4007,7 +4001,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   } =
     trait_impl
   in
-  let llbc_name = item_meta.name in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
     translate_trait_decl_ref trait_impl.item_meta.span
@@ -4017,7 +4010,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
-      llbc_name
+      item_meta.name
   in
   let generics, preds =
     translate_generic_params trait_impl.item_meta.span llbc_generics
@@ -4043,7 +4036,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   {
     def_id;
-    llbc_name;
     name;
     item_meta;
     impl_trait;
@@ -4070,11 +4062,10 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
   } =
     decl
   in
-  let llbc_name = item_meta.name in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
-      llbc_name
+      item_meta.name
   in
   let generics, preds =
     translate_generic_params decl.item_meta.span llbc_generics
@@ -4084,7 +4075,6 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
     span = item_meta.span;
     def_id;
     item_meta;
-    llbc_name;
     name;
     llbc_generics;
     generics;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index cadf8cbd..672fb22f 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -442,7 +442,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     let types_map = builtin_types_map () in
     List.map
       (fun (def : Pure.type_decl) ->
-        match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None)
+        match_name_find_opt ctx.trans_ctx def.item_meta.name types_map <> None)
       defs
   in
 
@@ -648,7 +648,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
     let funs_map = builtin_funs_map () in
     List.map
       (fun (trans : pure_fun_translation) ->
-        match_name_find_opt ctx.trans_ctx trans.f.llbc_name funs_map <> None)
+        match_name_find_opt ctx.trans_ctx trans.f.item_meta.name funs_map
+        <> None)
       pure_ls
   in
 
@@ -727,7 +728,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
   (* Check if the trait declaration is builtin, in which case we ignore it *)
   let open ExtractBuiltin in
   if
-    match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+    match_name_find_opt ctx.trans_ctx trait_decl.item_meta.name
       (builtin_trait_decls_map ())
     = None
   then (
@@ -752,7 +753,7 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     let trait_impl =
       TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
     in
-    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
       trait_impl.impl_trait.decl_generics
       (builtin_trait_impls_map ())
   in
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index bd281a82..a7e81535 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
 [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 826:
+[Error] In file Translate.ml, line 827:
 Mutually recursive trait declarations are not supported
 
 Uncaught exception:
   
   (Failure
-    "In file Translate.ml, line 826:\
-   \nIn file Translate.ml, line 826:\
+    "In file Translate.ml, line 827:\
+   \nIn file Translate.ml, line 827:\
    \nMutually recursive trait declarations are not supported")
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 852, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 979, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1528, characters 5-42
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 853, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 980, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1529, characters 5-42
 Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66