summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-23 23:35:52 +0100
committerSon Ho2021-11-23 23:35:52 +0100
commit5681f27485f39f12b1d0e7ee6ea09329b7bdfacd (patch)
treec680325966b84bce185bbb000ea0420688bec470
parentec241ca38b763d29ab6ac51a601f9930bf47c5ea (diff)
Start working on eval_rvalue
-rw-r--r--src/Interpreter.ml30
1 files changed, 28 insertions, 2 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 541e70d1..4c5d0532 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -411,6 +411,9 @@ let lookup_loan_from_borrow_id (config : config) (l : BorrowId.id) (env : env) :
This function updates the shared loan to a mutable loan (we then update
the borrow). Of course, the shared loan must contain exactly one borrow id
(the one we give as parameter), otherwise we can't promote it.
+
+ TODO: this is wrong, we need to check the shared value and end the loans
+ inside (eventually...).
*)
let promote_shared_loan_to_mut_loan (config : config) (l : BorrowId.id)
(env0 : env) : typed_value * env =
@@ -1264,5 +1267,28 @@ let eval_operand (config : config) (ctx : eval_ctx) (op : operand) :
(ctx3, v)))
(*
-let rec update_env_along_read_place (config : config) (access : access_kind)
- (p : place) (env : env) : typed_value * env =*)
+let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
+ eval_ctx * typed_value =
+ match rvalue with
+ | Use op -> eval_operand config ctx op
+ | Ref (p, bkind) -> (
+ match bkind with
+ | Expressions.Shared ->
+ (* Access the value *)
+ let access = Read in
+ let env1 = update_env_along_read_place config access p ctx.env in
+ let env2 = collect_borrows_at_place config access p env1 in
+ (* Update the value *)
+ ()
+ | Expressions.Mut -> ()
+ | Expressions.TwoPhaseMut -> ())
+ | UnaryOp (unop, op) -> ()
+ | BinaryOp (binop, op1, op2) -> ()
+ | Discriminant p -> ()
+ | Aggregate (aggregate_kind, ops) -> ()
+ *)
+
+(* TODO:
+ update activate_inactivated_mut_borrow (need to end loans inside)
+ update write_value
+ *)