diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 61 |
1 files changed, 55 insertions, 6 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 851726c3..17253fb8 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -779,11 +779,6 @@ let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) (** Paths *) -type access_kind = - | Read (** We can go inside borrows and loans *) - | Write (** Don't enter shared borrows or shared loans *) - | Move (** Don't enter borrows or loans *) - (** When we fail reading from or writing to a path, it might be because we need to update the environment by ending borrows, expanding symbolic values, etc. The following type is used to convey this information. *) @@ -979,7 +974,7 @@ let rec access_projection (access : projection_access) (env : env) environment, if we managed to access the place, or the precise reason why we failed. *) -let access_place (access : projection_access) (env : env) +let access_place (access : projection_access) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : place) (env : env) : (env * typed_value) path_access_result = @@ -994,6 +989,60 @@ let access_place (access : projection_access) (env : env) (* Return *) Ok (env2, res.read) +type access_kind = + | Read (** We can go inside borrows and loans *) + | Write (** Don't enter shared borrows or shared loans *) + | Move (** Don't enter borrows or loans *) + +let access_kind_to_projection_access (access : access_kind) : projection_access + = + match access with + | Read -> + { + enter_shared_loans = true; + enter_mut_borrows = true; + lookup_shared_borrows = true; + } + | Write -> + { + enter_shared_loans = false; + enter_mut_borrows = true; + lookup_shared_borrows = false; + } + | Move -> + { + enter_shared_loans = false; + enter_mut_borrows = false; + lookup_shared_borrows = false; + } + +(** Read the value at a given place *) +let read_place (config : config) (access : access_kind) (p : place) (env : env) + : typed_value path_access_result = + let access = access_kind_to_projection_access access in + (* The update function is the identity *) + let update v = v in + match access_place access update p env with + | Error err -> Error err + | Ok (env1, read_value) -> + (* Note that we ignore the new environment: it should be the same as the + original one. + *) + if config.check_invariants then assert (env1 = env); + Ok read_value + +(** Update the value at a given place *) +let write_place (config : config) (access : access_kind) (p : place) + (nv : typed_value) (env : env) : env path_access_result = + let access = access_kind_to_projection_access access in + (* The update function substitutes the value with the new value *) + let update _ = nv in + match access_place access update p env with + | Error err -> Error err + | Ok (env1, _) -> + (* We ignore the read value *) + Ok env1 + (* (* TODO: loans |