Merge pull request #175 from AeneasVerif/afromher/meta

Rename meta into span

1 files changed, 117 insertions, 117 deletions

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index bae48f24..51be02c8 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -47,7 +47,7 @@ type borrow_kind = BMut | BShared | BReserved
     - loans and borrows are correctly related
     - a two-phase borrow can't point to a value inside an abstraction
  *)
-let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
+let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) :
     unit =
   (* Link all the borrow ids to a representant - necessary because of shared
    * borrows/loans *)
@@ -55,7 +55,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
   (* Link all the id representants to a borrow information *)
   let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in
   let context_to_string () : string =
-    eval_ctx_to_string ~meta:(Some meta) ctx
+    eval_ctx_to_string ~span:(Some span) ctx
     ^ "- representants:\n"
     ^ ids_reprs_to_string "  " !ids_reprs
     ^ "\n- info:\n"
@@ -78,12 +78,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
     let infos = !borrows_infos in
     (* Use the first borrow id as representant *)
     let repr_bid = BorrowId.Set.min_elt bids in
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem repr_bid infos)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem repr_bid infos)) span;
     (* Insert the mappings to the representant *)
     let reprs =
       BorrowId.Set.fold
         (fun bid reprs ->
-          sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta;
+          sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) span;
           BorrowId.Map.add bid repr_bid reprs)
         bids reprs
     in
@@ -106,8 +106,8 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
     let reprs = !ids_reprs in
     let infos = !borrows_infos in
     (* Sanity checks *)
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta;
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid infos)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) span;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid infos)) span;
     (* Add the mapping for the representant *)
     let reprs = BorrowId.Map.add bid bid reprs in
     (* Add the mapping for the loan info *)
@@ -155,10 +155,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid
           | AIgnoredMutLoan (None, _)
           | AIgnoredSharedLoan _
-          | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+          | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
           | AEndedSharedLoan (_, _)
           | AEndedIgnoredMutLoan
-              { given_back = _; child = _; given_back_meta = _ } ->
+              { given_back = _; child = _; given_back_span = _ } ->
               (* Do nothing *)
               ()
         in
@@ -184,7 +184,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           "find_info: could not find the representant of borrow "
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
-        craise __FILE__ __LINE__ meta err
+        craise __FILE__ __LINE__ span err
   in
 
   let update_info (bid : BorrowId.id) (info : borrow_info) : unit =
@@ -196,7 +196,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
         (fun x ->
           match x with
           | Some _ -> Some info
-          | None -> craise __FILE__ __LINE__ meta "Unreachable")
+          | None -> craise __FILE__ __LINE__ span "Unreachable")
         !borrows_infos
     in
     borrows_infos := infos
@@ -210,14 +210,14 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
     (* Check that the borrow kind is consistent *)
     (match (info.loan_kind, kind) with
     | RShared, (BShared | BReserved) | RMut, BMut -> ()
-    | _ -> craise __FILE__ __LINE__ meta "Invariant not satisfied");
+    | _ -> craise __FILE__ __LINE__ span "Invariant not satisfied");
     (* A reserved borrow can't point to a value inside an abstraction *)
     sanity_check __FILE__ __LINE__
       (kind <> BReserved || not info.loan_in_abs)
-      meta;
+      span;
     (* Insert the borrow id *)
     let borrow_ids = info.borrow_ids in
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) span;
     let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in
     (* Update the info in the map *)
     update_info bid info
@@ -272,7 +272,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
   List.iter
     (fun (rkind, bid) ->
       let info = find_info bid in
-      sanity_check __FILE__ __LINE__ (info.loan_kind = rkind) meta)
+      sanity_check __FILE__ __LINE__ (info.loan_kind = rkind) span)
     !ignored_loans;
 
   (* Then, check the borrow infos *)
@@ -283,12 +283,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
       sanity_check __FILE__ __LINE__
         (BorrowId.Set.elements info.loan_ids
         = BorrowId.Set.elements info.borrow_ids)
