Rename env_value to env_elem

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