diff options
Diffstat (limited to 'compiler/PureMicroPasses.ml')
| -rw-r--r-- | compiler/PureMicroPasses.ml | 22 |
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; |