-        meta;
+        span;
       match info.loan_kind with
       | RMut ->
           sanity_check __FILE__ __LINE__
             (BorrowId.Set.cardinal info.loan_ids = 1)
-            meta
+            span
       | RShared -> ())
     !borrows_infos
 
@@ -296,7 +296,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
     - borrows/loans can't contain ⊥ or reserved mut borrows
     - shared loans can't contain mutable loans
  *)
-let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
+let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
   let visitor =
     object
       inherit [_] iter_eval_ctx as super
@@ -305,7 +305,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
         (* No ⊥ inside borrowed values *)
         sanity_check __FILE__ __LINE__
           (Config.allow_bottom_below_borrow || not info.outer_borrow)
-          meta
+          span
 
       method! visit_ABottom _info =
         (* ⊥ inside an abstraction is not the same as in a regular value *)
@@ -318,7 +318,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
           | VSharedLoan (_, _) -> set_outer_shared info
           | VMutLoan _ ->
               (* No mutable loan inside a shared loan *)
-              sanity_check __FILE__ __LINE__ (not info.outer_shared) meta;
+              sanity_check __FILE__ __LINE__ (not info.outer_shared) span;
               set_outer_mut info
         in
         (* Continue exploring *)
@@ -330,7 +330,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
           match bc with
           | VSharedBorrow _ -> set_outer_shared info
           | VReservedMutBorrow _ ->
-              sanity_check __FILE__ __LINE__ (not info.outer_borrow) meta;
+              sanity_check __FILE__ __LINE__ (not info.outer_borrow) span;
               set_outer_shared info
           | VMutBorrow (_, _) -> set_outer_mut info
         in
@@ -343,12 +343,12 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
           match lc with
           | AMutLoan (_, _) -> set_outer_mut info
           | ASharedLoan (_, _, _) -> set_outer_shared info
-          | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } ->
+          | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } ->
               set_outer_mut info
           | AEndedSharedLoan (_, _) -> set_outer_shared info
           | AIgnoredMutLoan (_, _) -> set_outer_mut info
           | AEndedIgnoredMutLoan
-              { given_back = _; child = _; given_back_meta = _ } ->
+              { given_back = _; child = _; given_back_span = _ } ->
               set_outer_mut info
           | AIgnoredSharedLoan _ -> set_outer_shared info
         in
@@ -375,15 +375,15 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
   let info = { outer_borrow = false; outer_shared = false } in
   visitor#visit_eval_ctx info ctx
 
-let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) :
+let check_literal_type (span : Meta.span) (cv : literal) (ty : literal_type) :
     unit =
   match (cv, ty) with
   | VScalar sv, TInteger int_ty ->
-      sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta
+      sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) span
   | VBool _, TBool | VChar _, TChar -> ()
-  | _ -> craise __FILE__ __LINE__ meta "Erroneous typing"
+  | _ -> craise __FILE__ __LINE__ span "Erroneous typing"
 
