From 7963e3ee84090b96308eebc68ee20532ea85c532 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 30 Nov 2021 20:59:30 +0100
Subject: Introduce [binder] and use them in place of [var] in the environments

---
 src/Contexts.ml    | 20 ++++++++++++++++----
 src/Interpreter.ml |  8 ++------
 src/Print.ml       | 11 ++++++++---
 src/Values.ml      |  2 ++
 4 files changed, 28 insertions(+), 13 deletions(-)

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 84c88e1c..1adb1a02 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -2,12 +2,19 @@ open Types
 open Values
 open CfimAst
 
+type binder = {
+  index : VarId.id;  (** Unique variable identifier *)
+  name : string option;  (** Possible name *)
+}
+[@@deriving show]
+(** A binder used in an environment, to map a variable to a value *)
+
 (** 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 var * typed_value | Abs of abs | Frame
+type env_value = Var of binder * typed_value | Abs of abs | Frame
 [@@deriving show]
 
 type env = env_value list [@@deriving show]
@@ -39,7 +46,7 @@ let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id =
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
-let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var =
+let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   (* TOOD: we might want to stop at the end of the frame *)
   let rec lookup env =
     match env with
@@ -94,6 +101,8 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
   in
   update env
 
+let var_to_binder (var : var) : binder = { index = var.index; name = var.name }
+
 (** Update a variable's value in an evaluation context.
 
     This is a helper function: it can break invariants and doesn't perform
@@ -110,7 +119,8 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
 *)
 let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
   assert (var.var_ty = v.ty);
-  { ctx with env = Var (var, v) :: ctx.env }
+  let bv = var_to_binder var in
+  { ctx with env = Var (bv, v) :: ctx.env }
 
 (** Push a list of variables.
 
@@ -120,7 +130,9 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
 let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
   assert (List.for_all (fun (var, value) -> var.var_ty = value.ty) vars);
-  let vars = List.map (fun (var, value) -> Var (var, value)) vars in
+  let vars =
+    List.map (fun (var, value) -> Var (var_to_binder var, value)) vars
+  in
   let vars = List.rev vars in
   { ctx with env = List.append vars ctx.env }
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c2e44039..d737f79d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2059,15 +2059,13 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list)
   | ( [],
       [ boxed_ty ],
       Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) ->
-      (* Sanity check for invariant *)
-      assert (input_var.var_ty = input_value.V.ty);
       (* Required type checking *)
       assert (input_value.V.ty = boxed_ty);
 
       (* Move the input value *)
       let ctx, moved_input_value =
         eval_operand config ctx
-          (E.Move (mk_place_from_var_id input_var.V.index))
+          (E.Move (mk_place_from_var_id input_var.C.index))
       in
 
       (* Create the box value *)
@@ -2107,8 +2105,6 @@ let eval_box_deref_mut_or_shared (config : C.config)
   | ( [],
       [ boxed_ty ],
       Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> (
-      (* Sanity check for invariant *)
-      assert (input_var.var_ty = input_value.V.ty);
       (* Required type checking. We must have:
          - input_value.ty == & (mut) Box<ty>
          - boxed_ty == ty
@@ -2121,7 +2117,7 @@ let eval_box_deref_mut_or_shared (config : C.config)
 
       (* Borrow the boxed value *)
       let p =
-        { E.var_id = input_var.V.index; projection = [ E.Deref; E.DerefBox ] }
+        { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
       in
       let borrow_kind = if is_mut then E.Mut else E.Shared in
       let rv = E.Ref (p, borrow_kind) in
diff --git a/src/Print.ml b/src/Print.ml
index bb172d5f..911de5e3 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -400,11 +400,16 @@ module PV = Values (* local module *)
 
 (** Pretty-printing for contexts *)
 module Contexts = struct
+  let binder_to_string (bv : C.binder) : string =
+    match bv.name with
+    | 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
       =
     match ev with
     | Var (var, tv) ->
-        PV.var_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
+        binder_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
     | Abs abs -> PV.abs_to_string fmt abs
     | Frame -> failwith "Can't print a Frame element"
 
@@ -456,8 +461,8 @@ module Contexts = struct
       type_ctx_to_adt_variant_to_string_fun ctx.type_context
     in
     let var_id_to_string vid =
-      let var = C.ctx_lookup_var ctx vid in
-      PV.var_to_string var
+      let bv = C.ctx_lookup_binder ctx vid in
+      binder_to_string bv
     in
     let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in
     {
diff --git a/src/Values.ml b/src/Values.ml
index 330f22d3..c7a79eae 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -17,6 +17,7 @@ module AbstractionId = IdGen ()
 
 module RegionId = IdGen ()
 
+(* TODO: move *)
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
@@ -26,6 +27,7 @@ type var = {
           function definitions *)
 }
 [@@deriving show]
+(** A variable, as used in a type definition *)
 
 (** A variable *)
 
-- 
cgit v1.2.3