Inverted meta and config argument orders (from meta -> config to config -> meta)

author: Escherichia 2024-03-25 12:06:05 +0100
committer: Escherichia 2024-03-28 15:27:35 +0100
commit: d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 (patch)
tree: 14c7bca01e105ec6bf3db8ccedb21d64ae4ae756
parent: 9b1a0d82c19375619904efe7e18e064701fb947b (diff)
20 files changed, 303 insertions, 303 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a9ca415e..6e2c15d7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -286,7 +286,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   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 fdef.meta config pop_return_value in
+  let cf_pop_frame = pop_frame config fdef.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
@@ -314,7 +314,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 fdef.meta config ctx abs.regions
+            apply_proj_borrows_on_input_value config fdef.meta ctx abs.regions
               abs.ancestors_regions ret_value ret_rty
           in
           (ctx, [ avalue ])
@@ -447,7 +447,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 fdef.meta config id cf)
+        (fun cf id -> end_abstraction config fdef.meta id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -513,7 +513,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 fdef.meta config pop_return_value in
+            let cf_pop = pop_frame config fdef.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return ret_value : m_fun =
              fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -563,7 +563,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             (* 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 fdef.meta config pop_return_value in
+            let cf_pop = pop_frame config fdef.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))
@@ -603,7 +603,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body fdef.meta config (Option.get fdef.body).body cf_finish ctx
+    eval_function_body config fdef.meta (Option.get fdef.body).body cf_finish ctx
   in
 
   (* Return *)
@@ -644,7 +644,7 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame fdef.meta config pop_return_value (fun _ _ -> None) ctx
+          pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
           craise
             fdef.meta
@@ -655,7 +655,7 @@ module Test = struct
     in
 
     (* Evaluate the function *)
-    let _ = eval_function_body body.meta config body.body cf_check ctx in
+    let _ = eval_function_body config body.meta body.body cf_check ctx in
     ()
 
   (** Small helper: return true if the function is a *transparent* unit function
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index be31d865..c7df2eca 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -245,7 +245,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
     give the value back.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv : typed_value)
+let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
   cassert (not (loans_in_value nv)) meta "TODO: error message";
@@ -267,7 +267,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   (* We sometimes need to reborrow values while giving a value back due: prepare that *)
   let allow_reborrows = true in
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* The visitor to give back the values *)
   let obj =
@@ -440,7 +440,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   apply_registered_reborrows ctx
 
 (** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions : RegionId.Set.t)
+let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions : RegionId.Set.t)
     (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
@@ -485,7 +485,7 @@ let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions
     end abstraction when ending this abstraction. When doing this, we need
     to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
  *)
-let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (bid : BorrowId.id)
+let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (bid : BorrowId.id)
     (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
@@ -588,7 +588,7 @@ let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared (meta : Meta.meta) _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
+let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -739,7 +739,7 @@ let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
     borrows. This kind of internal reshuffling. should be similar to ending
     abstractions (it is tantamount to ending *sub*-abstractions).
  *)
-let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_borrow_content)
+let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_borrow_content)
     (ctx : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
@@ -763,14 +763,14 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
       (* Update the context *)
-      give_back_value meta config l tv ctx
+      give_back_value config meta l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
       cassert (l' = l) meta "TODO: error message";
       (* Check that the borrow is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
       cassert (l' = l) meta "TODO: error message";
@@ -783,7 +783,7 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       *)
       let sv = convert_avalue_to_given_back_value meta av in
       (* Update the context *)
-      give_back_avalue_to_same_abstraction meta config l av
+      give_back_avalue_to_same_abstraction config meta l av
         (mk_typed_value_from_symbolic_value sv)
         ctx
   | Abstract (ASharedBorrow l') ->
@@ -792,12 +792,12 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       (* Check that the borrow is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
       cassert (borrow_in_asb l asb) meta "TODO: error message";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract
       ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
       | AEndedSharedBorrow ) ->
@@ -852,7 +852,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -900,22 +900,22 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
            * inside another borrow *)
           let allowed_abs' = None in
           (* End the outer borrows *)
-          let cc = end_borrows_aux meta config chain allowed_abs' bids in
+          let cc = end_borrows_aux config meta chain allowed_abs' bids in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
-          let cc = end_borrow_aux meta config chain allowed_abs' bid in
+          let cc = end_borrow_aux config meta chain allowed_abs' bid in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterAbs abs_id ->
           (* The borrow is inside an abstraction: end the whole abstraction *)
-          let cf_end_abs = end_abstraction_aux meta config chain abs_id in
+          let cf_end_abs = end_abstraction_aux config meta chain abs_id in
           (* Compose with a sanity check *)
           comp cf_end_abs cf_check cf ctx)
   | Ok (ctx, None) ->
@@ -934,7 +934,7 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
           cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans"
       | _ -> ());
       (* Give back the value *)
-      let ctx = give_back meta config l bc ctx in
+      let ctx = give_back config meta l bc ctx in
       (* Do a sanity check and continue *)
       let cc = cf_check in
       (* Save a snapshot of the environment for the name generation *)
@@ -942,7 +942,7 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
       (* Compose *)
       cc cf ctx
 
-and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the borrow ids,
@@ -950,10 +950,10 @@ and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_
    * a matter of taste, and may make debugging easier *)
   let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
   List.fold_left
-    (fun cf id -> end_borrow_aux meta config chain allowed_abs id cf)
+    (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf)
     cf ids
 
-and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -991,7 +991,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
              ^ " as it is set as non-endable");
 
       (* End the parent abstractions first *)
-      let cc = end_abstractions_aux meta config chain abs.parents in
+      let cc = end_abstractions_aux config meta chain abs.parents in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1003,7 +1003,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       in
 
       (* End the loans inside the abstraction *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1014,7 +1014,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
-      let cc = comp cc (end_abstraction_borrows meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_borrows config meta chain abs_id) in
 
       (* End the regions owned by the abstraction - note that we don't need to
        * relookup the abstraction: the set of regions in an abstraction never
@@ -1030,7 +1030,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Remove all the references to the id of the current abstraction, and remove
        * the abstraction itself.
        * **Rk.**: this is where we synthesize the updated symbolic AST *)
-      let cc = comp cc (end_abstraction_remove_from_context meta config abs_id) in
+      let cc = comp cc (end_abstraction_remove_from_context config meta abs_id) in
 
       (* Debugging *)
       let cc =
@@ -1052,7 +1052,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Apply the continuation *)
       cc cf ctx
 
-and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_ids : AbstractionId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
@@ -1060,10 +1060,10 @@ and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or
    * a matter of taste, and may make debugging easier *)
   let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
   List.fold_left
-    (fun cf id -> end_abstraction_aux meta config chain id cf)
+    (fun cf id -> end_abstraction_aux config meta chain id cf)
     cf abs_ids
 
-and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Lookup the abstraction *)
@@ -1081,23 +1081,23 @@ and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_o
       (* There are loans: end the corresponding borrows, then recheck *)
       let cc : cm_fun =
         match bids with
-        | Borrow bid -> end_borrow_aux meta config chain None bid
-        | Borrows bids -> end_borrows_aux meta config chain None bids
+        | Borrow bid -> end_borrow_aux config meta chain None bid
+        | Borrows bids -> end_borrows_aux config meta chain None bids
       in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       (* Continue *)
       cc cf ctx
   | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
        * which intersect this proj_loans, then end the proj_loans itself *)
-      let cc = end_proj_loans_symbolic meta config chain abs_id abs.regions sv in
+      let cc = end_proj_loans_symbolic config meta chain abs_id abs.regions sv in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       (* Continue *)
       cc cf ctx
 
-and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -1185,13 +1185,13 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
-            give_back_value meta config bid sv ctx
+            give_back_value config meta bid sv ctx
         | ASharedBorrow bid ->
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = ABorrow AEndedSharedBorrow in
             let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give back *)
-            give_back_shared meta config bid ctx
+            give_back_shared config meta bid ctx
         | AProjSharedBorrow asb ->
             (* Retrieve the borrow ids *)
             let bids =
@@ -1210,7 +1210,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             (* Give back the shared borrows *)
             let ctx =
               List.fold_left
-                (fun ctx bid -> give_back_shared meta config bid ctx)
+                (fun ctx bid -> give_back_shared config meta bid ctx)
                 ctx bids
             in
             (* Continue *)
@@ -1220,7 +1220,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             craise meta "Unexpected"
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
   (* There are symbolic borrows: end them, then reexplore *)
   | FoundAProjBorrows (sv, proj_ty) ->
       log#ldebug
