item_meta

9 files changed, 81 insertions, 80 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 656d2f27..8080e08c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1932,10 +1932,11 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
   match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
   | Some name ->
       (* Yes: register the custom binding *)
-      ctx_add def.meta decl name ctx
+      ctx_add def.item_meta.meta decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
-      let name = ctx_compute_global_name def.meta ctx def.name in
+      let name = ctx_compute_global_name def.item_meta.meta ctx def.name in
+
       let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
       (* If this is a provided constant (i.e., the default value for a constant
          in a trait declaration) we add a suffix. Otherwise there is a clash
@@ -1944,8 +1945,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       let suffix =
         match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
       in
-      let ctx = ctx_add def.meta decl (name ^ suffix) ctx in
-      let ctx = ctx_add def.meta body (name ^ suffix ^ "_body") ctx in
+      let ctx = ctx_add def.item_meta.meta decl (name ^ suffix) ctx in
+      let ctx = ctx_add def.item_meta.meta body (name ^ suffix ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index f194d4e5..d98efc8d 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -147,7 +147,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       (* Sanity check: global bodies don't contain stateful calls *)
       cassert __FILE__ __LINE__
         ((not f.is_global_decl_body) || not !stateful)
-        f.meta "Global definition containing a stateful call in its body";
+        f.item_meta.meta "Global definition containing a stateful call in its body";
       let builtin_info = get_builtin_info f in
       let has_builtin_info = builtin_info <> None in
       group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
@@ -171,11 +171,11 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
     let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in
     cassert __FILE__ __LINE__
       ((not is_global_decl_body) || List.length d = 1)
-      (List.hd d).meta
+      (List.hd d).item_meta.meta
       "This global definition is in a group of mutually recursive definitions";
     cassert __FILE__ __LINE__
       ((not !group_has_builtin_info) || List.length d = 1)
-      (List.hd d).meta
+      (List.hd d).item_meta.meta
       "This builtin function belongs to a group of mutually recursive \
        definitions";
     (* We ignore on purpose functions that cannot fail and consider they *can*
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 769e3144..d9af063e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -196,12 +196,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     (List.for_all
        (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
        (sg.output :: sg.inputs))
-    fdef.meta "Nested borrows are not supported yet";
+    fdef.item_meta.meta "Nested borrows are not supported yet";
   cassert __FILE__ __LINE__
     (List.for_all
        (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
        (sg.output :: sg.inputs))
-    fdef.meta "ADTs containing borrows are not supported yet";
+    fdef.item_meta.meta "ADTs containing borrows are not supported yet";
 
   (* Create the context *)
   let regions_hierarchy =
@@ -211,23 +211,23 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx fdef.meta ctx region_groups sg.generics.types
+    initialize_eval_ctx fdef.item_meta.meta ctx region_groups sg.generics.types
       sg.generics.const_generics
   in
   (* Instantiate the signature. This updates the context because we compute
      at the same time the normalization map for the associated types.
   *)
   let ctx, inst_sg =
-    symbolic_instantiate_fun_sig fdef.meta ctx fdef.signature regions_hierarchy
+    symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
       fdef.kind
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
-    List.map (fun ty -> mk_fresh_symbolic_value fdef.meta ty) inst_sg.inputs
+    List.map (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta ty) inst_sg.inputs
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
-  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.meta;
+  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.meta;
   let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
       eval_ctx * typed_avalue list =
     (* Project over the values - we use *loan* projectors, as explained above *)
@@ -249,14 +249,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     Collections.List.split_at (List.tl body.locals) body.arg_count
   in
   (* Push the return variable (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_var fdef.meta ctx ret_var in
+  let ctx = ctx_push_uninitialized_var fdef.item_meta.meta ctx ret_var in
   (* Push the input variables (initialized with symbolic values) *)
   let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
   let ctx =
-    ctx_push_vars fdef.meta ctx (List.combine input_vars input_values)
+    ctx_push_vars fdef.item_meta.meta ctx (List.combine input_vars input_values)
   in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars fdef.meta ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -290,7 +290,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       ^ "\n- inside_loop: "
       ^ Print.bool_to_string inside_loop
       ^ "\n- ctx:\n"
-      ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.meta) ctx));
+      ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.item_meta.meta) ctx));
   (* We need to instantiate the function signature - to retrieve
    * the return type. Note that it is important to re-generate
    * an instantiation of the signature, so that we use fresh
@@ -299,13 +299,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let _, ret_inst_sg =
-    symbolic_instantiate_fun_sig fdef.meta ctx fdef.signature regions_hierarchy
+    symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
       fdef.kind
   in
   let ret_rty = ret_inst_sg.output in
   (* Move the return value out of the return variable *)
   let pop_return_value = is_regular_return in
-  let cf_pop_frame = pop_frame config fdef.meta pop_return_value in
+  let cf_pop_frame = pop_frame config fdef.item_meta.meta pop_return_value in
 
   (* We need to find the parents regions/abstractions of the region we
    * will end - this will allow us to, first, mark the other return
@@ -333,7 +333,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
         let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
             eval_ctx * typed_avalue list =
           let ctx, avalue =
-            apply_proj_borrows_on_input_value config fdef.meta ctx abs.regions
+            apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx abs.regions
               abs.ancestors_regions ret_value ret_rty
           in
           (ctx, [ avalue ])
@@ -349,7 +349,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
         let region_can_end rid =
           RegionGroupId.Set.mem rid parent_and_current_rgs
         in
-        sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.meta;
+        sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.item_meta.meta;
         let ctx =
           create_push_abstractions_from_abs_region_groups
             (fun rg_id -> SynthRet rg_id)
@@ -439,7 +439,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                 sanity_check __FILE__ __LINE__
                   (if Option.is_some loop_id then loop_id = Some loop_id'
                    else true)
-                  fdef.meta;
+                  fdef.item_meta.meta;
                 (* Loop abstractions *)
                 let rg_id' = Option.get rg_id' in
                 if rg_id' = back_id && inside_loop then
@@ -448,7 +448,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
                 sanity_check __FILE__ __LINE__ (loop_id = Some loop_id')
-                  fdef.meta;
+                  fdef.item_meta.meta;
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
     let cf_end_target_abs cf =
       List.fold_left
-        (fun cf id -> end_abstraction config fdef.meta id cf)
+        (fun cf id -> end_abstraction config fdef.item_meta.meta id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -534,7 +534,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
           let fwd_e =
             (* Pop the frame and retrieve the returned value at the same time*)
             let pop_return_value = true in
-            let cf_pop = pop_frame config fdef.meta pop_return_value in
+            let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return ret_value : m_fun =
              fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -551,7 +551,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             match res with
             | Return -> None
             | LoopReturn loop_id -> Some loop_id
-            | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
           in
           let is_regular_return = true in
           let inside_loop = Option.is_some loop_id in
@@ -577,14 +577,14 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             match res with
             | EndEnterLoop _ -> false
             | EndContinue _ -> true
-            | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
           in
           (* Forward translation *)
           let fwd_e =
             (* Pop the frame - there is no returned value to pop: in the
                translation we will simply call the loop function *)
             let pop_return_value = false in
-            let cf_pop = pop_frame config fdef.meta pop_return_value in
+            let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return _ret_value : m_fun =
              fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -618,7 +618,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
          * the executions can lead to a panic *)
         if synthesize then Some SA.Panic else None
     | Unit | Break _ | Continue _ ->
-        craise __FILE__ __LINE__ fdef.meta
+        craise __FILE__ __LINE__ fdef.item_meta.meta
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
@@ -652,14 +652,14 @@ module Test = struct
     (* Sanity check - *)
     sanity_check __FILE__ __LINE__
       (fdef.signature.generics = empty_generic_params)
-      fdef.meta;
-    sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta;
+      fdef.item_meta.meta;
+    sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.item_meta.meta;
 
     (* Create the evaluation context *)
-    let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
+    let ctx = initialize_eval_ctx fdef.item_meta.meta decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars fdef.meta ctx body.locals in
+    let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx body.locals in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -668,9 +668,9 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
+          pop_frame config fdef.item_meta.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
-          craise __FILE__ __LINE__ fdef.meta
+          craise __FILE__ __LINE__ fdef.item_meta.meta
             ("Unit test failed (concrete execution) on: "
             ^ Print.Types.name_to_string
                 (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index de89f316..064fff29 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1063,13 +1063,13 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
       (* Treat the evaluation of the global as a call to the global body *)
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
-      (eval_transparent_function_call_concrete config global.meta global.body
+      (eval_transparent_function_call_concrete config global.item_meta.meta global.body
          call)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
-      cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.meta
+      cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta
         "Const globals should not contain regions";
       (* Instantiate the type  *)
       (* There shouldn't be any reference to Self *)
@@ -1082,9 +1082,9 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
         Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
           global.ty
       in
-      let sval = mk_fresh_symbolic_value global.meta ty in
+      let sval = mk_fresh_symbolic_value global.item_meta.meta ty in
       let cc =
-        assign_to_place config global.meta
+        assign_to_place config global.item_meta.meta
           (mk_typed_value_from_symbolic_value sval)
           dest
       in
@@ -1368,7 +1368,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
   (* Sanity check: same number of inputs *)
   sanity_check __FILE__ __LINE__
     (List.length call.args = List.length def.signature.inputs)
-    def.meta;
+    def.item_meta.meta;
   (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
   cassert __FILE__ __LINE__
     (List.for_all
@@ -1381,7 +1381,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
        (inst_sg.output :: inst_sg.inputs))
     meta "ADTs containing borrows are not supported yet";
   (* Evaluate the function call *)
-  eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
+  eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func def.signature
     regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
     cf ctx
 
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a46ef79c..c84cd39c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -446,7 +446,7 @@ let apply_passes (crate : crate) : crate =
          report to the user the fact that we will ignore the function body *)
       let fmt = Print.Crate.crate_to_fmt_env crate in
       let name = Print.name_to_string fmt f.name in
-      save_error __FILE__ __LINE__ (Some f.meta)
+      save_error __FILE__ __LINE__ (Some f.item_meta.meta)
         ("Ignoring the body of '" ^ name ^ "' because of previous error");
       { f with body = None }
   in
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 713cdef9..c05e9f24 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -323,7 +323,7 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
     List.map
       (fun ((fid, d) : FunDeclId.id * fun_decl) ->
         ( FRegular fid,
-          (Types.name_to_string env d.name, d.signature, Some d.meta) ))
+          (Types.name_to_string env d.name, d.signature, Some d.item_meta.meta) ))
       (FunDeclId.Map.bindings fun_decls)
   in
   let assumed =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 15b52237..2fa68329 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -584,16 +584,16 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let name = Print.Types.name_to_string env def.name in
   let { T.regions; types; const_generics; trait_clauses } = def.generics in
   (* Can't translate types with regions for now *)
-  cassert __FILE__ __LINE__ (regions = []) def.meta
+  cassert __FILE__ __LINE__ (regions = []) def.item_meta.meta
     "ADTs containing borrows are not supported yet";
   let trait_clauses =
-    List.map (translate_trait_clause def.meta) trait_clauses
+    List.map (translate_trait_clause def.item_meta.meta) trait_clauses
   in
   let generics = { types; const_generics; trait_clauses } in
-  let kind = translate_type_decl_kind def.meta def.T.kind in
-  let preds = translate_predicates def.meta def.preds in
+  let kind = translate_type_decl_kind def.item_meta.meta def.T.kind in
+  let preds = translate_predicates def.item_meta.meta def.preds in
   let is_local = def.is_local in
-  let meta = def.meta in
+  let meta = def.item_meta.meta in
   {
     def_id;
     is_local;
@@ -1262,7 +1262,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
   let regions_hierarchy =
     FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies
   in
-  let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).meta in
+  let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.meta in
   translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx
     (FunId (FRegular fun_id)) regions_hierarchy sg input_names
 
@@ -2186,7 +2186,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                   | PeIdent (s, _) -> s
                   | PeImpl _ ->
                       (* We shouldn't get there *)
-                      craise __FILE__ __LINE__ decl.meta "Unexpected")
+                      craise __FILE__ __LINE__ decl.item_meta.meta "Unexpected")
             in
             name ^ "_back"
           in
@@ -3839,7 +3839,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         (* Add a match over the fuel, if necessary *)
         let body =
           if function_decreases_fuel effect_info then
-            wrap_in_match_fuel def.meta ctx.fuel0 ctx.fuel body
+            wrap_in_match_fuel def.item_meta.meta ctx.fuel0 ctx.fuel body
           else body
         in
         (* Sanity check *)
@@ -3884,7 +3884,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
             (List.for_all
                (fun (var, ty) -> (var : var).ty = ty)
                (List.combine inputs signature.inputs))
-            def.meta;
+            def.item_meta.meta;
         Some { inputs; inputs_lvs; body }
   in
 
@@ -3900,7 +3900,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     {
       def_id;
       is_local = def.is_local;
-      meta = def.meta;
+      meta = def.item_meta.meta;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3938,7 +3938,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     def_id;
     is_local;
     name = llbc_name;
-    meta;
+    item_meta;
     generics = llbc_generics;
     preds;
     parent_clauses = llbc_parent_clauses;
@@ -3955,23 +3955,23 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params trait_decl.meta llbc_generics in
-  let preds = translate_predicates trait_decl.meta preds in
+  let generics = translate_generic_params trait_decl.item_meta.meta llbc_generics in
+  let preds = translate_predicates trait_decl.item_meta.meta preds in
   let parent_clauses =
-    List.map (translate_trait_clause trait_decl.meta) llbc_parent_clauses
+    List.map (translate_trait_clause trait_decl.item_meta.meta) llbc_parent_clauses
   in
   let consts =
     List.map
       (fun (name, (ty, id)) ->
-        (name, (translate_fwd_ty trait_decl.meta type_infos ty, id)))
+        (name, (translate_fwd_ty trait_decl.item_meta.meta type_infos ty, id)))
       consts
   in
   let types =
     List.map
       (fun (name, (trait_clauses, ty)) ->
         ( name,
-          ( List.map (translate_trait_clause trait_decl.meta) trait_clauses,
-            Option.map (translate_fwd_ty trait_decl.meta type_infos) ty ) ))
+          ( List.map (translate_trait_clause trait_decl.item_meta.meta) trait_clauses,
+            Option.map (translate_fwd_ty trait_decl.item_meta.meta type_infos) ty ) ))
       types
   in
   {
@@ -3979,7 +3979,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     llbc_name;
     name;
-    meta;
+    meta = item_meta.meta;
     generics;
     llbc_generics;
     preds;
@@ -3997,7 +3997,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     A.def_id;
     is_local;
     name = llbc_name;
-    meta;
+    item_meta;
     impl_trait = llbc_impl_trait;
     generics = llbc_generics;
     preds;
@@ -4011,8 +4011,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
-    translate_trait_decl_ref trait_impl.meta
-      (translate_fwd_ty trait_impl.meta type_infos)
+    translate_trait_decl_ref trait_impl.item_meta.meta
+      (translate_fwd_ty trait_impl.item_meta.meta type_infos)
       llbc_impl_trait
   in
   let name =
@@ -4020,15 +4020,15 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params trait_impl.meta llbc_generics in
-  let preds = translate_predicates trait_impl.meta preds in
+  let generics = translate_generic_params trait_impl.item_meta.meta llbc_generics in
+  let preds = translate_predicates trait_impl.item_meta.meta preds in
   let parent_trait_refs =
-    List.map (translate_strait_ref trait_impl.meta) parent_trait_refs
+    List.map (translate_strait_ref trait_impl.item_meta.meta) parent_trait_refs
   in
   let consts =
     List.map
       (fun (name, (ty, id)) ->
-        (name, (translate_fwd_ty trait_impl.meta type_infos ty, id)))
+        (name, (translate_fwd_ty trait_impl.item_meta.meta type_infos ty, id)))
       consts
   in
   let types =
@@ -4036,9 +4036,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       (fun (name, (trait_refs, ty)) ->
         ( name,
           ( List.map
-              (translate_fwd_trait_ref trait_impl.meta type_infos)
+              (translate_fwd_trait_ref trait_impl.item_meta.meta type_infos)
               trait_refs,
-            translate_fwd_ty trait_impl.meta type_infos ty ) ))
+            translate_fwd_ty trait_impl.item_meta.meta type_infos ty ) ))
       types
   in
   {
@@ -4046,7 +4046,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     llbc_name;
     name;
-    meta;
+    meta = item_meta.meta;
     impl_trait;
     llbc_impl_trait;
     generics;
@@ -4062,7 +4062,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
 let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
     global_decl =
   let {
-    A.meta;
+    A.item_meta;
     def_id;
     is_local;
     name = llbc_name;
@@ -4079,11 +4079,11 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params decl.meta llbc_generics in
-  let preds = translate_predicates decl.meta preds in
-  let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in
+  let generics = translate_generic_params decl.item_meta.meta llbc_generics in
+  let preds = translate_predicates decl.item_meta.meta preds in
+  let ty = translate_fwd_ty decl.item_meta.meta ctx.type_ctx.type_infos ty in
   {
-    meta;
+    meta = item_meta.meta;
     def_id;
     is_local;
     llbc_name;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 9460c5f4..222b3c57 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
 
   let ctx =
     {
-      meta = fdef.meta;
+      meta = fdef.item_meta.meta;
       decls_ctx = trans_ctx;
       SymbolicToPure.bid = None;
       sg;
@@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
           SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx
         in
         { ctx with forward_inputs }
-    | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+    | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
   in
 
   (* Add the backward inputs *)
@@ -486,7 +486,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
   let global_decls = ctx.trans_ctx.global_ctx.global_decls in
   let global = GlobalDeclId.Map.find id global_decls in
   let trans = FunDeclId.Map.find global.body ctx.trans_funs in
-  sanity_check __FILE__ __LINE__ (trans.loops = []) global.meta;
+  sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta;
   let body = trans.f in
 
   let is_opaque = Option.is_none body.Pure.body in
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index e6621c7a..987df6ca 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -289,7 +289,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             (List.map
                (fun v -> List.map (fun f -> f.field_ty) v.fields)
                variants)
-      | Opaque -> craise __FILE__ __LINE__ def.meta "unreachable"
+      | Opaque -> craise __FILE__ __LINE__ def.item_meta.meta "unreachable"
     in
     (* Explore the types and accumulate information *)
     let type_decl_info = TypeDeclId.Map.find def.def_id infos in