Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

1 files changed, 40 insertions, 25 deletions

diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 527434c1..2c7d213f 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -2,51 +2,64 @@ open Utils
 open TypesUtils
 open Types
 open Values
-module TA = TypesAnalysis
-include PrimitiveValuesUtils
+include Charon.ValuesUtils
 
 (** Utility exception *)
 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 = VBottom; 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")
+  match v with VSymbolic v -> v | _ -> raise (Failure "Unexpected")
 
 (** 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
+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 =
   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 -
@@ -72,7 +85,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 *)
@@ -130,14 +143,15 @@ 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
       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)
@@ -157,12 +171,12 @@ 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 *)
-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**.
@@ -171,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
@@ -212,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
@@ -237,7 +252,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