Start implementing monomorphic versions of the map visitors

1 files changed, 156 insertions, 82 deletions

diff --git a/src/Values.ml b/src/Values.ml
index 4acce0e6..7b5e9537 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -66,23 +66,23 @@ type symbolic_proj_comp = {
  *)
 
 (** Polymorphic iter visitor *)
-class virtual ['self] iter_'r_ty_base =
+class ['self] iter_'r_ty_base =
   object (self : 'self)
     method visit_ty : 'env 'r. ('env -> 'r -> unit) -> 'env -> 'r ty -> unit =
       fun _visit_'r _env _ty -> ()
   end
 
-(** Polymorphic map visitor *)
-class virtual ['self] map_'r_ty_base =
-  object (self : 'self)
-    method visit_ty
-        : 'env 'r_0 'r_1. ('env -> 'r_0 -> 'r_1) -> 'env -> 'r_0 ty -> 'r_1 ty =
-      fun _visit_'r _env ty ->
-        (* We should use a ty visitor, but in practice we don't need to
-         * visit types, and for the non-generic visit methods (which will
-         * preserve 'r_0) we will override this method with identity *)
-        raise Errors.Unimplemented
-  end
+(*(** Polymorphic map visitor *)
+  class ['self] map_'r_ty_base =
+    object (self : 'self)
+      method visit_ty
+          : 'env 'r_0 'r_1. ('env -> 'r_0 -> 'r_1) -> 'env -> 'r_0 ty -> 'r_1 ty =
+        fun _visit_'r _env ty ->
+          (* We should use a ty visitor, but in practice we don't need to
+           * visit types, and for the non-generic visit methods (which will
+           * preserve 'r_0) we will override this method with identity *)
+          raise Errors.Unimplemented
+  end*)
 
 (** A generic, untyped value, used in the environments.
 
@@ -124,16 +124,16 @@ and ('r, 'sv, 'bc, 'lc) g_typed_value = {
         polymorphic = true;
         (* Heirs expect a polymorphic class *)
         concrete = true;
-      },
-    visitors
-      {
-        name = "map_g_typed_value";
-        variety = "map";
-        ancestors = [ "map_'r_ty_base" ];
-        polymorphic = true;
-        (* Heirs expect a polymorphic class *)
-        concrete = true;
-      }]
+      }
+  (* visitors
+     {
+       name = "map_g_typed_value";
+       variety = "map";
+       ancestors = [ "map_'r_ty_base" ];
+       polymorphic = true;
+       (* Heirs expect a polymorphic class *)
+       concrete = true;
+     }*)]
 
 class ['self] iter_typed_value_base =
   object (self : 'self)
@@ -146,17 +146,17 @@ class ['self] iter_typed_value_base =
       fun _env _ -> ()
   end
 
-class ['self] map_typed_value_base =
-  object (self : 'self)
-    inherit [_] map_g_typed_value
+(*class ['self] map_typed_value_base =
+    object (self : 'self)
+      inherit [_] map_g_typed_value
 
-    method visit_erased_region : 'env. 'env -> erased_region -> erased_region =
-      fun _env r -> r
+      method visit_erased_region : 'env. 'env -> erased_region -> erased_region =
+        fun _env r -> r
 
-    method visit_symbolic_proj_comp
-        : 'env. 'env -> symbolic_proj_comp -> symbolic_proj_comp =
-      fun _env pc -> pc
-  end
+      method visit_symbolic_proj_comp
+          : 'env. 'env -> symbolic_proj_comp -> symbolic_proj_comp =
+        fun _env pc -> pc
+  end*)
 
 type value =
   (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value
@@ -200,28 +200,28 @@ and typed_value =
         ancestors = [ "iter_typed_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
-      },
-    visitors
-      {
-        name = "map_typed_value_incomplete";
-        variety = "map";
-        ancestors = [ "map_typed_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        concrete = true;
-      }]
+      }
+  (* visitors
+     {
+       name = "map_typed_value_incomplete";
+       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) *)
 
-(** Override some undefined functions *)
-class ['self] map_typed_value =
-  object (self : 'self)
-    inherit [_] map_typed_value_incomplete
+(*(** Override some undefined functions *)
+  class ['self] map_typed_value =
+    object (self : 'self)
+      inherit [_] map_typed_value_incomplete
 
-    method! visit_typed_value (env : 'env) (tv : typed_value) : typed_value =
-      let value = self#visit_value env tv.value in
-      (* Ignore the type *)
-      let ty = tv.ty in
-      { value; ty }
-  end
+      method! visit_typed_value (env : 'env) (tv : typed_value) : typed_value =
+        let value = self#visit_value env tv.value in
+        (* Ignore the type *)
+        let ty = tv.ty in
+        { value; ty }
+  end*)
 
 type abstract_shared_borrows =
   | AsbSet of BorrowId.set_t
@@ -253,21 +253,21 @@ class ['self] iter_typed_avalue_base =
       fun _env _asb -> ()
   end
 
-class ['self] map_typed_avalue_base =
-  object (self : 'self)
-    inherit [_] map_g_typed_value
+(*class ['self] map_typed_avalue_base =
+    object (self : 'self)
+      inherit [_] map_g_typed_value
 
-    method visit_region : 'env. 'env -> region -> region = fun _env r -> r
+      method visit_region : 'env. 'env -> region -> region = fun _env r -> r
 
-    method visit_aproj : 'env. 'env -> aproj -> aproj = fun env p -> p
+      method visit_aproj : 'env. 'env -> aproj -> aproj = fun env p -> p
 
-    method visit_typed_value : 'env. 'env -> typed_value -> typed_value =
-      fun _env v -> v
+      method visit_typed_value : 'env. 'env -> typed_value -> typed_value =
+        fun _env v -> v
 
-    method visit_abstract_shared_borrows
-        : 'env. 'env -> abstract_shared_borrows -> abstract_shared_borrows =
-      fun _env asb -> asb
-  end
+      method visit_abstract_shared_borrows
+          : 'env. 'env -> abstract_shared_borrows -> abstract_shared_borrows =
+        fun _env asb -> asb
+  end*)
 
 type avalue = (region, aproj, aborrow_content, aloan_content) g_value
 (** Abstraction values are used inside of abstractions to properly model
@@ -307,27 +307,27 @@ 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_incomplete";
-        variety = "map";
-        ancestors = [ "map_typed_avalue_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        concrete = true;
-      }]
-
-(** Override some undefined functions *)
-class ['self] map_typed_avalue =
-  object (self : 'self)
-    inherit [_] map_typed_avalue_incomplete
-
-    method! visit_typed_avalue (env : 'env) (tv : typed_avalue) : typed_avalue =
-      let value = self#visit_avalue env tv.value in
-      (* Ignore the type *)
-      let ty = tv.ty in
-      { value; ty }
-  end
+      }
+  (* visitors
+     {
+       name = "map_typed_avalue_incomplete";
+       variety = "map";
+       ancestors = [ "map_typed_avalue_base" ];
+       nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+       concrete = true;
+     }*)]
+
+(*(** Override some undefined functions *)
+  class ['self] map_typed_avalue =
+    object (self : 'self)
+      inherit [_] map_typed_avalue_incomplete
+
+      method! visit_typed_avalue (env : 'env) (tv : typed_avalue) : typed_avalue =
+        let value = self#visit_avalue env tv.value in
+        (* Ignore the type *)
+        let ty = tv.ty in
+        { value; ty }
+  end*)
 
 type abs = {
   abs_id : AbstractionId.id;
@@ -345,3 +345,77 @@ type abs = {
     In order to model the relations between the borrows, we use "abstraction values",
     which are a special kind of value.
 *)
+
+class virtual ['self] map_g_value =
+  object (self : 'self)
+    inherit [_] VisitorsRuntime.map
+
+    method virtual visit_'sv : 'monomorphic. 'env -> 'sv -> 'sv
+
+    method virtual visit_'bc : 'monomorphic. 'env -> 'bc -> 'bc
+
+    method virtual visit_'lc : 'monomorphic. 'env -> 'lc -> 'lc
+
+    method visit_Concrete
+        : 'monomorphic. 'env -> constant_value -> ('r, 'sv, 'bc, 'lv) g_value =
+      fun _env cv -> Concrete cv
+
+    method visit_Adt
+        : 'monomorphic.
+          'env -> ('r, 'sv, 'bc, 'lc) g_adt_value -> ('r, 'sv, 'bc, 'lc) g_value
+        =
+      fun env av ->
+        let av = self#visit_g_adt_value env av in
+        Adt av
+
+    method visit_Bottom : 'monomorphic. 'env -> ('r, 'sv, 'bc, 'lv) g_value =
+      fun _env -> Bottom
+
+    method visit_Borrow
+        : 'monomorphic. 'env -> 'bc -> ('r, 'sv, 'bc, 'lv) g_value =
+      fun env bc -> Borrow (self#visit_'bc env bc)
+
+    method visit_Loan : 'monomorphic. 'env -> 'lc -> ('r, 'sv, 'bc, 'lv) g_value
+        =
+      fun env lc -> Loan (self#visit_'lc env lc)
+
+    method visit_Symbolic
+        : 'monomorphic. 'env -> 'sv -> ('r, 'sv, 'bc, 'lv) g_value =
+      fun env sv -> Symbolic (self#visit_'sv env sv)
+
+    method visit_g_value
+        : 'monomorphic.
+          'env -> ('r, 'sv, 'bc, 'lv) g_value -> ('r, 'sv, 'bc, 'lv) g_value =
+      fun env v ->
+        match v with
+        | Concrete cv -> self#visit_Concrete env cv
+        | Adt av -> Adt (self#visit_g_adt_value env av)
+        | Bottom -> self#visit_Bottom env
+        | Borrow bc -> self#visit_Borrow env bc
+        | Loan lc -> self#visit_Loan env lc
+        | Symbolic sv -> self#visit_Symbolic env sv
+
+    method visit_g_adt_value
+        : 'monomorphic.
+          'env ->
+          ('r, 'sv, 'bc, 'lv) g_adt_value ->
+          ('r, 'sv, 'bc, 'lv) g_adt_value =
+      fun env av ->
+        let variant_id = av.variant_id in
+        let field_values =
+          self#visit_list self#visit_g_typed_value env av.field_values
+        in
+        { variant_id; field_values }
+
+    method visit_g_typed_value
+        : 'monomorphic.
+          'env ->
+          ('r, 'sv, 'bc, 'lv) g_typed_value ->
+          ('r, 'sv, 'bc, 'lv) g_typed_value =
+      fun env v ->
+        let value = self#visit_g_value env v.value in
+        let ty = self#visit_ty env v.ty in
+        { value; ty }
+
+    method visit_ty : 'monomorphic. 'env -> 'r ty -> 'r ty = fun _env ty -> ty
+  end