-let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
+let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
   (* TODO: the type of aloans doens't make sense: they have a type
    * of the shape [& (mut) T] where they should have type [T]...
    * This messes a bit the type invariant checks when checking the
@@ -403,20 +403,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
 
       method! visit_EBinding info binder v =
         (* We also check that the regions are erased *)
-        sanity_check __FILE__ __LINE__ (ty_is_ety v.ty) meta;
+        sanity_check __FILE__ __LINE__ (ty_is_ety v.ty) span;
         super#visit_EBinding info binder v
 
       method! visit_symbolic_value inside_abs v =
         (* Check that the types have regions *)
-        sanity_check __FILE__ __LINE__ (ty_is_rty v.sv_ty) meta;
+        sanity_check __FILE__ __LINE__ (ty_is_rty v.sv_ty) span;
         super#visit_symbolic_value inside_abs v
 
       method! visit_typed_value info tv =
         (* Check that the types have erased regions *)
-        sanity_check __FILE__ __LINE__ (ty_is_ety tv.ty) meta;
+        sanity_check __FILE__ __LINE__ (ty_is_ety tv.ty) span;
         (* Check the current pair (value, type) *)
         (match (tv.value, tv.ty) with
-        | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty
+        | VLiteral cv, TLiteral ty -> check_literal_type span cv ty
         (* ADT case *)
         | VAdt av, TAdt (TAdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
@@ -425,33 +425,33 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             (* Check the number of parameters *)
             sanity_check __FILE__ __LINE__
               (List.length generics.regions = List.length def.generics.regions)
-              meta;
+              span;
             sanity_check __FILE__ __LINE__
               (List.length generics.types = List.length def.generics.types)
-              meta;
+              span;
             (* Check that the variant id is consistent *)
             (match (av.variant_id, def.kind) with
             | Some variant_id, Enum variants ->
                 sanity_check __FILE__ __LINE__
                   (VariantId.to_int variant_id < List.length variants)
-                  meta
+                  span
             | None, Struct _ -> ()
-            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
+            | _ -> craise __FILE__ __LINE__ span "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def
+              AssociatedTypes.type_decl_get_inst_norm_field_etypes span ctx def
                 av.variant_id generics
             in
             let fields_with_types = List.combine av.field_values field_types in
             List.iter
               (fun ((v, ty) : typed_value * ty) ->
-                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
+                sanity_check __FILE__ __LINE__ (v.ty = ty) span)
               fields_with_types
         (* Tuple case *)
         | VAdt av, TAdt (TTuple, generics) ->
-            sanity_check __FILE__ __LINE__ (generics.regions = []) meta;
-            sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
-            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
+            sanity_check __FILE__ __LINE__ (generics.regions = []) span;
+            sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) span;
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
@@ -459,11 +459,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             in
             List.iter
               (fun ((v, ty) : typed_value * ty) ->
-                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
+                sanity_check __FILE__ __LINE__ (v.ty = ty) span)
               fields_with_types
         (* Assumed type case *)
         | VAdt av, TAdt (TAssumed aty_id, generics) -> (
-            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) span;
             match
               ( aty_id,
                 av.field_values,
@@ -473,14 +473,14 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             with
             (* Box *)
             | TBox, [ inner_value ], [], [ inner_ty ], [] ->
-                sanity_check __FILE__ __LINE__ (inner_value.ty = inner_ty) meta
+                sanity_check __FILE__ __LINE__ (inner_value.ty = inner_ty) span
             | TArray, inner_values, _, [ inner_ty ], [ cg ] ->
                 (* *)
                 sanity_check __FILE__ __LINE__
                   (List.for_all
                      (fun (v : typed_value) -> v.ty = inner_ty)
                      inner_values)
-                  meta;
+                  span;
                 (* The length is necessarily concrete *)
                 let len =
                   (ValuesUtils.literal_as_scalar
@@ -489,46 +489,46 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
                 in
                 sanity_check __FILE__ __LINE__
                   (Z.of_int (List.length inner_values) = len)
-                  meta
+                  span
             | (TSlice | TStr), _, _, _, _ ->
-                craise __FILE__ __LINE__ meta "Unexpected"
-            | _ -> craise __FILE__ __LINE__ meta "Erroneous type")
+                craise __FILE__ __LINE__ span "Unexpected"
+            | _ -> craise __FILE__ __LINE__ span "Erroneous type")
         | VBottom, _ -> (* Nothing to check *) ()
         | VBorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let _, glc = lookup_loan meta ek_all bid ctx in
+                let _, glc = lookup_loan span ek_all bid ctx in
                 match glc with
                 | Concrete (VSharedLoan (_, sv))
                 | Abstract (ASharedLoan (_, sv, _)) ->
-                    sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) meta
-                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
+                    sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span
+                | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
             | VMutBorrow (_, bv), RMut ->
                 sanity_check __FILE__ __LINE__
                   ((* Check that the borrowed value has the proper type *)
                    bv.ty = ref_ty)
-                  meta
-            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing")
+                  span
+            | _ -> craise __FILE__ __LINE__ span "Erroneous typing")
         | VLoan lc, ty -> (
             match lc with
             | VSharedLoan (_, sv) ->
-                sanity_check __FILE__ __LINE__ (sv.ty = ty) meta
+                sanity_check __FILE__ __LINE__ (sv.ty = ty) span
             | VMutLoan bid -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let glc = lookup_borrow meta ek_all bid ctx in
+                let glc = lookup_borrow span ek_all bid ctx in
                 match glc with
                 | Concrete (VMutBorrow (_, bv)) ->
-                    sanity_check __FILE__ __LINE__ (bv.ty = ty) meta
+                    sanity_check __FILE__ __LINE__ (bv.ty = ty) span
                 | Abstract (AMutBorrow (_, sv)) ->
                     sanity_check __FILE__ __LINE__
                       (Substitute.erase_regions sv.ty = ty)
-                      meta
-                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context"))
+                      span
+                | _ -> craise __FILE__ __LINE__ span "Inconsistent context"))
         | VSymbolic sv, ty ->
             let ty' = Substitute.erase_regions sv.sv_ty in
