Start working on printing for avalues

3 files changed, 54 insertions, 32 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index be6a3c58..51a22072 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -23,6 +23,8 @@ module type Id = sig
 
   module Set : Set.S with type elt = id
 
+  val set_to_string : Set.t -> string
+
   val id_of_json : Yojson.Basic.t -> (id, string) result
 
   val vector_of_json :
@@ -63,6 +65,10 @@ module IdGen () : Id = struct
     let compare = compare
   end)
 
+  let set_to_string ids =
+    let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
+    "{" ^ String.concat ", " (List.rev ids) ^ "}"
+
   let id_of_json js =
     match js with
     | `Int i -> Ok i
diff --git a/src/Print.ml b/src/Print.ml
index 1ad2f5cb..47350324 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -211,15 +211,8 @@ module Values = struct
 
   let symbolic_proj_comp_to_string (fmt : rtype_formatter)
       (sp : symbolic_proj_comp) : string =
-    let regions =
-      RegionId.Set.fold
-        (fun id ids -> region_id_to_string id :: ids)
-        sp.rset_ended []
-    in
-    let regions = String.concat "," (List.rev regions) in
-    "proj_comp {" ^ regions ^ "} ("
-    ^ symbolic_value_to_string fmt sp.svalue
-    ^ ")"
+    let regions = RegionId.set_to_string sp.rset_ended in
+    "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"
 
   let rec typed_value_to_string (fmt : value_formatter) (v : typed_value) :
       string =
@@ -268,12 +261,23 @@ module Values = struct
       string =
     match lc with
     | SharedLoan (loans, v) ->
-        let loans =
-          BorrowId.Set.fold
-            (fun lid loans -> BorrowId.to_string lid :: loans)
-            loans []
-        in
-        let loans = String.concat ", " (List.rev loans) in
+        let loans = BorrowId.set_to_string loans in
         "@shared_loan({" ^ loans ^ "}, " ^ typed_value_to_string fmt v ^ ")"
     | MutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋"
+
+  let rec abstract_shared_borrows_to_string (fmt : value_formatter)
+      (abs : abstract_shared_borrows) : string =
+    match abs with
+    | AsbSet bs -> BorrowId.set_to_string bs
+    | AsbProjReborrows (sv, rty) ->
+        "{"
+        ^ symbolic_value_id_to_string sv.sv_id
+        ^ " : "
+        ^ ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
+        ^ " <: "
+        ^ ty_to_string (value_to_rtype_formatter fmt) rty
+    | AsbUnion (asb1, asb2) ->
+        abstract_shared_borrows_to_string fmt asb1
+        ^ " U "
+        ^ abstract_shared_borrows_to_string fmt asb2
 end
diff --git a/src/Values.ml b/src/Values.ml
index 0fe928fa..5ebc97b0 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -114,10 +114,10 @@ and assumed_value = Box of typed_value
 
 and typed_value = { value : value; ty : ety }
 
-type abstract_shared_borrow =
-  | AsvSet of BorrowId.Set.t
-  | AsvProjReborrows of symbolic_value * rty
-  | AsvUntion of abstract_shared_borrow * abstract_shared_borrow
+type abstract_shared_borrows =
+  | AsbSet of BorrowId.Set.t
+  | AsbProjReborrows of symbolic_value * rty
+  | AsbUnion of abstract_shared_borrows * abstract_shared_borrows
       (** TODO: explanations *)
 
 (** Abstraction values are used inside of abstractions to properly model
@@ -131,20 +131,10 @@ type avalue =
   | AAdt of aadt_value
   | ATuple of typed_avalue FieldId.vector
   | ABottom
+  | ALoan of aloan_content
+  | ABorrow of aborrow_content
   | AAssumed of aassumed_value
-  | AMutBorrow of BorrowId.id * typed_avalue
-  | ASharedBorrow of BorrowId.id
-  | AMutLoan of BorrowId.id * typed_avalue
-  | ASharedLoan of BorrowId.Set.t * value * typed_avalue
-  | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *)
-  | AEndedSharedLoan of value * typed_avalue
-  | AIgnoredMutLoan of BorrowId.id * typed_avalue
-  | AIgnoredMutBorrow of typed_avalue
-  | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *)
-  | AIgnoredSharedBorrow of abstract_shared_borrow
-  | AIgnoredSharedLoan of abstract_shared_borrow
-  | AProjLoans of symbolic_value
-  | AProjBorrows of symbolic_value * rty
+  | AProj of aproj
 
 and aadt_value = {
   adef_id : TypeDefId.id;
@@ -154,8 +144,30 @@ and aadt_value = {
   afield_values : typed_avalue FieldId.vector;
 }
 
+and aloan_content =
+  | AMutLoan of BorrowId.id * typed_avalue
+  | ASharedLoan of BorrowId.Set.t * value * typed_avalue
+  | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *)
+  | AEndedSharedLoan of value * typed_avalue
+  | AIgnoredMutLoan of BorrowId.id * typed_avalue
+  | AIgnoredSharedLoan of abstract_shared_borrows
+
+(** Note that when a borrow content is ended, it is replaced by Bottom (while
+    we need to track ended loans more precisely, especially because of their
+    children values) *)
+and aborrow_content =
+  | AMutBorrow of BorrowId.id * typed_avalue
+  | ASharedBorrow of BorrowId.id
+  | AIgnoredMutBorrow of typed_avalue
+  | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *)
+  | AIgnoredSharedBorrow of abstract_shared_borrows
+
 and aassumed_value = ABox of typed_avalue
 
+and aproj =
+  | AProjLoans of symbolic_value
+  | AProjBorrows of symbolic_value * rty
+
 and typed_avalue = { avalue : avalue; aty : rty }
 
 type abs = {