diff options
author | Son Ho | 2021-12-07 16:57:47 +0100 |
---|---|---|
committer | Son Ho | 2021-12-07 16:57:47 +0100 |
commit | 8c0c84d0e748a3e7bf3625ca58428d0cff022947 (patch) | |
tree | a240221f98a2e883665bc3dd0f7a7076dc4e1ce3 /src | |
parent | 54c48b00f70343a46575890c262f28c09e00e043 (diff) |
Update update_loan
Diffstat (limited to 'src')
-rw-r--r-- | src/Interpreter.ml | 38 |
1 files changed, 8 insertions, 30 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d97ab5a8..19636ce5 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -165,17 +165,18 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : | None -> failwith "Unreachable" | Some lc -> lc -(** Update a loan content in a value. +(** Update a loan content. The loan is referred to by a borrow id. This is a helper function: it might break invariants. *) -let update_loan_in_value (r : bool ref) (ek : exploration_kind) - (l : V.BorrowId.id) (nlc : V.loan_content) (v : V.typed_value) : - V.typed_value = +let update_loan (ek : exploration_kind) (l : V.BorrowId.id) + (nlc : V.loan_content) (env : C.env) : C.env = (* We use a reference to check that we update exactly one loan: when updating - * inside values, we check we don't update more than one loan. *) + * inside values, we check we don't update more than one loan. Then, upon + * returning we check that we updated at least once. *) + let r = ref false in let set_ref r = assert (not !r); r := true @@ -183,7 +184,7 @@ let update_loan_in_value (r : bool ref) (ek : exploration_kind) let obj = object - inherit [_] V.map_typed_value as super + 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 @@ -209,30 +210,7 @@ let update_loan_in_value (r : bool ref) (ek : exploration_kind) *) end in - let v = obj#visit_typed_value r v in - v - -(** Update a loan content. - - The loan is referred to by a borrow id. - - This is a helper function: it might break invariants. - - TODO: use visitors for environments. - *) -let update_loan (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.loan_content) (env : C.env) : C.env = - (* We use a reference to check that we update exactly one loan. - * [update_loan_in_value] checks that we update at most once. - * We then check that we updated at least once before returning. *) - let r = ref false in - let update_loan_in_env_value (ev : C.env_value) : C.env_value = - match ev with - | C.Var (vid, v) -> Var (vid, update_loan_in_value r ek l nlc v) - | C.Abs _ -> raise Unimplemented (* TODO *) - | C.Frame -> C.Frame - in - let env = List.map update_loan_in_env_value env in + let env = obj#visit_env r env in (* Check that we updated at least one loan *) assert !r; env |