From 49c51d173e9d8ea2cb74f04f8224e864db065f0d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 14 Jan 2022 23:12:48 +0100
Subject: Improve printing of symbolic values in abstractions

---
 TODO.md       |  5 ++---
 src/Print.ml  | 34 ++++++++++++++++------------------
 src/Values.ml |  6 +++---
 3 files changed, 21 insertions(+), 24 deletions(-)

diff --git a/TODO.md b/TODO.md
index 4f4df18c..9b0e0b64 100644
--- a/TODO.md
+++ b/TODO.md
@@ -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.
-- 
cgit v1.2.3