module T = Types module V = Values module E = Expressions module C = Contexts module Subst = Substitute module L = Logging open InterpreterBorrowsCore (** Auxiliary function. Apply a proj_borrows on a shared borrow. Note that when projecting over shared values, we generate {!type:V.abstract_shared_borrows}, not {!type:V.avalue}s. Parameters: [regions] [ancestor_regions] [see] [original_sv_ty] *) val apply_proj_loans_on_symbolic_expansion : T.RegionId.Set.t -> T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue (** Convert a symbolic expansion *which is not a borrow* to a value *) val symbolic_expansion_non_borrow_to_value : V.symbolic_value -> V.symbolic_expansion -> V.typed_value (** Convert a symbolic expansion *which is not a shared borrow* to a value. If the expansion is a mutable reference expansion, it converts it to a borrow. This function is meant to be used when reducing projectors over borrows, during a symbolic expansion. *) val symbolic_expansion_non_shared_borrow_to_value : V.symbolic_value -> V.symbolic_expansion -> V.typed_value (** Auxiliary function to prepare reborrowing operations (used when applying projectors). Returns two functions: - a function to generate fresh re-borrow ids, and register the reborrows - a function to apply the reborrows in a context Those functions are of course stateful. Parameters: - [config] - [allow_reborrows] *) val prepare_reborrows : C.config -> bool -> (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) (** Apply (and reduce) a projector over borrows to an avalue. We use this for instance to spread the borrows present in the inputs of a function into the regions introduced for this function. For instance: {[ fn f<'a, 'b, T>(x: &'a T, y: &'b T) ]} If we call `f` with `x -> shared_borrow l0` and `y -> shared_borrow l1`, then for the region introduced for `'a` we need to project the value for `x` to a shared aborrow, and we need to ignore the borrow in `y`, because it belongs to the other region. Parameters: - [check_symbolic_no_ended]: controls whether we check or not whether symbolic values don't contain already ended regions. This check is activated when applying projectors upon calling a function (because we need to check that function arguments don't contain ⊥), but deactivated when expanding symbolic values: {[ fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32); let p = f(&mut x, &mut y); // p -> @s0 assert(x == ...); // end 'a let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions ]} - [ctx] - [fresh_reborrow]: a function which generates fresh ids for reborrows, and registers the reborrows (to be applied later to the context). When applying projections on shared values, we need to apply reborrows. This is a bit annoying because, with the way we compute the projection on borrows, we can't update the context immediately. Instead, we remember the list of borrows we have to insert in the context *afterwards*. See {!prepare_reborrows} - [regions]: the regions to project - [ancestor_regions] - [v]: the value on which to apply the projection - [ty]: the projection type (is used to map borrows to regions, or in other words to interpret the borrows as belonging to some regions). Remember that [v] doesn't contain region information. For instance, if we have: [v <: ty] where: - [v = mut_borrow l ...] - [ty = Ref (r, ...)] then we interpret the borrow [l] as belonging to region [r] *) val apply_proj_borrows : bool -> C.eval_ctx -> (V.BorrowId.id -> V.BorrowId.id) -> T.RegionId.Set.t -> T.RegionId.Set.t -> V.typed_value -> T.rty -> V.typed_avalue (** Parameters: - [config] - [ctx] - [regions]: the regions to project - [ancestors_regions] - [v]: the value on which to apply the projection - [ty]: the type (with regions) to use for the projection *) val apply_proj_borrows_on_input_value : C.config -> C.eval_ctx -> T.RegionId.Set.t -> T.RegionId.Set.t -> V.typed_value -> T.rty -> C.eval_ctx * V.typed_avalue