Merge branch 'main' into afromher/recursive_projectors

1 files changed, 97 insertions, 97 deletions

diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index a01be046..2628b26a 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -72,10 +72,10 @@ let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string =
   String.concat " -> " ids
 
 (** Add a borrow or abs id to a chain of ids, while checking that we don't loop *)
-let add_borrow_or_abs_id_to_chain (meta : Meta.meta) (msg : string)
+let add_borrow_or_abs_id_to_chain (span : Meta.span) (msg : string)
     (id : borrow_or_abs_id) (ids : borrow_or_abs_ids) : borrow_or_abs_ids =
   if List.mem id ids then
-    craise __FILE__ __LINE__ meta
+    craise __FILE__ __LINE__ span
       (msg ^ "detected a loop in the chain of ids: "
       ^ borrow_or_abs_ids_chain_to_string (id :: ids))
   else id :: ids
@@ -94,25 +94,25 @@ let add_borrow_or_abs_id_to_chain (meta : Meta.meta) (msg : string)
     TODO: is there a way of deriving such a comparison?
     TODO: rename
  *)
-let rec compare_rtys (meta : Meta.meta) (default : bool)
+let rec compare_rtys (span : Meta.span) (default : bool)
     (combine : bool -> bool -> bool)
     (compare_regions : region -> region -> bool) (ty1 : rty) (ty2 : rty) : bool
     =
-  let compare = compare_rtys meta default combine compare_regions in
+  let compare = compare_rtys span default combine compare_regions in
   (* Sanity check - TODO: don't do this at every recursive call *)
-  sanity_check __FILE__ __LINE__ (ty_is_rty ty1 && ty_is_rty ty2) meta;
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty1 && ty_is_rty ty2) span;
   (* Normalize the associated types *)
   match (ty1, ty2) with
   | TLiteral lit1, TLiteral lit2 ->
-      sanity_check __FILE__ __LINE__ (lit1 = lit2) meta;
+      sanity_check __FILE__ __LINE__ (lit1 = lit2) span;
       default
   | TAdt (id1, generics1), TAdt (id2, generics2) ->
-      sanity_check __FILE__ __LINE__ (id1 = id2) meta;
+      sanity_check __FILE__ __LINE__ (id1 = id2) span;
       (* There are no regions in the const generics, so we ignore them,
          but we still check they are the same, for sanity *)
       sanity_check __FILE__ __LINE__
         (generics1.const_generics = generics2.const_generics)
-        meta;
+        span;
 
       (* We also ignore the trait refs *)
 
@@ -146,7 +146,7 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
       combine params_b tys_b
   | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) ->
       (* Sanity check *)
-      sanity_check __FILE__ __LINE__ (kind1 = kind2) meta;
+      sanity_check __FILE__ __LINE__ (kind1 = kind2) span;
       (* Explanation for the case where we check if projections intersect:
        * the projections intersect if the borrows intersect or their contents
        * intersect. *)
@@ -154,19 +154,19 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
       let tys_b = compare ty1 ty2 in
       combine regions_b tys_b
   | TVar id1, TVar id2 ->
-      sanity_check __FILE__ __LINE__ (id1 = id2) meta;
+      sanity_check __FILE__ __LINE__ (id1 = id2) span;
       default
   | TTraitType _, TTraitType _ ->
       (* The types should have been normalized. If after normalization we
          get trait types, we can consider them as variables *)
-      sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
+      sanity_check __FILE__ __LINE__ (ty1 = ty2) span;
       default
   | _ ->
       log#ltrace
         (lazy
           ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
          ^ "\n- ty2: " ^ show_ty ty2));
-      internal_error __FILE__ __LINE__ meta
+      internal_error __FILE__ __LINE__ span
 
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
@@ -175,14 +175,14 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
     Note that the two abstractions have different views (in terms of regions)
     of the symbolic value (hence the two region types).
 *)
-let projections_intersect (meta : Meta.meta) (ty1 : rty)
+let projections_intersect (span : Meta.span) (ty1 : rty)
     (rset1 : RegionId.Set.t) (ty2 : rty) (rset2 : RegionId.Set.t) : bool =
   let default = false in
   let combine b1 b2 = b1 || b2 in
   let compare_regions r1 r2 =
     region_in_set r1 rset1 && region_in_set r2 rset2
   in