@@ -1234,10 +1234,10 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-        give_back_symbolic_value meta config abs.regions proj_ty sv nsv ctx
+        give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
   (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
   | FoundBorrowContent bc ->
       log#ldebug
@@ -1255,7 +1255,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             | Error _ -> craise meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give back *)
-                give_back_shared meta config bid ctx)
+                give_back_shared config meta bid ctx)
         | VMutBorrow (bid, v) -> (
             (* Replace the mut borrow with bottom *)
             let allow_inner_loans = false in
@@ -1266,14 +1266,14 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
-                give_back_value meta config bid v ctx)
+                give_back_value config meta bid v ctx)
         | VReservedMutBorrow _ -> craise meta "Unreachable"
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
+and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   let ctx, abs = ctx_remove_abs meta ctx abs_id in
@@ -1297,7 +1297,7 @@ and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value)
     : cm_fun =
  fun cf ctx ->
@@ -1360,7 +1360,7 @@ and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow
             AbstractionId.Set.empty abs_ids
         in
         (* End the abstractions and continue *)
-        end_abstractions_aux meta config chain abs_ids cf ctx
+        end_abstractions_aux config meta chain abs_ids cf ctx
       in
       (* End the internal borrows projectors and the loans projector *)
       let cf_end_internal : cm_fun =
@@ -1413,35 +1413,35 @@ and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow
         cf ctx)
       else
         (* The borrows proj comes from a different abstraction: end it. *)
-        let cc = end_abstraction_aux meta config chain abs_id' in
+        let cc = end_abstraction_aux config meta chain abs_id' in
         (* Retry ending the projector of loans *)
         let cc =
-          comp cc (end_proj_loans_symbolic meta config chain abs_id regions sv)
+          comp cc (end_proj_loans_symbolic config meta chain abs_id regions sv)
         in
         (* Sanity check *)
         let cc = comp cc cf_check in
         (* Continue *)
         cc cf ctx
 
-let end_borrow (meta : Meta.meta ) config : BorrowId.id -> cm_fun = end_borrow_aux meta config [] None
+let end_borrow config (meta : Meta.meta ) : BorrowId.id -> cm_fun = end_borrow_aux config meta [] None
 
-let end_borrows (meta : Meta.meta ) config : BorrowId.Set.t -> cm_fun =
-  end_borrows_aux meta config [] None
+let end_borrows config (meta : Meta.meta ) : BorrowId.Set.t -> cm_fun =
+  end_borrows_aux config meta [] None
 
-let end_abstraction meta config = end_abstraction_aux meta config []
-let end_abstractions meta config = end_abstractions_aux meta config []
+let end_abstraction config meta = end_abstraction_aux config meta []
+let end_abstractions config meta = end_abstractions_aux config meta []
 
-let end_borrow_no_synth meta config id ctx =
-  get_cf_ctx_no_synth meta (end_borrow meta config id) ctx
+let end_borrow_no_synth config meta id ctx =
+  get_cf_ctx_no_synth meta (end_borrow config meta id) ctx
 
-let end_borrows_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth meta (end_borrows meta config ids) ctx
+let end_borrows_no_synth config meta ids ctx =
+  get_cf_ctx_no_synth meta (end_borrows config meta ids) ctx
 
-let end_abstraction_no_synth meta config id ctx =
-  get_cf_ctx_no_synth meta (end_abstraction meta config id) ctx
+let end_abstraction_no_synth config meta id ctx =
+  get_cf_ctx_no_synth meta (end_abstraction config meta id) ctx
 
-let end_abstractions_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth meta (end_abstractions meta config ids) ctx
+let end_abstractions_no_synth config meta ids ctx =
+  get_cf_ctx_no_synth meta (end_abstractions config meta ids) ctx
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1532,7 +1532,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
   cf ctx
 
 (** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : BorrowId.id) : cm_fun
+let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : BorrowId.id) : cm_fun
     =
  fun cf ctx ->
   (* Lookup the value *)
@@ -1550,11 +1550,11 @@ let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : Bo
           (* End the loans *)
           let cc =
             match lc with
-            | VSharedLoan (bids, _) -> end_borrows meta config bids
-            | VMutLoan bid -> end_borrow meta config bid
+            | VSharedLoan (bids, _) -> end_borrows config meta bids
+            | VMutLoan bid -> end_borrow config meta bid
           in
           (* Recursive call *)
-          let cc = comp cc (promote_reserved_mut_borrow meta config l) in
+          let cc = comp cc (promote_reserved_mut_borrow config meta l) in
           (* Continue *)
           cc cf ctx
       | None ->
@@ -1570,7 +1570,7 @@ let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : Bo
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
-          let cc = end_borrows meta config bids in
+          let cc = end_borrows config meta bids in
           (* Promote the loan - TODO: this will fail if the value contains
            * any loans. In practice, it shouldn't, but we could also
            * look for loans inside the value and end them before promoting
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 95a27245..fbd2cd7a 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -15,30 +15,30 @@ val reborrow_shared : Meta.meta -> BorrowId.id -> BorrowId.id -> eval_ctx -> eva
     If the borrow is inside another borrow/an abstraction or contains loans,
     [end_borrow] will end those borrows/abstractions/loans first.
   *)
-val end_borrow : Meta.meta -> config -> BorrowId.id -> cm_fun
+val end_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
 
 (** End a set of borrows identified by their ids, while preserving the invariants. *)
-val end_borrows : Meta.meta -> config -> BorrowId.Set.t -> cm_fun
+val end_borrows : config -> Meta.meta -> BorrowId.Set.t -> cm_fun
 
 (** End an abstraction while preserving the invariants. *)
-val end_abstraction : Meta.meta -> config -> AbstractionId.id -> cm_fun
+val end_abstraction : config -> Meta.meta -> AbstractionId.id -> cm_fun
 
 (** End a set of abstractions while preserving the invariants. *)
-val end_abstractions : Meta.meta -> config -> AbstractionId.Set.t -> cm_fun
+val end_abstractions : config -> Meta.meta -> AbstractionId.Set.t -> cm_fun
 
 (** End a borrow and return the resulting environment, ignoring synthesis *)
-val end_borrow_no_synth : Meta.meta -> config -> BorrowId.id -> eval_ctx -> eval_ctx
+val end_borrow_no_synth : config -> Meta.meta -> BorrowId.id -> eval_ctx -> eval_ctx
 
 (** End a set of borrows and return the resulting environment, ignoring synthesis *)
-val end_borrows_no_synth : Meta.meta -> config -> BorrowId.Set.t -> eval_ctx -> eval_ctx
+val end_borrows_no_synth : config -> Meta.meta -> BorrowId.Set.t -> eval_ctx -> eval_ctx
 
 (** End an abstraction and return the resulting environment, ignoring synthesis *)
 val end_abstraction_no_synth :
-  Meta.meta -> config -> AbstractionId.id -> eval_ctx -> eval_ctx
+  config -> Meta.meta -> AbstractionId.id -> eval_ctx -> eval_ctx
 
 (** End a set of abstractions and return the resulting environment, ignoring synthesis *)
 val end_abstractions_no_synth :
-  Meta.meta -> config -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
+  config -> Meta.meta -> AbstractionId.Set.t -> eval_ctx -> eval_ctx
 
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
@@ -49,7 +49,7 @@ val end_abstractions_no_synth :
     the corresponding shared loan with a mutable loan (after having ended the
     other shared borrows which point to this loan).
  *)
-val promote_reserved_mut_borrow : Meta.meta -> config -> BorrowId.id -> cm_fun
+val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun
 
 (** Transform an abstraction to an abstraction where the values are not
     structured.
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 9448f3e8..2f886714 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -48,7 +48,7 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.meta)
     (allow_reborrows : bool) (proj_kind : proj_kind)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
@@ -56,7 +56,7 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* Visitor to apply the expansion *)
   let obj =
@@ -146,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
 (** Auxiliary function.
     Apply a symbolic expansion to avalues in a context.
 *)
