Rename meta into span

1 files changed, 165 insertions, 165 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index f2686cc6..ab7eb50c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
   *)
 type names_map = {
   id_to_name : string IdMap.t;
-  name_to_id : (id * Meta.meta option) StringMap.t;
+  name_to_id : (id * Meta.span option) StringMap.t;
       (** The name to id map is used to look for name clashes, and generate nice
           debugging messages: if there is a name clash, it is useful to know
           precisely which identifiers are mapped to the same name...
@@ -254,15 +254,15 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
+    ((id1, span1) : id * Meta.span option) (id2 : id) (span2 : Meta.span option)
     (name : string) : unit =
-  let meta_to_string (meta : Meta.meta option) =
-    match meta with
+  let span_to_string (span : Meta.span option) =
+    match span with
     | None -> ""
-    | Some meta -> "\n  " ^ Errors.meta_to_string meta
+    | Some span -> "\n  " ^ Errors.span_to_string span
   in
-  let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
-  let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
+  let id1 = "\n- " ^ id_to_string id1 ^ span_to_string span1 in
+  let id2 = "\n- " ^ id_to_string id2 ^ span_to_string span2 in
   let err =
     "Name clash detected: the following identifiers are bound to the same name \
      \"" ^ name ^ "\":" ^ id1 ^ id2
@@ -270,36 +270,36 @@ let report_name_collision (id_to_string : id -> string)
   in
   (* Register the error.
 
-     We don't link this error to any meta information because we already put
+     We don't link this error to any span information because we already put
      the span information about the two problematic definitions in the error
      message above. *)
   save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
-    (id * Meta.meta option) option =
+    (id * Meta.span option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
-    (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
+    (span : Meta.span option) (name : string) (nm : names_map) : unit =
   match names_map_get_id_from_name name nm with
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      report_name_collision id_to_string clash id meta name
+      report_name_collision id_to_string clash id span name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+let names_map_add_unchecked ((id, span) : id * Meta.span option) (name : string)
     (nm : names_map) : names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
+  let name_to_id = StringMap.add name (id, span) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+let names_map_add (id_to_string : id -> string) ((id, span) : id * span option)
     (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
-  names_map_check_collision id_to_string id meta name nm;
+  names_map_check_collision id_to_string id span name nm;
   (* Sanity check *)
   (if StringSet.mem name nm.names_set then
      let err =
@@ -307,9 +307,9 @@ let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
        ^ ":\nThe chosen name is already in the names set: " ^ name
      in
      (* If we fail hard on errors, raise an exception *)
-     save_error __FILE__ __LINE__ meta err);
+     save_error __FILE__ __LINE__ span err);
   (* Insert *)
-  names_map_add_unchecked (id, meta) name nm
+  names_map_add_unchecked (id, span) name nm
 
 (** The unsafe names map stores mappings from identifiers to names which might
     collide. For some backends and some names, it might be acceptable to have
@@ -396,7 +396,7 @@ let allow_collisions (id : id) : bool =
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
 let names_maps_add (id_to_string : id -> string) (id : id)
-    (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
+    (span : Meta.span option) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -411,7 +411,7 @@ let names_maps_add (id_to_string : id -> string) (id : id)
   *)
   if allow_collisions id then (
     (* Check with the ids which are considered to be strict on collisions *)
-    names_map_check_collision id_to_string id meta name nm.strict_names_map;
+    names_map_check_collision id_to_string id span name nm.strict_names_map;
     {
       nm with
       unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -426,15 +426,15 @@ let names_maps_add (id_to_string : id -> string) (id : id)
     *)
     let strict_names_map =
       if strict_collisions id then
-        names_map_add id_to_string (id, meta) name nm.strict_names_map
+        names_map_add id_to_string (id, span) name nm.strict_names_map
       else nm.strict_names_map
     in
-    let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
+    let names_map = names_map_add id_to_string (id, span) name nm.names_map in
     { nm with strict_names_map; names_map }
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_get (meta : Meta.meta option) (id_to_string : id -> string)
+let names_maps_get (span : Meta.span option) (id_to_string : id -> string)
     (id : id) (nm : names_maps) : string =
   (* We do not use the same name map if we allow/disallow collisions *)
   let map_to_string (m : string IdMap.t) : string =
@@ -454,7 +454,7 @@ let names_maps_get (meta : Meta.meta option) (id_to_string : id -> string)
           "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
           ^ map_to_string m
         in
-        save_error __FILE__ __LINE__ meta err;
+        save_error __FILE__ __LINE__ span err;
         "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
   else
     let m = nm.names_map.id_to_name in
@@ -465,7 +465,7 @@ let names_maps_get (meta : Meta.meta option) (id_to_string : id -> string)
           "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
           ^ map_to_string m
         in
-        save_error __FILE__ __LINE__ meta err;
+        save_error __FILE__ __LINE__ span err;
         "(ERROR: \"" ^ id_to_string id ^ "\")"
 
 type names_map_init = {
@@ -491,9 +491,9 @@ let names_maps_add_assumed_variant (id_to_string : id -> string)
   names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
 
 let names_maps_add_function (id_to_string : id -> string)
-    ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+    ((fid, span) : fun_id * span option) (name : string) (nm : names_maps) :
     names_maps =
-  names_maps_add id_to_string (FunId fid) meta name nm
+  names_maps_add id_to_string (FunId fid) span name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -537,7 +537,7 @@ let scalar_name (ty : literal_type) : string =
     functions, etc.
  *)
 type extraction_ctx = {
-  (* mutable _meta : Meta.meta; *)
+  (* mutable _span : Meta.span; *)
   crate : A.crate;
   trans_ctx : trans_ctx;
   names_maps : names_maps;
@@ -599,17 +599,17 @@ let llbc_fun_id_to_string (ctx : extraction_ctx) =
 let fun_id_to_string (ctx : extraction_ctx) =
   PrintPure.regular_fun_id_to_string (extraction_ctx_to_fmt_env ctx)
 
-let adt_variant_to_string (meta : Meta.meta option) (ctx : extraction_ctx) =
-  PrintPure.adt_variant_to_string ~meta (extraction_ctx_to_fmt_env ctx)
+let adt_variant_to_string (span : Meta.span option) (ctx : extraction_ctx) =
+  PrintPure.adt_variant_to_string ~span (extraction_ctx_to_fmt_env ctx)
 
-let adt_field_to_string (meta : Meta.meta option) (ctx : extraction_ctx) =
-  PrintPure.adt_field_to_string ~meta (extraction_ctx_to_fmt_env ctx)
+let adt_field_to_string (span : Meta.span option) (ctx : extraction_ctx) =
+  PrintPure.adt_field_to_string ~span (extraction_ctx_to_fmt_env ctx)
 
 (** Debugging function, used when communicating name collisions to the user,
     and also to print ids for internal debugging (in case of lookup miss for
     instance).
  *)
-let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
+let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
     string =
   let trait_decl_id_to_string (id : A.TraitDeclId.id) : string =
     let trait_name = trait_decl_id_to_string ctx id in
@@ -638,11 +638,11 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
   | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id
   | VariantId (id, variant_id) ->
       let type_name = type_id_to_string ctx id in
-      let variant_name = adt_variant_to_string meta ctx id (Some variant_id) in
+      let variant_name = adt_variant_to_string span ctx id (Some variant_id) in
       "type name: " ^ type_name ^ ", variant name: " ^ variant_name
   | FieldId (id, field_id) ->
       let type_name = type_id_to_string ctx id in
-      let field_name = adt_field_to_string meta ctx id field_id in
+      let field_name = adt_field_to_string span ctx id field_id in
       "type name: " ^ type_name ^ ", field name: " ^ field_name
   | UnknownId -> "keyword"
   | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
@@ -668,119 +668,119 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
       trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name
   | TraitSelfClauseId -> "trait_self_clause"
 
-let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
+let ctx_add (span : Meta.span) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
-  let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
+  let id_to_string (id : id) : string = id_to_string (Some span) id ctx in
   let names_maps =
-    names_maps_add id_to_string id (Some meta) name ctx.names_maps
+    names_maps_add id_to_string id (Some span) name ctx.names_maps
   in
   { ctx with names_maps }
 
-let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
+let ctx_get (span : Meta.span option) (id : id) (ctx : extraction_ctx) : string
     =
-  let id_to_string (id : id) : string = id_to_string meta id ctx in
-  names_maps_get meta id_to_string id ctx.names_maps
+  let id_to_string (id : id) : string = id_to_string span id ctx in
+  names_maps_get span id_to_string id ctx.names_maps
 
-let ctx_get_global (meta : Meta.meta) (id : A.GlobalDeclId.id)
+let ctx_get_global (span : Meta.span) (id : A.GlobalDeclId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (GlobalId id) ctx
+  ctx_get (Some span) (GlobalId id) ctx
 
-let ctx_get_function (meta : Meta.meta) (id : fun_id) (ctx : extraction_ctx) :
+let ctx_get_function (span : Meta.span) (id : fun_id) (ctx : extraction_ctx) :
     string =
-  ctx_get (Some meta) (FunId id) ctx
+  ctx_get (Some span) (FunId id) ctx
 
-let ctx_get_local_function (meta : Meta.meta) (id : A.FunDeclId.id)
+let ctx_get_local_function (span : Meta.span) (id : A.FunDeclId.id)
     (lp : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get_function meta (FromLlbc (FunId (FRegular id), lp)) ctx
+  ctx_get_function span (FromLlbc (FunId (FRegular id), lp)) ctx
 
-let ctx_get_type (meta : Meta.meta option) (id : type_id) (ctx : extraction_ctx)
+let ctx_get_type (span : Meta.span option) (id : type_id) (ctx : extraction_ctx)
     : string =
-  sanity_check_opt_meta __FILE__ __LINE__ (id <> TTuple) meta;
-  ctx_get meta (TypeId id) ctx
+  sanity_check_opt_span __FILE__ __LINE__ (id <> TTuple) span;
+  ctx_get span (TypeId id) ctx
 
-let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id)
+let ctx_get_local_type (span : Meta.span) (id : TypeDeclId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get_type (Some meta) (TAdtId id) ctx
+  ctx_get_type (Some span) (TAdtId id) ctx
 
-let ctx_get_assumed_type (meta : Meta.meta option) (id : assumed_ty)
+let ctx_get_assumed_type (span : Meta.span option) (id : assumed_ty)
     (ctx : extraction_ctx) : string =
-  ctx_get_type meta (TAssumed id) ctx
+  ctx_get_type span (TAssumed id) ctx
 
-let ctx_get_trait_constructor (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_constructor (span : Meta.span) (id : trait_decl_id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitDeclConstructorId id) ctx
+  ctx_get (Some span) (TraitDeclConstructorId id) ctx
 
-let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string
+let ctx_get_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) : string
     =
-  ctx_get (Some meta) TraitSelfClauseId ctx
+  ctx_get (Some span) TraitSelfClauseId ctx
 
-let ctx_get_trait_decl (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_decl (span : Meta.span) (id : trait_decl_id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitDeclId id) ctx
+  ctx_get (Some span) (TraitDeclId id) ctx
 
-let ctx_get_trait_impl (meta : Meta.meta) (id : trait_impl_id)
+let ctx_get_trait_impl (span : Meta.span) (id : trait_impl_id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitImplId id) ctx
+  ctx_get (Some span) (TraitImplId id) ctx
 
-let ctx_get_trait_item (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_item (span : Meta.span) (id : trait_decl_id)
     (item_name : string) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitItemId (id, item_name)) ctx
+  ctx_get (Some span) (TraitItemId (id, item_name)) ctx
 
-let ctx_get_trait_const (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_const (span : Meta.span) (id : trait_decl_id)
     (item_name : string) (ctx : extraction_ctx) : string =
-  ctx_get_trait_item meta id item_name ctx
+  ctx_get_trait_item span id item_name ctx
 
-let ctx_get_trait_type (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_type (span : Meta.span) (id : trait_decl_id)
     (item_name : string) (ctx : extraction_ctx) : string =
-  ctx_get_trait_item meta id item_name ctx
+  ctx_get_trait_item span id item_name ctx
 
-let ctx_get_trait_method (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_method (span : Meta.span) (id : trait_decl_id)
     (item_name : string) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitMethodId (id, item_name)) ctx
+  ctx_get (Some span) (TraitMethodId (id, item_name)) ctx
 
-let ctx_get_trait_parent_clause (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_parent_clause (span : Meta.span) (id : trait_decl_id)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitParentClauseId (id, clause)) ctx
+  ctx_get (Some span) (TraitParentClauseId (id, clause)) ctx
 
-let ctx_get_trait_item_clause (meta : Meta.meta) (id : trait_decl_id)
+let ctx_get_trait_item_clause (span : Meta.span) (id : trait_decl_id)
     (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TraitItemClauseId (id, item, clause)) ctx
+  ctx_get (Some span) (TraitItemClauseId (id, item, clause)) ctx
 
-let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) :
+let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) :
     string =
-  ctx_get (Some meta) (VarId id) ctx
+  ctx_get (Some span) (VarId id) ctx
 
-let ctx_get_type_var (meta : Meta.meta) (id : TypeVarId.id)
+let ctx_get_type_var (span : Meta.span) (id : TypeVarId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TypeVarId id) ctx
+  ctx_get (Some span) (TypeVarId id) ctx
 
-let ctx_get_const_generic_var (meta : Meta.meta) (id : ConstGenericVarId.id)
+let ctx_get_const_generic_var (span : Meta.span) (id : ConstGenericVarId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (ConstGenericVarId id) ctx
+  ctx_get (Some span) (ConstGenericVarId id) ctx
 
-let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id)
+let ctx_get_local_trait_clause (span : Meta.span) (id : TraitClauseId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (LocalTraitClauseId id) ctx
+  ctx_get (Some span) (LocalTraitClauseId id) ctx
 
-let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id)
+let ctx_get_field (span : Meta.span) (type_id : type_id) (field_id : FieldId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (FieldId (type_id, field_id)) ctx
+  ctx_get (Some span) (FieldId (type_id, field_id)) ctx
 
-let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx)
+let ctx_get_struct (span : Meta.span) (def_id : type_id) (ctx : extraction_ctx)
     : string =
-  ctx_get (Some meta) (StructId def_id) ctx
+  ctx_get (Some span) (StructId def_id) ctx
 
-let ctx_get_variant (meta : Meta.meta) (def_id : type_id)
+let ctx_get_variant (span : Meta.span) (def_id : type_id)
     (variant_id : VariantId.id) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (VariantId (def_id, variant_id)) ctx
+  ctx_get (Some span) (VariantId (def_id, variant_id)) ctx
 
-let ctx_get_decreases_proof (meta : Meta.meta) (def_id : A.FunDeclId.id)
+let ctx_get_decreases_proof (span : Meta.span) (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx
+  ctx_get (Some span) (DecreasesProofId (FRegular def_id, loop_id)) ctx
 
-let ctx_get_termination_measure (meta : Meta.meta) (def_id : A.FunDeclId.id)
+let ctx_get_termination_measure (span : Meta.span) (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get (Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx
+  ctx_get (Some span) (TerminationMeasureId (FRegular def_id, loop_id)) ctx
 
 (** Small helper to compute the name of a unary operation *)
 let unop_name (unop : unop) : string =
@@ -1256,7 +1256,7 @@ let initialize_names_maps () : names_maps =
 
     Remark: can return [None] for some backends like HOL4.
  *)
-let type_decl_kind_to_qualif (meta : Meta.meta) (kind : decl_kind)
+let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
     (type_kind : type_decl_kind option) : string option =
   match !backend with
   | FStar -> (
@@ -1284,7 +1284,7 @@ let type_decl_kind_to_qualif (meta : Meta.meta) (kind : decl_kind)
           (* This is for traits *)
           Some "Record"
       | _ ->
-          craise __FILE__ __LINE__ meta
+          craise __FILE__ __LINE__ span
             ("Unexpected: (" ^ show_decl_kind kind ^ ", "
             ^ Print.option_to_string show_type_decl_kind type_kind
             ^ ")"))
@@ -1341,17 +1341,17 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
 
     TODO: move inside the formatter?
  *)
-let type_keyword (meta : Meta.meta) =
+let type_keyword (span : Meta.span) =
   match !backend with
   | FStar -> "Type0"
   | Coq | Lean -> "Type"
-  | HOL4 -> craise __FILE__ __LINE__ meta "Unexpected"
+  | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
 
 (** Helper *)
-let name_last_elem_as_ident (meta : Meta.meta) (n : llbc_name) : string =
+let name_last_elem_as_ident (span : Meta.span) (n : llbc_name) : string =
   match Collections.List.last n with
   | PeIdent (s, _) -> s
-  | PeImpl _ -> craise __FILE__ __LINE__ meta "Unexpected"
+  | PeImpl _ -> craise __FILE__ __LINE__ span "Unexpected"
 
 (** Helper
 
@@ -1360,22 +1360,22 @@ let name_last_elem_as_ident (meta : Meta.meta) (n : llbc_name) : string =
     we remove it. We ignore disambiguators (there may be collisions, but we
     check if there are).
  *)
-let ctx_prepare_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_prepare_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : llbc_name =
   (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
   match name with
   | (PeIdent (crate, _) as id) :: name ->
       if crate = ctx.crate.name then name else id :: name
   | _ ->
-      craise __FILE__ __LINE__ meta
+      craise __FILE__ __LINE__ span
         ("Unexpected name shape: "
         ^ TranslateCore.name_to_string ctx.trans_ctx name)
 
 (** Helper *)
-let ctx_compute_simple_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_simple_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : string list =
   (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
-  let name = ctx_prepare_name meta ctx name in
+  let name = ctx_prepare_name span ctx name in
   name_to_simple_name ctx.trans_ctx name
 
 (** Helper *)
@@ -1383,14 +1383,14 @@ let ctx_compute_simple_type_name = ctx_compute_simple_name
 
 (** Helper *)
 
-let ctx_compute_type_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_type_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : string =
-  flatten_name (ctx_compute_simple_type_name meta ctx name)
+  flatten_name (ctx_compute_simple_type_name span ctx name)
 
 (** Provided a basename, compute a type name. *)
-let ctx_compute_type_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) =
-  let name = ctx_compute_type_name_no_suffix meta ctx name in
+  let name = ctx_compute_type_name_no_suffix span ctx name in
   match !backend with
   | FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
   | Coq | HOL4 -> name ^ "_t"
@@ -1407,7 +1407,7 @@ let ctx_compute_type_name (meta : Meta.meta) (ctx : extraction_ctx)
     access then causes trouble because not all provers accept syntax like
     [x.3] where [x] is a tuple.
  *)
-let ctx_compute_field_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
     (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option)
     : string =
   let field_name_s =
@@ -1423,7 +1423,7 @@ let ctx_compute_field_name (meta : Meta.meta) (ctx : extraction_ctx)
     else field_name_s
   else
     let def_name =
-      ctx_compute_type_name_no_suffix meta ctx def_name ^ "_" ^ field_name_s
+      ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ field_name_s
     in
     match !backend with
     | Lean | HOL4 -> def_name
@@ -1433,14 +1433,14 @@ let ctx_compute_field_name (meta : Meta.meta) (ctx : extraction_ctx)
     - type name
     - variant name
  *)
-let ctx_compute_variant_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx)
     (def_name : llbc_name) (variant : string) : string =
   match !backend with
   | FStar | Coq | HOL4 ->
       let variant = to_camel_case variant in
       if !variant_concatenate_type_name then
         StringUtils.capitalize_first_letter
-          (ctx_compute_type_name_no_suffix meta ctx def_name ^ "_" ^ variant)
+          (ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ variant)
       else variant
   | Lean -> variant
 
@@ -1455,14 +1455,14 @@ let ctx_compute_variant_name (meta : Meta.meta) (ctx : extraction_ctx)
     Inputs:
     - type name
 *)
-let ctx_compute_struct_constructor (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_struct_constructor (span : Meta.span) (ctx : extraction_ctx)
     (basename : llbc_name) : string =
-  let tname = ctx_compute_type_name meta ctx basename in
+  let tname = ctx_compute_type_name span ctx basename in
   ExtractBuiltin.mk_struct_constructor tname
 
-let ctx_compute_fun_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
     (fname : llbc_name) : string =
-  let fname = ctx_compute_simple_name meta ctx fname in
+  let fname = ctx_compute_simple_name span ctx fname in
   (* TODO: don't convert to snake case for Coq, HOL4, F* *)
   let fname = flatten_name fname in
   match !backend with
@@ -1470,15 +1470,15 @@ let ctx_compute_fun_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx)
   | Lean -> fname
 
 (** Provided a basename, compute the name of a global declaration. *)
-let ctx_compute_global_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : string =
   match !Config.backend with
   | Coq | FStar | HOL4 ->
       let parts =
-        List.map to_snake_case (ctx_compute_simple_name meta ctx name)
+        List.map to_snake_case (ctx_compute_simple_name span ctx name)
       in
       String.concat "_" parts
-  | Lean -> flatten_name (ctx_compute_simple_name meta ctx name)
+  | Lean -> flatten_name (ctx_compute_simple_name span ctx name)
 
 (** Helper function: generate a suffix for a function name, i.e., generates
     a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1509,10 +1509,10 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string =
     - loop id (if pertinent)
     TODO: use the fun id for the assumed functions.
  *)
-let ctx_compute_fun_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
     (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string
     =
-  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
   (* Compute the suffix *)
   let suffix = default_fun_suffix num_loops loop_id in
   (* Concatenate *)
@@ -1520,7 +1520,7 @@ let ctx_compute_fun_name (meta : Meta.meta) (ctx : extraction_ctx)
 
 let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     : string =
-  ctx_compute_type_name trait_decl.meta ctx trait_decl.llbc_name
+  ctx_compute_type_name trait_decl.span ctx trait_decl.llbc_name
 
 let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     (trait_impl : trait_impl) : string =
@@ -1533,7 +1533,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
   let name =
     let params = trait_impl.llbc_generics in
     let args = trait_impl.llbc_impl_trait.decl_generics in
-    let name = ctx_prepare_name trait_impl.meta ctx trait_decl.llbc_name in
+    let name = ctx_prepare_name trait_impl.span ctx trait_decl.llbc_name in
     trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
   in
   let name = flatten_name name in
@@ -1670,17 +1670,17 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
       the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
-let ctx_compute_termination_measure_name (meta : Meta.meta)
+let ctx_compute_termination_measure_name (span : Meta.span)
     (ctx : extraction_ctx) (_fid : A.FunDeclId.id) (fname : llbc_name)
     (num_loops : int) (loop_id : LoopId.id option) : string =
-  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
     match !Config.backend with
     | FStar -> "_decreases"
     | Lean -> "_terminates"
-    | Coq | HOL4 -> craise __FILE__ __LINE__ meta "Unexpected"
+    | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -1699,16 +1699,16 @@ let ctx_compute_termination_measure_name (meta : Meta.meta)
       the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
-let ctx_compute_decreases_proof_name (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
     (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
     (loop_id : LoopId.id option) : string =
-  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
     match !Config.backend with
     | Lean -> "_decreases"
-    | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ meta "Unexpected"
+    | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -1726,7 +1726,7 @@ let ctx_compute_decreases_proof_name (meta : Meta.meta) (ctx : extraction_ctx)
     if necessary to prevent name clashes: the burden of name clashes checks
     is thus on the caller's side.
  *)
-let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
+let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
     (basename : string option) (ty : ty) : string =
   (* Small helper to derive var names from ADT type names.
 
@@ -1739,7 +1739,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
     let cl = to_snake_case name in
     let cl = String.split_on_char '_' cl in
     let cl = List.filter (fun s -> String.length s > 0) cl in
-    sanity_check __FILE__ __LINE__ (List.length cl > 0) meta;
+    sanity_check __FILE__ __LINE__ (List.length cl > 0) span;
     let cl = List.map (fun s -> s.[0]) cl in
     StringUtils.string_of_chars cl
   in
@@ -1842,85 +1842,85 @@ let name_append_index (basename : string) (i : int) : string =
   basename ^ string_of_int i
 
 (** Generate a unique type variable name and add it to the context *)
-let ctx_add_type_var (meta : Meta.meta) (basename : string) (id : TypeVarId.id)
+let ctx_add_type_var (span : Meta.span) (basename : string) (id : TypeVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
   let name = ctx_compute_type_var_basename ctx basename in
   let name =
     basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
   in
-  let ctx = ctx_add meta (TypeVarId id) name ctx in
+  let ctx = ctx_add span (TypeVarId id) name ctx in
   (ctx, name)
 
 (** Generate a unique const generic variable name and add it to the context *)
-let ctx_add_const_generic_var (meta : Meta.meta) (basename : string)
+let ctx_add_const_generic_var (span : Meta.span) (basename : string)
     (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string
     =
   let name = ctx_compute_const_generic_var_basename ctx basename in
   let name =
     basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
   in
-  let ctx = ctx_add meta (ConstGenericVarId id) name ctx in
+  let ctx = ctx_add span (ConstGenericVarId id) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_type_var} *)
-let ctx_add_type_vars (meta : Meta.meta) (vars : (string * TypeVarId.id) list)
+let ctx_add_type_vars (span : Meta.span) (vars : (string * TypeVarId.id) list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
-    (fun ctx (name, id) -> ctx_add_type_var meta name id ctx)
+    (fun ctx (name, id) -> ctx_add_type_var span name id ctx)
     ctx vars
 
 (** Generate a unique variable name and add it to the context *)
-let ctx_add_var (meta : Meta.meta) (basename : string) (id : VarId.id)
+let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
   let name =
     basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
-  let ctx = ctx_add meta (VarId id) name ctx in
+  let ctx = ctx_add span (VarId id) name ctx in
   (ctx, name)
 
 (** Generate a unique variable name for the trait self clause and add it to the context *)
-let ctx_add_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) :
+let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
     extraction_ctx * string =
   let basename = trait_self_clause_basename in
   let name =
     basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
-  let ctx = ctx_add meta TraitSelfClauseId name ctx in
+  let ctx = ctx_add span TraitSelfClauseId name ctx in
   (ctx, name)
 
 (** Generate a unique trait clause name and add it to the context *)
-let ctx_add_local_trait_clause (meta : Meta.meta) (basename : string)
+let ctx_add_local_trait_clause (span : Meta.span) (basename : string)
     (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string =
   let name =
     basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
-  let ctx = ctx_add meta (LocalTraitClauseId id) name ctx in
+  let ctx = ctx_add span (LocalTraitClauseId id) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_var} *)
-let ctx_add_vars (meta : Meta.meta) (vars : var list) (ctx : extraction_ctx) :
+let ctx_add_vars (span : Meta.span) (vars : var list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (v : var) ->
-      let name = ctx_compute_var_basename meta ctx v.basename v.ty in
-      ctx_add_var meta name v.id ctx)
+      let name = ctx_compute_var_basename span ctx v.basename v.ty in
+      ctx_add_var span name v.id ctx)
     ctx vars
 
-let ctx_add_type_params (meta : Meta.meta) (vars : type_var list)
+let ctx_add_type_params (span : Meta.span) (vars : type_var list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
-    (fun ctx (var : type_var) -> ctx_add_type_var meta var.name var.index ctx)
+    (fun ctx (var : type_var) -> ctx_add_type_var span var.name var.index ctx)
     ctx vars
 
-let ctx_add_const_generic_params (meta : Meta.meta)
+let ctx_add_const_generic_params (span : Meta.span)
     (vars : const_generic_var list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (var : const_generic_var) ->
-      ctx_add_const_generic_var meta var.name var.index ctx)
+      ctx_add_const_generic_var span var.name var.index ctx)
     ctx vars
 
 (** Returns the lists of names for:
@@ -1932,7 +1932,7 @@ let ctx_add_const_generic_params (meta : Meta.meta)
     pretty names for the trait clauses. See {!ctx_compute_trait_clause_name}
     for additional information.
   *)
-let ctx_add_local_trait_clauses (meta : Meta.meta)
+let ctx_add_local_trait_clauses (span : Meta.span)
     (current_def_name : Types.name) (llbc_generics : Types.generic_params)
     (clauses : trait_clause list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
@@ -1942,7 +1942,7 @@ let ctx_add_local_trait_clauses (meta : Meta.meta)
         ctx_compute_trait_clause_basename ctx current_def_name llbc_generics
           c.clause_id
       in
-      ctx_add_local_trait_clause meta basename c.clause_id ctx)
+      ctx_add_local_trait_clause span basename c.clause_id ctx)
     ctx clauses
 
 (** Returns the lists of names for:
@@ -1954,15 +1954,15 @@ let ctx_add_local_trait_clauses (meta : Meta.meta)
     pretty names for the trait clauses. See {!ctx_compute_trait_clause_name}
     for additional information.
   *)
-let ctx_add_generic_params (meta : Meta.meta) (current_def_name : Types.name)
+let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
     (llbc_generics : Types.generic_params) (generics : generic_params)
     (ctx : extraction_ctx) :
     extraction_ctx * string list * string list * string list =
   let { types; const_generics; trait_clauses } = generics in
-  let ctx, tys = ctx_add_type_params meta types ctx in
-  let ctx, cgs = ctx_add_const_generic_params meta const_generics ctx in
+  let ctx, tys = ctx_add_type_params span types ctx in
+  let ctx, cgs = ctx_add_const_generic_params span const_generics ctx in
   let ctx, tcs =
-    ctx_add_local_trait_clauses meta current_def_name llbc_generics
+    ctx_add_local_trait_clauses span current_def_name llbc_generics
       trait_clauses ctx
   in
   (ctx, tys, cgs, tcs)
@@ -1970,20 +1970,20 @@ let ctx_add_generic_params (meta : Meta.meta) (current_def_name : Types.name)
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx_compute_decreases_proof_name def.meta ctx def.def_id def.llbc_name
+    ctx_compute_decreases_proof_name def.span ctx def.def_id def.llbc_name
       def.num_loops def.loop_id
   in
-  ctx_add def.meta
+  ctx_add def.span
     (DecreasesProofId (FRegular def.def_id, def.loop_id))
     name ctx
 
 let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx_compute_termination_measure_name def.meta ctx def.def_id def.llbc_name
+    ctx_compute_termination_measure_name def.span ctx def.def_id def.llbc_name
       def.num_loops def.loop_id
   in
-  ctx_add def.meta
+  ctx_add def.span
     (TerminationMeasureId (FRegular def.def_id, def.loop_id))
     name ctx
 
@@ -1998,10 +1998,10 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
   match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
   | Some name ->
       (* Yes: register the custom binding *)
-      ctx_add def.item_meta.meta decl name ctx
+      ctx_add def.item_meta.span decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
-      let name = ctx_compute_global_name def.item_meta.meta ctx def.name in
+      let name = ctx_compute_global_name def.item_meta.span ctx def.name in
 
       let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
       (* If this is a provided constant (i.e., the default value for a constant
@@ -2011,26 +2011,26 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       let suffix =
         match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
       in
-      let ctx = ctx_add def.item_meta.meta decl (name ^ suffix) ctx in
-      let ctx = ctx_add def.item_meta.meta body (name ^ suffix ^ "_body") ctx in
+      let ctx = ctx_add def.item_meta.span decl (name ^ suffix) ctx in
+      let ctx = ctx_add def.item_meta.span body (name ^ suffix ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
   (* Add the function name *)
-  ctx_compute_fun_name def.meta ctx def.llbc_name def.num_loops def.loop_id
+  ctx_compute_fun_name def.span ctx def.llbc_name def.num_loops def.loop_id
 
 (* TODO: move to Extract *)
 let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
   (* Sanity check: the function should not be a global body - those are handled
    * separately *)
-  sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.meta;
+  sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
   (* Lookup the LLBC def to compute the region group information *)
   let def_id = def.def_id in
   (* Add the function name *)
   let def_name = ctx_compute_fun_name def ctx in
   let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in
-  ctx_add def.meta (FunId (FromLlbc fun_id)) def_name ctx
+  ctx_add def.span (FunId (FromLlbc fun_id)) def_name ctx
 
 let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
     =
-  ctx_compute_type_name def.meta ctx def.llbc_name
+  ctx_compute_type_name def.span ctx def.llbc_name