summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-14 23:12:48 +0100
committerSon Ho2022-01-14 23:12:48 +0100
commit49c51d173e9d8ea2cb74f04f8224e864db065f0d (patch)
treef8e26e66306b676c67ef7b2acf3cd047446ceceb /src
parentc0be587543e96255e50b39145d35589536b44c8d (diff)
Improve printing of symbolic values in abstractions
Diffstat (limited to 'src')
-rw-r--r--src/Print.ml34
-rw-r--r--src/Values.ml6
2 files changed, 19 insertions, 21 deletions
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.