-let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta)
     (allow_reborrows : bool) (original_sv : symbolic_value)
     (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind
+    apply_symbolic_expansion_to_target_avalues config meta allow_reborrows proj_kind
       original_sv expansion ctx
   in
   (* First target the loan projectors, then the borrow projectors *)
@@ -187,7 +187,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s
   (* Return *)
   ctx
 
-let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
@@ -196,7 +196,7 @@ let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
   let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
-  apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
+  apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
     expansion ctx
 
 (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
@@ -275,7 +275,7 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations
       craise
         meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
-let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
+let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : rty) : cm_fun =
  fun cf ctx ->
@@ -380,7 +380,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
-    apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv see
+    apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see
       ctx
   in
   (* Call the continuation *)
@@ -390,7 +390,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
     expr
 
 (** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
+let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
@@ -413,7 +413,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
-        apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
+        apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
           see ctx
       in
       (* Apply the continuation *)
@@ -422,7 +422,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
       S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
         see expr
   | RShared ->
-      expand_symbolic_value_shared_borrow meta config original_sv original_sv_place
+      expand_symbolic_value_shared_borrow config meta original_sv original_sv_place
         ref_ty cf ctx
 
 (** A small helper.
@@ -441,7 +441,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config)
+let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Meta.meta)
     (sv : symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
@@ -457,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
         let ctx =
           match see_opt with
           | None -> ctx
-          | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx
+          | Some see -> apply_symbolic_expansion_non_borrow config meta sv see ctx
         in
         (* Debug *)
         log#ldebug
@@ -484,7 +484,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
   let seel = List.map fst see_cf_l in
   S.synthesize_symbolic_expansion meta sv sv_place seel subterms
 
-let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -498,10 +498,10 @@ let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_val
   let see_false = SeLiteral (VBool false) in
   let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
   (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-  apply_branching_symbolic_expansions_non_borrow meta config original_sv
+  apply_branching_symbolic_expansions_non_borrow config meta original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
@@ -530,7 +530,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
         let see = Collections.List.to_cons_nil seel in
         (* Apply in the context *)
         let ctx =
-          apply_symbolic_expansion_non_borrow meta config original_sv see ctx
+          apply_symbolic_expansion_non_borrow config meta original_sv see ctx
         in
         (* Call the continuation *)
         let expr = cf ctx in
@@ -539,7 +539,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
           original_sv_place see expr
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow meta config original_sv original_sv_place region
+        expand_symbolic_value_borrow config meta original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
         craise
@@ -562,7 +562,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -584,12 +584,12 @@ let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_valu
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
-      apply_branching_symbolic_expansions_non_borrow meta config original_sv
+      apply_branching_symbolic_expansions_non_borrow config meta original_sv
         original_sv_place seel cf_after_join ctx
   | _ ->
       craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
-let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (int_type : integer_type)
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
@@ -609,7 +609,7 @@ let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_valu
   in
   let seel = List.append seel [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
-  apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel
+  apply_branching_symbolic_expansions_non_borrow config meta sv sv_place seel
     cf_after_join
 
 (** Expand all the symbolic values which contain borrows.
@@ -620,7 +620,7 @@ let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_valu
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
@@ -677,10 +677,10 @@ let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) :
                      (option [greedy_expand_symbolics_with_borrows] of \
                      [config]): "
                    ^ name_to_string ctx def.name)
-            else expand_symbolic_value_no_branching meta config sv None
+            else expand_symbolic_value_no_branching config meta sv None
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching meta config sv None
+            expand_symbolic_value_no_branching config meta sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
             craise
@@ -695,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) :
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun =
+let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
-    greedy_expand_symbolics_with_borrows meta config cf ctx)
+    greedy_expand_symbolics_with_borrows config meta cf ctx)
   else cf ctx
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 3540d04c..8b0b386a 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -12,11 +12,11 @@ type proj_kind = LoanProj | BorrowProj
     This function does *not* update the synthesis.
 *)
 val apply_symbolic_expansion_non_borrow :
-  Meta.meta -> config -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx
+  config -> Meta.meta -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx
 
 (** Expand a symhbolic value, without branching *)
 val expand_symbolic_value_no_branching :
-  Meta.meta -> config -> symbolic_value -> SA.mplace option -> cm_fun
+  config -> Meta.meta -> symbolic_value -> SA.mplace option -> cm_fun
 
 (** Expand a symbolic enumeration (leads to branching if the enumeration has
     more than one variant).
@@ -32,7 +32,7 @@ val expand_symbolic_value_no_branching :
       then call it).
  *)
 val expand_symbolic_adt :
-  Meta.meta -> config -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun
+  config -> Meta.meta -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun
 
 (** Expand a symbolic boolean.
 
@@ -41,8 +41,8 @@ val expand_symbolic_adt :
     parameter (here, there are exactly two branches).
  *)
 val expand_symbolic_bool :
-  Meta.meta -> 
-  config ->
+  config -> 
+  Meta.meta ->
   symbolic_value ->
   SA.mplace option ->
   st_cm_fun ->
@@ -70,8 +70,8 @@ val expand_symbolic_bool :
     switch. The continuation is thus for the execution *after* the switch.
  *)
 val expand_symbolic_int :
-  Meta.meta -> 
-  config ->
+  config -> 
+  Meta.meta ->
   symbolic_value ->
   SA.mplace option ->
   integer_type ->
@@ -83,4 +83,4 @@ val expand_symbolic_int :
 (** If this mode is activated through the [config], greedily expand the symbolic
     values which need to be expanded. See {!type:Contexts.config} for more information.
  *)
-val greedy_expand_symbolic_values : Meta.meta -> config -> cm_fun
+val greedy_expand_symbolic_values : config -> Meta.meta -> cm_fun
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index f82c7130..d74e0751 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -24,7 +24,7 @@ let log = Logging.expressions_log
     Note that the place should have been prepared so that there are no remaining
     loans.
 *)
-let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
+let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Small helper *)
@@ -37,7 +37,7 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching meta config sv (Some (mk_mplace meta p ctx))
+          expand_symbolic_value_no_branching config meta sv (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -60,19 +60,19 @@ let read_place (meta : Meta.meta) (access : access_kind) (p : place) (cf : typed
   (* Call the continuation *)
   cf v ctx
 
-let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
+let access_rplace_reorganize_and_read (config : config) (meta : Meta.meta)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Make sure we can evaluate the path *)
-  let cc = update_ctx_along_read_place meta config access p in
+  let cc = update_ctx_along_read_place config meta access p in
   (* End the proper loans at the place itself *)
-  let cc = comp cc (end_loans_at_place meta config access p) in
+  let cc = comp cc (end_loans_at_place config meta access p) in
   (* Expand the copyable values which contain borrows (which are necessarily shared
    * borrows) *)
   let cc =
     if expand_prim_copy then
-      comp cc (expand_primitively_copyable_at_place meta config access p)
+      comp cc (expand_primitively_copyable_at_place config meta access p)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -80,10 +80,10 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (config : config) (meta : Meta.meta) (expand_prim_copy : bool)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
-  access_rplace_reorganize_and_read meta config expand_prim_copy access p
+  access_rplace_reorganize_and_read config meta expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
@@ -225,7 +225,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta) (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
@@ -238,18 +238,18 @@ let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : o
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
-        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
     | Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
-        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
   in
   (* Apply *)
   prepare cf ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
-let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operand)
+let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operand)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
@@ -359,7 +359,7 @@ let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operan
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   (* Debug *)
@@ -369,34 +369,34 @@ let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : type
      ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
-    (prepare_eval_operand_reorganize meta config op)
-    (eval_operand_no_reorganize meta config op)
+    (prepare_eval_operand_reorganize config meta op)
+    (eval_operand_no_reorganize config meta op)
     cf ctx
 
 (** Small utility.
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta) (ops : operand list) :
     cm_fun =
-  fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
+  fold_left_apply_continuation (prepare_eval_operand_reorganize config meta) ops
 
 (** Evaluate several operands. *)
-let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
+let eval_operands (config : config) (meta : Meta.meta) (ops : operand list)
     (cf : typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
-  let prepare = prepare_eval_operands_reorganize meta config ops in
+  let prepare = prepare_eval_operands_reorganize config meta ops in
   (* Evaluate the operands *)
   let eval =
-    fold_left_list_apply_continuation (eval_operand_no_reorganize meta config) ops
+    fold_left_list_apply_continuation (eval_operand_no_reorganize config meta) ops
   in
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand) (op2 : operand)
     (cf : typed_value * typed_value -> m_fun) : m_fun =
-  let eval_op = eval_operands meta config [ op1; op2 ] in
+  let eval_op = eval_operands config meta [ op1; op2 ] in
   let use_res cf res =
     match res with
     | [ v1; v2 ] -> cf (v1, v2)
@@ -404,10 +404,10 @@ let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let eval_op = eval_operand meta config op in
+  let eval_op = eval_operand config meta op in
   (* Apply the unop *)
   let apply cf (v : typed_value) : m_fun =
     match (unop, v.value) with
