Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

1 files changed, 9 insertions, 21 deletions

diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index 3beba610..f8d979f4 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -1,13 +1,6 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module LA = LlbcAst
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module L = Logging
-module Inv = Invariants
-module S = SynthesizeSymbolic
+open Expressions
+open Values
+open Contexts
 open Cps
 open InterpreterPaths
 
@@ -19,7 +12,7 @@ open InterpreterPaths
     This function doesn't reorganize the context to make sure we can read
     the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first.
  *)
-val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
+val read_place : access_kind -> place -> (typed_value -> m_fun) -> m_fun
 
 (** Auxiliary function.
 
@@ -38,12 +31,7 @@ val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
     primitively copyable and contain borrows.
  *)
 val access_rplace_reorganize_and_read :
-  C.config ->
-  bool ->
-  access_kind ->
-  E.place ->
-  (V.typed_value -> m_fun) ->
-  m_fun
+  config -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
 
 (** Evaluate an operand.
 
@@ -54,11 +42,11 @@ val access_rplace_reorganize_and_read :
     of the environment, before evaluating all the operands at once.
     Use {!eval_operands} instead.
  *)
-val eval_operand : C.config -> E.operand -> (V.typed_value -> m_fun) -> m_fun
+val eval_operand : config -> operand -> (typed_value -> m_fun) -> m_fun
 
 (** Evaluate several operands at once. *)
 val eval_operands :
-  C.config -> E.operand list -> (V.typed_value list -> m_fun) -> m_fun
+  config -> operand list -> (typed_value list -> m_fun) -> m_fun
 
 (** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
@@ -68,7 +56,7 @@ val eval_operands :
     reads should have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
-  C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun
+  config -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun
 
 (** Evaluate a fake read (update the context so that we can read a place) *)
-val eval_fake_read : C.config -> E.place -> cm_fun
+val eval_fake_read : config -> place -> cm_fun