diff options
author | Son Ho | 2022-12-02 10:02:32 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | 533d6d93c63b30a49475d5e09d3de08047b297f7 (patch) | |
tree | bc7194ec4e220ff566b9a81cf8bce51381e28659 /compiler/InterpreterBorrows.mli | |
parent | 175949360a0208d826be89463c916fbaaa7fa8a4 (diff) |
Update the comments in Values and make minor modifications
Diffstat (limited to '')
-rw-r--r-- | compiler/InterpreterBorrows.mli | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 6a8fb87c..a2a1cfde 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -215,14 +215,23 @@ type merge_duplicates_funcs = { abs'01 { mut_borrow l0, mut_borrow l2 } ]} + Also, 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. + Parameters: - [kind] - [can_end] - - [merge_funs]: in the case it can happen that a loan or a borrow appears in - both abstractions, we use those functions to merge the different occurrences - (such things can happen when joining environments: we might temporarily - duplicate borrows during the join, before merging those borrows together). - For instance, this happens for the following abstractions is forbidden: + - [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 ! |