@@ -452,11 +452,11 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand meta config op in
+  let eval_op = eval_operand config meta op in
   (* Generate a fresh symbolic value to store the result *)
   let apply cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -479,11 +479,11 @@ let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (o
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
-  | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
+  | ConcreteMode -> eval_unary_op_concrete config meta unop op cf
+  | SymbolicMode -> eval_unary_op_symbolic config meta unop op cf
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
@@ -558,10 +558,10 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
         | Ne | Eq -> craise meta "Unreachable")
     | _ -> craise meta "Invalid inputs for binop"
 
-let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands meta config op1 op2 in
+  let eval_ops = eval_two_operands config meta op1 op2 in
   (* Compute the result of the binop *)
   let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
@@ -570,11 +570,11 @@ let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands meta config op1 op2 in
+  let eval_ops = eval_two_operands config meta op1 op2 in
   (* Compute the result of applying the binop *)
   let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
    fun ctx ->
@@ -617,13 +617,13 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
-  | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 cf
+  | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 cf
 
-let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : borrow_kind)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
@@ -644,7 +644,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
 
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read meta config expand_prim_copy access p
+        access_rplace_reorganize_and_read config meta expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -694,7 +694,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
       let access = Write in
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read meta config expand_prim_copy access p
+        access_rplace_reorganize_and_read config meta expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -715,10 +715,10 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind : aggregate_kind)
     (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_operands meta config ops in
+  let eval_ops = eval_operands config meta ops in
   (* Compute the value *)
   let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
    fun ctx ->
@@ -782,7 +782,7 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind :
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (config : config) (meta : Meta.meta) (rvalue : rvalue)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
@@ -794,12 +794,12 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue
   let comp_wrap f = comp f wrap_in_result cf in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> comp_wrap (eval_operand meta config op) ctx
-  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
-  | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
-  | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
+  | Use op -> comp_wrap (eval_operand config meta op) ctx
+  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config meta p bkind) ctx
+  | UnaryOp (unop, op) -> eval_unary_op config meta unop op cf ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op config meta binop op1 op2 cf ctx
   | Aggregate (aggregate_kind, ops) ->
-      comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
+      comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx
   | Discriminant _ ->
       craise
         meta
@@ -807,11 +807,11 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue
             the AST"
   | Global _ -> craise meta "Unreachable"
 
-let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
+let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
   let expand_prim_copy = false in
   let cf_prepare cf =
-    access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
+    access_rplace_reorganize_and_read config meta expand_prim_copy Read p cf
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index 69455682..76627c40 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -31,7 +31,7 @@ val read_place : Meta.meta -> access_kind -> place -> (typed_value -> m_fun) ->
     primitively copyable and contain borrows.
  *)
 val access_rplace_reorganize_and_read :
-  Meta.meta -> config -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
+  config -> Meta.meta -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
 
 (** Evaluate an operand.
 
@@ -42,11 +42,11 @@ val access_rplace_reorganize_and_read :
     of the environment, before evaluating all the operands at once.
     Use {!eval_operands} instead.
  *)
-val eval_operand : Meta.meta -> config -> operand -> (typed_value -> m_fun) -> m_fun
+val eval_operand : config -> Meta.meta -> operand -> (typed_value -> m_fun) -> m_fun
 
 (** Evaluate several operands at once. *)
 val eval_operands :
-  Meta.meta -> config -> operand list -> (typed_value list -> m_fun) -> m_fun
+  config -> Meta.meta -> operand list -> (typed_value list -> m_fun) -> m_fun
 
 (** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
@@ -56,7 +56,7 @@ val eval_operands :
     reads should have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
-  Meta.meta -> config -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun
+  config -> Meta.meta -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun
 
 (** Evaluate a fake read (update the context so that we can read a place) *)
-val eval_fake_read : Meta.meta -> config -> place -> cm_fun
+val eval_fake_read : config -> Meta.meta -> place -> cm_fun
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 98aa0e14..4d4b709e 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -75,7 +75,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
 
   (* Compute the fixed point at the loop entrance *)
   let fp_ctx, fixed_ids, rg_to_abs =
-    compute_loop_entry_fixed_point meta config loop_id eval_loop_body ctx
+    compute_loop_entry_fixed_point config meta loop_id eval_loop_body ctx
   in
 
   (* Debug *)
@@ -125,7 +125,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
           - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx
        ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx));
     let end_expr : SymbolicAst.expression option =
-      match_ctx_with_target meta config loop_id true fp_bl_corresp fp_input_svalues
+      match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues
         fixed_ids fp_ctx cf ctx
     in
     log#ldebug
@@ -158,7 +158,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
                 - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx
              ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx));
           let cc =
-            match_ctx_with_target meta config loop_id false fp_bl_corresp
+            match_ctx_with_target config meta loop_id false fp_bl_corresp
               fp_input_svalues fixed_ids fp_ctx
           in
           cc cf ctx
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 508d0f0c..ef2c5698 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -437,7 +437,7 @@ let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx
     eval_ctx =
   get_cf_ctx_no_synth meta (prepare_ashared_loans meta (Some loop_id)) ctx
 
-let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
+let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
     eval_ctx * ids_sets * abs RegionGroupId.Map.t =
   (* The continuation for when we exit the loop - we register the
@@ -510,10 +510,10 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
           (* End those borrows and abstractions *)
           let end_borrows_abs blids aids ctx =
             let ctx =
-              InterpreterBorrows.end_borrows_no_synth meta config blids ctx
+              InterpreterBorrows.end_borrows_no_synth config meta blids ctx
             in
             let ctx =
-              InterpreterBorrows.end_abstractions_no_synth meta config aids ctx
+              InterpreterBorrows.end_abstractions_no_synth config meta aids ctx
             in
             ctx
           in
@@ -544,7 +544,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
 
     (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
-      loop_join_origin_with_continue_ctxs meta config loop_id fixed_ids ctx1 !ctxs
+      loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1 !ctxs
     in
     ctxs := [];
     ctx2
@@ -699,7 +699,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                   abs.kind = SynthInput rg_id) meta "TODO :  error message ";
                 (* End this abstraction *)
                 let ctx =
-                  InterpreterBorrows.end_abstraction_no_synth meta config abs_id ctx
+                  InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx
                 in
                 (* Explore the context, and check which abstractions are not there anymore *)
                 let ids, _ = compute_ctx_ids ctx in
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index d727e9bd..4568bf79 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -77,8 +77,8 @@ val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
     the values which are read or modified (some symbolic values may be ignored).
  *)
 val compute_loop_entry_fixed_point :
-  Meta.meta -> 
-  config ->
+  config -> 
+  Meta.meta ->
   loop_id ->
   Cps.st_cm_fun ->
   eval_ctx ->
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index b8d5094b..c4709b7e 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -636,7 +636,7 @@ let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   in
   { ctx with env }
 
-let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
+let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (fixed_ids : ids_sets) (old_ctx : eval_ctx) (ctxl : eval_ctx list) :
     (eval_ctx * eval_ctx list) * eval_ctx =
   (* # Join with the new contexts, one by one
@@ -657,9 +657,9 @@ let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (lo
         let ctx =
           match err with
           | LoanInRight bid ->
-              InterpreterBorrows.end_borrow_no_synth meta config bid ctx
+              InterpreterBorrows.end_borrow_no_synth config meta bid ctx
           | LoansInRight bids ->
-              InterpreterBorrows.end_borrows_no_synth meta config bids ctx
+              InterpreterBorrows.end_borrows_no_synth config meta bids ctx
           | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
               craise meta "Unexpected"
         in
diff --git a/compiler/InterpreterLoopsJoinCtxs.mli b/compiler/InterpreterLoopsJoinCtxs.mli
index e79e6a25..d92b3750 100644
--- a/compiler/InterpreterLoopsJoinCtxs.mli
+++ b/compiler/InterpreterLoopsJoinCtxs.mli
@@ -104,8 +104,8 @@ val join_ctxs : Meta.meta -> loop_id -> ids_sets -> eval_ctx -> eval_ctx -> ctx_
     - [ctxl]
  *)
 val loop_join_origin_with_continue_ctxs :
-  Meta.meta ->
   config ->
+  Meta.meta ->
   loop_id ->
   ids_sets ->
   eval_ctx ->
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 033e51c1..2e700c50 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1400,7 +1400,7 @@ let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_c
     (match_ctxs meta check_equivalent fixed_ids lookup_shared_value
        lookup_shared_value ctx0 ctx1)
 
-let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
+let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun =
  fun cf tgt_ctx ->
   (* Debug *)
@@ -1528,8 +1528,8 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id
       (* Exception: end the corresponding borrows, and continue *)
       let cc =
         match e with
-        | LoanInRight bid -> InterpreterBorrows.end_borrow meta config bid
-        | LoansInRight bids -> InterpreterBorrows.end_borrows meta config bids
+        | LoanInRight bid -> InterpreterBorrows.end_borrow config meta bid
+        | LoansInRight bids -> InterpreterBorrows.end_borrows config meta bids
         | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
             craise meta "Unexpected"
       in
@@ -1837,7 +1837,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
       BorrowId.Set.of_list
         (List.map snd (BorrowId.Map.bindings !src_fresh_borrows_map))
     in
-    let cc = InterpreterBorrows.end_borrows meta config new_borrows in
+    let cc = InterpreterBorrows.end_borrows config meta new_borrows in
 
     (* Compute the loop input values *)
     let input_values =
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 0db1ff1d..4a6d24a9 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -300,8 +300,8 @@ val prepare_match_ctx_with_target :
    - [src_ctx]
  *)
 val match_ctx_with_target :
