Merge value and avalue

2 files changed, 107 insertions, 92 deletions

diff --git a/src/Print.ml b/src/Print.ml
index 3e769796..be6f4186 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -199,9 +199,24 @@ module Values = struct
     let regions = V.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 : V.typed_value) :
-      string =
-    let ety_fmt = value_to_etype_formatter fmt in
+  type ('r, 'sv, 'bc, 'lc) gen_value_formatter = {
+    r_to_string : 'r -> string;
+    sv_to_string : 'sv -> string;
+    bc_to_string : 'bc -> string;
+    lc_to_string : 'lc -> string;
+  }
+  (** Auxiliary record: we use it to factorize value formatting *)
+
+  let rec g_typed_value_to_string (fmt : value_formatter)
+      (gfmt : ('r, 'sv, 'bc, 'lc) gen_value_formatter)
+      (v : ('r, 'sv, 'bc, 'lc) V.g_typed_value) : string =
+    let ty_fmt : 'r PT.type_formatter =
+      {
+        PT.r_to_string = gfmt.r_to_string;
+        PT.type_var_id_to_string = fmt.type_var_id_to_string;
+        PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      }
+    in
     match v.value with
     | Concrete cv -> constant_value_to_string cv
     | Adt av ->
@@ -216,7 +231,7 @@ module Values = struct
           | None -> fmt.type_def_id_to_string def_id
         in
         let field_values =
-          List.map (typed_value_to_string fmt) av.field_values
+          List.map (g_typed_value_to_string fmt gfmt) av.field_values
         in
         if List.length field_values > 0 then
           match fmt.adt_field_names def_id av.V.variant_id with
@@ -235,16 +250,30 @@ module Values = struct
         else adt_ident
     | Tuple values ->
         let values =
-          String.concat ", " (List.map (typed_value_to_string fmt) values)
+          String.concat ", "
+            (List.map (g_typed_value_to_string fmt gfmt) values)
         in
         "(" ^ values ^ ")"
-    | Bottom -> "⊥ : " ^ PT.ety_to_string ety_fmt v.ty
+    | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
     | Assumed av -> (
-        match av with Box bv -> "@Box(" ^ typed_value_to_string fmt bv ^ ")")
-    | Borrow bc -> borrow_content_to_string fmt bc
-    | Loan lc -> loan_content_to_string fmt lc
-    | Symbolic sp ->
-        symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) sp
+        match av with
+        | Box bv -> "@Box(" ^ g_typed_value_to_string fmt gfmt bv ^ ")")
+    | Borrow bc -> gfmt.bc_to_string bc
+    | Loan lc -> gfmt.lc_to_string lc
+    | Symbolic s -> gfmt.sv_to_string s
+
+  let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) :
+      string =
+    let gfmt =
+      {
+        r_to_string = PT.erased_region_to_string;
+        sv_to_string =
+          symbolic_proj_comp_to_string (value_to_rtype_formatter fmt);
+        bc_to_string = borrow_content_to_string fmt;
+        lc_to_string = loan_content_to_string fmt;
+      }
+    in
+    g_typed_value_to_string fmt gfmt v
 
   and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
       string =
@@ -284,36 +313,26 @@ module Values = struct
         ^ " U "
         ^ abstract_shared_borrows_to_string fmt asb2
 
+  let 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
+        ^ ")"
+    | AProjBorrows (sv, rty) ->
+        "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
+
   let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
       string =
-    let rty_fmt = value_to_rtype_formatter fmt in
-    match v.avalue with
-    | AConcrete cv -> constant_value_to_string cv
-    | AAdt av ->
-        let adt_ident =
-          match av.avariant_id with
-          | Some vid -> fmt.adt_variant_to_string av.adef_id vid
-          | None -> fmt.type_def_id_to_string av.adef_id
-        in
-        let field_values = av.afield_values in
-        if List.length field_values > 0 then
-          let field_values =
-            String.concat " "
-              (List.map (typed_avalue_to_string fmt) field_values)
-          in
-          adt_ident ^ " " ^ field_values
-        else adt_ident
-    | ATuple values ->
-        let values =
-          String.concat ", " (List.map (typed_avalue_to_string fmt) values)
-        in
-        "(" ^ values ^ ")"
-    | ABottom -> "⊥ : " ^ PT.rty_to_string rty_fmt v.aty
-    | ALoan lc -> aloan_content_to_string fmt lc
-    | ABorrow bc -> aborrow_content_to_string fmt bc
-    | AAssumed av -> (
-        match av with ABox bv -> "@Box(" ^ typed_avalue_to_string fmt bv ^ ")")
-    | AProj pv -> aproj_to_string fmt pv
+    let gfmt =
+      {
+        r_to_string = PT.region_to_string fmt.r_to_string;
+        sv_to_string = aproj_to_string fmt;
+        bc_to_string = aborrow_content_to_string fmt;
+        lc_to_string = aloan_content_to_string fmt;
+      }
+    in
+    g_typed_value_to_string fmt gfmt v
 
   and aloan_content_to_string (fmt : value_formatter) (lc : V.aloan_content) :
       string =
@@ -371,15 +390,6 @@ module Values = struct
         ^ abstract_shared_borrows_to_string fmt sb
         ^ ")"
 
-  and 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
-        ^ ")"
-    | AProjBorrows (sv, rty) ->
-        "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
-
   let abs_to_string (fmt : value_formatter) (abs : V.abs) : string =
     let avs =
       List.map (fun av -> "  " ^ typed_avalue_to_string fmt av) abs.avalues