-            sanity_check __FILE__ __LINE__ (ty' = ty) meta
-        | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
+            sanity_check __FILE__ __LINE__ (ty' = ty) span
+        | _ -> craise __FILE__ __LINE__ span "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_value info tv
 
@@ -542,7 +542,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
        * *)
       method! visit_typed_avalue info atv =
         (* Check that the types have regions *)
-        sanity_check __FILE__ __LINE__ (ty_is_rty atv.ty) meta;
+        sanity_check __FILE__ __LINE__ (ty_is_rty atv.ty) span;
         (* Check the current pair (value, type) *)
         (match (atv.value, atv.ty) with
         (* ADT case *)
@@ -553,37 +553,37 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             (* Check the number of parameters *)
             sanity_check __FILE__ __LINE__
               (List.length generics.regions = List.length def.generics.regions)
-              meta;
+              span;
             sanity_check __FILE__ __LINE__
               (List.length generics.types = List.length def.generics.types)
-              meta;
+              span;
             sanity_check __FILE__ __LINE__
               (List.length generics.const_generics
               = List.length def.generics.const_generics)
-              meta;
+              span;
             (* Check that the variant id is consistent *)
             (match (av.variant_id, def.kind) with
             | Some variant_id, Enum variants ->
                 sanity_check __FILE__ __LINE__
                   (VariantId.to_int variant_id < List.length variants)
-                  meta
+                  span
             | None, Struct _ -> ()
-            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
+            | _ -> craise __FILE__ __LINE__ span "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def
+              AssociatedTypes.type_decl_get_inst_norm_field_rtypes span ctx def
                 av.variant_id generics
             in
             let fields_with_types = List.combine av.field_values field_types in
             List.iter
               (fun ((v, ty) : typed_avalue * ty) ->
-                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
+                sanity_check __FILE__ __LINE__ (v.ty = ty) span)
               fields_with_types
         (* Tuple case *)
         | AAdt av, TAdt (TTuple, generics) ->
-            sanity_check __FILE__ __LINE__ (generics.regions = []) meta;
-            sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
-            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
+            sanity_check __FILE__ __LINE__ (generics.regions = []) span;
+            sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) span;
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
@@ -591,11 +591,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             in
             List.iter
               (fun ((v, ty) : typed_avalue * ty) ->
-                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
+                sanity_check __FILE__ __LINE__ (v.ty = ty) span)
               fields_with_types
         (* Assumed type case *)
         | AAdt av, TAdt (TAssumed aty_id, generics) -> (
-            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) span;
             match
               ( aty_id,
                 av.field_values,
@@ -605,101 +605,101 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             with
             (* Box *)
             | TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
-                sanity_check __FILE__ __LINE__ (boxed_value.ty = boxed_ty) meta
-            | _ -> craise __FILE__ __LINE__ meta "Erroneous type")
+                sanity_check __FILE__ __LINE__ (boxed_value.ty = boxed_ty) span
+            | _ -> craise __FILE__ __LINE__ span "Erroneous type")
         | ABottom, _ -> (* Nothing to check *) ()
         | ABorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | AMutBorrow (_, av), RMut ->
                 (* Check that the child value has the proper type *)
-                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta
+                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span
             | ASharedBorrow bid, RShared -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let _, glc = lookup_loan meta ek_all bid ctx in
+                let _, glc = lookup_loan span ek_all bid ctx in
                 match glc with
                 | Concrete (VSharedLoan (_, sv))
                 | Abstract (ASharedLoan (_, sv, _)) ->
                     sanity_check __FILE__ __LINE__
                       (sv.ty = Substitute.erase_regions ref_ty)
-                      meta
-                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
+                      span
+                | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
             | AIgnoredMutBorrow (_opt_bid, av), RMut ->
-                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta
-            | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ },
+                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span
+            | ( AEndedIgnoredMutBorrow { given_back; child; given_back_span = _ },
                 RMut ) ->