-  Meta.meta ->
   config ->
+  Meta.meta ->
   loop_id ->
   bool ->
   borrow_loan_corresp ->
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index c7141064..6ec12d6f 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -445,7 +445,7 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
   | Ok ctx -> ctx
   | Error _ -> craise meta "Unreachable"
 
-let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access : access_kind)
+let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
@@ -454,9 +454,9 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
   | Error err ->
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows meta config bids
-        | FailMutLoan bid -> end_borrow meta config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
+        | FailSharedLoan bids -> end_borrows config meta bids
+        | FailMutLoan bid -> end_borrow config meta bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
         | FailSymbolic (i, sp) ->
             (* Expand the symbolic value *)
             let proj, _ =
@@ -464,16 +464,16 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
                 (List.length p.projection - i)
             in
             let prefix = { p with projection = proj } in
-            expand_symbolic_value_no_branching meta config sp
+            expand_symbolic_value_no_branching config meta sp
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
             craise meta "Found [Bottom] while reading a place"
         | FailBorrow _ -> craise meta "Could not read a borrow"
       in
-      comp cc (update_ctx_along_read_place meta config access p) cf ctx
+      comp cc (update_ctx_along_read_place config meta access p) cf ctx
 
-let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (access : access_kind)
+let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
@@ -484,12 +484,12 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
       (* Update the context *)
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows meta config bids
-        | FailMutLoan bid -> end_borrow meta config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
+        | FailSharedLoan bids -> end_borrows config meta bids
+        | FailMutLoan bid -> end_borrow config meta bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching meta config sp
+            expand_symbolic_value_no_branching config meta sp
               (Some (Synth.mk_mplace meta p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the {!Bottom} value *)
@@ -502,12 +502,12 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
         | FailBorrow _ -> craise meta "Could not write to a borrow"
       in
       (* Retry *)
-      comp cc (update_ctx_along_write_place meta config access p) cf ctx
+      comp cc (update_ctx_along_write_place config meta access p) cf ctx
 
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access_kind) (p : place)
+let rec end_loans_at_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place)
     : cm_fun =
  fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
@@ -525,7 +525,7 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             (* Nothing special to do *) super#visit_borrow_content env bc
         | VReservedMutBorrow bid ->
             (* We need to activate reserved borrows *)
-            let cc = promote_reserved_mut_borrow meta config bid in
+            let cc = promote_reserved_mut_borrow config meta bid in
             raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
@@ -536,11 +536,11 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             match access with
             | Read -> super#visit_VSharedLoan env bids v
             | Write | Move ->
-                let cc = end_borrows meta config bids in
+                let cc = end_borrows config meta bids in
                 raise (UpdateCtx cc))
         | VMutLoan bid ->
             (* We always need to end mutable borrows *)
-            let cc = end_borrow meta config bid in
+            let cc = end_borrow config meta bid in
             raise (UpdateCtx cc)
     end
   in
@@ -560,9 +560,9 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
   with UpdateCtx cc ->
     (* We need to update the context: compose the caugth continuation with
      * a recursive call to reinspect the value *)
-    comp cc (end_loans_at_place meta config access p) cf ctx
+    comp cc (end_loans_at_place config meta access p) cf ctx
 
-let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place) : cm_fun =
+let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
@@ -586,8 +586,8 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
         (* There are: end them then retry *)
         let cc =
           match c with
-          | LoanContent (VSharedLoan (bids, _)) -> end_borrows meta config bids
-          | LoanContent (VMutLoan bid) -> end_borrow meta config bid
+          | LoanContent (VSharedLoan (bids, _)) -> end_borrows config meta bids
+          | LoanContent (VMutLoan bid) -> end_borrow config meta bid
           | BorrowContent _ -> craise meta "Unreachable"
         in
         (* Retry *)
@@ -610,7 +610,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   (* Continue *)
   cc cf ctx
 
-let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_value -> m_fun) :
+let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   log#ldebug
@@ -619,9 +619,9 @@ let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_
      ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx));
   (* Access the place *)
   let access = Write in
-  let cc = update_ctx_along_write_place meta config access p in
+  let cc = update_ctx_along_write_place config meta access p in
   (* End the borrows and loans, starting with the borrows *)
-  let cc = comp cc (drop_outer_loans_at_lplace meta config p) in
+  let cc = comp cc (drop_outer_loans_at_lplace config meta p) in
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index faa68688..f1c481ca 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -13,13 +13,13 @@ type access_kind = Read | Write | Move
     updates the environment (by ending borrows, expanding symbolic values, etc.)
     until it manages to fully access the provided place.
  *)
-val update_ctx_along_read_place : Meta.meta -> config -> access_kind -> place -> cm_fun
+val update_ctx_along_read_place : config -> Meta.meta -> access_kind -> place -> cm_fun
 
 (** Update the environment to be able to write to a place.
 
     See {!update_ctx_along_read_place}.
 *)
-val update_ctx_along_write_place : Meta.meta -> config -> access_kind -> place -> cm_fun
+val update_ctx_along_write_place : config -> Meta.meta -> access_kind -> place -> cm_fun
 
 (** Read the value at a given place.
 
@@ -74,7 +74,7 @@ val compute_expanded_bottom_adt_value :
     that the place is *inside* a borrow, if we end the borrow, we won't be able
     to reinsert the value back).
  *)
-val drop_outer_loans_at_lplace : Meta.meta -> config -> place -> cm_fun
+val drop_outer_loans_at_lplace : config -> Meta.meta -> place -> cm_fun
 
 (** End the loans at a given place: read the value, if it contains a loan,
     end this loan, repeat.
@@ -85,7 +85,7 @@ val drop_outer_loans_at_lplace : Meta.meta -> config -> place -> cm_fun
     when moving values, we can't move a value which contains loans and thus need
     to end them, etc.
  *)
-val end_loans_at_place : Meta.meta -> config -> access_kind -> place -> cm_fun
+val end_loans_at_place : config -> Meta.meta -> access_kind -> place -> cm_fun
 
 (** Small utility.
 
@@ -96,4 +96,4 @@ val end_loans_at_place : Meta.meta -> config -> access_kind -> place -> cm_fun
     place. This value should not contain any outer loan (and we check it is the
     case). Note that this value is very likely to contain ⊥ subvalues.
   *)
-val prepare_lplace : Meta.meta -> config -> place -> (typed_value -> m_fun) -> m_fun
+val prepare_lplace : config -> Meta.meta -> place -> (typed_value -> m_fun) -> m_fun
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index fff23aec..7eaa7659 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -468,7 +468,7 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id)
   (* Return *)
   ctx
 
-let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bool) :
+let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bool) :
     (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) =
   let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -492,7 +492,7 @@ let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bo
   (fresh_reborrow, apply_registered_reborrows)
 
 (** [ty] shouldn't have erased regions *)
-let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx : eval_ctx)
+let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta) (ctx : eval_ctx)
     (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
   cassert (ty_is_rty ty) meta "TODO: error message";
@@ -500,7 +500,7 @@ let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx
   let allow_reborrows = true in
   (* Prepare the reborrows *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* Apply the projector *)
   let av =
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 7ffe4917..64ad1b29 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -43,7 +43,7 @@ val symbolic_expansion_non_shared_borrow_to_value :
     - [allow_reborrows]
  *)
 val prepare_reborrows :
-  Meta.meta -> config -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
+  config -> Meta.meta -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
 
 (** Apply (and reduce) a projector over borrows to an avalue.
     We use this for instance to spread the borrows present in the inputs
@@ -116,8 +116,8 @@ val apply_proj_borrows :
       erased regions)
  *)
 val apply_proj_borrows_on_input_value :
-  Meta.meta ->
   config ->
