summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-03 17:51:11 +0100
committerSon Ho2021-12-03 17:51:11 +0100
commitdeb37902bf8b7946f31a3b36f8c5adbaddbfb5a6 (patch)
tree731a227194497d28e5b973733b5f0bc8915370cb /src
parent1bbc4497642ab6c43a7b1425d012a97370a4cb87 (diff)
Implement iter visitors for typed_avalue
Diffstat (limited to '')
-rw-r--r--src/Values.ml59
1 files changed, 41 insertions, 18 deletions
diff --git a/src/Values.ml b/src/Values.ml
index b9835ba1..87c6ec9f 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -69,7 +69,7 @@ type symbolic_proj_comp = {
class virtual ['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 -> ()
+ fun _visit_'r _env _ty -> ()
end
(** A generic, untyped value, used in the environments.
@@ -113,15 +113,15 @@ and ('r, 'sv, 'bc, 'lc) g_typed_value = {
concrete = true;
}]
-class virtual ['self] iter_typed_value_base =
+class ['self] iter_typed_value_base =
object (self : 'self)
inherit [_] iter_g_typed_value
method visit_erased_region : 'env. 'env -> erased_region -> unit =
- fun env _ -> ()
+ fun _env _ -> ()
method visit_symbolic_proj_comp : 'env. 'env -> symbolic_proj_comp -> unit =
- fun env _ -> ()
+ fun _env _ -> ()
end
type value =
@@ -144,8 +144,8 @@ and typed_value =
name = "iter_typed_value";
variety = "iter";
ancestors = [ "iter_typed_value_base" ];
- polymorphic = true;
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
}]
(** "Regular" typed value (we map variables to typed values) *)
@@ -182,8 +182,25 @@ type aproj =
| AProjBorrows of symbolic_value * rty
[@@deriving show]
-type avalue =
- (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_value
+type region = RegionVarId.id Types.region [@@deriving show]
+
+class ['self] iter_typed_avalue_base =
+ object (self : 'self)
+ inherit [_] iter_g_typed_value
+
+ method visit_region : 'env. 'env -> region -> unit = fun _env _r -> ()
+
+ method visit_aproj : 'env. 'env -> aproj -> unit = fun env _ -> ()
+
+ method visit_typed_value : 'env. 'env -> typed_value -> unit =
+ fun _env _v -> ()
+
+ method visit_abstract_shared_borrows
+ : 'env. 'env -> abstract_shared_borrows -> unit =
+ fun _env _asb -> ()
+ end
+
+type avalue = (region, aproj, aborrow_content, aloan_content) g_value
(** Abstraction values are used inside of abstractions to properly model
borrowing relations introduced by function calls.
@@ -191,28 +208,34 @@ type avalue =
part of it is thus "abstracted" away.
*)
-and aadt_value =
- (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_adt_value
+and aadt_value = (region, aproj, aborrow_content, aloan_content) g_adt_value
-and typed_avalue =
- (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_typed_value
-[@@deriving show]
+and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
+[@@deriving
+ show,
+ visitors
+ {
+ name = "iter_typed_avalue";
+ variety = "iter";
+ ancestors = [ "iter_typed_avalue_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ }]
and aloan_content =
- | AMutLoan of BorrowId.id * typed_avalue
- | ASharedLoan of BorrowId.set_t * typed_value * typed_avalue
+ | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
+ | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue
| AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
| AEndedSharedLoan of typed_value * typed_avalue
- | AIgnoredMutLoan of BorrowId.id * typed_avalue
+ | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
| AIgnoredSharedLoan of abstract_shared_borrows
-[@@deriving show]
(** 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
+ | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
+ | ASharedBorrow of (BorrowId.id[@opaque])
| AIgnoredMutBorrow of typed_avalue
| AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
| AIgnoredSharedBorrow of abstract_shared_borrows