From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:28:56 +0100
Subject: Remove the 'r type variable from the ty type definition

---
 compiler/ValuesUtils.ml | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

(limited to 'compiler/ValuesUtils.ml')

diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 527434c1..24485002 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -9,13 +9,27 @@ include PrimitiveValuesUtils
 exception FoundSymbolicValue of symbolic_value
 
 let mk_unit_value : typed_value =
-  { value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
+  { value = VAdt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
 
-let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }
-let mk_typed_avalue (ty : rty) (value : avalue) : typed_avalue = { value; ty }
-let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
-let mk_abottom (ty : rty) : typed_avalue = { value = ABottom; ty }
-let mk_aignored (ty : rty) : typed_avalue = { value = AIgnored; ty }
+let mk_typed_value (ty : ty) (value : value) : typed_value =
+  assert (ty_is_ety ty);
+  { value; ty }
+
+let mk_typed_avalue (ty : ty) (value : avalue) : typed_avalue =
+  assert (ty_is_rty ty);
+  { value; ty }
+
+let mk_bottom (ty : ty) : typed_value =
+  assert (ty_is_ety ty);
+  { value = Bottom; ty }
+
+let mk_abottom (ty : ty) : typed_avalue =
+  assert (ty_is_rty ty);
+  { value = ABottom; ty }
+
+let mk_aignored (ty : ty) : typed_avalue =
+  assert (ty_is_rty ty);
+  { value = AIgnored; ty }
 
 let value_as_symbolic (v : value) : symbolic_value =
   match v with Symbolic v -> v | _ -> raise (Failure "Unexpected")
@@ -23,7 +37,7 @@ let value_as_symbolic (v : value) : symbolic_value =
 (** Box a value *)
 let mk_box_value (v : typed_value) : typed_value =
   let box_ty = mk_box_ty v.ty in
-  let box_v = Adt { variant_id = None; field_values = [ v ] } in
+  let box_v = VAdt { variant_id = None; field_values = [ v ] } in
   mk_typed_value box_ty box_v
 
 let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false
@@ -46,7 +60,7 @@ let is_unit (v : typed_value) : bool =
   ty_is_unit v.ty
   &&
   match v.value with
-  | Adt av -> av.variant_id = None && av.field_values = []
+  | VAdt av -> av.variant_id = None && av.field_values = []
   | _ -> false
 
 (** Check if a value contains a *concrete* borrow (i.e., a [Borrow] value -
-- 
cgit v1.2.3


From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:41:58 +0100
Subject: Add the "V" prefix to most variants related to values

---
 compiler/ValuesUtils.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'compiler/ValuesUtils.ml')

diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 24485002..7880fc3a 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -21,7 +21,7 @@ let mk_typed_avalue (ty : ty) (value : avalue) : typed_avalue =
 
 let mk_bottom (ty : ty) : typed_value =
   assert (ty_is_ety ty);
-  { value = Bottom; ty }
+  { value = VBottom; ty }
 
 let mk_abottom (ty : ty) : typed_avalue =
   assert (ty_is_rty ty);
@@ -32,7 +32,7 @@ let mk_aignored (ty : ty) : typed_avalue =
   { value = AIgnored; ty }
 
 let value_as_symbolic (v : value) : symbolic_value =
-  match v with Symbolic v -> v | _ -> raise (Failure "Unexpected")
+  match v with VSymbolic v -> v | _ -> raise (Failure "Unexpected")
 
 (** Box a value *)
 let mk_box_value (v : typed_value) : typed_value =
@@ -40,20 +40,20 @@ let mk_box_value (v : typed_value) : typed_value =
   let box_v = VAdt { variant_id = None; field_values = [ v ] } in
   mk_typed_value box_ty box_v
 
-let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false
+let is_bottom (v : value) : bool = match v with VBottom -> true | _ -> false
 
 let is_aignored (v : avalue) : bool =
   match v with AIgnored -> true | _ -> false
 
 let is_symbolic (v : value) : bool =
-  match v with Symbolic _ -> true | _ -> false
+  match v with VSymbolic _ -> true | _ -> false
 
 let as_symbolic (v : value) : symbolic_value =
-  match v with Symbolic s -> s | _ -> raise (Failure "Unexpected")
+  match v with VSymbolic s -> s | _ -> raise (Failure "Unexpected")
 
 let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
   match v.value with
-  | Borrow (MutBorrow (bid, bv)) -> (bid, bv)
+  | VBorrow (VMutBorrow (bid, bv)) -> (bid, bv)
   | _ -> raise (Failure "Unexpected")
 
 let is_unit (v : typed_value) : bool =
@@ -86,7 +86,7 @@ let reserved_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-      method! visit_ReservedMutBorrow _env _ = raise Found
+      method! visit_VReservedMutBorrow _env _ = raise Found
     end
   in
   (* We use exceptions *)
@@ -151,7 +151,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
     object
       inherit [_] iter_typed_value
 
-      method! visit_Symbolic _ sv =
+      method! visit_VSymbolic _ sv =
         let ty = sv.sv_ty in
         if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
           raise (FoundSymbolicValue sv)
@@ -171,7 +171,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
  *)
 let rec value_strip_shared_loans (v : typed_value) : typed_value =
   match v.value with
-  | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
+  | VLoan (VSharedLoan (_, v')) -> value_strip_shared_loans v'
   | _ -> v
 
 (** Check if a symbolic value has borrows *)
@@ -251,7 +251,7 @@ let value_remove_shared_loans (v : typed_value) : typed_value =
 
       method! visit_typed_value env v =
         match v.value with
-        | Loan (SharedLoan (_, sv)) -> self#visit_typed_value env sv
+        | VLoan (VSharedLoan (_, sv)) -> self#visit_typed_value env sv
         | _ -> super#visit_typed_value env v
     end
   in
-- 
cgit v1.2.3


From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 15 Nov 2023 22:03:21 +0100
Subject: Start updating the name type, cleanup the names and the module
 abbrevs

---
 compiler/ValuesUtils.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'compiler/ValuesUtils.ml')

diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 7880fc3a..0d3533c2 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -2,7 +2,6 @@ open Utils
 open TypesUtils
 open Types
 open Values
-module TA = TypesAnalysis
 include PrimitiveValuesUtils
 
 (** Utility exception *)
@@ -144,8 +143,9 @@ let outer_loans_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
-let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
-    (v : typed_value) : symbolic_value option =
+let find_first_primitively_copyable_sv_with_borrows
+    (type_infos : TypesAnalysis.type_infos) (v : typed_value) :
+    symbolic_value option =
   (* The visitor *)
   let obj =
     object
@@ -175,8 +175,8 @@ let rec value_strip_shared_loans (v : typed_value) : typed_value =
   | _ -> v
 
 (** Check if a symbolic value has borrows *)
-let symbolic_value_has_borrows (infos : TA.type_infos) (sv : symbolic_value) :
-    bool =
+let symbolic_value_has_borrows (infos : TypesAnalysis.type_infos)
+    (sv : symbolic_value) : bool =
   ty_has_borrows infos sv.sv_ty
 
 (** Check if a value has borrows in **a general sense**.
@@ -185,7 +185,7 @@ let symbolic_value_has_borrows (infos : TA.type_infos) (sv : symbolic_value) :
     - there are concrete borrows
     - there are symbolic values which may contain borrows
  *)
-let value_has_borrows (infos : TA.type_infos) (v : value) : bool =
+let value_has_borrows (infos : TypesAnalysis.type_infos) (v : value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
@@ -226,7 +226,8 @@ let value_has_loans (v : value) : bool =
     - there are symbolic values which may contain borrows (symbolic values
       can't contain loans).
  *)
-let value_has_loans_or_borrows (infos : TA.type_infos) (v : value) : bool =
+let value_has_loans_or_borrows (infos : TypesAnalysis.type_infos) (v : value) :
+    bool =
   let obj =
     object
       inherit [_] iter_typed_value
-- 
cgit v1.2.3


From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 12:15:37 +0100
Subject: Rename PrimitiveValues to Values

---
 compiler/ValuesUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/ValuesUtils.ml')

diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 0d3533c2..2c7d213f 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -2,7 +2,7 @@ open Utils
 open TypesUtils
 open Types
 open Values
-include PrimitiveValuesUtils
+include Charon.ValuesUtils
 
 (** Utility exception *)
 exception FoundSymbolicValue of symbolic_value
-- 
cgit v1.2.3