diff options
| author | Son Ho | 2022-01-14 23:12:48 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-14 23:12:48 +0100 |
| commit | 49c51d173e9d8ea2cb74f04f8224e864db065f0d (patch) | |
| tree | f8e26e66306b676c67ef7b2acf3cd047446ceceb /src/Values.ml | |
| parent | c0be587543e96255e50b39145d35589536b44c8d (diff) | |
Improve printing of symbolic values in abstractions
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Values.ml b/src/Values.ml index 7ba16ae2..31f47709 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -339,7 +339,7 @@ and aloan_content = px -> shared_loan l0 ``` *) - | AEndedMutLoan of { given_back : typed_avalue; child : typed_avalue } + | AEndedMutLoan of { child : typed_avalue; given_back : typed_avalue } (** An ended mutable loan in an abstraction. We need it because abstractions must keep track of the values we gave back to them, so that we can correctly instantiate @@ -394,7 +394,7 @@ and aloan_content = > x -> mut_borrow l0 (mut_borrow l1 @s1) ``` *) - | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue } + | AEndedIgnoredMutLoan of { child : typed_avalue; given_back : typed_avalue } (** Similar to [AEndedMutLoan], for ignored loans *) | AIgnoredSharedLoan of typed_avalue (** An ignored shared loan. @@ -536,8 +536,8 @@ and aborrow_content = when generating the pure translation. *) | AEndedIgnoredMutBorrow of { - given_back_loans_proj : typed_avalue; child : typed_avalue; + given_back_loans_proj : typed_avalue; } (** See the explanations for [AIgnoredMutBorrow] *) | AProjSharedBorrow of abstract_shared_borrows (** A projected shared borrow. |