+  Meta.meta ->
   eval_ctx ->
   RegionId.Set.t ->
   RegionId.Set.t ->
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index b71daac5..253d90cc 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -19,7 +19,7 @@ module S = SynthesizeSymbolic
 let log = L.statements_log
 
 (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
-let drop_value (meta : Meta.meta) (config : config) (p : place) : cm_fun =
+let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -29,9 +29,9 @@ let drop_value (meta : Meta.meta) (config : config) (p : place) : cm_fun =
   let access = Write in
   (* First make sure we can access the place, by ending loans or expanding
    * symbolic values along the path, for instance *)
-  let cc = update_ctx_along_read_place meta config access p in
+  let cc = update_ctx_along_read_place config meta access p in
   (* Prepare the place (by ending the outer loans *at* the place). *)
-  let cc = comp cc (prepare_lplace meta config p) in
+  let cc = comp cc (prepare_lplace config meta p) in
   (* Replace the value with {!Bottom} *)
   let replace cf (v : typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
@@ -94,7 +94,7 @@ let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun =
     dummy variable and putting in its destination (after having checked that
     preparing the destination didn't introduce ⊥).
  *)
-let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p : place) : cm_fun =
+let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p : place) : cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -106,7 +106,7 @@ let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p :
   let rvalue_vid = fresh_dummy_var_id () in
   let cc = push_dummy_var rvalue_vid rv in
   (* Prepare the destination *)
-  let cc = comp cc (prepare_lplace meta config p) in
+  let cc = comp cc (prepare_lplace config meta p) in
   (* Retrieve the rvalue from the dummy variable *)
   let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in
   (* Update the destination *)
@@ -136,11 +136,11 @@ let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p :
   comp cc move_dest cf ctx
 
 (** Evaluate an assertion, when the scrutinee is not symbolic *)
-let eval_assertion_concrete (meta : Meta.meta) (config : config) (assertion : assertion) :
+let eval_assertion_concrete (config : config) (meta : Meta.meta) (assertion : assertion) :
     st_cm_fun =
  fun cf ctx ->
   (* There won't be any symbolic expansions: fully evaluate the operand *)
-  let eval_op = eval_operand meta config assertion.cond in
+  let eval_op = eval_operand config meta assertion.cond in
   let eval_assert cf (v : typed_value) : m_fun =
    fun ctx ->
     match v.value with
@@ -160,10 +160,10 @@ let eval_assertion_concrete (meta : Meta.meta) (config : config) (assertion : as
     a call to [assert ...] then continue in the success branch (and thus
     expand the boolean to [true]).
  *)
-let eval_assertion (meta : Meta.meta) (config : config) (assertion : assertion) : st_cm_fun =
+let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) : st_cm_fun =
  fun cf ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand meta config assertion.cond in
+  let eval_op = eval_operand config meta assertion.cond in
   (* Evaluate the assertion *)
   let eval_assert cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -176,7 +176,7 @@ let eval_assertion (meta : Meta.meta) (config : config) (assertion : assertion)
     match v.value with
     | VLiteral (VBool _) ->
         (* Delegate to the concrete evaluation function *)
-        eval_assertion_concrete meta config assertion cf ctx
+        eval_assertion_concrete config meta assertion cf ctx
     | VSymbolic sv ->
         cassert (config.mode = SymbolicMode) meta "TODO: Error message";
         cassert (sv.sv_ty = TLiteral TBool) meta "TODO: Error message";
@@ -185,7 +185,7 @@ let eval_assertion (meta : Meta.meta) (config : config) (assertion : assertion)
          * We will of course synthesize an assertion in the generated code
          * (see below). *)
         let ctx =
-          apply_symbolic_expansion_non_borrow meta config sv (SeLiteral (VBool true))
+          apply_symbolic_expansion_non_borrow config meta sv (SeLiteral (VBool true))
             ctx
         in
         (* Continue *)
@@ -210,7 +210,7 @@ let eval_assertion (meta : Meta.meta) (config : config) (assertion : assertion)
       a variant with all its fields set to {!Bottom}.
       For instance, something like: [Cons Bottom Bottom].
  *)
-let set_discriminant (meta : Meta.meta) (config : config) (p : place) (variant_id : VariantId.id) :
+let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_id : VariantId.id) :
     st_cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -221,8 +221,8 @@ let set_discriminant (meta : Meta.meta) (config : config) (p : place) (variant_i
       ^ "\n- initial context:\n" ^ eval_ctx_to_string meta ctx));
   (* Access the value *)
   let access = Write in
-  let cc = update_ctx_along_read_place meta config access p in
-  let cc = comp cc (prepare_lplace meta config p) in
+  let cc = update_ctx_along_read_place config meta access p in
+  let cc = comp cc (prepare_lplace config meta p) in
   (* Update the value *)
   let update_value cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -248,7 +248,7 @@ let set_discriminant (meta : Meta.meta) (config : config) (p : place) (variant_i
                       (Some variant_id) generics
                 | _ -> craise meta "Unreachable"
               in
-              assign_to_place meta config bottom_v p (cf Unit) ctx)
+              assign_to_place config meta bottom_v p (cf Unit) ctx)
     | TAdt ((TAdtId _ as type_id), generics), VBottom ->
         let bottom_v =
           match type_id with
