summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml220
1 files changed, 114 insertions, 106 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ad7bdba1..7d396a84 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -130,44 +130,37 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
object
inherit [_] C.iter_env_concrete as super
- method! visit_MutBorrow env bid mv =
- if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv else ()
- (** Control the diving into mutable borrows *)
-
- (* TODO
- method! visit_Loan env lc =
- match lc with
- | V.SharedLoan (bids, sv) ->
- (* Check if this is the loan we are looking for, and control the dive *)
- if V.BorrowId.Set.mem l bids then
- raise (FoundLoanContent (V.SharedLoan (bids, sv)))
- else if ek.enter_shared_loans then
- super#visit_SharedLoan env bids sv
- else ()
- | V.MutLoan bid ->
- (* Check if this is the loan we are looking for *)
- if bid = l then raise (FoundLoanContent (V.MutLoan bid))
- else super#visit_MutLoan env bid
- (** We reimplement [visit_Loan] (rather than the more precise functions
- [visit_SharedLoan], etc.) on purpose: as we have an exhaustive match
- below, we are more resilient to definition updates (the compiler
- is our friend).
- *)
- *)
- method! visit_SharedLoan env bids sv =
- if V.BorrowId.Set.mem l bids then
- raise (FoundLoanContent (V.SharedLoan (bids, sv)))
- else if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
- else ()
- (** Shared loan: checks if this is the loan we are looking for, and
- control the dive.
- *)
+ method! visit_borrow_content env bc =
+ match bc with
+ | V.SharedBorrow bid ->
+ (* Nothing specific to do *)
+ super#visit_SharedBorrow env bid
+ | V.InactivatedMutBorrow bid ->
+ (* Nothing specific to do *)
+ super#visit_InactivatedMutBorrow env bid
+ | V.MutBorrow (bid, mv) ->
+ (* Control the dive *)
+ if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ else ()
- method! visit_MutLoan env bid =
- if bid = l then raise (FoundLoanContent (V.MutLoan bid))
- else super#visit_MutLoan env bid
- (** Mut loan: checks if this is the loan we are looking for
- *)
+ method! visit_loan_content env lc =
+ match lc with
+ | V.SharedLoan (bids, sv) ->
+ (* Check if this is the loan we are looking for, and control the dive *)
+ if V.BorrowId.Set.mem l bids then
+ raise (FoundLoanContent (V.SharedLoan (bids, sv)))
+ else if ek.enter_shared_loans then
+ super#visit_SharedLoan env bids sv
+ else ()
+ | V.MutLoan bid ->
+ (* Check if this is the loan we are looking for *)
+ if bid = l then raise (FoundLoanContent (V.MutLoan bid))
+ else super#visit_MutLoan env bid
+ (** We reimplement [visit_Loan] (rather than the more precise functions
+ [visit_SharedLoan], etc.) on purpose: as we have an exhaustive match
+ below, we are more resilient to definition updates (the compiler
+ is our friend).
+ *)
end
in
(* We use exceptions *)
@@ -208,28 +201,35 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
object
inherit [_] C.map_env_concrete 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 (
- set_ref env;
- 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 (
- set_ref env;
- nlc)
- else super#visit_MutLoan env bid
- (** Mut loan: checks if this is the loan we are looking for
- *)
+ method! visit_borrow_content env bc =
+ match bc with
+ | V.SharedBorrow _ | V.InactivatedMutBorrow _ ->
+ (* Nothing specific to do *)
+ super#visit_borrow_content env bc
+ | V.MutBorrow (bid, mv) ->
+ (* Control the dive into mutable borrows *)
+ if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ else V.MutBorrow (bid, mv)
+
+ method! visit_loan_content env lc =
+ match lc with
+ | V.SharedLoan (bids, sv) ->
+ (* Shared loan: check if this is the loan we are looking for, and
+ control the dive. *)
+ if V.BorrowId.Set.mem l bids then (
+ set_ref env;
+ nlc)
+ else if ek.enter_shared_loans then
+ super#visit_SharedLoan env bids sv
+ else V.SharedLoan (bids, sv)
+ | V.MutLoan bid ->
+ (* Mut loan: checks if this is the loan we are looking for *)
+ if bid = l then (
+ set_ref env;
+ nlc)
+ else super#visit_MutLoan env bid
+ (** We reimplement [visit_loan_content] (rather than one of the sub-
+ functions) on purpose: exhaustive matches are good for maintenance *)
end
in
@@ -245,24 +245,31 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
object
inherit [_] C.iter_env_concrete as super
- method! visit_MutBorrow env bid mv =
- if bid = l then raise (FoundBorrowContent (V.MutBorrow (bid, mv)))
- else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
- else ()
- (** Check the borrow id and control the diving *)
-
- method! visit_SharedBorrow _env bid =
- if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid)) else ()
- (** Check the borrow id *)
-
- method! visit_InactivatedMutBorrow _env bid =
- if bid = l then raise (FoundBorrowContent (V.InactivatedMutBorrow bid))
- else ()
- (** Check the borrow id *)
+ method! visit_borrow_content env bc =
+ match bc with
+ | V.MutBorrow (bid, mv) ->
+ (* Check the borrow id and control the dive *)
+ if bid = l then raise (FoundBorrowContent (V.MutBorrow (bid, mv)))
+ else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ else ()
+ | V.SharedBorrow bid ->
+ (* Check the borrow id *)
+ if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid))
+ else ()
+ | V.InactivatedMutBorrow bid ->
+ (* Check the borrow id *)
+ if bid = l then
+ raise (FoundBorrowContent (V.InactivatedMutBorrow bid))
+ else ()
- method! visit_SharedLoan env bids sv =
- if ek.enter_shared_loans then super#visit_SharedLoan env bids sv else ()
- (** Control the diving *)
+ method! visit_loan_content env lc =
+ match lc with
+ | V.MutLoan bid ->
+ (* Nothing special to do *) super#visit_MutLoan env bid
+ | V.SharedLoan (bids, sv) ->
+ (* Control the dive *)
+ if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
+ else ()
end
in
(* We use exceptions *)
@@ -302,36 +309,37 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
object
inherit [_] C.map_env_concrete as super
- method! visit_MutBorrow env bid mv =
- if bid = l then (
- set_ref env;
- nbc)
- else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
- else V.MutBorrow (bid, mv)
- (** Check the id and control diving *)
-
- method! visit_SharedBorrow env bid =
- if bid = l then (
- set_ref env;
- nbc)
- else super#visit_SharedBorrow env bid
- (** Check the id *)
-
- method! visit_InactivatedMutBorrow env bid =
- if bid = l then (
- set_ref env;
- nbc)
- else super#visit_InactivatedMutBorrow env bid
- (** Check the id *)
-
- method! visit_SharedLoan env bids sv =
- if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
- else V.SharedLoan (bids, sv)
- (** Control the dive *)
-
- method! visit_MutLoan env bid =
- (* Nothing specific to do for mutable loans *)
- super#visit_MutLoan env bid
+ method! visit_borrow_content env bc =
+ match bc with
+ | V.MutBorrow (bid, mv) ->
+ (* Check the id and control dive *)
+ if bid = l then (
+ set_ref env;
+ nbc)
+ else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ else V.MutBorrow (bid, mv)
+ | V.SharedBorrow bid ->
+ (* Check the id *)
+ if bid = l then (
+ set_ref env;
+ nbc)
+ else super#visit_SharedBorrow env bid
+ | V.InactivatedMutBorrow bid ->
+ (* Check the id *)
+ if bid = l then (
+ set_ref env;
+ nbc)
+ else super#visit_InactivatedMutBorrow env bid
+
+ method! visit_loan_content env lc =
+ match lc with
+ | V.SharedLoan (bids, sv) ->
+ (* Control the dive *)
+ if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
+ else V.SharedLoan (bids, sv)
+ | V.MutLoan bid ->
+ (* Nothing specific to do *)
+ super#visit_MutLoan env bid
end
in