-                sanity_check __FILE__ __LINE__ (given_back.ty = ref_ty) meta;
-                sanity_check __FILE__ __LINE__ (child.ty = ref_ty) meta
+                sanity_check __FILE__ __LINE__ (given_back.ty = ref_ty) span;
+                sanity_check __FILE__ __LINE__ (child.ty = ref_ty) span
             | AProjSharedBorrow _, RShared -> ()
-            | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
+            | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
         | ALoan lc, aty -> (
             match lc with
             | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
               -> (
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta;
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span;
                 (* Lookup the borrowed value to check it has the proper type *)
-                let glc = lookup_borrow meta ek_all bid ctx in
+                let glc = lookup_borrow span ek_all bid ctx in
                 match glc with
                 | Concrete (VMutBorrow (_, bv)) ->
                     sanity_check __FILE__ __LINE__
                       (bv.ty = Substitute.erase_regions borrowed_aty)
-                      meta
+                      span
                 | Abstract (AMutBorrow (_, sv)) ->
                     sanity_check __FILE__ __LINE__
                       (Substitute.erase_regions sv.ty
                       = Substitute.erase_regions borrowed_aty)
-                      meta
-                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
+                      span
+                | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
             | AIgnoredMutLoan (None, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span
             | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 sanity_check __FILE__ __LINE__
                   (sv.ty = Substitute.erase_regions borrowed_aty)
-                  meta;
+                  span;
                 (* TODO: the type of aloans doesn't make sense, see above *)
-                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta
-            | AEndedMutLoan { given_back; child; given_back_meta = _ }
-            | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } ->
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span
+            | AEndedMutLoan { given_back; child; given_back_span = _ }
+            | AEndedIgnoredMutLoan { given_back; child; given_back_span = _ } ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 sanity_check __FILE__ __LINE__
                   (given_back.ty = borrowed_aty)
-                  meta;
-                sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) meta
+                  span;
+                sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) span
             | AIgnoredSharedLoan child_av ->
                 sanity_check __FILE__ __LINE__
                   (child_av.ty = aloan_get_expected_child_type aty)
-                  meta)
+                  span)
         | ASymbolic aproj, ty -> (
             let ty1 = Substitute.erase_regions ty in
             match aproj with
             | AProjLoans (sv, _) ->
                 let ty2 = Substitute.erase_regions sv.sv_ty in
-                sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
+                sanity_check __FILE__ __LINE__ (ty1 = ty2) span;
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
                 sanity_check __FILE__ __LINE__
                   (ty_has_regions_in_set abs.regions sv.sv_ty)
-                  meta
+                  span
             | AProjBorrows (sv, proj_ty) ->
                 let ty2 = Substitute.erase_regions sv.sv_ty in
-                sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
+                sanity_check __FILE__ __LINE__ (ty1 = ty2) span;
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
                 sanity_check __FILE__ __LINE__
                   (ty_has_regions_in_set abs.regions proj_ty)
-                  meta
+                  span
             | AEndedProjLoans (_msv, given_back_ls) ->
                 List.iter
                   (fun (_, proj) ->
                     match proj with
                     | AProjBorrows (_sv, ty') ->
-                        sanity_check __FILE__ __LINE__ (ty' = ty) meta
+                        sanity_check __FILE__ __LINE__ (ty' = ty) span
                     | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
-                    | _ -> craise __FILE__ __LINE__ meta "Unexpected")
+                    | _ -> craise __FILE__ __LINE__ span "Unexpected")
                   given_back_ls
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
@@ -708,9 +708,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
-                ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
+                ^ typed_avalue_to_string ~span:(Some span) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            internal_error __FILE__ __LINE__ meta);
+            internal_error __FILE__ __LINE__ span);
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
@@ -749,7 +749,7 @@ type sv_info = {
     - the union of the aproj_loans contains the aproj_borrows applied on the
       same symbolic values
  *)
-let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
+let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit =
   (* Small utility *)
   let module M = SymbolicValueId.Map in
   let infos : sv_info M.t ref = ref M.empty in
@@ -819,19 +819,19 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
      * projectors of borrows in abstractions *)
     sanity_check __FILE__ __LINE__
       (info.env_count = 0 || info.aproj_borrows = [])
