diff options
Diffstat (limited to 'src/Values.ml')
| -rw-r--r-- | src/Values.ml | 116 |
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*) |