From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/PureMicroPasses.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index e58b318a..95c74a7b 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -222,7 +222,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   (* Register a variable for constraints propagation - used when an variable is
    * introduced (left-hand side of a left binding) *)
   let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
-    sanity_check (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta;
+    sanity_check __FILE__ __LINE__ (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta;
     match v.basename with
     | None -> ctx
     | Some name ->
@@ -756,7 +756,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
             else if variant_id = result_fail_id then
               (* Fail case *)
               self#visit_expression env rv.e
-            else craise def.meta "Unexpected"
+            else craise __FILE__ __LINE__ def.meta "Unexpected"
         | App _ ->
             (* This might be the tuple case *)
             if not monadic then
@@ -1198,13 +1198,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Opaque -> craise def.meta "Unreachable"
+                  | Enum _ | Opaque -> craise __FILE__ __LINE__ def.meta "Unreachable"
                   | Struct fields -> fields
                 in
                 let num_fields = List.length fields in
                 (* In order to simplify, there must be as many arguments as
                  * there are fields *)
-                sanity_check (num_fields > 0) def.meta;
+                sanity_check __FILE__ __LINE__ (num_fields > 0) def.meta;
                 if num_fields = List.length args then
                   (* We now need to check that all the arguments are of the form:
                    * [x.field] for some variable [x], and where the projection
@@ -1240,7 +1240,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     if List.for_all (fun (_, y) -> y = x) end_args then (
                       (* We can substitute *)
                       (* Sanity check: all types correct *)
-                      sanity_check
+                      sanity_check __FILE__ __LINE__
                         (List.for_all
                            (fun (generics1, _) -> generics1 = generics)
                            args)
@@ -1399,7 +1399,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               { fwd_info; effect_info = loop_fwd_effect_info; ignore_output }
             in
-            cassert
+            cassert __FILE__ __LINE__
               (fun_sig_info_is_wf loop_fwd_sig_info)
               def.meta "TODO: error message";
 
@@ -1441,7 +1441,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               (* Introduce the forward input state *)
               let fwd_state_var, fwd_state_lvs =
-                cassert
+                cassert __FILE__ __LINE__
                   (loop_fwd_effect_info.stateful
                   = Option.is_some loop.input_state)
                   def.meta "TODO: error message";
@@ -1577,7 +1577,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     let arg, args = Collections.List.pop args in
                     mk_apps def.meta arg args
                 | BoxFree ->
-                    sanity_check (args = []) def.meta;
+                    sanity_check __FILE__ __LINE__ (args = []) def.meta;
                     mk_unit_rvalue
                 | SliceIndexShared | SliceIndexMut | ArrayIndexShared
                 | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
@@ -1772,7 +1772,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               (* TODO: this information should be computed in SymbolicToPure and
                * store in an enum ("monadic" should be an enum, not a bool). *)
               let re_ty = Option.get (opt_destruct_result def.meta re.ty) in
-              sanity_check (lv.ty = re_ty) def.meta;
+              sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.meta;
               let err_vid = fresh_id () in
               let err_var : var =
                 {
@@ -2025,7 +2025,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
         ^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
         ^ "\n"));
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
-    sanity_check (Option.is_some decl.loop_id) decl.meta;
+    sanity_check __FILE__ __LINE__ (Option.is_some decl.loop_id) decl.meta;
 
     let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
 
@@ -2177,7 +2177,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
           in
 
           let fwd_info = { fwd_info; effect_info; ignore_output } in
-          sanity_check (fun_sig_info_is_wf fwd_info) decl.meta;
+          sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf fwd_info) decl.meta;
           let signature =
             {
               generics;
-- 
cgit v1.2.3