-  compare_rtys meta default combine compare_regions ty1 ty2
+  compare_rtys span default combine compare_regions ty1 ty2
 
 (** Check if the first projection contains the second projection.
     We use this function when checking invariants.
@@ -190,14 +190,14 @@ let projections_intersect (meta : Meta.meta) (ty1 : rty)
     The regions in the types shouldn't be erased (this function will raise an exception
     otherwise).
 *)
-let projection_contains (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t)
+let projection_contains (span : Meta.span) (ty1 : rty) (rset1 : RegionId.Set.t)
     (ty2 : rty) (rset2 : RegionId.Set.t) : bool =
   let default = true in
   let combine b1 b2 = b1 && b2 in
   let compare_regions r1 r2 =
     region_in_set r1 rset1 || not (region_in_set r2 rset2)
   in
-  compare_rtys meta default combine compare_regions ty1 ty2
+  compare_rtys span default combine compare_regions ty1 ty2
 
 (** Lookup a loan content.
 
@@ -207,7 +207,7 @@ let projection_contains (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t)
     the {!InterpreterUtils.abs_or_var_id} is not necessarily {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.VarId} or
     {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.DummyVarId}: there can be concrete loans in abstractions (in the shared values).
  *)
-let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (ctx : eval_ctx) : (abs_or_var_id * g_loan_content) option =
   (* We store here whether we are inside an abstraction or a value - note that we
    * could also track that with the environment, it would probably be more idiomatic
@@ -262,16 +262,16 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
             if BorrowId.Set.mem l bids then
               raise (FoundGLoanContent (Abstract lc))
             else super#visit_ASharedLoan env bids v av
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AIgnoredSharedLoan _ ->
             super#visit_aloan_content env lc
 
       method! visit_EBinding env bv v =
-        sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) span;
         abs_or_var :=
           Some
             (match bv with
@@ -281,7 +281,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
         abs_or_var := None
 
       method! visit_EAbs env abs =
-        sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) span;
         if ek.enter_abs then (
           abs_or_var := Some (AbsId abs.abs_id);
           super#visit_EAbs env abs;
@@ -296,17 +296,17 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
   with FoundGLoanContent lc -> (
     match !abs_or_var with
     | Some abs_or_var -> Some (abs_or_var, lc)
-    | None -> craise __FILE__ __LINE__ meta "Inconsistent state")
+    | None -> craise __FILE__ __LINE__ span "Inconsistent state")
 
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
     Raises an exception if no loan was found.
  *)
-let lookup_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let lookup_loan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (ctx : eval_ctx) : abs_or_var_id * g_loan_content =
-  match lookup_loan_opt meta ek l ctx with
-  | None -> craise __FILE__ __LINE__ meta "Unreachable"
+  match lookup_loan_opt span ek l ctx with
+  | None -> craise __FILE__ __LINE__ span "Unreachable"
   | Some res -> res
 
 (** Update a loan content.
@@ -315,14 +315,14 @@ let lookup_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
     This is a helper function: it might break invariants.
  *)
-let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let update_loan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (nlc : loan_content) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we update exactly one loan: when updating
    * inside values, we check we don't update more than one loan. Then, upon
    * returning we check that we updated at least once. *)
   let r = ref false in
   let update () : loan_content =
-    sanity_check __FILE__ __LINE__ (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) span;
     r := true;
     nlc
   in
@@ -369,7 +369,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one loan *)
-  sanity_check __FILE__ __LINE__ !r meta;
+  sanity_check __FILE__ __LINE__ !r span;
   ctx
 
 (** Update a abstraction loan content.
@@ -378,14 +378,14 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
     This is a helper function: it might break invariants.
  *)
-let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (nlc : aloan_content) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we update exactly one loan: when updating
    * inside values, we check we don't update more than one loan. Then, upon
    * returning we check that we updated at least once. *)
   let r = ref false in
   let update () : aloan_content =
-    sanity_check __FILE__ __LINE__ (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) span;
     r := true;
     nlc
   in
@@ -401,11 +401,11 @@ let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
         | ASharedLoan (bids, v, av) ->
             if BorrowId.Set.mem l bids then update ()
             else super#visit_ASharedLoan env bids v av
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AIgnoredSharedLoan _ ->
             super#visit_aloan_content env lc
 
@@ -418,7 +418,7 @@ let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one loan *)
-  sanity_check __FILE__ __LINE__ !r meta;
+  sanity_check __FILE__ __LINE__ !r span;
   ctx
 
 (** Lookup a borrow content from a borrow id. *)