-      meta;
+      span;
     (* A symbolic value containing borrows can't be duplicated (i.e., copied):
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
-      sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
+      sanity_check __FILE__ __LINE__ (info.env_count <= 1) span;
     (* A duplicated symbolic value is necessarily copyable *)
     sanity_check __FILE__ __LINE__
       (info.env_count <= 1 || ty_is_copyable info.ty)
-      meta;
+      span;
 
     sanity_check __FILE__ __LINE__
       (info.aproj_borrows = [] || info.aproj_loans <> [])
-      meta;
+      span;
     (* At the same time:
      * - check that the loans don't intersect
      * - compute the set of regions for which we project loans
@@ -845,7 +845,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
               (fun rid regions ->
                 sanity_check __FILE__ __LINE__
                   (not (RegionId.Set.mem rid regions))
-                  meta;
+                  span;
                 RegionId.Set.add rid regions)
               regions linfo.regions
           in
@@ -856,22 +856,22 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
     List.iter
       (fun binfo ->
         sanity_check __FILE__ __LINE__
-          (projection_contains meta info.ty loan_regions binfo.proj_ty
+          (projection_contains span info.ty loan_regions binfo.proj_ty
              binfo.regions)
-          meta)
+          span)
       info.aproj_borrows;
     ()
   in
 
   M.iter check_info !infos
 
-let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit =
+let check_invariants (span : Meta.span) (ctx : eval_ctx) : unit =
   if !Config.sanity_checks then (
     log#ldebug
       (lazy
-        ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-    check_loans_borrows_relation_invariant meta ctx;
-    check_borrowed_values_invariant meta ctx;
-    check_typing_invariant meta ctx;
-    check_symbolic_values meta ctx)
+        ("Checking invariants:\n" ^ eval_ctx_to_string ~span:(Some span) ctx));
+    check_loans_borrows_relation_invariant span ctx;
+    check_borrowed_values_invariant span ctx;
+    check_typing_invariant span ctx;
+    check_symbolic_values span ctx)
   else log#ldebug (lazy "Not checking invariants (check is not activated)")