diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterUtils.ml | 41 |
1 files changed, 25 insertions, 16 deletions
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index a24cd543..9ffab771 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -17,7 +17,8 @@ let log = Logging.interpreter_log (** Auxiliary function - call a function which requires a continuation, and return the let context given to the continuation *) -let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) : eval_ctx = +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 = sanity_check (!nctx = None) meta; @@ -62,9 +63,14 @@ 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:(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 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 @@ -77,19 +83,20 @@ let mk_place_from_var_id (var_id : VarId.id) : place = { var_id; projection = [] } (** Create a fresh symbolic value *) -let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value = +let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value = (* Sanity check *) sanity_check (ty_is_rty ty) meta; let sv_id = fresh_symbolic_value_id () in let svalue = { sv_id; sv_ty = ty } in svalue -let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : symbolic_value = +let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : + symbolic_value = 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 = +let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value = sanity_check (ty_is_rty rty) meta; let ty = Substitute.erase_regions rty in (* Generate the fresh a symbolic value *) @@ -97,7 +104,8 @@ let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value = let value = VSymbolic value in { value; ty } -let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : typed_value = +let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta) + (ty : ty) : typed_value = sanity_check (ty_no_regions ty) meta; mk_fresh_symbolic_typed_value meta ty @@ -125,8 +133,9 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t) else { value = AIgnored; ty = svalue.sv_ty } (** 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 = +let mk_aproj_borrows_from_symbolic_value (meta : Meta.meta) + (proj_regions : RegionId.Set.t) (svalue : symbolic_value) (proj_ty : ty) : + aproj = sanity_check (ty_is_rty proj_ty) meta; if ty_has_regions_in_set proj_regions proj_ty then AProjBorrows (svalue, proj_ty) @@ -141,8 +150,8 @@ let borrow_in_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) : bool = List.exists (borrow_is_asb bid) asb (** TODO: move *) -let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id) (asb : abstract_shared_borrows) : - abstract_shared_borrows = +let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id) + (asb : abstract_shared_borrows) : abstract_shared_borrows = let removed = ref 0 in let asb = List.filter @@ -460,8 +469,8 @@ let initialize_eval_ctx (meta : Meta.meta) (ctx : decls_ctx) region ids. This is mostly used in preparation of function calls (when evaluating in symbolic mode). *) -let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_args) - (tr_self : trait_instance_id) (sg : fun_sig) +let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) + (generics : generic_args) (tr_self : trait_instance_id) (sg : fun_sig) (regions_hierarchy : region_var_groups) : inst_fun_sig = log#ldebug (lazy @@ -514,8 +523,8 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_ in (* Substitute the signature *) let inst_sig = - AssociatedTypes.ctx_subst_norm_signature meta ctx asubst rsubst tsubst cgsubst - tr_subst tr_self sg regions_hierarchy + AssociatedTypes.ctx_subst_norm_signature meta ctx asubst rsubst tsubst + cgsubst tr_subst tr_self sg regions_hierarchy in (* Return *) inst_sig |