@@ -462,7 +462,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
         | AIgnoredMutBorrow (_, _)
         | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedBorrow ->
             super#visit_aborrow_content env bc
         | AProjSharedBorrow asb ->
@@ -484,10 +484,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
 
     Raise an exception if no loan was found
 *)
-let lookup_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let lookup_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (ctx : eval_ctx) : g_borrow_content =
   match lookup_borrow_opt ek l ctx with
-  | None -> craise __FILE__ __LINE__ meta "Unreachable"
+  | None -> craise __FILE__ __LINE__ span "Unreachable"
   | Some lc -> lc
 
 (** Update a borrow content.
@@ -496,14 +496,14 @@ let lookup_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
     This is a helper function: it might break invariants.   
  *)
-let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let update_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (nbc : borrow_content) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we update exactly one borrow: when updating
    * inside values, we check we don't update more than one borrow. Then, upon
    * returning we check that we updated at least once. *)
   let r = ref false in
   let update () : borrow_content =
-    sanity_check __FILE__ __LINE__ (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) span;
     r := true;
     nbc
   in
@@ -544,7 +544,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one borrow *)
-  sanity_check __FILE__ __LINE__ !r meta;
+  sanity_check __FILE__ __LINE__ !r span;
   ctx
 
 (** Update an abstraction borrow content.
@@ -553,14 +553,14 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
     This is a helper function: it might break invariants.     
  *)
-let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
+let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (nv : avalue) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we update exactly one borrow: when updating
    * inside values, we check we don't update more than one borrow. Then, upon
    * returning we check that we updated at least once. *)
   let r = ref false in
   let update () : avalue =
-    sanity_check __FILE__ __LINE__ (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) span;
     r := true;
     nv
   in
@@ -591,7 +591,7 @@ let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
 
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that we updated at least one borrow *)
-  cassert __FILE__ __LINE__ !r meta "No borrow was updated";
+  cassert __FILE__ __LINE__ !r span "No borrow was updated";
   ctx
 
 (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *)
@@ -669,13 +669,13 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
   | FoundLoanContent lc -> Some (LoanContent lc)
   | FoundBorrowContent bc -> Some (BorrowContent bc)
 
-let proj_borrows_intersects_proj_loans (meta : Meta.meta)
+let proj_borrows_intersects_proj_loans (span : Meta.span)
     (proj_borrows : RegionId.Set.t * symbolic_value * rty)
     (proj_loans : RegionId.Set.t * symbolic_value) : bool =
   let b_regions, b_sv, b_ty = proj_borrows in
   let l_regions, l_sv = proj_loans in
   if same_symbolic_id b_sv l_sv then
-    projections_intersect meta l_sv.sv_ty l_regions b_ty b_regions
+    projections_intersect span l_sv.sv_ty l_regions b_ty b_regions
   else false
 
 (** Result of looking up aproj_borrows which intersect a given aproj_loans in
@@ -703,24 +703,24 @@ type looked_up_aproj_borrows =
     
     This is a helper function.
 *)
-let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta)
+let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
     (lookup_shared : bool) (regions : RegionId.Set.t) (sv : symbolic_value)
     (ctx : eval_ctx) : looked_up_aproj_borrows option =
   let found : looked_up_aproj_borrows option ref = ref None in
   let set_non_shared ((id, ty) : AbstractionId.id * rty) : unit =
     match !found with
     | None -> found := Some (NonSharedProj (id, ty))
-    | Some _ -> craise __FILE__ __LINE__ meta "Unreachable"
+    | Some _ -> craise __FILE__ __LINE__ span "Unreachable"
   in
   let add_shared (x : AbstractionId.id * rty) : unit =
     match !found with
     | None -> found := Some (SharedProjs [ x ])
     | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl))
-    | Some (NonSharedProj _) -> craise __FILE__ __LINE__ meta "Unreachable"
+    | Some (NonSharedProj _) -> craise __FILE__ __LINE__ span "Unreachable"
   in
   let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty =
     if
-      proj_borrows_intersects_proj_loans meta
+      proj_borrows_intersects_proj_loans span
         (abs.regions, sv', proj_ty)
         (regions, sv)
     then
@@ -736,7 +736,7 @@ let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta)
       method! visit_abstract_shared_borrow abs asb =
         (* Sanity check *)
         (match !found with
-        | Some (NonSharedProj _) -> craise __FILE__ __LINE__ meta "Unreachable"
+        | Some (NonSharedProj _) -> craise __FILE__ __LINE__ span "Unreachable"
         | _ -> ());
         (* Explore *)
         if lookup_shared then
