Still need to fill the TODO: error message and check some meta but it builds

10 files changed, 186 insertions, 178 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 246fc82f..3d0fe75f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2381,7 +2381,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
             in
             let ty () =
               F.pp_print_space fmt ();
-              extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty clause
+              extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
             in
             extract_trait_decl_item ctx fmt item_name ty)
           clauses)
@@ -2396,7 +2396,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
         in
         let ty () =
           F.pp_print_space fmt ();
-          extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty clause
+          extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
         in
         extract_trait_decl_item ctx fmt item_name ty)
       decl.parent_clauses;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index f6b891cc..18729af4 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -425,7 +425,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_get (meta : Meta.meta) (id_to_string : id -> string) (id : id) (nm : names_maps) :
+let names_maps_get ?(meta = None) (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 =
@@ -446,7 +446,7 @@ let names_maps_get (meta : Meta.meta) (id_to_string : id -> string) (id : id) (n
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.fail_hard then craise meta err
+        if !Config.fail_hard then craise_opt_meta meta err
         else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
   else
     let m = nm.names_map.id_to_name in
@@ -458,7 +458,7 @@ let names_maps_get (meta : Meta.meta) (id_to_string : id -> string) (id : id) (n
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.fail_hard then craise meta err
+        if !Config.fail_hard then craise_opt_meta meta err
         else "(ERROR: \"" ^ id_to_string id ^ "\")"
 
 type names_map_init = {
@@ -591,17 +591,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) (ctx : extraction_ctx) =
-  PrintPure.adt_variant_to_string meta (extraction_ctx_to_fmt_env ctx)
+let adt_variant_to_string ?(meta = None) (ctx : extraction_ctx) =
+  PrintPure.adt_variant_to_string ~meta:meta (extraction_ctx_to_fmt_env ctx)
 
-let adt_field_to_string (meta : Meta.meta) (ctx : extraction_ctx) =
-  PrintPure.adt_field_to_string meta (extraction_ctx_to_fmt_env ctx)
+let adt_field_to_string ?(meta = None) (ctx : extraction_ctx) =
+  PrintPure.adt_field_to_string ~meta:meta (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) (id : id) (ctx : extraction_ctx) : string =
+let id_to_string ?(meta = None) (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
     "trait_decl: " ^ trait_name ^ " (id: " ^ A.TraitDeclId.to_string id ^ ")"
@@ -629,11 +629,11 @@ let id_to_string (meta : Meta.meta) (id : id) (ctx : extraction_ctx) : string =
   | 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 ~meta:meta 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 ~meta:meta ctx id field_id in
       "type name: " ^ type_name ^ ", field name: " ^ field_name
   | UnknownId -> "keyword"
   | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
@@ -660,54 +660,54 @@ let id_to_string (meta : Meta.meta) (id : id) (ctx : extraction_ctx) : string =
   | TraitSelfClauseId -> "trait_self_clause"
 
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
-  let id_to_string (id : id) : string = id_to_string meta id ctx in
+  let id_to_string (id : id) : string = id_to_string ~meta:(Some meta) id ctx in
   let names_maps = names_maps_add id_to_string id name ctx.names_maps in
   { ctx with names_maps }
 
-let ctx_get (meta : Meta.meta) (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 (* TODO check if we can remove the meta arg, same for following functions*)
+let ctx_get ?(meta = None) (id : id) (ctx : extraction_ctx) : string =
+  let id_to_string (id : id) : string = id_to_string ~meta:meta id ctx in
+  names_maps_get ~meta:meta id_to_string id ctx.names_maps (* TODO check if we can remove the meta arg, same for following functions*)
 
 let ctx_get_global (meta : Meta.meta) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get meta (GlobalId id) ctx
+  ctx_get ~meta:(Some meta) (GlobalId id) ctx
 
 let ctx_get_function (meta : Meta.meta) (id : fun_id) (ctx : extraction_ctx) : string =
-  ctx_get meta (FunId id) ctx
+  ctx_get ~meta:(Some meta) (FunId id) ctx
 
 let ctx_get_local_function (meta : Meta.meta) (id : A.FunDeclId.id) (lp : LoopId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get_function meta (FromLlbc (FunId (FRegular id), lp)) ctx
 
-let ctx_get_type (meta : Meta.meta) (id : type_id) (ctx : extraction_ctx) : string =
-  cassert (id <> TTuple) meta "T";
-  ctx_get meta (TypeId id) ctx
+let ctx_get_type ?(meta=None) (id : type_id) (ctx : extraction_ctx) : string =
+  cassert_opt_meta (id <> TTuple) meta "T";
+  ctx_get ~meta:meta (TypeId id) ctx
 
 let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get_type meta (TAdtId id) ctx
+  ctx_get_type ~meta:(Some meta) (TAdtId id) ctx
 
-let ctx_get_assumed_type (meta : Meta.meta) (id : assumed_ty) (ctx : extraction_ctx) : string =
-  ctx_get_type meta (TAssumed id) ctx
+let ctx_get_assumed_type ?(meta = None) (id : assumed_ty) (ctx : extraction_ctx) : string =
+  ctx_get_type ~meta:meta (TAssumed id) ctx
 
 let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) :
     string =
   let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-  ctx_get meta (TraitDeclConstructorId id) ctx
+  ctx_get ~meta:(Some meta) (TraitDeclConstructorId id) ctx
 
 let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string =
-  ctx_get meta TraitSelfClauseId ctx
+  ctx_get ~meta:(Some meta) TraitSelfClauseId ctx
 
 let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
   let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-  ctx_get meta (TraitDeclId id) ctx
+  ctx_get ~meta:(Some meta) (TraitDeclId id) ctx
 
 let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
   let meta = (TraitImplId.Map.find id ctx.trans_trait_impls).meta in
-  ctx_get meta (TraitImplId id) ctx
+  ctx_get ~meta:(Some meta) (TraitImplId id) ctx
 
 let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
     let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-    ctx_get meta (TraitItemId (id, item_name)) ctx
+    ctx_get ~meta:(Some meta) (TraitItemId (id, item_name)) ctx
 
 let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
@@ -720,51 +720,51 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
 let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
     let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-  ctx_get meta (TraitMethodId (id, item_name)) ctx
+  ctx_get ~meta:(Some meta) (TraitMethodId (id, item_name)) ctx
 
 let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
     (ctx : extraction_ctx) : string =
     let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-  ctx_get meta (TraitParentClauseId (id, clause)) ctx
+  ctx_get ~meta:(Some meta) (TraitParentClauseId (id, clause)) ctx
 
 let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
     let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
-  ctx_get meta (TraitItemClauseId (id, item, clause)) ctx
+  ctx_get ~meta:(Some meta) (TraitItemClauseId (id, item, clause)) ctx
 
 let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string =
-  ctx_get meta (VarId id) ctx
+  ctx_get ~meta:(Some meta) (VarId id) ctx
 
 let ctx_get_type_var (meta : Meta.meta) (id : TypeVarId.id) (ctx : extraction_ctx) : string =
-  ctx_get meta (TypeVarId id) ctx
+  ctx_get ~meta:(Some meta) (TypeVarId id) ctx
 
 let ctx_get_const_generic_var (meta : Meta.meta) (id : ConstGenericVarId.id) (ctx : extraction_ctx)
     : string =
-  ctx_get meta (ConstGenericVarId id) ctx
+  ctx_get ~meta:(Some meta) (ConstGenericVarId id) ctx
 
 let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id) (ctx : extraction_ctx) :
     string =
-  ctx_get meta (LocalTraitClauseId id) ctx
+  ctx_get ~meta:(Some meta) (LocalTraitClauseId id) ctx
 
 let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id)
     (ctx : extraction_ctx) : string =
     (* let meta = (TypeDeclId.Map.find type_id ctx.trans_types).meta in TODO : check how to get meta *)
-  ctx_get meta (FieldId (type_id, field_id)) ctx
+  ctx_get ~meta:(Some meta) (FieldId (type_id, field_id)) ctx
 
 let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx) : string =
-  ctx_get meta (StructId def_id) ctx
+  ctx_get ~meta:(Some meta) (StructId def_id) ctx
 
 let ctx_get_variant (meta : Meta.meta) (def_id : type_id) (variant_id : VariantId.id)
     (ctx : extraction_ctx) : string =
-  ctx_get meta (VariantId (def_id, variant_id)) ctx
+  ctx_get ~meta:(Some meta) (VariantId (def_id, variant_id)) ctx
 
 let ctx_get_decreases_proof (meta : Meta.meta) (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get meta (DecreasesProofId (FRegular def_id, loop_id)) ctx
+  ctx_get ~meta:(Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx
 
 let ctx_get_termination_measure (meta : Meta.meta) (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get meta (TerminationMeasureId (FRegular def_id, loop_id)) ctx
+  ctx_get ~meta:(Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx
 
 (** Small helper to compute the name of a unary operation *)
 let unop_name (unop : unop) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 51ed7f5a..0329d968 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -287,7 +287,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_string fmt
             ("val [" ^ String.concat ", " names ^ "] = DefineDiv ‘")
         else (
-          assert (List.length names = 1);
+          assert (List.length names = 1) (* TODO: Error message, meta todo*);
           let name = List.hd names in
           F.pp_print_string fmt ("val " ^ name ^ " = Define ‘"));
         F.pp_print_cut fmt ()
@@ -470,7 +470,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               if print_paren then F.pp_print_string fmt "(";
               (* TODO: for now, only the opaque *functions* are extracted in the
                  opaque module. The opaque *types* are assumed. *)
-              F.pp_print_string fmt (ctx_get_type meta type_id ctx);
+              F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx);
               (* We might need to filter the type arguments, if the type
                  is builtin (for instance, we filter the global allocator type
                  argument for `Vec`). *)
@@ -496,7 +496,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
           | HOL4 ->
               let { types; const_generics; trait_refs } = generics in
               (* Const generics are not supported in HOL4 *)
-              assert (const_generics = []);
+              cassert (const_generics = []) meta "Const generics are not supported in HOL4";
               let print_tys =
                 match type_id with
                 | TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
@@ -513,7 +513,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
                   (extract_rec true) types;
                 if print_paren then F.pp_print_string fmt ")";
                 F.pp_print_space fmt ());
-              F.pp_print_string fmt (ctx_get_type meta type_id ctx);
+              F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx);
               if trait_refs <> [] then (
                 F.pp_print_space fmt ();
                 Collections.List.iter_link (F.pp_print_space fmt)
@@ -554,7 +554,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
             F.pp_print_string fmt type_name
         | _ ->
             (* HOL4 doesn't have 1st class types *)
-            assert (!backend <> HOL4);
+            cassert (!backend <> HOL4) meta "TODO: Error message";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
 
@@ -606,7 +606,7 @@ and extract_generic_args (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.form
         (extract_ty meta ctx fmt no_params_tys true)
         types);
     if const_generics <> [] then (
-      assert (!backend <> HOL4);
+      cassert (!backend <> HOL4) meta "TODO: Error message";
       F.pp_print_space fmt ();
       Collections.List.iter_link (F.pp_print_space fmt)
         (extract_const_generic meta ctx fmt true)
@@ -878,7 +878,7 @@ let extract_type_decl_variant (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F
     List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
   in
   (* Sanity check: HOL4 doesn't support const generics *)
-  assert (cg_params = [] || !backend <> HOL4);
+  cassert (cg_params = [] || !backend <> HOL4) meta "TODO: Error message";
   (* Print the final type *)
   if !backend <> HOL4 then (
     F.pp_print_space fmt ();
@@ -1076,7 +1076,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
     else (
       (* We extract for Coq or Lean, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type *)
-      assert (is_rec && (!backend = Coq || !backend = Lean));
+      cassert (is_rec && (!backend = Coq || !backend = Lean)) def.meta "TODO: error message";
       (* Small trick: in Lean we use namespaces, meaning we don't need to prefix
          the constructor name with the name of the type at definition site,
          i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
@@ -1130,10 +1130,11 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
   in
   extract_comment fmt (sl @ [ span ] @ name)
 
-let extract_trait_clause_type meta (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_trait_clause_type (* (meta : Meta.meta) TODO check if right meta*) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
   let trait_name = ctx_get_trait_decl clause.trait_id ctx in
   F.pp_print_string fmt trait_name;
+  let meta = (TraitDeclId.Map.find clause.trait_id ctx.trans_trait_decls).meta in
   extract_generic_args meta ctx fmt no_params_tys clause.generics
 
 (** Insert a space, if necessary *)
@@ -1176,7 +1177,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
     (trait_clauses : string list) : unit =
   let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
   (* HOL4 doesn't support const generics *)
-  assert (cg_params = [] || !backend <> HOL4);
+  cassert (cg_params = [] || !backend <> HOL4) meta "HOL4 doesn't support const generics";
   let left_bracket (implicit : bool) =
     if implicit && !backend <> FStar then F.pp_print_string fmt "{"
     else F.pp_print_string fmt "("
@@ -1257,7 +1258,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
           F.pp_print_space fmt ();
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
-          extract_trait_clause_type meta ctx fmt no_params_tys clause;
+          extract_trait_clause_type ctx fmt no_params_tys clause;
           (* ) *)
           right_bracket as_implicits;
           if use_arrows then (
@@ -1323,7 +1324,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
     (extract_body : bool) : unit =
   (* Sanity check *)
-  assert (extract_body || !backend <> HOL4);
+  cassert (extract_body || !backend <> HOL4) def.meta "TODO: error message";
   let is_tuple_struct =
     TypesUtils.type_decl_from_decl_id_is_tuple_struct
       ctx.trans_ctx.type_ctx.type_infos def.def_id
@@ -1394,7 +1395,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   | None -> F.pp_print_string fmt def_name);
   (* HOL4 doesn't support const generics, and type definitions in HOL4 don't
      support trait clauses *)
-  assert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4);
+  cassert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) def.meta "HOL4 doesn't support const generics, and type definitions in HOL4 don't support trait clauses";
   (* Print the generic parameters *)
   extract_generic_params def.meta ctx_body fmt type_decl_group ~use_forall def.generics
     type_params cg_params trait_clauses;
@@ -1463,9 +1464,9 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.meta def.def_id ctx in
   (* Generic parameters are unsupported *)
-  assert (def.generics.const_generics = []);
+  cassert (def.generics.const_generics = []) def.meta "Generic parameters are unsupported";
   (* Trait clauses on type definitions are unsupported *)
-  assert (def.generics.trait_clauses = []);
+  cassert (def.generics.trait_clauses = []) def.meta "Trait clauses on type definitions are unsupported";
   (* Types  *)
   (* Count the number of parameters *)
   let num_params = List.length def.generics.types in
@@ -1488,7 +1489,7 @@ let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.meta def.def_id ctx in
   (* Sanity check *)
-  assert (def.generics = empty_generic_params);
+  cassert (def.generics = empty_generic_params) def.meta "TODO: error message";
   (* Generate the declaration *)
   F.pp_print_space fmt ();
   F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”");
@@ -1564,7 +1565,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
-  assert (!backend = Coq);
+  cassert (!backend = Coq) decl.meta "TODO: error message";
   (* Generating the [Arguments] instructions is useful only if there are parameters *)
   let num_params =
     List.length decl.generics.types
@@ -1610,7 +1611,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
-  assert (!backend = Coq);
+  cassert (!backend = Coq) decl.meta "TODO: error message";
   match decl.kind with
   | Opaque | Enum _ -> ()
   | Struct fields ->
@@ -1770,7 +1771,7 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
         extract_type_decl_record_field_projectors ctx fmt kind decl)
 
 (** Extract the state type declaration. *)
-let extract_state_type (meta : Meta.meta) (fmt : F.formatter) (ctx : extraction_ctx)
+let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
     (kind : decl_kind) : unit =
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
@@ -1781,14 +1782,14 @@ let extract_state_type (meta : Meta.meta) (fmt : F.formatter) (ctx : extraction_
    * one line *)
   F.pp_open_hvbox fmt 0;
   (* Retrieve the name *)
-  let state_name = ctx_get_assumed_type meta TState ctx in
+  let state_name = ctx_get_assumed_type TState ctx in
   (* The syntax for Lean and Coq is almost identical. *)
   let print_axiom () =
     let axiom =
       match !backend with
       | Coq -> "Axiom"
       | Lean -> "axiom"
-      | FStar | HOL4 -> craise meta "Unexpected"
+      | FStar | HOL4 -> raise (Failure "Unexpected")
     in
     F.pp_print_string fmt axiom;
     F.pp_print_space fmt ();
@@ -1802,7 +1803,7 @@ let extract_state_type (meta : Meta.meta) (fmt : F.formatter) (ctx : extraction_
   (* The kind should be [Assumed] or [Declared] *)
   (match kind with
   | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast ->
-      craise meta "Unexpected"
+      raise (Failure "Unexpected")
   | Assumed -> (
       match !backend with
       | FStar ->
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 3e887741..6ef4a13b 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -53,8 +53,8 @@ type abs_borrows_loans_maps = {
     regions.
  *)
 module type PrimMatcher = sig
-  val match_etys : eval_ctx -> eval_ctx -> ety -> ety -> ety
-  val match_rtys : eval_ctx -> eval_ctx -> rty -> rty -> rty
+  val match_etys : Meta.meta -> eval_ctx -> eval_ctx -> ety -> ety -> ety
+  val match_rtys : Meta.meta -> eval_ctx -> eval_ctx -> rty -> rty -> rty
 
   (** The input primitive values are not equal *)
   val match_distinct_literals :
@@ -111,6 +111,7 @@ module type PrimMatcher = sig
       [v]: the result of matching the shared values coming from the two loans
    *)
   val match_shared_loans :
+    Meta.meta ->
     eval_ctx ->
     eval_ctx ->
     ety ->
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 08d18407..0e0a06e3 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -43,8 +43,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
          match Id0.Map.find_opt id0 !map with
          | None -> ()
          | Some set ->
-             assert (
-               (not check_not_already_registered) || not (Id1.Set.mem id1 set)));
+             cassert (
+               (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta "TODO: error message");
       (* Update the mapping *)
       map :=
         Id0.Map.update id0
@@ -53,10 +53,10 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
             | None -> Some (Id1.Set.singleton id1)
             | Some ids ->
                 (* Sanity check *)
-                assert (not check_singleton_sets);
-                assert (
+                cassert (not check_singleton_sets) meta "TODO: error message";
+                cassert (
                   (not check_not_already_registered)
-                  || not (Id1.Set.mem id1 ids));
+                  || not (Id1.Set.mem id1 ids)) meta "TODO: error message";
                 (* Update *)
                 Some (Id1.Set.add id1 ids))
           !map
@@ -144,14 +144,14 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
 
     TODO: probably don't need to take [match_regions] as input anymore.
  *)
-let rec match_types (match_distinct_types : ty -> ty -> ty)
+let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty)
     (match_regions : region -> region -> region) (ty0 : ty) (ty1 : ty) : ty =
-  let match_rec = match_types match_distinct_types match_regions in
+  let match_rec = match_types meta match_distinct_types match_regions in
   match (ty0, ty1) with
   | TAdt (id0, generics0), TAdt (id1, generics1) ->
-      assert (id0 = id1);
-      assert (generics0.const_generics = generics1.const_generics);
-      assert (generics0.trait_refs = generics1.trait_refs);
+      cassert (id0 = id1) meta "T";
+      cassert (generics0.const_generics = generics1.const_generics) meta "T";
+      cassert (generics0.trait_refs = generics1.trait_refs) meta "T";
       let id = id0 in
       let const_generics = generics1.const_generics in
       let trait_refs = generics1.trait_refs in
@@ -168,17 +168,17 @@ let rec match_types (match_distinct_types : ty -> ty -> ty)
       let generics = { regions; types; const_generics; trait_refs } in
       TAdt (id, generics)
   | TVar vid0, TVar vid1 ->
-      assert (vid0 = vid1);
+      cassert (vid0 = vid1) meta "T";
       let vid = vid0 in
       TVar vid
   | TLiteral lty0, TLiteral lty1 ->
-      assert (lty0 = lty1);
+      cassert (lty0 = lty1) meta "T";
       ty0
   | TNever, TNever -> ty0
   | TRef (r0, ty0, k0), TRef (r1, ty1, k1) ->
       let r = match_regions r0 r1 in
       let ty = match_rec ty0 ty1 in
-      assert (k0 = k1);
+      cassert (k0 = k1) meta "T";
       let k = k0 in
       TRef (r, ty, k)
   | _ -> match_distinct_types ty0 ty1
@@ -187,7 +187,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
   let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
       (v0 : typed_value) (v1 : typed_value) : typed_value =
     let match_rec = match_typed_values meta ctx0 ctx1 in
-    let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in
+    let ty = M.match_etys meta ctx0 ctx1 v0.ty v1.ty in
     (* Using ValuesUtils.value_has_borrows on purpose here: we want
        to make explicit the fact that, though we have to pick
        one of the two contexts (ctx0 here) to call value_has_borrows,
@@ -210,8 +210,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
           { value; ty = v1.ty }
         else (
           (* For now, we don't merge ADTs which contain borrows *)
-          assert (not (value_has_borrows v0.value));
-          assert (not (value_has_borrows v1.value));
+          cassert (not (value_has_borrows v0.value)) meta "ADTs which contain borrows are not merged yet";
+          cassert (not (value_has_borrows v1.value)) meta "ADTs which contain borrows are not merged yet";
           (* Merge *)
           M.match_distinct_adts meta ctx0 ctx1 ty av0 av1)
     | VBottom, VBottom -> v0
@@ -226,10 +226,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
           | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) ->
               let bv = match_rec bv0 bv1 in
 
-              assert (
+              cassert (
                 not
                   (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
-                     bv.value));
+                     bv.value)) meta "T";
               let bid, bv =
                 M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
               in
@@ -252,8 +252,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
           match (lc0, lc1) with
           | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) ->
               let sv = match_rec sv0 sv1 in
-              assert (not (value_has_borrows sv.value));
-              let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in
+              cassert (not (value_has_borrows sv.value)) meta "T";
+              let ids, sv = M.match_shared_loans meta ctx0 ctx1 ty ids0 ids1 sv in
               VSharedLoan (ids, sv)
           | VMutLoan id0, VMutLoan id1 ->
               let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in
@@ -265,8 +265,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
     | VSymbolic sv0, VSymbolic sv1 ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
-        assert (not (value_has_borrows v0.value));
-        assert (not (value_has_borrows v1.value));
+        cassert (not (value_has_borrows v0.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
+        cassert (not (value_has_borrows v1.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
         (* Match *)
         let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in
         { v1 with value = VSymbolic sv }
@@ -310,7 +310,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
 
     let match_rec = match_typed_values meta ctx0 ctx1 in
     let match_arec = match_typed_avalues meta ctx0 ctx1 in
-    let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in
+    let ty = M.match_rtys meta ctx0 ctx1 v0.ty v1.ty in
     match (v0.value, v1.value) with
     | AAdt av0, AAdt av1 ->
         if av0.variant_id = av1.variant_id then
@@ -373,7 +373,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
             log#ldebug (lazy "match_typed_avalues: shared loans");
             let sv = match_rec sv0 sv1 in
             let av = match_arec av0 av1 in
-            assert (not (value_has_borrows sv.value));
+            cassert (not (value_has_borrows sv.value)) meta "T";
             M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1
               av1 ty sv av
         | AMutLoan (id0, av0), AMutLoan (id1, av1) ->
@@ -403,14 +403,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
   let push_absl (absl : abs list) : unit = List.iter push_abs absl
 
-  let match_etys _ _ ty0 ty1 =
-    assert (ty0 = ty1);
+  let match_etys (meta : Meta.meta) _ _ ty0 ty1 =
+    cassert (ty0 = ty1) meta "T";
     ty0
 
-  let match_rtys _ _ ty0 ty1 =
+  let match_rtys (meta : Meta.meta) _ _ ty0 ty1 =
     (* The types must be equal - in effect, this forbids to match symbolic
        values containing borrows *)
-    assert (ty0 = ty1);
+    cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows";
     ty0
 
   let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
@@ -424,7 +424,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
        updates
     *)
     let check_no_borrows ctx (v : typed_value) =
-      assert (not (value_has_borrows ctx v.value))
+      cassert (not (value_has_borrows ctx v.value)) meta "ADTs should not contain borrows"
     in
     List.iter (check_no_borrows ctx0) adt0.field_values;
     List.iter (check_no_borrows ctx1) adt1.field_values;
@@ -559,11 +559,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          do so, we won't introduce reborrows like above: the forward loop function
          will update [v], while the backward loop function will return nothing.
       *)
-      assert (
-        not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value));
+      cassert (
+        not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "T";
 
       if bv0 = bv1 then (
-        assert (bv0 = bv);
+        cassert (bv0 = bv) meta "T";
         (bid0, bv))
       else
         let rid = fresh_region_id () in
@@ -571,7 +571,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
         let kind = RMut in
         let bv_ty = bv.ty in
-        assert (ty_no_regions bv_ty);
+        cassert (ty_no_regions bv_ty) meta "T";
         let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
         let borrow_av =
@@ -624,7 +624,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue =
         let bv_ty = bv.ty in
-        assert (ty_no_regions bv_ty);
+        cassert (ty_no_regions bv_ty) meta "T";
         let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in
         { value; ty = borrow_ty }
       in
@@ -654,7 +654,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       (* Return the new borrow *)
       (bid2, sv)
 
-  let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+  let match_shared_loans (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
       (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
       loan_id_set * typed_value =
     (* Check if the ids are the same - Rem.: we forbid the sets of loans
@@ -671,7 +671,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       raise (ValueMatchFailure (LoansInRight extra_ids_right));
 
     (* This should always be true if we get here *)
-    assert (ids0 = ids1);
+    cassert (ids0 = ids1) meta "This should always be true if we get here ";
     let ids = ids0 in
 
     (* Return *)
@@ -691,13 +691,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     let id1 = sv1.sv_id in
     if id0 = id1 then (
       (* Sanity check *)
-      assert (sv0 = sv1);
+      cassert (sv0 = sv1) meta "T";
       (* Return *)
       sv0)
     else (
       (* The caller should have checked that the symbolic values don't contain
          borrows *)
-      assert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty));
+      cassert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta "The caller should have checked that the symbolic values don't contain borrows";
       (* We simply introduce a fresh symbolic value *)
       mk_fresh_symbolic_value meta sv0.sv_ty)
 
@@ -709,8 +709,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
        If there are loans in the regular value, raise an exception.
     *)
     let type_infos = ctx0.type_ctx.type_infos in
-    assert (not (ty_has_borrows type_infos sv.sv_ty));
-    assert (not (ValuesUtils.value_has_borrows type_infos v.value));
+    cassert (not (ty_has_borrows type_infos sv.sv_ty)) meta "Check that:
+    - there are no borrows in the symbolic value
+    - there are no borrows in the \"regular\" value
+    If there are loans in the regular value, raise an exception.";
+    cassert (not (ValuesUtils.value_has_borrows type_infos v.value)) meta "Check that:
+    - there are no borrows in the symbolic value
+    - there are no borrows in the \"regular\" value
+    If there are loans in the regular value, raise an exception.";
     let value_is_left = not left in
     (match InterpreterBorrowsCore.get_first_loan_in_value v with
     | None -> ()
@@ -804,14 +810,14 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
   (** Small utility *)
   let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues
 
-  let match_etys _ _ ty0 ty1 =
-    assert (ty0 = ty1);
+  let match_etys (meta : Meta.meta) _ _ ty0 ty1 =
+    cassert (ty0 = ty1) meta "T";
     ty0
 
-  let match_rtys _ _ ty0 ty1 =
+  let match_rtys (meta : Meta.meta) _ _ ty0 ty1 =
     (* The types must be equal - in effect, this forbids to match symbolic
        values containing borrows *)
-    assert (ty0 = ty1);
+    cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows";
     ty0
 
   let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
@@ -835,7 +841,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
     (* There can't be bottoms in borrowed values *)
     (bid1, bv1)
 
-  let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+  let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
       (_ : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
       loan_id_set * typed_value =
     (* There can't be bottoms in shared loans *)
@@ -983,10 +989,10 @@ struct
   let match_aids = GetSetAid.match_es "match_aids: " S.aid_map
 
   (** *)
-  let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
+  let match_etys (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
     if ty0 <> ty1 then raise (Distinct "match_etys") else ty0
 
-  let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
+  let match_rtys (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
     let match_distinct_types _ _ = raise (Distinct "match_rtys") in
     let match_regions r0 r1 =
       match (r0, r1) with
@@ -996,7 +1002,7 @@ struct
           RFVar rid
       | _ -> raise (Distinct "match_rtys")
     in
-    match_types match_distinct_types match_regions ty0 ty1
+    match_types meta match_distinct_types match_regions ty0 ty1
 
   let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
       (_ : literal) (_ : literal) : typed_value =
@@ -1042,7 +1048,7 @@ struct
     let bid = match_borrow_id bid0 bid1 in
     (bid, bv)
 
-  let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+  let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
       (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
       loan_id_set * typed_value =
     let ids = match_loan_ids ids0 ids1 in
@@ -1052,7 +1058,7 @@ struct
       (bid1 : loan_id) : loan_id =
     match_loan_id bid0 bid1
 
-  let match_symbolic_values (_ : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+  let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
       (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value =
     let id0 = sv0.sv_id in
     let id1 = sv1.sv_id in
@@ -1071,12 +1077,12 @@ struct
       let sv_id =
         GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1
       in
-      let sv_ty = match_rtys ctx0 ctx1 sv0.sv_ty sv1.sv_ty in
+      let sv_ty = match_rtys meta ctx0 ctx1 sv0.sv_ty sv1.sv_ty in
       let sv = { sv_id; sv_ty } in
       sv
     else (
       (* Check: fixed values are fixed *)
-      assert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map));
+      cassert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta "Fixed values should be fixed";
 
       (* Update the symbolic value mapping *)
       let sv1 = mk_typed_value_from_symbolic_value sv1 in
@@ -1093,10 +1099,10 @@ struct
       (sv : symbolic_value) (v : typed_value) : typed_value =
     if S.check_equiv then raise (Distinct "match_symbolic_with_other")
     else (
-      assert left;
+      cassert left meta "T";
       let id = sv.sv_id in
       (* Check: fixed values are fixed *)
-      assert (not (SymbolicValueId.InjSubst.mem id !S.sid_map));
+      cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed";
       (* Update the binding for the target symbolic value *)
       S.sid_to_value_map :=
         SymbolicValueId.Map.add_strict id v !S.sid_to_value_map;
@@ -1314,17 +1320,17 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
            be the same and their values equal (and the borrows/loans/symbolic *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Fixed values: the values must be equal *)
-          assert (b0 = b1);
-          assert (v0 = v1);
+          cassert (b0 = b1) meta "The fixed values should be equal";
+          cassert (v0 = v1) meta "The fixed values should be equal";
           (* The ids present in the left value must be fixed *)
           let ids, _ = compute_typed_value_ids v0 in
-          assert ((not S.check_equiv) || ids_are_fixed ids));
+          cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "T";
         (* We still match the values - allows to compute mappings (which
            are the identity actually) *)
         let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in
         match_envs env0' env1'
     | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' ->
-        assert (b0 = b1);
+        cassert (b0 = b1) meta "T";
         (* Match the values *)
         let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in
         (* Continue *)
@@ -1335,10 +1341,10 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs");
           (* Still in the prefix: the abstractions must be the same *)
-          assert (abs0 = abs1);
+          cassert (abs0 = abs1) meta "The abstractions should be the same";
           (* Their ids must be fixed *)
           let ids, _ = compute_abs_ids abs0 in
-          assert ((not S.check_equiv) || ids_are_fixed ids);
+          cassert ((not S.check_equiv) || ids_are_fixed ids) meta "The ids should be fixed";
           (* Continue *)
           match_envs env0' env1')
         else (
@@ -1442,11 +1448,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id
           (fun (var0, var1) ->
             match (var0, var1) with
             | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) ->
-                assert (b0 = b1);
+                cassert (b0 = b1) meta "T";
                 let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
                 ()
             | EBinding (BVar b0, v0), EBinding (BVar b1, v1) ->
-                assert (b0 = b1);
+                cassert (b0 = b1) meta "T";
                 let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
                 ()
             | _ -> craise meta "Unexpected")
@@ -1479,11 +1485,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id
           (fun (var0, var1) ->
             match (var0, var1) with
             | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) ->
-                assert (b0 = b1);
+                cassert (b0 = b1) meta "T";
                 let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
                 (var1, v)
             | EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) ->
-                assert (b0 = b1);
+                cassert (b0 = b1) meta "T";
                 let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
                 (var1, v)
             | _ -> craise meta "Unexpected")
@@ -1584,7 +1590,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
     let filt_src_env, new_absl, new_dummyl =
       ctx_split_fixed_new meta fixed_ids src_ctx
     in
-    assert (new_dummyl = []);
+    cassert (new_dummyl = []) meta "T";
     let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
     let filt_src_ctx = { src_ctx with env = filt_src_env } in
 
@@ -1720,7 +1726,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
        abstractions and in the *variable bindings* once we allow symbolic
        values containing borrows to not be eagerly expanded.
     *)
-    assert Config.greedy_expand_symbolics_with_borrows;
+    cassert Config.greedy_expand_symbolics_with_borrows meta "T";
 
     (* Update the borrows and loans in the abstractions of the target context.
 
@@ -1789,8 +1795,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
               (* No mapping: this means that the borrow was mapped when
                  we matched values (it doesn't come from a fresh abstraction)
                  and because of this, it should actually be mapped to itself *)
-              assert (
-                BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id);
+              cassert (
+                BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta "The borrow should mapped to itself: no mapping  means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) ";
               id
           | Some id -> id
 
@@ -1802,8 +1808,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
         method! visit_abs env abs =
           match abs.kind with
           | Loop (loop_id', rg_id, kind) ->
-              assert (loop_id' = loop_id);
-              assert (kind = LoopSynthInput);
+              cassert (loop_id' = loop_id) meta "T";
+              cassert (kind = LoopSynthInput) meta "T";
               let can_end = false in
               let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
               let abs = { abs with kind; can_end } in
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index c6db7f2e..c7141064 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -354,7 +354,7 @@ let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_i
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
-  let def = ctx_lookup_type_decl ctx def_id in (*TODO: check if can be moved before assert ?*)
+  let def = ctx_lookup_type_decl ctx def_id in
   cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
   (* Compute the field types *)
   let field_types =
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index e71b7b68..b71daac5 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1551,7 +1551,7 @@ and eval_function_body (meta : Meta.meta) (config : config) (body : statement) :
      * checking the invariants *)
     let cc = greedy_expand_symbolic_values body.meta config in
     (* Sanity check *)
-    let cc = comp_check_ctx cc (Invariants.check_invariants meta) in
+    let cc = comp_check_ctx cc (Invariants.check_invariants meta) in (* Check if right meta *)
     (* Continue *)
     cc (cf res)
   in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 618a8afc..3008e1bd 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -294,7 +294,7 @@ let mplace_to_string (env : fmt_env) (p : mplace) : string =
   let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in
   mprojection_to_string env name p.projection
 
-let adt_variant_to_string (meta : Meta.meta) (env : fmt_env) (adt_id : type_id)
+let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
     (variant_id : VariantId.id option) : string =
   match adt_id with
   | TTuple -> "Tuple"
@@ -308,29 +308,29 @@ let adt_variant_to_string (meta : Meta.meta) (env : fmt_env) (adt_id : type_id)
       match aty with
       | TState | TArray | TSlice | TStr | TRawPtr _ ->
           (* Those types are opaque: we can't get there *)
-          craise meta "Unreachable"
+          craise_opt_meta meta "Unreachable"
       | TResult ->
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then "@Result::Return"
           else if variant_id = result_fail_id then "@Result::Fail"
           else
-            craise meta "Unreachable: improper variant id for result type"
+            craise_opt_meta meta "Unreachable: improper variant id for result type"
       | TError ->
           let variant_id = Option.get variant_id in
           if variant_id = error_failure_id then "@Error::Failure"
           else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
-          else craise meta "Unreachable: improper variant id for error type"
+          else craise_opt_meta meta "Unreachable: improper variant id for error type"
       | TFuel ->
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then "@Fuel::Zero"
           else if variant_id = fuel_succ_id then "@Fuel::Succ"
-          else craise meta "Unreachable: improper variant id for fuel type")
+          else craise_opt_meta meta "Unreachable: improper variant id for fuel type")
 
-let adt_field_to_string (meta : Meta.meta) (env : fmt_env) (adt_id : type_id)
+let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
     (field_id : FieldId.id) : string =
   match adt_id with
   | TTuple ->
-      craise meta "Unreachable"
+      craise_opt_meta meta "Unreachable"
       (* Tuples don't use the opaque field id for the field indices, but [int] *)
   | TAdtId def_id -> (
       (* "Regular" ADT *)
@@ -343,10 +343,10 @@ let adt_field_to_string (meta : Meta.meta) (env : fmt_env) (adt_id : type_id)
       match aty with
       | TState | TFuel | TArray | TSlice | TStr ->
           (* Opaque types: we can't get there *)
-          craise meta "Unreachable"
+          craise_opt_meta meta "Unreachable"
       | TResult | TError | TRawPtr _ ->
           (* Enumerations: we can't get there *)
-          craise meta "Unreachable")
+          craise_opt_meta meta "Unreachable")
 
 (** TODO: we don't need a general function anymore (it is now only used for
     patterns)
@@ -611,13 +611,13 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s
             (global_decl_id_to_string env global_id, generics)
         | AdtCons adt_cons_id ->
             let variant_s =
-              adt_variant_to_string meta env adt_cons_id.adt_id
+              adt_variant_to_string ~meta:(Some meta) env adt_cons_id.adt_id
                 adt_cons_id.variant_id
             in
             (ConstStrings.constructor_prefix ^ variant_s, [])
         | Proj { adt_id; field_id } ->
-            let adt_s = adt_variant_to_string meta env adt_id None in
-            let field_s = adt_field_to_string meta env adt_id field_id in
+            let adt_s = adt_variant_to_string ~meta:(Some meta) env adt_id None in
+            let field_s = adt_field_to_string ~meta:(Some meta) env adt_id field_id in
             (* Adopting an F*-like syntax *)
             (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, [])
         | TraitConst (trait_ref, const_name) ->
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6e3a537e..63605b9c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -878,7 +878,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
   if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
 
 (** Small utility. *)
-let compute_raw_fun_effect_info (* (meta : Meta.meta) *) (fun_infos : fun_info A.FunDeclId.Map.t)
+let compute_raw_fun_effect_info  (meta : Meta.meta) (fun_infos : fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
@@ -896,7 +896,7 @@ let compute_raw_fun_effect_info (* (meta : Meta.meta) *) (fun_infos : fun_info A
         is_rec = info.is_rec || Option.is_some lid;
       }
   | FunId (FAssumed aid) ->
-      assert (lid = None) (* meta "TODO: error message" *);
+      cassert (lid = None) meta "TODO: error message";
       {
         can_fail = Assumed.assumed_fun_can_fail aid;
         stateful_group = false;
@@ -921,7 +921,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
           in
           { info with is_rec = info.is_rec || Option.is_some lid }
       | FunId (FAssumed _) ->
-          compute_raw_fun_effect_info (* ctx.fun_decl.meta *) ctx.fun_ctx.fun_infos fun_id lid gid)
+          compute_raw_fun_effect_info ctx.fun_decl.meta ctx.fun_ctx.fun_infos fun_id lid gid)
   | Some lid -> (
       (* This is necessarily for the current function *)
       match fun_id with
@@ -981,7 +981,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta)
 
   (* Is the forward function stateful, and can it fail? *)
   let fwd_effect_info =
-    compute_raw_fun_effect_info fun_infos fun_id None None
+    compute_raw_fun_effect_info meta fun_infos fun_id None None
   in
   (* Compute the forward inputs *)
   let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in
@@ -1099,7 +1099,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta)
       RegionGroupId.id * back_sg_info =
     let gid = rg.id in
     let back_effect_info =
-      compute_raw_fun_effect_info fun_infos fun_id None (Some gid)
+      compute_raw_fun_effect_info meta fun_infos fun_id None (Some gid)
     in
     let inputs_no_state = translate_back_inputs_for_gid gid in
     let inputs_no_state =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2ee1324b..11b179db 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -352,7 +352,7 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     [is_rec]: [true] if the types are recursive. Necessarily [true] if there is
     > 1 type to extract.
  *)
-let export_types_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
+let export_types_group (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit =
   assert (ids <> []) (* meta "TODO: Error message" *);
   let export_type = export_type fmt config ctx in
@@ -493,7 +493,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     Rem.: this function doesn't check [config.extract_fun_decls]: it should have
     been checked by the caller.
  *)
-let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
+let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (is_rec : bool) (decls : Pure.fun_decl list) : unit =
   (* Utility to check a function has a decrease clause *)
   let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -504,7 +504,7 @@ let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (conf
   (* Extract the function declarations *)
   (* Check if the functions are mutually recursive *)
   let is_mut_rec = List.length decls > 1 in
-  cassert ((not is_mut_rec) || is_rec) meta "TODO: Error message";
+  assert ((not is_mut_rec) || is_rec);
   let decls_length = List.length decls in
   (* We open and close the declaration group with [{start, end}_fun_decl_group].
 
@@ -568,7 +568,7 @@ let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (conf
     In case of (non-mutually) recursive functions, we use a simple procedure to
     check if the forward and backward functions are mutually recursive.
  *)
-let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
+let export_functions_group (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit =
   (* Check if the definition are builtin - if yes they must be ignored.
      Note that if one definition in the group is builtin, then all the
@@ -584,7 +584,7 @@ let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config :
 
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
-    cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message"
+    assert (List.for_all (fun b -> b) builtin)
   else
     (* Utility to check a function has a decrease clause *)
     let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -616,11 +616,11 @@ let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config :
               | FStar ->
                   Extract.extract_template_fstar_decreases_clause ctx fmt decl
               | Coq ->
-                  craise
-                    meta "Coq doesn't have decreases/termination clauses"
+                  raise
+                    (Failure "Coq doesn't have decreases/termination clauses")
               | HOL4 ->
-                  craise
-                    meta "HOL4 doesn't have decreases/termination clauses"
+                  raise
+                    (Failure "HOL4 doesn't have decreases/termination clauses")
           in
           extract_decrease f.f;
           List.iter extract_decrease f.loops)
@@ -639,7 +639,7 @@ let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config :
 
        (* Extract the subgroups *)
        let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
-         export_functions_group_scc meta fmt config ctx is_rec decls
+         export_functions_group_scc fmt config ctx is_rec decls
        in
        List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
 
@@ -658,7 +658,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
   let open ExtractBuiltin in
   if
     match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
-      (builtin_trait_decls_map trait_decl.meta ())
+      (builtin_trait_decls_map ())
     = None
   then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
@@ -694,16 +694,16 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     split the definitions between different files (or not), we can control
     what is precisely extracted.
  *)
-let extract_definitions (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
+let extract_definitions (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order.
      - [extract_decl]: extract the type declaration (if not filtered)
      - [extract_extra_info]: extra the extra type information (e.g.,
        the [Arguments] information in Coq).
   *)
-  let export_functions_group = export_functions_group meta fmt config ctx in
+  let export_functions_group = export_functions_group fmt config ctx in
   let export_global = export_global fmt config ctx in
-  let export_types_group = export_types_group meta fmt config ctx in
+  let export_types_group = export_types_group fmt config ctx in
   let export_trait_decl_group id =
     export_trait_decl fmt config ctx id true false
   in
@@ -716,7 +716,7 @@ let extract_definitions (meta : Meta.meta) (fmt : Format.formatter) (config : ge
     let kind =
       if config.interface then ExtractBase.Declared else ExtractBase.Assumed
     in
-    Extract.extract_state_type meta fmt ctx kind
+    Extract.extract_state_type fmt ctx kind
   in
 
   let export_decl_group (dg : declaration_group) : unit =
@@ -785,7 +785,7 @@ type extract_file_info = {
   custom_includes : string list;
 }
 
-let extract_file (meta : Meta.meta) (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
+let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
     : unit =
   (* Open the file and create the formatter *)
   let out = open_out fi.filename in
@@ -885,7 +885,7 @@ let extract_file (meta : Meta.meta) (config : gen_config) (ctx : gen_ctx) (fi :
   Format.pp_open_vbox fmt 0;
 
   (* Extract the definitions *)
-  extract_definitions meta fmt config ctx;
+  extract_definitions fmt config ctx;
 
   (* Close the box and end the formatting *)
   Format.pp_close_box fmt ();
@@ -1080,7 +1080,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     let ( ^^ ) = Filename.concat in
     if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
     if needs_clauses_module then (
-      assert !Config.split_files (* meta "TODO: Error message META?" *);
+      assert !Config.split_files;
       mkdir_if (dest_dir ^^ crate_name ^^ "Clauses")));
 
   (* Copy the "Primitives" file, if necessary *)
@@ -1230,7 +1230,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              custom_includes = [];
            }
          in
-         extract_file meta opaque_config ctx file_info;
+         extract_file opaque_config ctx file_info;
          (* Return the additional dependencies *)
          [ opaque_imported_module ])
        else []
@@ -1271,7 +1271,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          custom_includes = opaque_types_module;
        }
      in
-     extract_file meta types_config ctx file_info;
+     extract_file types_config ctx file_info;
 
      (* Extract the template clauses *)
      (if needs_clauses_module && !Config.extract_template_decreases_clauses then
@@ -1300,7 +1300,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             custom_includes = [];
           }
         in
-        extract_file meta template_clauses_config ctx file_info);
+        extract_file template_clauses_config ctx file_info);
 
      (* Extract the opaque fun declarations, if needed *)
      let opaque_funs_module =
@@ -1356,7 +1356,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              custom_includes = [ types_module ];
            }
          in
-         extract_file meta opaque_config ctx file_info;
+         extract_file opaque_config ctx file_info;
          (* Return the additional dependencies *)
          [ opaque_imported_module ])
        else []
@@ -1397,7 +1397,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
            [ types_module ] @ opaque_funs_module @ clauses_module;
        }
      in
-     extract_file meta fun_config ctx file_info)
+     extract_file fun_config ctx file_info)
    else
      let gen_config =
        {
@@ -1430,7 +1430,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          custom_includes = [];
        }
      in
-     extract_file meta gen_config ctx file_info);
+     extract_file gen_config ctx file_info);
 
   (* Generate the build file *)
   match !Config.backend with