Move more definitions and do more cleanup

8 files changed, 74 insertions, 67 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 38c79b66..ca1f87f1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -4,6 +4,7 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 open Utils
+open ValuesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterProjectors
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index b08c8749..e379eacd 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -6,6 +6,7 @@ open Errors
 module C = Contexts
 module Subst = Substitute
 module L = Logging
+open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = Synthesis
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 841c22cf..d4de318b 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -5,6 +5,8 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 module S = Synthesis
+open TypesUtils
+open ValuesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterBorrows
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 92ea6483..105adb5a 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -10,6 +10,13 @@ open Utils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
+(** A symbolic expansion *)
+type symbolic_expansion =
+  | SeConcrete of V.constant_value
+  | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
+  | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
+  | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
+
 (** Auxiliary function.
 
     Apply a proj_borrows on a shared borrow.
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 0b7d8f21..5e0375d0 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -126,51 +126,6 @@ exception FoundGBorrowContent of g_borrow_content
 exception FoundGLoanContent of g_loan_content
 (** Utility exception *)
 
-(** Check if a value contains a borrow *)
-let borrows_in_value (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_borrow_content _env _ = raise Found
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
-(** Check if a value contains inactivated mutable borrows *)
-let inactivated_in_value (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_InactivatedMutBorrow _env _ = raise Found
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
-(** Check if a value contains a loan *)
-let loans_in_value (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_loan_content _env _ = raise Found
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
 let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     bool =
   let obj =
@@ -201,13 +156,6 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     false
   with Found -> true
 
-(** TODO: move to InterpreterSymbolic or sth *)
-type symbolic_expansion =
-  | SeConcrete of V.constant_value
-  | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
-  | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
-  | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
-
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
     the regions which are already ended inside the abstraction don't
@@ -319,18 +267,3 @@ let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
     obj#visit_typed_avalue () v;
     false
   with Found -> true
-
-(** Return true if a type is "primitively copyable".
-  *
-  * "primitively copyable" means that copying instances of this type doesn't
-  * require calling dedicated functions defined through the Copy trait. It
-  * is the case for types like integers, shared borrows, etc.
-  *)
-let rec type_is_primitively_copyable (ty : T.ety) : bool =
-  match ty with
-  | T.Adt ((T.AdtId _ | T.Assumed _), _, _) -> false
-  | T.Adt (T.Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys
-  | T.TypeVar _ | T.Never | T.Str | T.Array _ | T.Slice _ -> false
-  | T.Bool | T.Char | T.Integer _ -> true
-  | T.Ref (_, _, T.Mut) -> false
-  | T.Ref (_, _, T.Shared) -> true
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index de482b18..85834e7a 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -6,6 +6,8 @@ module Subst = Substitute
 module A = CfimAst
 module L = Logging
 open InterpreterUtils
+open InterpreterProjectors
+(* for symbolic_expansion definition *)
 
 (* TODO: the below functions have very "rough" signatures and do nothing: I
  * defined them so that the places where we should update the synthesized
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 878ac989..a658adce 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -108,3 +108,18 @@ let ty_has_regions (ty : ety) : bool =
     obj#visit_ty () ty;
     false
   with Found -> true
+
+(** Return true if a type is "primitively copyable".
+  *
+  * "primitively copyable" means that copying instances of this type doesn't
+  * require calling dedicated functions defined through the Copy trait. It
+  * is the case for types like integers, shared borrows, etc.
+  *)
+let rec type_is_primitively_copyable (ty : ety) : bool =
+  match ty with
+  | Adt ((AdtId _ | Assumed _), _, _) -> false
+  | Adt (Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys
+  | TypeVar _ | Never | Str | Array _ | Slice _ -> false
+  | Bool | Char | Integer _ -> true
+  | Ref (_, _, Mut) -> false
+  | Ref (_, _, Shared) -> true
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 4a503a65..f4a10287 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -1,3 +1,4 @@
+open Utils
 open TypesUtils
 open Types
 open Values
@@ -12,3 +13,48 @@ 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
   mk_typed_value box_ty box_v
+
+(** Check if a value contains a borrow *)
+let borrows_in_value (v : typed_value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+
+      method! visit_borrow_content _env _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
+(** Check if a value contains inactivated mutable borrows *)
+let inactivated_in_value (v : typed_value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+
+      method! visit_InactivatedMutBorrow _env _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
+(** Check if a value contains a loan *)
+let loans_in_value (v : typed_value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+
+      method! visit_loan_content _env _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true