summaryrefslogtreecommitdiff
path: root/compiler/InterpreterUtils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterUtils.ml')
-rw-r--r--compiler/InterpreterUtils.ml22
1 files changed, 11 insertions, 11 deletions
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index be8400f7..a24cd543 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -20,7 +20,7 @@ let log = Logging.interpreter_log
let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) : eval_ctx =
let nctx = ref None in
let cf ctx =
- cassert (!nctx = None) meta "TODO: error message";
+ sanity_check (!nctx = None) meta;
nctx := Some ctx;
None
in
@@ -62,9 +62,9 @@ let statement_to_string ctx = Print.EvalCtx.statement_to_string ctx "" " "
let statement_to_string_with_tab ctx =
Print.EvalCtx.statement_to_string ctx " " " "
-let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string meta ctx "" " "
-let env_to_string meta ctx env = eval_ctx_to_string meta { ctx with env }
-let abs_to_string meta ctx = Print.EvalCtx.abs_to_string meta ctx "" " "
+let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string ~meta:(Some meta) ctx "" " "
+let env_to_string meta ctx env = eval_ctx_to_string ~meta:(Some meta) { ctx with env }
+let abs_to_string meta ctx = Print.EvalCtx.abs_to_string ~meta:(Some meta) ctx "" " "
let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool =
sv0.sv_id = sv1.sv_id
@@ -85,12 +85,12 @@ let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value =
svalue
let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : symbolic_value =
- cassert (ty_no_regions ty) meta "TODO: error message";
+ sanity_check (ty_no_regions ty) meta;
mk_fresh_symbolic_value meta ty
(** Create a fresh symbolic value *)
let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value =
- cassert (ty_is_rty rty) meta "TODO: error message";
+ sanity_check (ty_is_rty rty) meta;
let ty = Substitute.erase_regions rty in
(* Generate the fresh a symbolic value *)
let value = mk_fresh_symbolic_value meta rty in
@@ -98,7 +98,7 @@ let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value =
{ value; ty }
let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : typed_value =
- cassert (ty_no_regions ty) meta "TODO: error message";
+ sanity_check (ty_no_regions ty) meta;
mk_fresh_symbolic_typed_value meta ty
(** Create a typed value from a symbolic value. *)
@@ -127,7 +127,7 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t)
(** Create a borrows projector from a symbolic value *)
let mk_aproj_borrows_from_symbolic_value (meta : Meta.meta) (proj_regions : RegionId.Set.t)
(svalue : symbolic_value) (proj_ty : ty) : aproj =
- cassert (ty_is_rty proj_ty) meta "TODO: error message";
+ sanity_check (ty_is_rty proj_ty) meta;
if ty_has_regions_in_set proj_regions proj_ty then
AProjBorrows (svalue, proj_ty)
else AIgnoredProjBorrows
@@ -153,7 +153,7 @@ let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id) (asb : abstrac
false))
asb
in
- cassert (!removed = 1) meta "TODO: error message";
+ sanity_check (!removed = 1) meta;
asb
(** We sometimes need to return a value whose type may vary depending on
@@ -499,8 +499,8 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_
(* Generate the type substitution
Note that for now we don't support instantiating the type parameters with
types containing regions. *)
- cassert (List.for_all TypesUtils.ty_no_regions generics.types) meta "TODO: error message";
- cassert (TypesUtils.trait_instance_id_no_regions tr_self) meta "TODO: error message";
+ sanity_check (List.for_all TypesUtils.ty_no_regions generics.types) meta;
+ sanity_check (TypesUtils.trait_instance_id_no_regions tr_self) meta;
let tsubst =
Substitute.make_type_subst_from_vars sg.generics.types generics.types
in