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 | |
parent | c0be587543e96255e50b39145d35589536b44c8d (diff) |
Improve printing of symbolic values in abstractions
-rw-r--r-- | TODO.md | 5 | ||||
-rw-r--r-- | src/Print.ml | 34 | ||||
-rw-r--r-- | src/Values.ml | 6 |
3 files changed, 21 insertions, 24 deletions
@@ -12,8 +12,6 @@ 5. add `mvalue` (meta values) stored in abstractions when ending loans -6. update the printing of mut_borrows and mut_loans ([s@0 <: ...]) and (s@0) - 7. fix the static regions (with projectors) * write an interesting example to study with Jonathan @@ -90,4 +88,5 @@ * invariant: if a symbolic value is present multiple times in the concrete environment, it means it is primitively copyable - + +* update the printing of mut_borrows and mut_loans ([s@0 <: ...]) and (s@0) diff --git a/src/Print.ml b/src/Print.ml index 2b681ec8..8067eae3 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -310,16 +310,14 @@ module Values = struct let rec aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string = match pv with | AProjLoans sv -> - "proj_loans (" - ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv - ^ ")" + "[" ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv ^ "]" | AProjBorrows (sv, rty) -> - "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" - | AEndedProjLoans aproj_opt -> - "ended_proj_loans (" - ^ option_to_string (aproj_to_string fmt) aproj_opt - ^ ")" - | AEndedProjBorrows -> "ended_proj_borrows" + "(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" + | AEndedProjLoans aproj_opt -> ( + match aproj_opt with + | None -> "_" + | Some aproj -> aproj_to_string fmt aproj) + | AEndedProjBorrows -> "_" | AIgnoredProjBorrows -> "_" let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) : @@ -384,10 +382,10 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ ")" | AEndedMutLoan ml -> - "@ended_mut_loan{ given_back=" - ^ typed_avalue_to_string fmt ml.given_back - ^ "; child=" + "@ended_mut_loan{" ^ typed_avalue_to_string fmt ml.child + ^ "; " + ^ typed_avalue_to_string fmt ml.given_back ^ " }" | AEndedSharedLoan (v, av) -> "@ended_shared_loan(" @@ -400,10 +398,10 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ ")" | AEndedIgnoredMutLoan ml -> - "@ended_ignored_mut_loan{ given_back=" - ^ typed_avalue_to_string fmt ml.given_back - ^ "; child: " + "@ended_ignored_mut_loan{ " ^ typed_avalue_to_string fmt ml.child + ^ "; " + ^ typed_avalue_to_string fmt ml.given_back ^ "}" | AIgnoredSharedLoan sl -> "@ignored_shared_loan(" ^ typed_avalue_to_string fmt sl ^ ")" @@ -423,10 +421,10 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ ")" | AEndedIgnoredMutBorrow { given_back_loans_proj; child } -> - "@ended_ignored_mut_borrow{ given_back_loans_proj=" - ^ typed_avalue_to_string fmt given_back_loans_proj - ^ "; child=" + "@ended_ignored_mut_borrow{ " ^ typed_avalue_to_string fmt child + ^ "; " + ^ typed_avalue_to_string fmt given_back_loans_proj ^ ")" | AProjSharedBorrow sb -> "@ignored_shared_borrow(" 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. |