diff --git a/src/Values.ml b/src/Values.ml
index f1fdfd6c..2ee2bdf5 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -69,51 +69,68 @@ type symbolic_proj_comp = {
 
     Parameterized by:
     - 'ty: type
+    - 'sv: symbolic value
     - 'bc: borrow content
     - 'lc: loan content
 
     Can be specialized for "regular" values or values in abstractions *)
-type ('ty, 'bc, 'lc) g_value =
+type ('r, 'sv, 'bc, 'lc) g_value =
   | Concrete of constant_value  (** Concrete (non-symbolic) value *)
-  | Adt of ('ty, 'bc, 'lc) g_adt_value  (** Enumerations and structures *)
-  | Tuple of ('ty, 'bc, 'lc) g_typed_value list
+  | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value  (** Enumerations and structures *)
+  | Tuple of ('r, 'sv, 'bc, 'lc) g_typed_value list
       (** Tuple - note that units are encoded as 0-tuples
           TODO: merge with Adt?
        *)
   | Bottom  (** No value (uninitialized or moved value) *)
-  | Assumed of ('ty, 'bc, 'lc) g_assumed_value
+  | Assumed of ('r, 'sv, 'bc, 'lc) g_assumed_value
       (** Value of an abstract type (Box, Vec, Cell...) *)
   | Borrow of 'bc  (** A borrowed value *)
   | Loan of 'lc  (** A loaned value *)
-  | Symbolic of symbolic_proj_comp  (** Unknown value *)
+  | Symbolic of 'sv  (** Unknown value *)
 [@@deriving show]
 
-and ('ty, 'bc, 'lc) g_adt_value = {
+and ('r, 'sv, 'bc, 'lc) g_adt_value = {
   variant_id : VariantId.id option;
-  field_values : ('ty, 'bc, 'lc) g_typed_value list;
+  field_values : ('r, 'sv, 'bc, 'lc) g_typed_value list;
 }
 [@@deriving show]
 (** "Generic" ADT value (not "GADT" value) *)
 
-and ('ty, 'bc, 'lc) g_assumed_value = Box of ('ty, 'bc, 'lc) g_typed_value
+and ('r, 'sv, 'bc, 'lc) g_assumed_value =
+  | Box of ('r, 'sv, 'bc, 'lc) g_typed_value
 [@@deriving show]
 
-and ('ty, 'bc, 'lc) g_typed_value = {
-  value : ('ty, 'bc, 'lc) g_value;
-  ty : 'ty;
+and ('r, 'sv, 'bc, 'lc) g_typed_value = {
+  value : ('r, 'sv, 'bc, 'lc) g_value;
+  ty : 'r ty;
 }
 [@@deriving show]
 
-type value = (ety, borrow_content, loan_content) g_value [@@deriving show]
+type value =
+  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value
+[@@deriving show]
+(** "Regular" value *)
 
-and adt_value = (ety, borrow_content, loan_content) g_adt_value
+and adt_value =
+  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value
 [@@deriving show]
 
-and assumed_value = (ety, borrow_content, loan_content) g_assumed_value
+and assumed_value =
+  ( erased_region,
+    symbolic_proj_comp,
+    borrow_content,
+    loan_content )
+  g_assumed_value
 [@@deriving show]
 
-and typed_value = (ety, borrow_content, loan_content) g_typed_value
+and typed_value =
+  ( erased_region,
+    symbolic_proj_comp,
+    borrow_content,
+    loan_content )
+  g_typed_value
 [@@deriving show]
+(** "Regular" typed value (we map variables to typed values) *)
 
 and borrow_content =
   | SharedBorrow of BorrowId.id  (** A shared value *)
@@ -143,33 +160,30 @@ type abstract_shared_borrows =
       (** TODO: explanations *)
 [@@deriving show]
 
+type aproj =
+  | AProjLoans of symbolic_value
+  | AProjBorrows of symbolic_value * rty
+[@@deriving show]
+
+type avalue =
+  (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_value
 (** Abstraction values are used inside of abstractions to properly model
     borrowing relations introduced by function calls.
 
     When calling a function, we lose information about the borrow graph:
     part of it is thus "abstracted" away.
 *)
-type avalue =
-  | AConcrete of constant_value
-  | AAdt of aadt_value
-  | ATuple of typed_avalue list
-  | ABottom
-  | ALoan of aloan_content
-  | ABorrow of aborrow_content
-  | AAssumed of aassumed_value
-  | AProj of aproj
-[@@deriving show]
-(*  TODO: merge with value *)
-
-and aadt_value = {
-  adef_id : TypeDefId.id;
-  avariant_id : VariantId.id option;
-  aregions : erased_region list;
-  atypes : rty list;
-  afield_values : typed_avalue list;
-}
+
+and aadt_value =
+  (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_adt_value
+
+and aassumed_value =
+  (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_assumed_value
+[@@deriving show]
+
+and typed_avalue =
+  (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_typed_value
 [@@deriving show]
-(* TODO: merge with adt_value *)
 
 and aloan_content =
   | AMutLoan of BorrowId.id * typed_avalue
@@ -191,15 +205,6 @@ and aborrow_content =
   | AIgnoredSharedBorrow of abstract_shared_borrows
 [@@deriving show]
 
-and aassumed_value = ABox of typed_avalue [@@deriving show]
-
-and aproj =
-  | AProjLoans of symbolic_value
-  | AProjBorrows of symbolic_value * rty
-[@@deriving show]
-
-and typed_avalue = { avalue : avalue; aty : rty } [@@deriving show]
-
 type abs = {
   abs_id : AbstractionId.id;
   parents : AbstractionId.set_t;  (** The parent abstractions *)