@@ -775,23 +775,23 @@ let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta)
     Returns the id of the owning abstraction, and the projection type used in
     this abstraction.
 *)
-let lookup_intersecting_aproj_borrows_not_shared_opt (meta : Meta.meta)
+let lookup_intersecting_aproj_borrows_not_shared_opt (span : Meta.span)
     (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) :
     (AbstractionId.id * rty) option =
   let lookup_shared = false in
   match
-    lookup_intersecting_aproj_borrows_opt meta lookup_shared regions sv ctx
+    lookup_intersecting_aproj_borrows_opt span lookup_shared regions sv ctx
   with
   | None -> None
   | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty)
-  | _ -> craise __FILE__ __LINE__ meta "Unexpected"
+  | _ -> craise __FILE__ __LINE__ span "Unexpected"
 
 (** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the
     values.
 
     This is a helper function: it might break invariants.
  *)
-let update_intersecting_aproj_borrows (meta : Meta.meta)
+let update_intersecting_aproj_borrows (span : Meta.span)
     (can_update_shared : bool)
     (update_shared : AbstractionId.id -> rty -> abstract_shared_borrows)
     (update_non_shared : AbstractionId.id -> rty -> aproj)
@@ -802,18 +802,18 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
   let add_shared () =
     match !shared with
     | None -> shared := Some true
-    | Some b -> sanity_check __FILE__ __LINE__ b meta
+    | Some b -> sanity_check __FILE__ __LINE__ b span
   in
   let set_non_shared () =
     match !shared with
     | None -> shared := Some false
     | Some _ ->
-        craise __FILE__ __LINE__ meta
+        craise __FILE__ __LINE__ span
           "Found unexpected intersecting proj_borrows"
   in
   let check_proj_borrows is_shared abs sv' proj_ty =
     if
-      proj_borrows_intersects_proj_loans meta
+      proj_borrows_intersects_proj_loans span
         (abs.regions, sv', proj_ty)
         (regions, sv)
     then (
@@ -830,7 +830,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
       method! visit_abstract_shared_borrows abs asb =
         (* Sanity check *)
         (match !shared with
-        | Some b -> sanity_check __FILE__ __LINE__ b meta
+        | Some b -> sanity_check __FILE__ __LINE__ b span
         | _ -> ());
         (* Explore *)
         if can_update_shared then
@@ -863,7 +863,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check that we updated the context at least once *)
-  cassert __FILE__ __LINE__ (Option.is_some !shared) meta
+  cassert __FILE__ __LINE__ (Option.is_some !shared) span
     "Context was not updated";
   (* Return *)
   ctx
@@ -875,12 +875,12 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
 
     This is a helper function: it might break invariants.
  *)
-let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta)
+let update_intersecting_aproj_borrows_non_shared (span : Meta.span)
     (regions : RegionId.Set.t) (sv : symbolic_value) (nv : aproj)
     (ctx : eval_ctx) : eval_ctx =
   (* Small helpers *)
   let can_update_shared = false in
-  let update_shared _ _ = craise __FILE__ __LINE__ meta "Unexpected" in
+  let update_shared _ _ = craise __FILE__ __LINE__ span "Unexpected" in
   let updated = ref false in
   let update_non_shared _ _ =
     (* We can update more than one borrow! *)
@@ -889,11 +889,11 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta)
   in
   (* Update *)
   let ctx =
-    update_intersecting_aproj_borrows meta can_update_shared update_shared
+    update_intersecting_aproj_borrows span can_update_shared update_shared
       update_non_shared regions sv ctx
   in
   (* Check that we updated at least once *)
-  sanity_check __FILE__ __LINE__ !updated meta;
+  sanity_check __FILE__ __LINE__ !updated span;
   (* Return *)
   ctx
 
@@ -902,15 +902,15 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta)
 
     This is a helper function: it might break invariants.
  *)
