diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 36 | ||||
| -rw-r--r-- | src/Values.ml | 8 |
2 files changed, 40 insertions, 4 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b968bfa6..fe1c1c6f 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -176,6 +176,42 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : | None -> failwith "Unreachable" | Some lc -> lc +(* +TODO: use this +(** Update a loan content in a value. + + The loan is referred to by a borrow id. + + This is a helper function: it might break invariants. + *) +let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) + (nlc : V.loan_content) (v : V.typed_value) : V.typed_value = + let obj = + object + inherit [_] V.map_typed_value as super + + method! visit_MutBorrow env bid mv = + if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv + else V.MutBorrow (bid, mv) + (** Control the diving into mutable borrows *) + + method! visit_SharedLoan env bids sv = + if V.BorrowId.Set.mem l bids then nlc + else if ek.enter_shared_loans then super#visit_SharedLoan env bids sv + else V.SharedLoan (bids, sv) + (** Shared loan: checks if this is the loan we are looking for, and + control the dive. + *) + + method! visit_MutLoan env bid = + if bid = l then nlc else super#visit_MutLoan env bid + (** Mut loan: checks if this is the loan we are looking for + *) + end + in + (* We use exceptions *) +obj#visit_typed_value () v*) + (** Update a loan content in a value. The loan is referred to by a borrow id. diff --git a/src/Values.ml b/src/Values.ml index 72d5c948..4acce0e6 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -214,10 +214,10 @@ and typed_value = (** Override some undefined functions *) class ['self] map_typed_value = object (self : 'self) - inherit [_] map_typed_value_incomplete as super + inherit [_] map_typed_value_incomplete method! visit_typed_value (env : 'env) (tv : typed_value) : typed_value = - let value = super#visit_value env tv.value in + let value = self#visit_value env tv.value in (* Ignore the type *) let ty = tv.ty in { value; ty } @@ -320,10 +320,10 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value (** Override some undefined functions *) class ['self] map_typed_avalue = object (self : 'self) - inherit [_] map_typed_avalue_incomplete as super + inherit [_] map_typed_avalue_incomplete method! visit_typed_avalue (env : 'env) (tv : typed_avalue) : typed_avalue = - let value = super#visit_avalue env tv.value in + let value = self#visit_avalue env tv.value in (* Ignore the type *) let ty = tv.ty in { value; ty } |