Remove g_value, g_typed_value, etc. to make values and abstract values

distinct

1 files changed, 90 insertions, 75 deletions

diff --git a/src/Values.ml b/src/Values.ml
index 633b2157..764612af 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -63,79 +63,54 @@ type symbolic_proj_comp = {
     
     "Complementary" stands for the fact that it is a projector over all the
     regions *but* the ones which are listed in the projector.
- *)
+*)
 
-(** Polymorphic iter visitor *)
-class ['self] iter_'r_ty_base =
+(** Ancestor for iter visitor for [typed_value] *)
+class ['self] iter_typed_value_base =
   object (self : 'self)
-    method visit_ty : 'env 'r. ('env -> 'r -> unit) -> 'env -> 'r ty -> unit =
-      fun _visit_'r _env _ty -> ()
-  end
+    inherit [_] VisitorsRuntime.iter
 
-(** A generic, untyped value, used in the environments.
+    method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
 
-    Parameterized by:
-    - 'ty: type
-    - 'sv: symbolic value
-    - 'bc: borrow content
-    - 'lc: loan content
+    method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
 
-    Can be specialized for "regular" values or values in abstractions.
+    method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit =
+      fun _ _ -> ()
 
-    TODO: unfactorize value and avalue. Making them instanciations of `g_value`
-    creates more problems than solutions, in particular when dealing with
-    visitors (which we can't automatically generate).
-*)
-type ('r, 'sv, 'bc, 'lc) g_value =
-  | Concrete of (constant_value[@opaque])  (** Concrete (non-symbolic) value *)
-  | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value
-      (** Enumerations, structures, tuples, assumed types. Note that units
-          are encoded as 0-tuples  *)
-  | Bottom  (** No value (uninitialized or moved value) *)
-  | Borrow of 'bc  (** A borrowed value *)
-  | Loan of 'lc  (** A loaned value *)
-  | Symbolic of 'sv  (** Unknown value *)
-
-and ('r, 'sv, 'bc, 'lc) g_adt_value = {
-  variant_id : VariantId.id option; [@opaque]
-  field_values : ('r, 'sv, 'bc, 'lc) g_typed_value list;
-}
+    method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
+  end
 
-(** "Generic" ADT value (not "GADT" value) *)
+(** Ancestor for map visitor for [typed_value] *)
+class ['self] map_typed_value_base =
+  object (self : 'self)
+    inherit [_] VisitorsRuntime.map
 
-and ('r, 'sv, 'bc, 'lc) g_typed_value = {
-  value : ('r, 'sv, 'bc, 'lc) g_value;
-  ty : 'r ty;
-}
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_g_typed_value";
-        variety = "iter";
-        ancestors = [ "iter_'r_ty_base" ];
-        polymorphic = true;
-        (* Heirs expect a polymorphic class *)
-        concrete = true;
-      }]
+    method visit_constant_value : 'env -> constant_value -> constant_value =
+      fun _ cv -> cv
 
-class ['self] iter_typed_value_base =
-  object (self : 'self)
-    inherit [_] iter_g_typed_value
+    method visit_erased_region : 'env -> erased_region -> erased_region =
+      fun _ r -> r
 
-    method visit_erased_region : 'env. 'env -> erased_region -> unit =
-      fun _env _ -> ()
+    method visit_symbolic_proj_comp
+        : 'env -> symbolic_proj_comp -> symbolic_proj_comp =
+      fun _ sv -> sv
 
-    method visit_symbolic_proj_comp : 'env. 'env -> symbolic_proj_comp -> unit =
-      fun _env _ -> ()
+    method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
   end
 
+(** An untyped value, used in the environments *)
 type value =
-  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value
-(** "Regular" value *)
+  | Concrete of constant_value  (** Concrete (non-symbolic) value *)
+  | Adt of adt_value  (** Enumerations and structures *)
+  | Bottom  (** No value (uninitialized or moved value) *)
+  | Borrow of borrow_content  (** A borrowed value *)
+  | Loan of loan_content  (** A loaned value *)
+  | Symbolic of symbolic_proj_comp  (** Unknown (symbolic) value *)
 
-and adt_value =
-  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value
+and adt_value = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_value list;
+}
 
 and borrow_content =
   | SharedBorrow of (BorrowId.id[@opaque])  (** A shared value *)
@@ -157,12 +132,7 @@ and loan_content =
   | SharedLoan of (BorrowId.set_t[@opaque]) * typed_value
   | MutLoan of (BorrowId.id[@opaque])
 
-and typed_value =
-  ( erased_region,
-    symbolic_proj_comp,
-    borrow_content,
-    loan_content )
-  g_typed_value
+and typed_value = { value : value; ty : ety }
 [@@deriving
   show,
     visitors
@@ -172,6 +142,14 @@ and typed_value =
         ancestors = [ "iter_typed_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
+      },
+    visitors
+      {
+        name = "map_typed_value";
+        variety = "map";
+        ancestors = [ "map_typed_value_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
       }]
 (** "Regular" typed value (we map variables to typed values) *)
 
@@ -189,24 +167,46 @@ type aproj =
 
 type region = RegionVarId.id Types.region [@@deriving show]
 
+(** Ancestor for iter visitor for [typed_avalue] *)
 class ['self] iter_typed_avalue_base =
   object (self : 'self)
-    inherit [_] iter_g_typed_value
+    inherit [_] iter_typed_value
+
+    method visit_region : 'env -> region -> unit = fun _ _ -> ()
+
+    method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
+
+    method visit_abstract_shared_borrows
+        : 'env -> abstract_shared_borrows -> unit =
+      fun _ _ -> ()
 
-    method visit_region : 'env. 'env -> region -> unit = fun _env _r -> ()
+    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+  end
+
+(** Ancestor for MAP visitor for [typed_avalue] *)
+class ['self] map_typed_avalue_base =
+  object (self : 'self)
+    inherit [_] map_typed_value
 
-    method visit_aproj : 'env. 'env -> aproj -> unit = fun env _ -> ()
+    method visit_region : 'env -> region -> region = fun _ r -> r
 
-    method visit_typed_value : 'env. 'env -> typed_value -> unit =
-      fun _env _v -> ()
+    method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
 
     method visit_abstract_shared_borrows
-        : 'env. 'env -> abstract_shared_borrows -> unit =
-      fun _env _asb -> ()
+        : 'env -> abstract_shared_borrows -> abstract_shared_borrows =
+      fun _ asb -> asb
+
+    method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
   end
 
-type avalue = (region, aproj, aborrow_content, aloan_content) g_value
-(** Abstraction values are used inside of abstractions to properly model
+type avalue =
+  | AConcrete of constant_value
+  | AAdt of aadt_value
+  | ABottom
+  | ALoan of aloan_content
+  | ABorrow of aborrow_content
+  | ASymbolic of aproj
+      (** 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:
@@ -214,7 +214,10 @@ type avalue = (region, aproj, aborrow_content, aloan_content) g_value
 *)
 
 (* TODO: rename to adt_avalue? *)
-and aadt_value = (region, aproj, aborrow_content, aloan_content) g_adt_value
+and aadt_value = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_avalue list;
+}
 
 and aloan_content =
   | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
@@ -234,7 +237,9 @@ and aborrow_content =
   | AIgnoredMutBorrow of typed_avalue
   | AIgnoredSharedBorrow of abstract_shared_borrows
 
-and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
+(* TODO: we may want to merge this with typed_value - would prevent some issues
+   when accessing fields... *)
+and typed_avalue = { value : avalue; ty : rty }
 [@@deriving
   show,
     visitors
@@ -244,6 +249,14 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
         ancestors = [ "iter_typed_avalue_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
+      },
+    visitors
+      {
+        name = "map_typed_avalue";
+        variety = "map";
+        ancestors = [ "map_typed_avalue_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
       }]
 
 type abs = {
@@ -263,6 +276,7 @@ type abs = {
     which are a special kind of value.
 *)
 
+(*
 (** Polymorphic version of the map visitor for [g_typed_value].
 
     The polymorphic visitor generated by the visitors macro caused some
@@ -575,3 +589,4 @@ class ['self] map_typed_avalue =
         : 'env -> abstract_shared_borrows -> aloan_content =
       fun _env asb -> AIgnoredSharedLoan asb
   end
+ *)