-let remove_intersecting_aproj_borrows_shared (meta : Meta.meta)
+let remove_intersecting_aproj_borrows_shared (span : Meta.span)
     (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx
     =
   (* Small helpers *)
   let can_update_shared = true in
   let update_shared _ _ = [] in
-  let update_non_shared _ _ = craise __FILE__ __LINE__ meta "Unexpected" in
+  let update_non_shared _ _ = craise __FILE__ __LINE__ span "Unexpected" in
   (* Update *)
-  update_intersecting_aproj_borrows meta can_update_shared update_shared
+  update_intersecting_aproj_borrows span can_update_shared update_shared
     update_non_shared regions sv ctx
 
 (** Updates the proj_loans intersecting some projection.
@@ -944,12 +944,12 @@ let remove_intersecting_aproj_borrows_shared (meta : Meta.meta)
     Note that the symbolic value at this place is necessarily equal to [sv],
     which is why we don't give it as parameters.
  *)
-let update_intersecting_aproj_loans (meta : Meta.meta)
+let update_intersecting_aproj_loans (span : Meta.span)
     (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value)
     (subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) :
     eval_ctx =
   (* *)
-  sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) meta;
+  sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) span;
   (* Small helpers for sanity checks *)
   let updated = ref false in
   let update abs local_given_back : aproj =
@@ -971,9 +971,9 @@ let update_intersecting_aproj_loans (meta : Meta.meta)
         | AProjLoans (sv', given_back) ->
             let abs = Option.get abs in
             if same_symbolic_id sv sv' then (
-              sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) meta;
+              sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) span;
               if
-                projections_intersect meta proj_ty proj_regions sv'.sv_ty
+                projections_intersect span proj_ty proj_regions sv'.sv_ty
                   abs.regions
               then update abs given_back
               else super#visit_aproj (Some abs) sproj)
@@ -983,7 +983,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta)
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check that we updated the context at least once *)
-  sanity_check __FILE__ __LINE__ !updated meta;
+  sanity_check __FILE__ __LINE__ !updated span;
   (* Return *)
   ctx
 
@@ -997,13 +997,13 @@ let update_intersecting_aproj_loans (meta : Meta.meta)
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
  *)
-let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
+let lookup_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id)
     (sv : symbolic_value) (ctx : eval_ctx) : (msymbolic_value * aproj) list =
   (* Small helpers for sanity checks *)
   let found = ref None in
   let set_found x =
     (* There is at most one projector which corresponds to the description *)
-    sanity_check __FILE__ __LINE__ (Option.is_none !found) meta;
+    sanity_check __FILE__ __LINE__ (Option.is_none !found) span;
     found := Some x
   in
   (* The visitor *)
@@ -1021,9 +1021,9 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
             super#visit_aproj abs sproj
         | AProjLoans (sv', given_back) ->
             let abs = Option.get abs in
-            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta;
+            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
             if sv'.sv_id = sv.sv_id then (
-              sanity_check __FILE__ __LINE__ (sv' = sv) meta;
+              sanity_check __FILE__ __LINE__ (sv' = sv) span;
               set_found given_back)
             else ());
         super#visit_aproj abs sproj
@@ -1042,13 +1042,13 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
  *)
-let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
+let update_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id)
     (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx =
   (* Small helpers for sanity checks *)
   let found = ref false in
   let update () =
     (* We update at most once *)
-    sanity_check __FILE__ __LINE__ (not !found) meta;
+    sanity_check __FILE__ __LINE__ (not !found) span;
     found := true;
     nproj
   in
@@ -1067,9 +1067,9 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
             super#visit_aproj abs sproj
         | AProjLoans (sv', _) ->
             let abs = Option.get abs in
-            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta;
+            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
             if sv'.sv_id = sv.sv_id then (
-              sanity_check __FILE__ __LINE__ (sv' = sv) meta;
+              sanity_check __FILE__ __LINE__ (sv' = sv) span;
               update ())
             else super#visit_aproj (Some abs) sproj
     end
@@ -1077,7 +1077,7 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Sanity check *)
-  sanity_check __FILE__ __LINE__ !found meta;
+  sanity_check __FILE__ __LINE__ !found span;
   (* Return *)
   ctx
 
@@ -1091,13 +1091,13 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id)
     
     TODO: factorize with {!update_aproj_loans}?
  *)
