Cleanup

8 files changed, 8 insertions, 17 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index f8a7b56b..0fe3a09a 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -27,8 +27,8 @@ let abstraction_id_counter, fresh_abstraction_id =
   AbstractionId.fresh_stateful_generator ()
 
 (** We shouldn't need to reset the global counters, but it might be good to
-    to it from time to time, every time we evaluate/synthesize a function for
-    instance.
+    do it from time to time, for instance every time we start evaluating/
+    synthesizing a function.
     
     The reasons are manifold:
     - it might prevent the counters from overflowing (although this seems
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ec15093d..2789517e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,4 +1,3 @@
-open Errors
 module L = Logging
 module T = Types
 module A = CfimAst
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index a18ccefb..1dd4d247 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -3,7 +3,6 @@ module V = Values
 module C = Contexts
 module Subst = Substitute
 module L = Logging
-open Utils
 open ValuesUtils
 open TypesUtils
 open InterpreterUtils
@@ -226,7 +225,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   (* We sometimes need to reborrow values while giving a value back due: prepare that *)
   let allow_reborrows = true in
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
+    prepare_reborrows config allow_reborrows
   in
   (* The visitor to give back the values *)
   let obj =
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 6e09c90c..bc2f5971 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -7,7 +7,6 @@ module V = Values
 module C = Contexts
 module Subst = Substitute
 module L = Logging
-open Utils
 open InterpreterUtils
 
 (** TODO: cleanup this a bit, once we have a better understanding about
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 2de06f24..345c3df3 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -10,7 +10,6 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 open TypesUtils
-open ValuesUtils
 module Inv = Invariants
 module S = Synthesis
 open InterpreterUtils
@@ -54,7 +53,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
+    prepare_reborrows config allow_reborrows
   in
   (* Visitor to apply the expansion *)
   let obj =
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 3fa824ab..036082eb 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -5,8 +5,6 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 open TypesUtils
-open ValuesUtils
-open Utils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
@@ -471,8 +469,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
     - a function to apply the reborrows in a context
     Those functions are of course stateful.
  *)
-let prepare_reborrows (config : C.config) (allow_reborrows : bool)
-    (ctx : C.eval_ctx) :
+let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
     (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
   let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -502,7 +499,7 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
   let allow_reborrows = true in
   (* Prepare the reborrows *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
+    prepare_reborrows config allow_reborrows
   in
   (* Apply the projector *)
   let av =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 40ef0d05..5f86fec2 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -6,10 +6,8 @@ module E = Expressions
 module C = Contexts
 module Subst = Substitute
 module A = CfimAst
-module L = Logging
-open TypesUtils
-open ValuesUtils
 open Utils
+open TypesUtils
 
 (** Some utilities *)
 
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 79fa4065..b0ecd554 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -71,4 +71,4 @@ let synthesize_function_call (_fid : A.fun_id)
 
 let synthesize_panic () : unit = ()
 
-let synthesize_assert (v : V.typed_value) : unit = ()
+let synthesize_assert (_v : V.typed_value) : unit = ()