Move some definitions to Contexts.ml and reactivate the warnings

3 files changed, 52 insertions, 45 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
new file mode 100644
index 00000000..be8e56fa
--- /dev/null
+++ b/src/Contexts.ml
@@ -0,0 +1,49 @@
+open Types
+open Values
+open Expressions
+open CfimAst
+open Print.Values
+open Errors
+
+type env_value = Var of VarId.id * typed_value | Abs of abs
+
+type env = env_value list
+
+let env_value_to_string (fmt : value_formatter) (ev : env_value) : string =
+  match ev with
+  | Var (vid, tv) ->
+      var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv
+  | Abs abs -> abs_to_string fmt abs
+
+let env_to_string (fmt : value_formatter) (env : env) : string =
+  "{\n"
+  ^ String.concat ";\n"
+      (List.map (fun ev -> "  " ^ env_value_to_string fmt ev) env)
+  ^ "\n}"
+
+type 'a eval_result = Stuck | Panic | Res of 'a
+
+type interpreter_mode = ConcreteMode | SymbolicMode
+
+type config = { mode : interpreter_mode; check_invariants : bool }
+
+type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id
+
+type stack_frame = { vars : var VarId.vector }
+(** A function frame
+
+    When using the interpreter in concrete mode (i.e, non symbolic) we
+    push a function frame whenever we enter a function body (and pop it
+    upon leaving it).
+ *)
+
+type eval_ctx = {
+  type_context : type_def TypeDefId.vector;
+  fun_context : fun_def FunDefId.vector;
+  type_vars : type_var TypeVarId.vector;
+  frames : stack_frame list;
+  env : env;
+  symbolic_counter : SymbolicValueId.generator;
+  borrows_counter : BorrowId.generator;
+}
+(** Evaluation context *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3b16a1e3..6e68d7b8 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -4,49 +4,7 @@ open Expressions
 open CfimAst
 open Print.Values
 open Errors
-
-type env_value = Var of VarId.id * typed_value | Abs of abs
-
-type env = env_value list
-
-let env_value_to_string (fmt : value_formatter) (ev : env_value) : string =
-  match ev with
-  | Var (vid, tv) ->
-      var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv
-  | Abs abs -> abs_to_string fmt abs
-
-let env_to_string (fmt : value_formatter) (env : env) : string =
-  "{\n"
-  ^ String.concat ";\n"
-      (List.map (fun ev -> "  " ^ env_value_to_string fmt ev) env)
-  ^ "\n}"
-
-type 'a eval_result = Stuck | Panic | Res of 'a
-
-type interpreter_mode = ConcreteMode | SymbolicMode
-
-type config = { mode : interpreter_mode; check_invariants : bool }
-
-type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id
-
-type stack_frame = { vars : var VarId.vector }
-(** A function frame
-
-    When using the interpreter in concrete mode (i.e, non symbolic) we
-    push a function frame whenever we enter a function body (and pop it
-    upon leaving it).
- *)
-
-type eval_ctx = {
-  type_context : type_def TypeDefId.vector;
-  fun_context : fun_def FunDefId.vector;
-  type_vars : type_var TypeVarId.vector;
-  frames : stack_frame list;
-  env : env;
-  symbolic_counter : SymbolicValueId.generator;
-  borrows_counter : BorrowId.generator;
-}
-(** Evaluation context *)
+open Contexts
 
 (** The following type identifies the relative position of expressions (in
     particular borrows) in other expressions.
diff --git a/src/dune b/src/dune
index 2d03b3f6..aa3e7c37 100644
--- a/src/dune
+++ b/src/dune
@@ -7,11 +7,11 @@
     :standard
     -safe-string
     -g
-    -w -8-9-11-33-20-21-26-27-39
+    -warn-error -8-9-11-33-20-21-26-27-39
   ))
   (release (flags
     :standard
     -safe-string
     -g
-    -w -8-9-11-33-20-21-26-27-39
+    -warn-error -8-9-11-33-20-21-26-27-39
   )))