@@ -257,7 +257,7 @@ let set_discriminant (meta : Meta.meta) (config : config) (p : place) (variant_i
                 generics
           | _ -> craise meta "Unreachable"
         in
-        assign_to_place meta config bottom_v p (cf Unit) ctx
+        assign_to_place config meta bottom_v p (cf Unit) ctx
     | _, VSymbolic _ ->
         cassert (config.mode = SymbolicMode) meta "The Config mode should be SymbolicMode";
         (* This is a bit annoying: in theory we should expand the symbolic value
@@ -316,11 +316,11 @@ let move_return_value (config : config) (meta : Meta.meta) (pop_return_value : b
  fun ctx ->
   if pop_return_value then
     let ret_vid = VarId.zero in
-    let cc = eval_operand meta config (Move (mk_place_from_var_id ret_vid)) in
+    let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in
     cc (fun v ctx -> cf (Some v) ctx) ctx
   else cf None ctx
 
-let pop_frame (meta : Meta.meta) (config : config) (pop_return_value : bool)
+let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
     (cf : typed_value option -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
@@ -364,7 +364,7 @@ let pop_frame (meta : Meta.meta) (config : config) (pop_return_value : bool)
     let cf_drop =
       List.fold_left
         (fun cf lid ->
-          drop_outer_loans_at_lplace meta config (mk_place_from_var_id lid) cf)
+          drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf)
         (cf ret_value) locals
     in
     (* Apply *)
@@ -402,15 +402,15 @@ let pop_frame (meta : Meta.meta) (config : config) (pop_return_value : bool)
   comp cc cf_pop cf ctx
 
 (** Pop the current frame and assign the returned value to its destination. *)
-let pop_frame_assign (meta : Meta.meta) (config : config) (dest : place) : cm_fun =
-  let cf_pop = pop_frame meta config true in
+let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) : cm_fun =
+  let cf_pop = pop_frame config meta true in
   let cf_assign cf ret_value : m_fun =
-    assign_to_place meta config (Option.get ret_value) dest cf
+    assign_to_place config meta (Option.get ret_value) dest cf
   in
   comp cf_pop cf_assign
 
 (** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_new_concrete (meta : Meta.meta) (config : config) (generics : generic_args) : cm_fun =
+let eval_box_new_concrete (config : config) (meta : Meta.meta) (generics : generic_args) : cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
   match
@@ -427,7 +427,7 @@ let eval_box_new_concrete (meta : Meta.meta) (config : config) (generics : gener
 
       (* Move the input value *)
       let cf_move =
-        eval_operand meta config (Move (mk_place_from_var_id input_var.index))
+        eval_operand config meta (Move (mk_place_from_var_id input_var.index))
       in
 
       (* Create the new box *)
@@ -442,7 +442,7 @@ let eval_box_new_concrete (meta : Meta.meta) (config : config) (generics : gener
 
         (* Move this value to the return variable *)
         let dest = mk_place_from_var_id VarId.zero in
-        let cf_assign = assign_to_place meta config box_v dest in
+        let cf_assign = assign_to_place config meta box_v dest in
 
         (* Continue *)
         cf_assign cf
@@ -471,7 +471,7 @@ let eval_box_new_concrete (meta : Meta.meta) (config : config) (generics : gener
     It thus updates the box value (by calling {!drop_value}) and updates
     the destination (by setting it to [()]).
 *)
-let eval_box_free (meta : Meta.meta) (config : config) (generics : generic_args)
+let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args)
     (args : operand list) (dest : place) : cm_fun =
  fun cf ctx ->
   match (generics.regions, generics.types, generics.const_generics, args) with
@@ -482,17 +482,17 @@ let eval_box_free (meta : Meta.meta) (config : config) (generics : generic_args)
        cassert (input_ty = boxed_ty)) meta "TODO: Error message";
 
       (* Drop the value *)
-      let cc = drop_value meta config input_box_place in
+      let cc = drop_value config meta input_box_place in
 
       (* Update the destination by setting it to [()] *)
-      let cc = comp cc (assign_to_place meta config mk_unit_value dest) in
+      let cc = comp cc (assign_to_place config meta mk_unit_value dest) in
 
       (* Continue *)
       cc cf ctx
   | _ -> craise meta "Inconsistent state"
 
 (** Evaluate a non-local function call in concrete mode *)
-let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fid : assumed_fun_id)
+let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) (fid : assumed_fun_id)
     (call : call) : cm_fun =
   let args = call.args in
   let dest = call.dest in
@@ -514,12 +514,12 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
       match fid with
       | BoxFree ->
           (* Degenerate case: box_free *)
-          eval_box_free meta config generics args dest
+          eval_box_free config meta generics args dest
       | _ ->
           (* "Normal" case: not box_free *)
           (* Evaluate the operands *)
           (*      let ctx, args_vl = eval_operands config ctx args in *)
-          let cf_eval_ops = eval_operands meta config args in
+          let cf_eval_ops = eval_operands config meta args in
 
           (* Evaluate the call
            *
@@ -553,7 +553,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
              * access to a body. *)
             let cf_eval_body : cm_fun =
               match fid with
-              | BoxNew -> eval_box_new_concrete meta config generics
+              | BoxNew -> eval_box_new_concrete config meta generics
               | BoxFree ->
                   (* Should have been treated above *)
                   craise meta "Unreachable"
@@ -566,7 +566,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
             let cc = comp cc cf_eval_body in
 
             (* Pop the frame *)
-            let cc = comp cc (pop_frame_assign meta config dest) in
+            let cc = comp cc (pop_frame_assign config meta dest) in
 
             (* Continue *)
             cc cf ctx
@@ -937,7 +937,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
   let cc = S.cf_save_snapshot in
   (* Expand the symbolic values if necessary - we need to do that before
    * checking the invariants *)
-  let cc = comp cc (greedy_expand_symbolic_values st.meta config) in
+  let cc = comp cc (greedy_expand_symbolic_values config st.meta) in
   (* Sanity check *)
   let cc = comp cc (Invariants.cf_check_invariants st.meta) in
 
@@ -958,7 +958,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
             eval_global config p gid generics cf ctx
         | _ ->
             (* Evaluate the rvalue *)
-            let cf_eval_rvalue = eval_rvalue_not_global st.meta config rvalue in
+            let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in
             (* Assign *)
             let cf_assign cf (res : (typed_value, eval_error) result) ctx =
               log#ldebug
@@ -968,7 +968,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
               match res with
               | Error EPanic -> cf Panic ctx
               | Ok rv -> (
-                  let expr = assign_to_place st.meta config rv p (cf Unit) ctx in
+                  let expr = assign_to_place config st.meta rv p (cf Unit) ctx in
                   (* Update the synthesized AST - here we store meta-information.
                    * We do it only in specific cases (it is not always useful, and
                    * also it can lead to issues - for instance, if we borrow a
@@ -990,12 +990,12 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
 
             (* Compose and apply *)
             comp cf_eval_rvalue cf_assign cf ctx)
-    | FakeRead p -> eval_fake_read st.meta config p (cf Unit) ctx
+    | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx
     | SetDiscriminant (p, variant_id) ->
-        set_discriminant st.meta config p variant_id cf ctx
-    | Drop p -> drop_value st.meta config p (cf Unit) ctx
-    | Assert assertion -> eval_assertion st.meta config assertion cf ctx
-    | Call call -> eval_function_call st.meta config call cf ctx
+        set_discriminant config st.meta p variant_id cf ctx
+    | Drop p -> drop_value config st.meta p (cf Unit) ctx
+    | Assert assertion -> eval_assertion config st.meta assertion cf ctx
+    | Call call -> eval_function_call config st.meta call cf ctx
     | Panic -> cf Panic ctx
     | Return -> cf Return ctx
     | Break i -> cf (Break i) ctx
@@ -1020,7 +1020,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
         InterpreterLoops.eval_loop config st.meta
           (eval_statement config loop_body)
           cf ctx
-    | Switch switch -> eval_switch st.meta config switch cf ctx
+    | Switch switch -> eval_switch config st.meta switch cf ctx
   in
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
@@ -1034,7 +1034,7 @@ 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 global.meta config global.body call) cf ctx
+      (eval_transparent_function_call_concrete config global.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}). *)
@@ -1052,13 +1052,13 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
       in
       let sval = mk_fresh_symbolic_value ty in
       let cc =
-        assign_to_place global.meta config (mk_typed_value_from_symbolic_value sval) dest
+        assign_to_place config global.meta (mk_typed_value_from_symbolic_value sval) dest
       in
       let e = cc (cf Unit) ctx in
       S.synthesize_global_eval gid generics sval e
 
 (** Evaluate a switch *)
-and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_fun =
+and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : st_cm_fun =
  fun cf ctx ->
   (* We evaluate the operand in two steps:
    * first we prepare it, then we check if its value is concrete or
@@ -1074,7 +1074,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
     match switch with
     | If (op, st1, st2) ->
         (* Evaluate the operand *)
-        let cf_eval_op = eval_operand meta config op in
+        let cf_eval_op = eval_operand config meta op in
         (* Switch on the value *)
         let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun =
          fun ctx ->
@@ -1093,7 +1093,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
                * the branches *)
               let cf_true : st_cm_fun = eval_statement config st1 in
               let cf_false : st_cm_fun = eval_statement config st2 in
-              expand_symbolic_bool meta config sv
+              expand_symbolic_bool config meta sv
                 (S.mk_opt_place_from_op meta op ctx)
                 cf_true cf_false cf ctx
           | _ -> craise meta "Inconsistent state"
@@ -1102,7 +1102,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
         comp cf_eval_op cf_if cf ctx
     | SwitchInt (op, int_ty, stgts, otherwise) ->
         (* Evaluate the operand *)
-        let cf_eval_op = eval_operand meta config op in
+        let cf_eval_op = eval_operand config meta op in
         (* Switch on the value *)
         let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun =
          fun ctx ->
@@ -1140,7 +1140,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
               (* Translate the otherwise branch *)
               let otherwise = eval_statement config otherwise in
               (* Expand and continue *)
-              expand_symbolic_int meta config sv
+              expand_symbolic_int config meta sv
                 (S.mk_opt_place_from_op meta op ctx)
                 int_ty stgts otherwise cf ctx
           | _ -> craise meta "Inconsistent state"
@@ -1152,7 +1152,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
         let access = Read in
         let expand_prim_copy = false in
         let cf_read_p cf : m_fun =
-          access_rplace_reorganize_and_read meta config expand_prim_copy access p cf
+          access_rplace_reorganize_and_read config meta expand_prim_copy access p cf
         in
         (* Match on the value *)
         let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun =
@@ -1175,11 +1175,11 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
           | VSymbolic sv ->
               (* Expand the symbolic value - may lead to branching *)
               let cf_expand =
-                expand_symbolic_adt meta config sv (Some (S.mk_mplace meta p ctx))
+                expand_symbolic_adt config meta sv (Some (S.mk_mplace meta p ctx))
               in
               (* Re-evaluate the switch - the value is not symbolic anymore,
                  which means we will go to the other branch *)
-              cf_expand (eval_switch meta config switch) cf ctx
+              cf_expand (eval_switch config meta switch) cf ctx
           | _ -> craise meta "Inconsistent state"
         in
         (* Compose *)
@@ -1189,44 +1189,44 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
   cf_match cf ctx
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
-and eval_function_call (meta : Meta.meta) (config : config) (call : call) : st_cm_fun =
+and eval_function_call (config : config) (meta : Meta.meta) (call : call) : st_cm_fun =
   (* There are several cases:
      - this is a local function, in which case we execute its body
      - this is an assumed function, in which case there is a special treatment
      - this is a trait method
   *)
   match config.mode with
-  | ConcreteMode -> eval_function_call_concrete meta config call
-  | SymbolicMode -> eval_function_call_symbolic meta config call
+  | ConcreteMode -> eval_function_call_concrete config meta call
+  | SymbolicMode -> eval_function_call_symbolic config meta call
 
