summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Values.ml')
-rw-r--r--src/Values.ml116
1 files changed, 115 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml
index c51f0b2c..1720dfc2 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -277,6 +277,7 @@ type avalue = (region, aproj, aborrow_content, aloan_content) g_value
part of it is thus "abstracted" away.
*)
+(* TODO: rename to adt_avalue? *)
and aadt_value = (region, aproj, aborrow_content, aloan_content) g_adt_value
and aloan_content =
@@ -285,6 +286,7 @@ and aloan_content =
| AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
| AEndedSharedLoan of typed_value * typed_avalue
| AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
+ | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
| AIgnoredSharedLoan of abstract_shared_borrows
(** Note that when a borrow content is ended, it is replaced by Bottom (while
@@ -294,7 +296,6 @@ and aborrow_content =
| 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
and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
@@ -497,3 +498,116 @@ class ['self] map_typed_value =
method visit_adt_value : 'monomorphic. 'env -> adt_value -> adt_value =
fun env v -> self#visit_g_adt_value env v
end
+
+(*class ['self] map_typed_avalue =
+ object (self : 'self)
+ inherit [_] map_g_typed_value
+
+ method visit_'sv : 'monomorphic. 'env -> aproj -> aproj =
+ fun env sv -> self#visit_aproj env sv
+
+ method visit_'bc : 'monomorphic. 'env -> aborrow_content -> aborrow_content
+ =
+ fun env bc -> self#visit_aborrow_content env bc
+
+ method visit_'lc : 'monomorphic. 'env -> aloan_content -> aloan_content =
+ fun env lc -> self#visit_aloan_content env lc
+
+ method visit_aproj : 'monomorphic. 'env -> aproj -> aproj =
+ fun _env sv -> sv
+
+ method visit_aborrow_content
+ : 'monomorphic. 'env -> aborrow_content -> aborrow_content =
+ fun env bc ->
+ match bc with
+ | AMutBorrow (bid, v) -> self#visit_AMutBorrow env bid v
+ | ASharedBorrow bid -> self#visit_ASharedBorrow env bid
+ | AIgnoredMutBorrow v -> self#visit_AIgnoredMutBorrow env v
+ | AIgnoredSharedBorrow asb -> self#visit_AIgnoredSharedBorrow env asb
+
+ method visit_AMutBorrow
+ : 'monomorphic. 'env -> BorrowId.id -> typed_avalue -> borrow_content =
+ fun env bid av ->
+ let av = self#visit_typed_avalue env av in
+ AMutBorrow (bid, av)
+
+ method visit_ASharedBorrow
+ : 'monomorphic. 'env -> BorrowId.id -> borrow_content =
+ fun _env bid -> ASharedBorrow bid
+
+ method visit_AIgnoredMutBorrow
+ : 'monomorphic. 'env -> typed_avalue -> borrow_content =
+ fun env av ->
+ let av = self#visit_typed_avalue env av in
+ AIgnoredMutBorrow av
+
+ method visit_AIgnoredSharedBorrow
+ : 'monomorphic. 'env -> abstract_shared_borrows -> borrow_content =
+ fun _env asb -> AIgnoredSharedBorrow asb
+
+ method visit_aloan_content
+ : 'monomorphic. 'env -> aloan_content -> aloan_content =
+ fun env lc ->
+ match lc with
+ | AMutLoan (bid, av) -> self#visit_AMutLoan env bids av
+ | ASharedLoan (bids, v, av) -> self#visit_ASharedLoan env bids v av
+ | AEndedMutLoan { given_back; child } ->
+ self#visit_AEndedMutLoan env given_back child
+ | AIgnoredMutLoan (bids, v) -> self#visit_AIgnoredMutLoan env bids v
+ | AEndedIgnoredMutLoan { given_back; child } ->
+ self#visit_AEndedIgnoredMutLoan env given_back child
+ | AIgnoredSharedLoan asb -> self#visit_AIgnoredSharedLoan env asb
+
+ method visit_AMutLoan
+ : 'monomorphic. 'env -> BorrowId.id -> typed_avalue -> loan_content =
+ fun env bid av ->
+ let av = self#visit_typed_avalue env av in
+ AMutLoan (bid, av)
+
+ method visit_ASharedLoan
+ : 'monomorphic.
+ 'env -> BorrowId.set_t -> typed_value -> typed_avalue -> loan_content
+ =
+ fun env bids v av ->
+ let v = self#visit_typed_value env v in
+ let av = self#visit_typed_avalue env av in
+ ASharedLoan (bids, v, av)
+
+ method visit_AEndedMutLoan
+ : 'monomorphic. 'env -> typed_value -> typed_avalue -> loan_content =
+ fun env given_back child ->
+ let given_back = self#visit_typed_value env given_back in
+ let child = self#visit_typed_avalue env child in
+ AEndedMutLoan { given_back; child }
+
+ method visit_AEndedSharedLoan
+ : 'monomorphic. 'env -> typed_value -> typed_avalue -> loan_content =
+ fun env v av ->
+ let v = self#visit_typed_value env v in
+ let av = self#visit_typed_avalue env av in
+ AEndedSharedLoan (v, av)
+
+ method visit_AIgnoredMutLoan
+ : 'monomorphic. 'env -> BorrowId.id -> typed_avalue -> loan_content =
+ fun env id av ->
+ let av = self#visit_typed_avalue env av in
+ AIgnoredMutLoan (id, av)
+
+ method visit_AEndedIgnoredMutLoan
+ : 'monomorphic. 'env -> typed_value -> typed_avalue -> loan_content =
+ fun env given_back child ->
+ let given_back = self#visit_typed_avalue env given_back in
+ let child = self#visit_typed_avalue env child in
+ AEndedIgnoredMutLoan { given_back; child }
+
+ method visit_AIgnoredSharedLoan
+ : 'monomorphic. 'env -> abstract_shared_borrows -> loan_content =
+ fun _env asb -> AIgnoredSharedLoan asb
+
+ method visit_typed_avalue
+ : 'monomorphic. 'env -> typed_avalue -> typed_avalue =
+ fun env v -> self#visit_g_typed_value env v
+
+ method visit_aadt_value : 'monomorphic. 'env -> aadt_value -> aadt_value =
+ fun env v -> self#visit_g_adt_value env v
+ end*)