diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Contexts.ml | 22 | ||||
| -rw-r--r-- | src/Interpreter.ml | 8 | ||||
| -rw-r--r-- | src/Print.ml | 5 |
3 files changed, 16 insertions, 19 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 62e4d7b9..2d09cb25 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -12,13 +12,11 @@ type binder = { (** Environment value: mapping from variable to value, abstraction (only used in symbolic mode) or stack frame delimiter. - - TODO: rename? Environment element or something? *) -type env_value = Var of binder * typed_value | Abs of abs | Frame +type env_elem = Var of binder * typed_value | Abs of abs | Frame [@@deriving show] -type env = env_value list [@@deriving show] +type env = env_elem list [@@deriving show] type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] @@ -156,7 +154,7 @@ class ['self] iter_frame_concrete = object (self : 'self) inherit [_] V.iter_typed_value - method visit_env_value_Var : 'acc -> binder -> typed_value -> unit = + method visit_env_elem_Var : 'acc -> binder -> typed_value -> unit = fun acc vid v -> self#visit_typed_value acc v method visit_env : 'acc -> env -> unit = @@ -164,7 +162,7 @@ class ['self] iter_frame_concrete = match env with | [] -> () | Var (vid, v) :: env -> - self#visit_env_value_Var acc vid v; + self#visit_env_elem_Var acc vid v; self#visit_env acc env | Abs _ :: _ -> failwith "Unexpected abstraction" | Frame :: _ -> (* We stop here *) () @@ -176,7 +174,7 @@ class ['self] iter_env_concrete = object (self : 'self) inherit [_] V.iter_typed_value - method visit_env_value_Var : 'acc -> binder -> typed_value -> unit = + method visit_env_elem_Var : 'acc -> binder -> typed_value -> unit = fun acc vid v -> self#visit_typed_value acc v method visit_env : 'acc -> env -> unit = @@ -184,7 +182,7 @@ class ['self] iter_env_concrete = match env with | [] -> () | Var (vid, v) :: env -> - self#visit_env_value_Var acc vid v; + self#visit_env_elem_Var acc vid v; self#visit_env acc env | Abs _ :: _ -> failwith "Unexpected abstraction" | Frame :: env -> self#visit_env acc env @@ -195,7 +193,7 @@ class ['self] map_frame_concrete = object (self : 'self) inherit [_] V.map_typed_value - method visit_env_value_Var : 'acc -> binder -> typed_value -> env_value = + method visit_env_elem_Var : 'acc -> binder -> typed_value -> env_elem = fun acc vid v -> let v = self#visit_typed_value acc v in Var (vid, v) @@ -205,7 +203,7 @@ class ['self] map_frame_concrete = match env with | [] -> [] | Var (vid, v) :: env -> - let v = self#visit_env_value_Var acc vid v in + let v = self#visit_env_elem_Var acc vid v in let env = self#visit_env acc env in v :: env | Abs _ :: _ -> failwith "Unexpected abstraction" @@ -218,7 +216,7 @@ class ['self] map_env_concrete = object (self : 'self) inherit [_] V.map_typed_value - method visit_env_value_Var : 'acc -> binder -> typed_value -> env_value = + method visit_env_elem_Var : 'acc -> binder -> typed_value -> env_elem = fun acc vid v -> let v = self#visit_typed_value acc v in Var (vid, v) @@ -228,7 +226,7 @@ class ['self] map_env_concrete = match env with | [] -> [] | Var (vid, v) :: env -> - let v = self#visit_env_value_Var acc vid v in + let v = self#visit_env_elem_Var acc vid v in let env = self#visit_env acc env in v :: env | Abs _ :: _ -> failwith "Unexpected abstraction" diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d34c20dc..8eebd241 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -567,7 +567,7 @@ let give_back_shared_to_abs _config _bid _abs : V.abs = *) let give_back_value (config : C.config) (bid : V.BorrowId.id) (v : V.typed_value) (env : C.env) : C.env = - let give_back_value_to_env_value ev : C.env_value = + let give_back_value_to_env_elem ev : C.env_elem = match ev with | C.Var (vid, destv) -> C.Var (vid, give_back_value_to_value config bid v destv) @@ -576,7 +576,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) C.Abs (give_back_value_to_abs config bid v abs) | C.Frame -> C.Frame in - List.map give_back_value_to_env_value env + List.map give_back_value_to_env_elem env (** Auxiliary function to end borrows. @@ -588,7 +588,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) check must be independently done before. *) let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = - let give_back_shared_to_env_value ev : C.env_value = + let give_back_shared_to_env_elem ev : C.env_elem = match ev with | C.Var (vid, destv) -> C.Var (vid, give_back_shared_to_value config bid destv) @@ -597,7 +597,7 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = C.Abs (give_back_shared_to_abs config bid abs) | C.Frame -> C.Frame in - List.map give_back_shared_to_env_value env + List.map give_back_shared_to_env_elem env (** When copying values, we duplicate the shared borrows. This is tantamount to reborrowing the shared value. The following function applies this change diff --git a/src/Print.ml b/src/Print.ml index 77bdcb5b..e8471704 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -424,8 +424,7 @@ module Contexts = struct | None -> PV.var_id_to_string bv.index | Some name -> name - let env_value_to_string (fmt : PV.value_formatter) (ev : C.env_value) : string - = + let env_elem_to_string (fmt : PV.value_formatter) (ev : C.env_elem) : string = match ev with | Var (var, tv) -> binder_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" @@ -435,7 +434,7 @@ module Contexts = struct let env_to_string (fmt : PV.value_formatter) (env : C.env) : string = "{\n" ^ String.concat "\n" - (List.map (fun ev -> " " ^ env_value_to_string fmt ev) env) + (List.map (fun ev -> " " ^ env_elem_to_string fmt ev) env) ^ "\n}" type ctx_formatter = PV.value_formatter |