changes after git rebase main

11 files changed, 50 insertions, 41 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0e86e187..43acba94 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -46,7 +46,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
           let f = def.f in
           let open ExtractBuiltin in
           let fun_id = (Pure.FunId (FRegular f.def_id), f.loop_id) in
-          ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
+          ctx_add f.meta (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
       | None ->
           (* Not builtin *)
           (* If this is a trait method implementation, we prefix the name with the
@@ -194,7 +194,7 @@ let extract_global (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
   (* Extract the global name *)
   F.pp_print_string fmt (ctx_get_global meta id ctx);
   (* Extract the generics *)
-  extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+  extract_generic_args meta ctx fmt TypeDeclId.Set.empty generics;
   if use_brackets then F.pp_print_string fmt ")";
   F.pp_close_box fmt ()
 
@@ -336,7 +336,7 @@ and extract_App (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (i
       | AdtCons adt_cons_id ->
           extract_adt_cons meta ctx fmt inside adt_cons_id qualif.generics args
       | Proj proj ->
-          extract_field_projector ctx fmt inside app proj qualif.generics args
+          extract_field_projector meta ctx fmt inside app proj qualif.generics args
       | TraitConst (trait_ref, const_name) ->
           extract_trait_ref meta ctx fmt TypeDeclId.Set.empty true trait_ref;
           let name =
@@ -1735,7 +1735,7 @@ let extract_global_decl_body_gen (meta : Meta.meta) (ctx : extraction_ctx) (fmt
 
   (* Extract the generic parameters *)
   let space = ref true in
-  extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space)
+  extract_generic_params meta ctx fmt TypeDeclId.Set.empty ~space:(Some space)
     generics type_params cg_params trait_clauses;
   if not !space then F.pp_print_space fmt ();
 
@@ -1838,6 +1838,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) (f
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : global_decl) (body : fun_decl) (interface : bool) : unit =
+
+  let meta = body.meta in
   cassert body.is_global_decl_body body.meta "TODO: Error message";
   cassert (body.signature.inputs = []) body.meta "TODO: Error message";
 
@@ -1865,7 +1867,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   in
   (* Add the type parameters *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params global.llbc_name global.llbc_generics global.generics
+    ctx_add_generic_params meta global.llbc_name global.llbc_generics global.generics
       ctx
   in
   match body.body with
@@ -2657,7 +2659,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
            is a provided constant or not *)
         let print_params () =
           if provided_id = Some id then
-            extract_generic_args ctx fmt TypeDeclId.Set.empty
+            extract_generic_args impl.meta ctx fmt TypeDeclId.Set.empty
               impl.impl_trait.decl_generics
           else
             let all_params =
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 022643f5..aae11f19 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1273,12 +1273,20 @@ let ctx_prepare_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name
       craise
         meta
            ("Unexpected name shape: "
-           ^ TranslateCore.name_to_string ctx.trans_ctx name))
+           ^ TranslateCore.name_to_string ctx.trans_ctx name)
+
+(** Helper *)
+let ctx_compute_simple_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) :
+    string list =
+  (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+  let name = ctx_prepare_name meta ctx name in
+  name_to_simple_name ctx.trans_ctx name
 
 (** Helper *)
 let ctx_compute_simple_type_name = ctx_compute_simple_name
 
 (** Helper *)
+
 let ctx_compute_type_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) :
     string =
   flatten_name (ctx_compute_simple_type_name meta ctx name)
@@ -1369,7 +1377,7 @@ let ctx_compute_global_name (meta : Meta.meta) (ctx : extraction_ctx) (name : ll
   | Coq | FStar | HOL4 ->
       let parts = List.map to_snake_case (ctx_compute_simple_name meta ctx name) in
       String.concat "_" parts
-  | Lean -> flatten_name (ctx_compute_simple_name ctx name)
+  | Lean -> flatten_name (ctx_compute_simple_name meta ctx name)
 
 (** Helper function: generate a suffix for a function name, i.e., generates
     a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1386,7 +1394,7 @@ let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
 (** A helper function: generates a function suffix.
     TODO: move all those helpers.
 *)
-let default_fun_suffix (meta : Meta.meta) (num_loops : int) (loop_id : LoopId.id option) : string =
+let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string =
   (* We only generate a suffix for the functions we generate from the loops *)
   default_fun_loop_suffix num_loops loop_id
 
@@ -1404,7 +1412,7 @@ let ctx_compute_fun_name (meta : Meta.meta) (ctx : extraction_ctx) (fname : llbc
     (num_loops : int) (loop_id : LoopId.id option) : string =
   let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
   (* Compute the suffix *)
-  let suffix = default_fun_suffix meta num_loops loop_id in
+  let suffix = default_fun_suffix num_loops loop_id in
   (* Concatenate *)
   fname ^ suffix
 
@@ -1423,7 +1431,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
   let name =
     let params = trait_impl.llbc_generics in
     let args = trait_impl.llbc_impl_trait.decl_generics in
-    let name = ctx_prepare_name ctx trait_decl.llbc_name in
+    let name = ctx_prepare_name trait_impl.meta ctx trait_decl.llbc_name in
     trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
   in
   let name = flatten_name name in
@@ -1879,7 +1887,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       ctx_add def.meta decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
-      let name = ctx_compute_global_name ctx def.name in
+      let name = ctx_compute_global_name def.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
@@ -1888,8 +1896,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 decl (name ^ suffix) ctx in
-      let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in
+      let ctx = ctx_add def.meta decl (name ^ suffix) ctx in
+      let ctx = ctx_add def.meta body (name ^ suffix ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a8143876..94acd08c 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -548,7 +548,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            cassert (trait_ref.generics = empty_generic_args) "TODO: Error message";
+            cassert (trait_ref.generics = empty_generic_args) meta "TODO: Error message";
             extract_trait_instance_id_with_dot meta ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index d2f1b5fb..89015f71 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -102,7 +102,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
           - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx
        ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
 
-    prepare_match_ctx_with_target config loop_id fixed_ids fp_ctx cf ctx
+    prepare_match_ctx_with_target config meta loop_id fixed_ids fp_ctx cf ctx
   in
 
   (* Actually match *)
@@ -264,7 +264,7 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
   | SymbolicMode ->
       (* Simplify the context by ending the unnecessary borrows/loans and getting
          rid of the useless symbolic values (which are in anonymous variables) *)
-      let cc = cleanup_fresh_values_and_abs config empty_ids_set in
+      let cc = cleanup_fresh_values_and_abs config meta empty_ids_set in
 
       (* We want to make sure the loop will *not* manipulate shared avalues
          containing themselves shared loans (i.e., nested shared loans in
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index f6ce9b32..f5bd4a35 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -23,7 +23,7 @@ exception FoundAbsId of AbstractionId.id
    - end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let rec end_useless_fresh_borrows_and_abs (config : config)
+let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
     (fixed_ids : ids_sets) : cm_fun =
  fun cf ctx ->
   let rec explore_env (env : env) : unit =
@@ -56,7 +56,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
     | EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)
       -> (
         (* Check if it is possible to end the abstraction: if yes, raise an exception *)
-        let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+        let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
         match opt_loan with
         | None ->
             (* No remaining loans: we can end the abstraction *)
@@ -66,7 +66,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
             explore_env env)
     | _ :: env -> explore_env env
   in
-  let rec_call = end_useless_fresh_borrows_and_abs config fixed_ids in
+  let rec_call = end_useless_fresh_borrows_and_abs config meta fixed_ids in
   try
     (* Explore the environment *)
     explore_env ctx.env;
@@ -74,10 +74,10 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
     cf ctx
   with
   | FoundAbsId abs_id ->
-      let cc = end_abstraction config abs_id in
+      let cc = end_abstraction config meta abs_id in
       comp cc rec_call cf ctx
   | FoundBorrowId bid ->
-      let cc = end_borrow config bid in
+      let cc = end_borrow config meta bid in
       comp cc rec_call cf ctx
 
 (* Explore the fresh anonymous values and replace all the values which are not
@@ -121,11 +121,11 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun =
    - also end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) :
+let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) :
     cm_fun =
  fun cf ctx ->
   comp
-    (end_useless_fresh_borrows_and_abs config fixed_ids)
+    (end_useless_fresh_borrows_and_abs config meta fixed_ids)
     (cleanup_fresh_values fixed_ids)
     cf ctx
 
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 4568bf79..54e4d780 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -13,7 +13,7 @@ open InterpreterLoopsCore
    - config
    - fixed ids (the fixeds ids are the ids we consider as non-fresh)
  *)
-val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun
+val cleanup_fresh_values_and_abs : config -> Meta.meta -> ids_sets -> Cps.cm_fun
 
 (** Prepare the shared loans in the abstractions by moving them to fresh
     abstractions.
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index c02d3117..24e588f2 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -459,8 +459,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     (* Lookup the shared values and match them - we do this mostly
        to make sure we end loans which might appear on one side
        and not on the other. *)
-    let sv0 = lookup_shared_value ctx0 bid0 in
-    let sv1 = lookup_shared_value ctx1 bid1 in
+    let sv0 = lookup_shared_value meta ctx0 bid0 in
+    let sv1 = lookup_shared_value meta ctx1 bid1 in
     let sv = match_rec sv0 sv1 in
     if bid0 = bid1 then bid0
     else
@@ -1544,7 +1544,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
   (* Apply the reorganization *)
   cf_reorganize_join_tgt cf tgt_ctx
 
-let match_ctx_with_target (config : config) (loop_id : LoopId.id)
+let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
     (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
     (src_ctx : eval_ctx) : st_cm_fun =
@@ -1562,7 +1562,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
      were introduced during the loop iterations)
   *)
   let cf_reorganize_join_tgt =
-    prepare_match_ctx_with_target config loop_id fixed_ids src_ctx
+    prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx
   in
 
   (* Introduce the "identity" abstractions for the loop re-entry.
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 4a6d24a9..a8002ad4 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -151,7 +151,7 @@ val ctxs_are_equivalent : Meta.meta -> ids_sets -> eval_ctx -> eval_ctx -> bool
 
  *)
 val prepare_match_ctx_with_target :
-  config -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
+  config -> Meta.meta -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
 
 (** Match a context with a target context.
 
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1df7176d..ab4686c9 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1140,7 +1140,7 @@ let simplify_let_then_return _ctx (def : fun_decl) =
               (* The first let-binding is monadic *)
               match opt_destruct_ret next_e with
               | Some e ->
-                  if match_pattern_and_expr def.meta lv e then rv.e else not_simpl_e
+                  if match_pattern_and_expr lv e then rv.e else not_simpl_e
               | None -> not_simpl_e
             else
               (* The first let-binding is not monadic *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e60d6870..3532b2dd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1325,7 +1325,7 @@ let compute_output_ty_from_decomposed (dsg : Pure.decomposed_fun_sig) : ty =
   in
   mk_output_ty_from_effect_info effect_info output
 
-let translate_fun_sig_from_decomposed (meta : Meta.meta) (dsg : Pure.decomposed_fun_sig) : fun_sig
+let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig) : fun_sig
     =
   let generics = dsg.generics in
   let llbc_generics = dsg.llbc_generics in
@@ -2512,7 +2512,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
            ^ "\nfunc type: "
            ^ pure_ty_to_string ctx func.ty
            ^ "\n\nargs:\n" ^ String.concat "\n" args));
-      let call = mk_apps func args in
+      let call = mk_apps ctx.fun_decl.meta func args in
       mk_let effect_info.can_fail output call next_e
 
 and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
@@ -2671,7 +2671,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       match func with
       | None -> next_e
       | Some func ->
-          let call = mk_apps func args in
+          let call = mk_apps ctx.fun_decl.meta func args in
           (* Add meta-information - this is slightly hacky: we look at the
              values consumed by the abstraction (note that those come from
              *before* we applied the fixed-point context) and use them to
@@ -3682,7 +3682,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let llbc_name = def.name in
   let name = name_to_string ctx llbc_name in
   (* Translate the signature *)
-  let signature = translate_fun_sig_from_decomposed def.meta ctx.sg in
+  let signature = translate_fun_sig_from_decomposed ctx.sg in
   (* Translate the body, if there is *)
   let body =
     match body with
@@ -3915,9 +3915,9 @@ 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 llbc_generics in
-  let preds = translate_predicates preds in
-  let ty = translate_fwd_ty ctx.type_ctx.type_infos ty 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
   {
     meta;
     def_id;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index f97d7ab1..9834fe81 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -447,9 +447,8 @@ 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 (trans.fwd.loops = []) global.meta;
-  sanity_check (trans.backs = []) global.meta;
-  let body = trans.fwd.f in
+  sanity_check (trans.loops = []) global.meta;
+  let body = trans.f in
 
   let is_opaque = Option.is_none body.Pure.body in
   (* Check if we extract the global *)