diff options
| -rw-r--r-- | src/Interpreter.ml | 63 |
1 files changed, 44 insertions, 19 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 878e8e17..9a581a10 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -61,6 +61,17 @@ type exploration_kind = { functions behave, by restraining the kind of therms they can enter. *) +(** We sometimes need to return a value whose type may vary depending on + whether we find it in a "concrete" value or an abstraction (ex.: loan + contents when we perform environment lookups by using borrow ids) *) +type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b + +type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs +(** Generic loan content: concrete or abstract *) + +type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs +(** Generic borrow content: concrete or abstract *) + exception Found (** Utility exception @@ -74,6 +85,12 @@ exception FoundBorrowContent of V.borrow_content exception FoundLoanContent of V.loan_content (** Utility exception *) +exception FoundGBorrowContent of g_borrow_content +(** Utility exception *) + +exception FoundGLoanContent of g_loan_content +(** Utility exception *) + (** Check if a value contains a borrow *) let borrows_in_value (v : V.typed_value) : bool = let obj = @@ -124,7 +141,7 @@ let loans_in_value (v : V.typed_value) : bool = The loan is referred to by a borrow id. *) let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - V.loan_content option = + g_loan_content option = let obj = object inherit [_] C.iter_env as super @@ -147,13 +164,13 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : | 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))) + raise (FoundGLoanContent (Concrete (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)) + if bid = l then raise (FoundGLoanContent (Concrete (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 @@ -168,7 +185,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : try obj#visit_env () env; None - with FoundLoanContent lc -> Some lc + with FoundGLoanContent lc -> Some lc (** Lookup a loan content. @@ -176,7 +193,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : Raises an exception if no loan was found. *) let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - V.loan_content = + g_loan_content = match lookup_loan_opt ek l env with | None -> failwith "Unreachable" | Some lc -> lc @@ -243,7 +260,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) (** Lookup a borrow content from a borrow id. *) let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) - : V.borrow_content option = + : g_borrow_content option = let obj = object inherit [_] C.iter_env as super @@ -252,17 +269,20 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) 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))) + if bid = l then + raise (FoundGBorrowContent (Concrete (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)) + if bid = l then + raise (FoundGBorrowContent (Concrete (V.SharedBorrow bid))) else () | V.InactivatedMutBorrow bid -> (* Check the borrow id *) if bid = l then - raise (FoundBorrowContent (V.InactivatedMutBorrow bid)) + raise + (FoundGBorrowContent (Concrete (V.InactivatedMutBorrow bid))) else () method! visit_loan_content env lc = @@ -281,14 +301,14 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) try obj#visit_env () env; None - with FoundBorrowContent lc -> Some lc + with FoundGBorrowContent lc -> Some lc (** Lookup a borrow content from a borrow id. Raise an exception if no loan was found *) let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - V.borrow_content = + g_borrow_content = match lookup_borrow_opt ek l env with | None -> failwith "Unreachable" | Some lc -> lc @@ -773,8 +793,9 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx.env with - | V.MutLoan _ -> failwith "Expected a shared loan, found a mut loan" - | V.SharedLoan (bids, sv) -> + | Concrete (V.MutLoan _) -> + failwith "Expected a shared loan, found a mut loan" + | Concrete (V.SharedLoan (bids, sv)) -> (* Check that there is only one borrow id (l) and update the loan *) assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); (* We need to check that there aren't any loans in the value: @@ -790,6 +811,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : let ctx = { ctx with env } in (* Return *) (ctx, sv) + | Abstract _ -> raise Unimplemented (** Helper function: see [activate_inactivated_mut_borrow]. @@ -804,12 +826,13 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in match lookup_borrow ek l ctx.env with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> + | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> failwith "Expected an inactivated mutable borrow" - | V.InactivatedMutBorrow _ -> + | Concrete (V.InactivatedMutBorrow _) -> (* Update it *) let env = update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx.env in { ctx with env } + | Abstract _ -> raise Unimplemented (** Promote an inactivated mut borrow to a mut borrow. @@ -822,8 +845,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx.env with - | V.MutLoan _ -> failwith "Unreachable" - | V.SharedLoan (bids, sv) -> ( + | Concrete (V.MutLoan _) -> failwith "Unreachable" + | Concrete (V.SharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be inactivated borrows inside the value. If we perform an update, do a recursive call to lookup the updated value *) @@ -857,6 +880,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) [promote_shared_loan_to_mut_loan] *) promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx) + | Abstract _ -> raise Unimplemented (** Paths *) @@ -1005,8 +1029,8 @@ let rec access_projection (access : projection_access) (env : C.env) (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then match lookup_loan ek bid env with - | V.MutLoan _ -> failwith "Expected a shared loan" - | V.SharedLoan (bids, sv) -> ( + | Concrete (V.MutLoan _) -> failwith "Expected a shared loan" + | Concrete (V.SharedLoan (bids, sv)) -> ( (* Explore the shared value *) match access_projection access env update p' sv with | Error err -> Error err @@ -1020,6 +1044,7 @@ let rec access_projection (access : projection_access) (env : C.env) in (* Return - note that we don't need to update the borrow itself *) Ok (env, { res with updated = v })) + | Abstract _ -> raise Unimplemented else Error (FailBorrow bc) | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) | V.MutBorrow (bid, bv) -> |