-and eval_function_call_concrete (meta : Meta.meta) (config : config) (call : call) : st_cm_fun =
+and eval_function_call_concrete (config : config) (meta : Meta.meta) (call : call) : st_cm_fun =
  fun cf ctx ->
   match call.func with
   | FnOpMove _ -> craise meta "Closures are not supported yet"
   | FnOpRegular func -> (
       match func.func with
       | FunId (FRegular fid) ->
-          eval_transparent_function_call_concrete meta config fid call cf ctx
+          eval_transparent_function_call_concrete config meta fid call cf ctx
       | FunId (FAssumed fid) ->
           (* Continue - note that we do as if the function call has been successful,
            * by giving {!Unit} to the continuation, because we place us in the case
            * where we haven't panicked. Of course, the translation needs to take the
            * panic case into account... *)
-          eval_assumed_function_call_concrete meta config fid call (cf Unit) ctx
+          eval_assumed_function_call_concrete config meta fid call (cf Unit) ctx
       | TraitMethod _ -> craise meta "Unimplemented")
 
-and eval_function_call_symbolic (meta : Meta.meta) (config : config) (call : call) : st_cm_fun =
+and eval_function_call_symbolic (config : config) (meta : Meta.meta) (call : call) : st_cm_fun =
   match call.func with
   | FnOpMove _ -> craise meta "Closures are not supported yet"
   | FnOpRegular func -> (
       match func.func with
       | FunId (FRegular _) | TraitMethod _ ->
-          eval_transparent_function_call_symbolic meta config call
+          eval_transparent_function_call_symbolic config meta call
       | FunId (FAssumed fid) ->
-          eval_assumed_function_call_symbolic meta config fid call func)
+          eval_assumed_function_call_symbolic config meta fid call func)
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
+and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
     (fid : FunDeclId.id) (call : call) : st_cm_fun =
   let args = call.args in
   let dest = call.dest in
@@ -1261,7 +1261,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
 
         (* Evaluate the input operands *)
         cassert (List.length args = body.arg_count) body.meta "TODO: Error message";
-        let cc = eval_operands body.meta config args in
+        let cc = eval_operands config body.meta args in
 
         (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
          * of the operands evaluation from above to the functions afterwards, while
@@ -1296,7 +1296,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
         let cc = comp cc (push_uninitialized_vars meta locals) in
 
         (* Execute the function body *)
-        let cc = comp cc (eval_function_body meta config body_st) in
+        let cc = comp cc (eval_function_body config meta body_st) in
 
         (* Pop the stack frame and move the return value to its destination *)
         let cf_finish cf res =
@@ -1305,7 +1305,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
           | Return ->
               (* Pop the stack frame, retrieve the return value, move it to
                * its destination and continue *)
-              pop_frame_assign meta config dest (cf Unit)
+              pop_frame_assign config meta dest (cf Unit)
           | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
           | EndContinue _ ->
               craise meta "Unreachable"
@@ -1316,7 +1316,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
         cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_transparent_function_call_symbolic (meta : Meta.meta) (config : config) (call : call) :
+and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) (call : call) :
     st_cm_fun =
  fun cf ctx ->
   let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg =
@@ -1325,7 +1325,7 @@ and eval_transparent_function_call_symbolic (meta : Meta.meta) (config : config)
   (* Sanity check *)
   cassert (List.length call.args = List.length def.signature.inputs) def.meta "TODO: Error message";
   (* Evaluate the function call *)
-  eval_function_call_symbolic_from_inst_sig def.meta config func def.signature
+  eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
     regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
     cf ctx
 
@@ -1340,7 +1340,7 @@ and eval_transparent_function_call_symbolic (meta : Meta.meta) (config : config)
     overriding them. We treat them as regular method, which take an additional
     trait ref as input.
  *)
-and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : config)
+and eval_function_call_symbolic_from_inst_sig (config : config) (meta : Meta.meta)
     (fid : fun_id_or_trait_method_ref) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig)
     (generics : generic_args)
@@ -1370,7 +1370,7 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
   let dest_place = Some (S.mk_mplace meta dest ctx) in
 
   (* Evaluate the input operands *)
-  let cc = eval_operands meta config args in
+  let cc = eval_operands config meta args in
 
   (* Generate the abstractions and insert them in the context *)
   let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in
@@ -1404,7 +1404,7 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
       let ctx, args_projs =
         List.fold_left_map
           (fun ctx (arg, arg_rty) ->
-            apply_proj_borrows_on_input_value meta config ctx abs.regions
+            apply_proj_borrows_on_input_value config meta ctx abs.regions
               abs.ancestors_regions arg arg_rty)
           ctx args_with_rtypes
       in
@@ -1431,7 +1431,7 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
   let cc = comp cc cf_call in
 
   (* Move the return value to its destination *)
-  let cc = comp cc (assign_to_place meta config ret_value dest) in
+  let cc = comp cc (assign_to_place config meta ret_value dest) in
 
   (* End the abstractions which don't contain loans and don't have parent
    * abstractions.
@@ -1461,7 +1461,7 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
       abs_ids := with_loans_abs;
       (* End the abstractions which can be ended *)
       let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in
-      let cc = InterpreterBorrows.end_abstractions meta config no_loans_abs in
+      let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in
       (* Recursive call *)
       let cc = comp cc end_abs_with_no_loans in
       (* Continue *)
@@ -1487,7 +1487,7 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
   cc (cf Unit) ctx
 
 (** Evaluate a non-local function call in symbolic mode *)
-and eval_assumed_function_call_symbolic (meta : Meta.meta) (config : config) (fid : assumed_fun_id)
+and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (fid : assumed_fun_id)
     (call : call) (func : fn_ptr) : st_cm_fun =
  fun cf ctx ->
   let generics = func.generics in
@@ -1509,7 +1509,7 @@ and eval_assumed_function_call_symbolic (meta : Meta.meta) (config : config) (fi
   | BoxFree ->
       (* Degenerate case: box_free - note that this is not really a function
        * call: no need to call a "synthesize_..." function *)
-      eval_box_free meta config generics args dest (cf Unit) ctx
+      eval_box_free config meta generics args dest (cf Unit) ctx
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1535,11 +1535,11 @@ and eval_assumed_function_call_symbolic (meta : Meta.meta) (config : config) (fi
       in
 
       (* Evaluate the function call *)
-      eval_function_call_symbolic_from_inst_sig meta config (FunId (FAssumed fid)) sg
+      eval_function_call_symbolic_from_inst_sig config meta (FunId (FAssumed fid)) sg
         regions_hierarchy inst_sig generics None args dest cf ctx
 
 (** Evaluate a statement seen as a function body *)
-and eval_function_body (meta : Meta.meta) (config : config) (body : statement) : st_cm_fun =
+and eval_function_body (config : config) (meta : Meta.meta) (body : statement) : st_cm_fun =
  fun cf ctx ->
   log#ldebug (lazy "eval_function_body:");
   let cc = eval_statement config body in
@@ -1549,7 +1549,7 @@ and eval_function_body (meta : Meta.meta) (config : config) (body : statement) :
      * delegate the check to the caller. *)
     (* Expand the symbolic values if necessary - we need to do that before
      * checking the invariants *)
-    let cc = greedy_expand_symbolic_values body.meta config in
+    let cc = greedy_expand_symbolic_values config body.meta in
     (* Sanity check *)
     let cc = comp_check_ctx cc (Invariants.check_invariants meta) in (* Check if right meta *)
     (* Continue *)
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 3b1285a6..519d2c8e 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -16,7 +16,7 @@ open Cps
     If the boolean is false, we don't move the return value, and call the
     continuation with [None].
  *)
-val pop_frame : Meta.meta -> config -> bool -> (typed_value option -> m_fun) -> m_fun
+val pop_frame : config -> Meta.meta -> bool -> (typed_value option -> m_fun) -> m_fun
 
 (** Helper.
 
@@ -48,4 +48,4 @@ val create_push_abstractions_from_abs_region_groups :
 val eval_statement : config -> statement -> st_cm_fun
 
 (** Evaluate a statement seen as a function body *)
-val eval_function_body : Meta.meta -> config -> statement -> st_cm_fun
+val eval_function_body : config -> Meta.meta -> statement -> st_cm_fun
author	Escherichia	2024-03-25 12:06:05 +0100
committer	Escherichia	2024-03-28 15:27:35 +0100
commit	d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 (patch)
tree	14c7bca01e105ec6bf3db8ccedb21d64ae4ae756
parent	9b1a0d82c19375619904efe7e18e064701fb947b (diff)