Add some error messages

8 files changed, 29 insertions, 25 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 083a38d1..27425a51 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -428,12 +428,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
   | TraitRef trait_ref ->
       (* The trait instance id necessarily refers to a local sub-clause. We
          can't project over it and can only peel off the [TraitRef] wrapper *)
-      cassert_opt_meta __FILE__ __LINE__
+      sanity_check_opt_meta __FILE__ __LINE__
         (trait_instance_id_is_local_clause trait_ref.trait_id)
-        ctx.meta "Trait instance id is not a local sub-clause";
-      cassert_opt_meta __FILE__ __LINE__
+        ctx.meta;
+      sanity_check_opt_meta __FILE__ __LINE__
         (trait_ref.generics = empty_generic_args)
-        ctx.meta "TODO: error message";
+        ctx.meta;
       (trait_ref.trait_id, None)
   | FnPointer ty ->
       let ty = norm_ctx_normalize_ty ctx ty in
@@ -482,9 +482,9 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) :
         (lazy
           ("norm_ctx_normalize_trait_ref: normalized to: "
           ^ trait_ref_to_string ctx trait_ref));
-      cassert_opt_meta __FILE__ __LINE__
+      sanity_check_opt_meta __FILE__ __LINE__
         (generics = empty_generic_args)
-        ctx.meta "TODO: error message";
+        ctx.meta;
       trait_ref
 
 (* Not sure this one is really necessary *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index d61ba410..48a1cce6 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -340,7 +340,9 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
                      value_as_symbolic meta cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
-      | CFnPtr _ -> craise __FILE__ __LINE__ meta "TODO: error message")
+      | CFnPtr _ ->
+          craise __FILE__ __LINE__ meta
+            "Function pointers are not supported yet")
   | Copy p ->
       (* Access the value *)
       let access = Read in
@@ -523,7 +525,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
-    exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "TODO: error message";
+    exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
+      "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
     exec_assert __FILE__ __LINE__
       (ty_is_primitively_copyable v1.ty)
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 6d814c5c..bd271ff4 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -243,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
                 (not
                    (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
                       bv.value))
-                M.meta "TODO: error message";
+                M.meta "The join of nested borrows is not supported yet";
               let bid, bv =
                 M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
               in
@@ -268,7 +268,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
               let sv = match_rec sv0 sv1 in
               cassert __FILE__ __LINE__
                 (not (value_has_borrows sv.value))
-                M.meta "TODO: error message";
+                M.meta "The join of nested borrows is not supported yet";
               let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in
               VSharedLoan (ids, sv)
           | VMutLoan id0, VMutLoan id1 ->
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index d7c20ae0..8b6eeb6c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -502,7 +502,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
     (ctx : eval_ctx) (regions : RegionId.Set.t)
     (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
     eval_ctx * typed_avalue =
-  cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message";
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta;
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 518d8bdd..d0c243bb 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -411,7 +411,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
               "Unreachable: improper variant id for result type"
       | TError ->
           cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta
-            "TODO: error message";
+            "Ill-formed error value";
           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"
@@ -422,7 +422,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then (
             cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta
-              "TODO: error message";
+              "Ill-formed full value";
             "@Fuel::Zero")
           else if variant_id = fuel_succ_id then
             match field_values with
@@ -435,7 +435,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
               "Unreachable: improper variant id for fuel type"
       | TArray | TSlice | TStr ->
           cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta
-            "TODO: error message";
+            "Ill-formed value";
           let field_values =
             List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
           in
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 91ee16dc..12b3387a 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1402,9 +1402,9 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               { fwd_info; effect_info = loop_fwd_effect_info; ignore_output }
             in
-            cassert __FILE__ __LINE__
+            sanity_check __FILE__ __LINE__
               (fun_sig_info_is_wf loop_fwd_sig_info)
-              def.meta "TODO: error message";
+              def.meta;
 
             let inputs_tys =
               let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
@@ -1444,10 +1444,10 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               (* Introduce the forward input state *)
               let fwd_state_var, fwd_state_lvs =
-                cassert __FILE__ __LINE__
+                sanity_check __FILE__ __LINE__
                   (loop_fwd_effect_info.stateful
                   = Option.is_some loop.input_state)
-                  def.meta "TODO: error message";
+                  def.meta;
                 match loop.input_state with
                 | None -> ([], [])
                 | Some input_state ->
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b9eebc25..177d8c24 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -77,7 +77,7 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta)
       ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics
   | TTuple ->
       cassert __FILE__ __LINE__ (generics.regions = []) meta
-        "Regions should be empty TODO: error message";
+        "Tuples don't have region parameters";
       generics.types
   | TAssumed aty -> (
       match aty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ccb4f585..4830f65a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -458,9 +458,7 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty =
       match type_id with
       | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
       | T.TTuple ->
-          cassert __FILE__ __LINE__
-            (generics.const_generics = [])
-            meta "TODO: error message";
+          sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
           mk_simpl_tuple_ty generics.types
       | T.TAssumed aty -> (
           match aty with
@@ -486,7 +484,8 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty =
   | TTraitType (trait_ref, type_name) ->
       let trait_ref = translate_strait_ref meta trait_ref in
       TTraitType (trait_ref, type_name)
-  | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+  | TArrow _ ->
+      craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
 
 and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) :
     generic_args =
@@ -659,7 +658,8 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos)
   | TTraitType (trait_ref, type_name) ->
       let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
       TTraitType (trait_ref, type_name)
-  | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+  | TArrow _ ->
+      craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
 
 and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos)
     (generics : T.generic_args) : generic_args =
@@ -768,7 +768,8 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
         let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
         Some (TTraitType (trait_ref, type_name))
       else None
-  | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+  | TArrow _ ->
+      craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)