summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2021-11-24 11:34:02 +0100
committerSon Ho2021-11-24 11:34:02 +0100
commitfc6505de45b4db4d9d9ae3e4d2259352c402f8cb (patch)
treee06e43dc6a5f24317fcfb1c1f9df98c42e7d439c /src/Interpreter.ml
parent77f66621eca3864b1f2c304d71e0abd386c6aa4b (diff)
Implement access_place
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml21
1 files changed, 21 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 66a8fbd1..851726c3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -973,6 +973,27 @@ let rec access_projection (access : projection_access) (env : env)
Ok (env1, { res with updated = nv })
else Error (FailSharedLoan bids)))
+(** Generic function to access (read/write) the value at a given place.
+
+ We return the value we read at the place and the (eventually) updated
+ environment, if we managed to access the place, or the precise reason
+ why we failed.
+ *)
+let access_place (access : projection_access) (env : env)
+ (* Function to (eventually) update the value we find *)
+ (update : typed_value -> typed_value) (p : place) (env : env) :
+ (env * typed_value) path_access_result =
+ (* Lookup the variable's value *)
+ let value = env_lookup_var_value env p.var_id in
+ (* Apply the projection *)
+ match access_projection access env update p.projection value with
+ | Error err -> Error err
+ | Ok (env1, res) ->
+ (* Update the value *)
+ let env2 = env_update_var_value env p.var_id res.updated in
+ (* Return *)
+ Ok (env2, res.read)
+
(*
(*
TODO: loans