summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PureMicroPasses.ml')
-rw-r--r--compiler/PureMicroPasses.ml22
1 files changed, 11 insertions, 11 deletions
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;