Add a "basename" field in Pure.var

2 files changed, 11 insertions, 8 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 45609273..02f6b1ba 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -82,17 +82,20 @@ type scalar_value = V.scalar_value
 
 type constant_value = V.constant_value
 
-type var = { id : VarId.id; ty : ty }
+type var = {
+  id : VarId.id;
+  basename : string option;
+      (** The "basename" is used to generate a meaningful name for the variable
+          (by potentially adding an index to uniquely identify it).
+       *)
+  ty : ty;
+}
 (** Because we introduce a lot of temporary variables, the list of variables
     is not fixed: we thus must carry all its information with the variable
     itself.
-    
-    TODO: add a field for the basename.
  *)
 
-type var_or_dummy =
-  | Var of var  (** TODO: use var_id, not var *)
-  | Dummy  (** Ignored value: `_`. *)
+type var_or_dummy = Var of var | Dummy  (** Ignored value: `_`. *)
 
 (** A left value (which appears on the left of assignments *)
 type lvalue =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 53073563..716b4e94 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -571,7 +571,7 @@ let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) :
   (* Generate the fresh variable *)
   let id, var_counter = VarId.fresh ctx.var_counter in
   let ty = ctx_translate_fwd_ty ctx sv.sv_ty in
-  let var = { id; ty } in
+  let var = { id; basename = None; ty } in
   (* Insert in the map *)
   let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in
   (* Update the context *)
@@ -587,7 +587,7 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx)
 let fresh_var (ty : ty) (ctx : bs_ctx) : bs_ctx * var =
   (* Generate the fresh variable *)
   let id, var_counter = VarId.fresh ctx.var_counter in
-  let var = { id; ty } in
+  let var = { id; basename = None; ty } in
   (* Update the context *)
   let ctx = { ctx with var_counter } in
   (* Return *)