From 309295376d22b1931ff7cb908e4d9283e86ecc50 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 1 Dec 2021 13:42:36 +0100
Subject: Move the var definition

---
 src/CfimAst.ml     | 11 +++++++++++
 src/CfimOfJson.ml  |  4 ++--
 src/Interpreter.ml |  4 ++--
 src/Print.ml       | 12 ++++++------
 src/Substitute.ml  |  4 ++--
 src/Values.ml      | 12 ------------
 6 files changed, 23 insertions(+), 24 deletions(-)

(limited to 'src')

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 9acf40ff..0e36f6df 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -5,6 +5,17 @@ open Expressions
 
 module FunDefId = IdGen ()
 
+type var = {
+  index : VarId.id;  (** Unique variable identifier *)
+  name : string option;
+  var_ty : ety;
+      (** The variable type - erased type, because variables are not used
+       ** in function signatures - TODO: useless? TODO: binder type for
+          function definitions *)
+}
+[@@deriving show]
+(** A variable, as used in a function definition *)
+
 type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
 [@@deriving show]
 
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 383b8410..f16ae601 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -172,14 +172,14 @@ let type_def_of_json (js : json) : (T.type_def, string) result =
         Ok { T.def_id; name; region_params; type_params; kind }
     | _ -> Error "")
 
-let var_of_json (js : json) : (V.var, string) result =
+let var_of_json (js : json) : (A.var, string) result =
   combine_error_msgs js "var_of_json"
     (match js with
     | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] ->
         let* index = V.VarId.id_of_json index in
         let* name = string_option_of_json name in
         let* var_ty = ety_of_json ty in
-        Ok { V.index; name; var_ty }
+        Ok { A.index; name; var_ty }
     | _ -> Error "")
 
 let big_int_of_json (js : json) : (V.big_int, string) result =
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index b936fa70..21124c48 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -48,9 +48,9 @@ let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value =
   { V.value; ty }
 
 (* TODO: move *)
-let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : V.var
+let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
     =
-  { V.index; name; var_ty }
+  { A.index; name; var_ty }
 
 (** Small helper *)
 let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
diff --git a/src/Print.ml b/src/Print.ml
index dc559dc3..9c1aaa94 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -176,9 +176,6 @@ module Values = struct
   let var_id_to_string (id : V.VarId.id) : string =
     "var@" ^ V.VarId.to_string id
 
-  let var_to_string (v : V.var) : string =
-    match v.name with None -> var_id_to_string v.index | Some name -> name
-
   let big_int_to_string (bi : V.big_int) : string = Z.to_string bi
 
   let scalar_value_to_string (sv : V.scalar_value) : string =
@@ -765,6 +762,9 @@ module CfimAst = struct
         ^ statement_to_string fmt (indent ^ indent_incr) indent_incr loop_st
         ^ "\n" ^ indent ^ "}"
 
+  let var_to_string (v : A.var) : string =
+    match v.name with None -> PV.var_id_to_string v.index | Some name -> name
+
   let fun_def_to_string (fmt : ast_formatter) (indent : string)
       (indent_incr : string) (def : A.fun_def) : string =
     let rty_fmt = ast_to_rtype_formatter fmt in
@@ -793,7 +793,7 @@ module CfimAst = struct
     let args = List.combine inputs sg.inputs in
     let args =
       List.map
-        (fun (var, rty) -> PV.var_to_string var ^ " : " ^ rty_to_string rty)
+        (fun (var, rty) -> var_to_string var ^ " : " ^ rty_to_string rty)
         args
     in
     let args = String.concat ", " args in
@@ -808,7 +808,7 @@ module CfimAst = struct
     let locals =
       List.map
         (fun var ->
-          indent ^ indent_incr ^ PV.var_to_string var ^ " : "
+          indent ^ indent_incr ^ var_to_string var ^ " : "
           ^ ety_to_string var.var_ty ^ ";")
         def.locals
     in
@@ -860,7 +860,7 @@ module Module = struct
     in
     let var_id_to_string vid =
       let var = V.VarId.nth def.locals vid in
-      PV.var_to_string var
+      PA.var_to_string var
     in
     let adt_variant_to_string =
       PC.type_ctx_to_adt_variant_to_string_fun type_context
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 9099155f..3a2358f8 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -193,11 +193,11 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety)
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
 let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
-    (def : A.fun_def) : V.var list * A.statement =
+    (def : A.fun_def) : A.var list * A.statement =
   let rsubst r = r in
   let locals =
     List.map
-      (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty })
+      (fun v -> { v with A.var_ty = ty_substitute rsubst tsubst v.A.var_ty })
       def.A.locals
   in
   let body = statement_substitute tsubst def.body in
diff --git a/src/Values.ml b/src/Values.ml
index 57a0aeb0..cb8a1200 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -17,18 +17,6 @@ module AbstractionId = IdGen ()
 
 module RegionId = IdGen ()
 
-(* TODO: move? *)
-type var = {
-  index : VarId.id;  (** Unique variable identifier *)
-  name : string option;
-  var_ty : ety;
-      (** The variable type - erased type, because variables are not used
-       ** in function signatures - TODO: useless? TODO: binder type for
-          function definitions *)
-}
-[@@deriving show]
-(** A variable, as used in a type definition *)
-
 (** A variable *)
 
 type big_int = Z.t
-- 
cgit v1.2.3