-let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id)
+let update_aproj_borrows (span : Meta.span) (abs_id : AbstractionId.id)
     (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx =
   (* Small helpers for sanity checks *)
   let found = ref false in
   let update () =
     (* We update at most once *)
-    sanity_check __FILE__ __LINE__ (not !found) meta;
+    sanity_check __FILE__ __LINE__ (not !found) span;
     found := true;
     nproj
   in
@@ -1116,9 +1116,9 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id)
             super#visit_aproj abs sproj
         | AProjBorrows (sv', _proj_ty) ->
             let abs = Option.get abs in
-            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta;
+            sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
             if sv'.sv_id = sv.sv_id then (
-              sanity_check __FILE__ __LINE__ (sv' = sv) meta;
+              sanity_check __FILE__ __LINE__ (sv' = sv) span;
               update ())
             else super#visit_aproj (Some abs) sproj
     end
@@ -1126,7 +1126,7 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id)
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Sanity check *)
-  sanity_check __FILE__ __LINE__ !found meta;
+  sanity_check __FILE__ __LINE__ !found span;
   (* Return *)
   ctx
 
@@ -1135,18 +1135,18 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id)
     Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified
     by a symbolic value and an abstraction id.
  *)
-let update_aproj_loans_to_ended (meta : Meta.meta) (abs_id : AbstractionId.id)
+let update_aproj_loans_to_ended (span : Meta.span) (abs_id : AbstractionId.id)
     (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Lookup the projector of loans *)
-  let given_back = lookup_aproj_loans meta abs_id sv ctx in
+  let given_back = lookup_aproj_loans span abs_id sv ctx in
   (* Create the new value for the projector *)
   let nproj = AEndedProjLoans (sv, given_back) in
   (* Insert it *)
-  let ctx = update_aproj_loans meta abs_id sv nproj ctx in
+  let ctx = update_aproj_loans span abs_id sv nproj ctx in
   (* Return *)
   ctx
 
-let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value)
+let no_aproj_over_symbolic_in_context (span : Meta.span) (sv : symbolic_value)
     (ctx : eval_ctx) : unit =
   (* The visitor *)
   let obj =
@@ -1164,7 +1164,7 @@ let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value)
   (* Apply *)
   try obj#visit_eval_ctx () ctx
   with Found ->
-    craise __FILE__ __LINE__ meta "update_aproj_loans_to_ended: failed"
+    craise __FILE__ __LINE__ span "update_aproj_loans_to_ended: failed"
 
 (** Helper function
 
@@ -1173,7 +1173,7 @@ let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value)
     
     **Remark:** we don't take the *ignored* mut/shared loans into account.
  *)
-let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) :
+let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
     borrow_ids_or_symbolic_value option =
   (* Explore to find a loan *)
   let obj =
@@ -1184,14 +1184,14 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) :
         match lc with
         | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
         | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
-        | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             super#visit_aloan_content env lc
         | AIgnoredMutLoan (_, _) ->
             (* Ignore *)
             super#visit_aloan_content env lc
         | AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
+            { given_back = _; child = _; given_back_span = _ }
         | AIgnoredSharedLoan _ ->
             (* Ignore *)
             super#visit_aloan_content env lc
@@ -1202,7 +1202,7 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) :
         | VMutLoan _ ->
             (* The mut loan linked to the mutable borrow present in a shared
              * value in an abstraction should be in an AProjBorrows *)
-            craise __FILE__ __LINE__ meta "Unreachable"
+            craise __FILE__ __LINE__ span "Unreachable"
         | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
 
       method! visit_aproj env sproj =
@@ -1226,9 +1226,9 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) :
       (* There are loan projections over symbolic values *)
       Some (SymbolicValue sv)
 
-let lookup_shared_value_opt (meta : Meta.meta) (ctx : eval_ctx)
+let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx)
     (bid : BorrowId.id) : typed_value option =
-  match lookup_loan_opt meta ek_all bid ctx with
+  match lookup_loan_opt span ek_all bid ctx with
   | None -> None
   | Some (_, lc) -> (
       match lc with
@@ -1236,6 +1236,6 @@ let lookup_shared_value_opt (meta : Meta.meta) (ctx : eval_ctx)
           Some sv
       | _ -> None)
 
-let lookup_shared_value (meta : Meta.meta) (ctx : eval_ctx) (bid : BorrowId.id)
+let lookup_shared_value (span : Meta.span) (ctx : eval_ctx) (bid : BorrowId.id)
     : typed_value =
-  Option.get (lookup_shared_value_opt meta ctx bid)
+  Option.get (lookup_shared_value_opt span ctx bid)