summaryrefslogtreecommitdiff
path: root/compiler/InterpreterBorrows.mli
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterBorrows.mli')
-rw-r--r--compiler/InterpreterBorrows.mli94
1 files changed, 68 insertions, 26 deletions
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 56df9344..cf14e94b 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -138,29 +138,50 @@ val convert_value_to_abstractions :
*)
type merge_duplicates_funcs = {
merge_amut_borrows :
- borrow_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+ borrow_id ->
+ rty ->
+ proj_marker ->
+ typed_avalue ->
+ rty ->
+ proj_marker ->
+ typed_avalue ->
+ typed_avalue;
(** Parameters:
- [id]
- [ty0]
+ - [pm0]
- [child0]
- [ty1]
+ - [pm1]
- [child1]
The children should be [AIgnored].
*)
- merge_ashared_borrows : borrow_id -> rty -> rty -> typed_avalue;
+ merge_ashared_borrows :
+ borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue;
(** Parameters:
- [id]
- [ty0]
+ - [pm0]
- [ty1]
+ - [pm1]
*)
merge_amut_loans :
- loan_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+ loan_id ->
+ rty ->
+ proj_marker ->
+ typed_avalue ->
+ rty ->
+ proj_marker ->
+ typed_avalue ->
+ typed_avalue;
(** Parameters:
- [id]
- [ty0]
+ - [pm0]
- [child0]
- [ty1]
+ - [pm1]
- [child1]
The children should be [AIgnored].
@@ -168,18 +189,22 @@ type merge_duplicates_funcs = {
merge_ashared_loans :
loan_id_set ->
rty ->
+ proj_marker ->
typed_value ->
typed_avalue ->
rty ->
+ proj_marker ->
typed_value ->
typed_avalue ->
typed_avalue;
(** Parameters:
- [ids]
- [ty0]
+ - [pm0]
- [sv0]
- [child0]
- [ty1]
+ - [pm1]
- [sv1]
- [child1]
*)
@@ -187,24 +212,36 @@ type merge_duplicates_funcs = {
(** Merge an abstraction into another abstraction.
- We insert the result of the merge in place of the second abstraction (and in
+ We insert the result of the merge in place of the first abstraction (and in
particular, we don't simply push the merged abstraction at the end of the
environment: this helps preserving the structure of the environment, when
computing loop fixed points for instance).
- When we merge two abstractions together, we remove the loans/borrows
- which appear in one and whose associated loans/borrows appear in the
- other. For instance:
+ When we merge two abstractions together, we remove the loans which appear
+ in the *left* abstraction and whose corresponding borrows appear in the
+ **right** abstraction.
+ For instance:
{[
abs'0 { mut_borrow l0, mut_loan l1 } // Rem.: mut_loan l1
abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1
~~>
- abs'01 { mut_borrow l0, mut_borrow l2 }
+ abs'2 { mut_borrow l0, mut_borrow l2 }
+ ]}
+
+ We also simplify the markers, when the same value appears in both abstractions
+ but with different markers. For instance:
+ {[
+ abs'0 { |mut_borrow l0|, mut_loan l1 }
+ abs'1 { ︙mut_borrow l0︙, mut_borrow l1 }
+
+ ~~>
+
+ abs'2 { mut_borrow l0 }
]}
- Also, we merge all their regions together. For instance, if [abs'0] projects
+ Finally, we merge all their regions together. For instance, if [abs'0] projects
region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0]
(the one with the smallest index in practice) and substitute [r1] with [r0]
in the whole context.
@@ -212,22 +249,10 @@ type merge_duplicates_funcs = {
Parameters:
- [kind]
- [can_end]
- - [merge_funs]: Those functions are used to merge borrows/loans with the
- *same ids*. For instance, when performing environment joins we may introduce
- abstractions which both contain loans/borrows with the same ids. When we
- later merge those abstractions together, we need to call a merge function
- to reconcile the borrows/loans. For instance, if both abstractions contain
- the same shared loan [l0], we will call {!merge_ashared_borrows} to derive
- a shared value for the merged shared loans.
-
- For instance, this happens for the following abstractions:
- {[
- abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
- abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
- ]}
- If you want to forbid this, provide [None]. In that case, [merge_into_abstraction]
- actually simply performs some sort of a union.
-
+ - [merge_funs]: those functions are used to merge borrows/loans with the
+ *same ids* but different markers. This is necessary when doing a collapse
+ (see the computation of joins).
+ If [merge_funs] are not provided, we check that there are no markers.
- [ctx]
- [abs_id0]
- [abs_id1]
@@ -235,7 +260,7 @@ type merge_duplicates_funcs = {
We return the updated context as well as the id of the new abstraction which
results from the merge.
*)
-val merge_into_abstraction :
+val merge_into_first_abstraction :
Meta.span ->
abs_kind ->
bool ->
@@ -244,3 +269,20 @@ val merge_into_abstraction :
AbstractionId.id ->
AbstractionId.id ->
eval_ctx * AbstractionId.id
+
+(** Reorder the loans and borrows in the fresh abstractions.
+
+ We do this in order to enforce some structure in the environments: this
+ allows us to find fixed-points. Note that this function needs to be
+ called typically after we merge abstractions together (see {!reduce_ctx}
+ and {!collapse_ctx} for instance).
+
+ Inputs:
+ - [span]
+ - [allow_markers]: disables some sanity checks (which check that projection
+ markers don't appear).
+ - [old_abs_ids]
+ - [eval_ctx]
+ *)
+val reorder_loans_borrows_in_fresh_abs :
+ Meta.span -> bool -> AbstractionId.Set.t -> eval_ctx -> eval_ctx