summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Values.ml238
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 22:00:37 +0000