Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

2 files changed, 237 insertions, 269 deletions

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 245f3b77..cc0580be 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -1,25 +1,20 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module LA = LlbcAst
+open Types
+open Values
+open LlbcAst
 open Scalars
-module E = Expressions
+open Expressions
 open Utils
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module L = Logging
+open Contexts
 open TypesUtils
 open ValuesUtils
-module Inv = Invariants
-module S = SynthesizeSymbolic
+open SynthesizeSymbolic
 open Cps
 open InterpreterUtils
 open InterpreterExpansion
 open InterpreterPaths
 
 (** The local logger *)
-let log = L.expressions_log
+let log = Logging.expressions_log
 
 (** As long as there are symbolic values at a given place (potentially in subvalues)
     which contain borrows and are primitively copyable, expand them.
@@ -29,8 +24,8 @@ let log = L.expressions_log
     Note that the place should have been prepared so that there are no remaining
     loans.
 *)
-let expand_primitively_copyable_at_place (config : C.config)
-    (access : access_kind) (p : E.place) : cm_fun =
+let expand_primitively_copyable_at_place (config : config)
+    (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Small helper *)
   let rec expand : cm_fun =
@@ -43,8 +38,7 @@ let expand_primitively_copyable_at_place (config : C.config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config sv
-            (Some (S.mk_mplace p ctx))
+          expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx))
         in
         comp cc expand cf ctx
   in
@@ -56,8 +50,8 @@ let expand_primitively_copyable_at_place (config : C.config)
     We also check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
-let read_place (access : access_kind) (p : E.place)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
+    m_fun =
  fun ctx ->
   let v = read_place access p ctx in
   (* Check that there are no bottoms in the value *)
@@ -67,9 +61,9 @@ let read_place (access : access_kind) (p : E.place)
   (* Call the continuation *)
   cf v ctx
 
-let access_rplace_reorganize_and_read (config : C.config)
-    (expand_prim_copy : bool) (access : access_kind) (p : E.place)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let access_rplace_reorganize_and_read (config : config)
+    (expand_prim_copy : bool) (access : access_kind) (p : place)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Make sure we can evaluate the path *)
   let cc = update_ctx_along_read_place config access p in
@@ -87,31 +81,30 @@ let access_rplace_reorganize_and_read (config : C.config)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
-    (access : access_kind) (p : E.place) : cm_fun =
+let access_rplace_reorganize (config : config) (expand_prim_copy : bool)
+    (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   access_rplace_reorganize_and_read config expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
 (** Convert an operand constant operand value to a typed value *)
-let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) :
-    V.typed_value =
+let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value =
   (* Check the type while converting - we actually need some information
      * contained in the type *)
   log#ldebug
     (lazy
       ("literal_to_typed_value:" ^ "\n- cv: "
-      ^ Print.PrimitiveValues.literal_to_string cv));
+      ^ Print.Values.literal_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
-  | PV.Bool, Bool v -> { V.value = V.Literal (Bool v); ty = T.Literal ty }
-  | Char, Char v -> { V.value = V.Literal (Char v); ty = T.Literal ty }
-  | Integer int_ty, PV.Scalar v ->
+  | TBool, VBool v -> { value = VLiteral (VBool v); ty = TLiteral ty }
+  | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty }
+  | TInteger int_ty, VScalar v ->
       (* Check the type and the ranges *)
       assert (int_ty = v.int_ty);
       assert (check_scalar_value_in_range v);
-      { V.value = V.Literal (PV.Scalar v); ty = T.Literal ty }
+      { value = VLiteral (VScalar v); ty = TLiteral ty }
   (* Remaining cases (invalid) *)
   | _, _ -> raise (Failure "Improperly typed constant value")
 
@@ -126,8 +119,8 @@ let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) :
     parameter to control this copy ([allow_adt_copy]). Note that here by ADT we
     mean the user-defined ADTs (not tuples or assumed types).
  *)
-let rec copy_value (allow_adt_copy : bool) (config : C.config)
-    (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
+let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
+    (v : typed_value) : eval_ctx * typed_value =
   log#ldebug
     (lazy
       ("copy_value: "
@@ -137,18 +130,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
    * we reverted the changes: the result was less clear actually. In particular,
    * the fact that we have exhaustive matches below makes very obvious the cases
    * in which we need to fail *)
-  match v.V.value with
-  | V.Literal _ -> (ctx, v)
-  | V.Adt av ->
+  match v.value with
+  | VLiteral _ -> (ctx, v)
+  | VAdt av ->
       (* Sanity check *)
-      (match v.V.ty with
-      | T.Adt (T.Assumed T.Box, _) ->
+      (match v.ty with
+      | TAdt (TAssumed TBox, _) ->
           raise (Failure "Can't copy an assumed value other than Option")
-      | T.Adt (T.AdtId _, _) as ty ->
+      | TAdt (TAdtId _, _) as ty ->
           assert (allow_adt_copy || ty_is_primitively_copyable ty)
-      | T.Adt (T.Tuple, _) -> () (* Ok *)
-      | T.Adt
-          ( T.Assumed (Slice | T.Array),
+      | TAdt (TTuple, _) -> () (* Ok *)
+      | TAdt
+          ( TAssumed (TSlice | TArray),
             {
               regions = [];
               types = [ ty ];
@@ -162,33 +155,33 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
           (copy_value allow_adt_copy config)
           ctx av.field_values
       in
-      (ctx, { v with V.value = V.Adt { av with field_values = fields } })
-  | V.Bottom -> raise (Failure "Can't copy ⊥")
-  | V.Borrow bc -> (
+      (ctx, { v with value = VAdt { av with field_values = fields } })
+  | VBottom -> raise (Failure "Can't copy ⊥")
+  | VBorrow bc -> (
       (* We can only copy shared borrows *)
       match bc with
-      | SharedBorrow bid ->
+      | VSharedBorrow bid ->
           (* We need to create a new borrow id for the copied borrow, and
            * update the context accordingly *)
-          let bid' = C.fresh_borrow_id () in
+          let bid' = fresh_borrow_id () in
           let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
-          (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
-      | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
-      | V.ReservedMutBorrow _ ->
+          (ctx, { v with value = VBorrow (VSharedBorrow bid') })
+      | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
+      | VReservedMutBorrow _ ->
           raise (Failure "Can't copy a reserved mut borrow"))
-  | V.Loan lc -> (
+  | VLoan lc -> (
       (* We can only copy shared loans *)
       match lc with
-      | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
-      | V.SharedLoan (_, sv) ->
+      | VMutLoan _ -> raise (Failure "Can't copy a mutable loan")
+      | VSharedLoan (_, sv) ->
           (* We don't copy the shared loan: only the shared value inside *)
           copy_value allow_adt_copy config ctx sv)
-  | V.Symbolic sp ->
+  | VSymbolic sp ->
       (* We can copy only if the type is "primitively" copyable.
        * Note that in the general case, copy is a trait: copying values
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
-      assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty));
+      assert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty));
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
        * is symbolic expansion. The important subcase is the expansion of shared
@@ -233,22 +226,21 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
-    cm_fun =
+let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
     match op with
-    | E.Constant _ ->
+    | Constant _ ->
         (* No need to reorganize the context *)
         cf ctx
-    | E.Copy p ->
+    | Copy p ->
         (* Access the value *)
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
         access_rplace_reorganize config expand_prim_copy access p cf ctx
-    | E.Move p ->
+    | Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
@@ -258,8 +250,8 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
   prepare cf ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
-let eval_operand_no_reorganize (config : C.config) (op : E.operand)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let eval_operand_no_reorganize (config : config) (op : operand)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
@@ -268,14 +260,14 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | E.Constant cv -> (
+  | Constant cv -> (
       match cv.value with
-      | E.CLiteral lit ->
-          cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
-      | E.CTraitConst (trait_ref, generics, const_name) -> (
-          assert (generics = TypesUtils.mk_empty_generic_args);
+      | CLiteral lit ->
+          cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx
+      | CTraitConst (trait_ref, generics, const_name) -> (
+          assert (generics = empty_generic_args);
           match trait_ref.trait_id with
-          | T.TraitImpl _ ->
+          | TraitImpl _ ->
               (* This shouldn't happen: if we refer to a concrete implementation, we
                  should directly refer to the top-level constant *)
               raise (Failure "Unreachable")
@@ -285,14 +277,13 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
               let ctx0 = ctx in
               (* Lookup the trait declaration to retrieve the type of the symbolic value *)
               let trait_decl =
-                C.ctx_lookup_trait_decl ctx
-                  trait_ref.trait_decl_ref.trait_decl_id
+                ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id
               in
               let _, (ty, _) =
                 List.find (fun (name, _) -> name = const_name) trait_decl.consts
               in
               (* Introduce a fresh symbolic value *)
-              let v = mk_fresh_symbolic_typed_value_from_ety V.TraitConst ty in
+              let v = mk_fresh_symbolic_typed_value TraitConst ty in
               (* Continue the evaluation *)
               let e = cf v ctx in
               (* We have to wrap the generated expression *)
@@ -304,13 +295,13 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
                        ( ctx0,
                          None,
                          value_as_symbolic v.value,
-                         SymbolicAst.TraitConstValue
+                         SymbolicAst.VaTraitConstValue
                            (trait_ref, generics, const_name),
                          e ))))
-      | E.CVar vid -> (
+      | CVar vid -> (
           let ctx0 = ctx in
           (* Lookup the const generic value *)
-          let cv = C.ctx_lookup_const_generic_value ctx vid in
+          let cv = ctx_lookup_const_generic_value ctx vid in
           (* Copy the value *)
           let allow_adt_copy = false in
           let ctx, v = copy_value allow_adt_copy config ctx cv in
@@ -322,17 +313,17 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
           | Some e ->
               (* If we are synthesizing a symbolic AST, it means that we are in symbolic
                  mode: the value of the const generic is necessarily symbolic. *)
-              assert (is_symbolic cv.V.value);
+              assert (is_symbolic cv.value);
               (* *)
               Some
                 (SymbolicAst.IntroSymbolic
                    ( ctx0,
                      None,
                      value_as_symbolic v.value,
-                     SymbolicAst.ConstGenericValue vid,
+                     SymbolicAst.VaCgValue vid,
                      e )))
-      | E.CFnPtr _ -> raise (Failure "TODO"))
-  | E.Copy p ->
+      | CFnPtr _ -> raise (Failure "TODO"))
+  | Copy p ->
       (* Access the value *)
       let access = Read in
       let cc = read_place access p in
@@ -353,7 +344,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
       in
       (* Compose and apply *)
       comp cc copy cf ctx
-  | E.Move p ->
+  | Move p ->
       (* Access the value *)
       let access = Move in
       let cc = read_place access p in
@@ -362,15 +353,15 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
         assert (not (bottom_in_value ctx.ended_regions v));
-        let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
+        let bottom : typed_value = { value = VBottom; ty = v.ty } in
         let ctx = write_place access p bottom ctx in
         cf v ctx
       in
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (config : C.config) (op : E.operand)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
+    m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
@@ -387,13 +378,13 @@ let eval_operand (config : C.config) (op : E.operand)
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list)
-    : cm_fun =
+let prepare_eval_operands_reorganize (config : config) (ops : operand list) :
+    cm_fun =
   fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
 
 (** Evaluate several operands. *)
-let eval_operands (config : C.config) (ops : E.operand list)
-    (cf : V.typed_value list -> m_fun) : m_fun =
+let eval_operands (config : config) (ops : operand list)
+    (cf : typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
   let prepare = prepare_eval_operands_reorganize config ops in
@@ -404,8 +395,8 @@ let eval_operands (config : C.config) (ops : E.operand list)
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand)
-    (cf : V.typed_value * V.typed_value -> m_fun) : m_fun =
+let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
+    (cf : typed_value * typed_value -> m_fun) : m_fun =
   let eval_op = eval_operands config [ op1; op2 ] in
   let use_res cf res =
     match res with
@@ -414,73 +405,73 @@ let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand)
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
   let eval_op = eval_operand config op in
   (* Apply the unop *)
-  let apply cf (v : V.typed_value) : m_fun =
-    match (unop, v.V.value) with
-    | E.Not, V.Literal (Bool b) ->
-        cf (Ok { v with V.value = V.Literal (Bool (not b)) })
-    | E.Neg, V.Literal (PV.Scalar sv) -> (
-        let i = Z.neg sv.PV.value in
+  let apply cf (v : typed_value) : m_fun =
+    match (unop, v.value) with
+    | Not, VLiteral (VBool b) ->
+        cf (Ok { v with value = VLiteral (VBool (not b)) })
+    | Neg, VLiteral (VScalar sv) -> (
+        let i = Z.neg sv.value in
         match mk_scalar sv.int_ty i with
         | Error _ -> cf (Error EPanic)
-        | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) }))
-    | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.Literal (PV.Scalar sv) -> (
+        | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) }))
+    | Cast (CastInteger (src_ty, tgt_ty)), VLiteral (VScalar sv) -> (
         assert (src_ty = sv.int_ty);
-        let i = sv.PV.value in
+        let i = sv.value in
         match mk_scalar tgt_ty i with
         | Error _ -> cf (Error EPanic)
         | Ok sv ->
-            let ty = T.Literal (Integer tgt_ty) in
-            let value = V.Literal (PV.Scalar sv) in
-            cf (Ok { V.ty; value }))
+            let ty = TLiteral (TInteger tgt_ty) in
+            let value = VLiteral (VScalar sv) in
+            cf (Ok { ty; value }))
     | _ -> raise (Failure "Invalid input for unop")
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
   let eval_op = eval_operand config op in
   (* Generate a fresh symbolic value to store the result *)
-  let apply cf (v : V.typed_value) : m_fun =
+  let apply cf (v : typed_value) : m_fun =
    fun ctx ->
-    let res_sv_id = C.fresh_symbolic_value_id () in
+    let res_sv_id = fresh_symbolic_value_id () in
     let res_sv_ty =
-      match (unop, v.V.ty) with
-      | E.Not, (T.Literal Bool as lty) -> lty
-      | E.Neg, (T.Literal (Integer _) as lty) -> lty
-      | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.Literal (Integer tgt_ty)
+      match (unop, v.ty) with
+      | Not, (TLiteral TBool as lty) -> lty
+      | Neg, (TLiteral (TInteger _) as lty) -> lty
+      | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty)
       | _ -> raise (Failure "Invalid input for unop")
     in
     let res_sv =
-      { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+      { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
     in
     (* Call the continuation *)
     let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
     (* Synthesize the symbolic AST *)
-    S.synthesize_unary_op ctx unop v
-      (S.mk_opt_place_from_op op ctx)
+    synthesize_unary_op ctx unop v
+      (mk_opt_place_from_op op ctx)
       res_sv None expr
   in
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op (config : config) (unop : unop) (op : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | C.ConcreteMode -> eval_unary_op_concrete config unop op cf
-  | C.SymbolicMode -> eval_unary_op_symbolic config unop op cf
+  | ConcreteMode -> eval_unary_op_concrete config unop op cf
+  | SymbolicMode -> eval_unary_op_symbolic config unop op cf
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
  *)
-let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
-    (v2 : V.typed_value) : (V.typed_value, eval_error) result =
+let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
+    (v2 : typed_value) : (typed_value, eval_error) result =
   (* Equality check binops (Eq, Ne) accept values from a wide variety of types.
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
@@ -489,53 +480,52 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
     (* Equality/inequality check is primitive only for a subset of types *)
     assert (ty_is_primitively_copyable v1.ty);
     let b = v1 = v2 in
-    Ok { V.value = V.Literal (Bool b); ty = T.Literal Bool })
+    Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
     (* For the non-equality operations, the input values are necessarily scalars *)
-    match (v1.V.value, v2.V.value) with
-    | V.Literal (PV.Scalar sv1), V.Literal (PV.Scalar sv2) -> (
+    match (v1.value, v2.value) with
+    | VLiteral (VScalar sv1), VLiteral (VScalar sv2) -> (
         (* There are binops which require the two operands to have the same
            type, and binops for which it is not the case.
            There are also binops which return booleans, and binops which
            return integers.
         *)
         match binop with
-        | E.Lt | E.Le | E.Ge | E.Gt ->
+        | Lt | Le | Ge | Gt ->
             (* The two operands must have the same type and the result is a boolean *)
             assert (sv1.int_ty = sv2.int_ty);
             let b =
               match binop with
-              | E.Lt -> Z.lt sv1.PV.value sv2.PV.value
-              | E.Le -> Z.leq sv1.PV.value sv2.PV.value
-              | E.Ge -> Z.geq sv1.PV.value sv2.PV.value
-              | E.Gt -> Z.gt sv1.PV.value sv2.PV.value
-              | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
-              | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
+              | Lt -> Z.lt sv1.value sv2.value
+              | Le -> Z.leq sv1.value sv2.value
+              | Ge -> Z.geq sv1.value sv2.value
+              | Gt -> Z.gt sv1.value sv2.value
+              | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
+              | Shr | Ne | Eq ->
                   raise (Failure "Unreachable")
             in
             Ok
-              ({ V.value = V.Literal (Bool b); ty = T.Literal Bool }
-                : V.typed_value)
-        | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr
-          -> (
+              ({ value = VLiteral (VBool b); ty = TLiteral TBool }
+                : typed_value)
+        | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
             (* The two operands must have the same type and the result is an integer *)
             assert (sv1.int_ty = sv2.int_ty);
             let res =
               match binop with
-              | E.Div ->
-                  if sv2.PV.value = Z.zero then Error ()
-                  else mk_scalar sv1.int_ty (Z.div sv1.PV.value sv2.PV.value)
-              | E.Rem ->
+              | Div ->
+                  if sv2.value = Z.zero then Error ()
+                  else mk_scalar sv1.int_ty (Z.div sv1.value sv2.value)
+              | Rem ->
                   (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
-                  if sv2.PV.value = Z.zero then Error ()
-                  else mk_scalar sv1.int_ty (Z.rem sv1.PV.value sv2.PV.value)
-              | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.PV.value sv2.PV.value)
-              | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.PV.value sv2.PV.value)
-              | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.PV.value sv2.PV.value)
-              | E.BitXor -> raise Unimplemented
-              | E.BitAnd -> raise Unimplemented
-              | E.BitOr -> raise Unimplemented
-              | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq ->
+                  if sv2.value = Z.zero then Error ()
+                  else mk_scalar sv1.int_ty (Z.rem sv1.value sv2.value)
+              | Add -> mk_scalar sv1.int_ty (Z.add sv1.value sv2.value)
+              | Sub -> mk_scalar sv1.int_ty (Z.sub sv1.value sv2.value)
+              | Mul -> mk_scalar sv1.int_ty (Z.mul sv1.value sv2.value)
+              | BitXor -> raise Unimplemented
+              | BitAnd -> raise Unimplemented
+              | BitOr -> raise Unimplemented
+              | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
                   raise (Failure "Unreachable")
             in
             match res with
@@ -543,97 +533,93 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
             | Ok sv ->
                 Ok
                   {
-                    V.value = V.Literal (PV.Scalar sv);
-                    ty = T.Literal (Integer sv1.int_ty);
+                    value = VLiteral (VScalar sv);
+                    ty = TLiteral (TInteger sv1.int_ty);
                   })
-        | E.Shl | E.Shr -> raise Unimplemented
-        | E.Ne | E.Eq -> raise (Failure "Unreachable"))
+        | Shl | Shr -> raise Unimplemented
+        | Ne | Eq -> raise (Failure "Unreachable"))
     | _ -> raise (Failure "Invalid inputs for binop")
 
-let eval_binary_op_concrete (config : C.config) (binop : E.binop)
-    (op1 : E.operand) (op2 : E.operand)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
+    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
   let eval_ops = eval_two_operands config op1 op2 in
   (* Compute the result of the binop *)
-  let compute cf (res : V.typed_value * V.typed_value) =
+  let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
     cf (eval_binary_op_concrete_compute binop v1 v2)
   in
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
-    (op1 : E.operand) (op2 : E.operand)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
+    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
   let eval_ops = eval_two_operands config op1 op2 in
   (* Compute the result of applying the binop *)
-  let compute cf ((v1, v2) : V.typed_value * V.typed_value) : m_fun =
+  let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
    fun ctx ->
     (* Generate a fresh symbolic value to store the result *)
-    let res_sv_id = C.fresh_symbolic_value_id () in
+    let res_sv_id = fresh_symbolic_value_id () in
     let res_sv_ty =
       if binop = Eq || binop = Ne then (
         (* Equality operations *)
         assert (v1.ty = v2.ty);
         (* Equality/inequality check is primitive only for a subset of types *)
         assert (ty_is_primitively_copyable v1.ty);
-        T.Literal Bool)
+        TLiteral TBool)
       else
         (* Other operations: input types are integers *)
-        match (v1.V.ty, v2.V.ty) with
-        | T.Literal (Integer int_ty1), T.Literal (Integer int_ty2) -> (
+        match (v1.ty, v2.ty) with
+        | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
             match binop with
-            | E.Lt | E.Le | E.Ge | E.Gt ->
+            | Lt | Le | Ge | Gt ->
                 assert (int_ty1 = int_ty2);
-                T.Literal Bool
-            | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
-            | E.BitOr ->
+                TLiteral TBool
+            | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
                 assert (int_ty1 = int_ty2);
-                T.Literal (Integer int_ty1)
-            | E.Shl | E.Shr -> raise Unimplemented
-            | E.Ne | E.Eq -> raise (Failure "Unreachable"))
+                TLiteral (TInteger int_ty1)
+            | Shl | Shr -> raise Unimplemented
+            | Ne | Eq -> raise (Failure "Unreachable"))
         | _ -> raise (Failure "Invalid inputs for binop")
     in
     let res_sv =
-      { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+      { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
     in
     (* Call the continuattion *)
     let v = mk_typed_value_from_symbolic_value res_sv in
     let expr = cf (Ok v) ctx in
     (* Synthesize the symbolic AST *)
-    let p1 = S.mk_opt_place_from_op op1 ctx in
-    let p2 = S.mk_opt_place_from_op op2 ctx in
-    S.synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
+    let p1 = mk_opt_place_from_op op1 ctx in
+    let p2 = mk_opt_place_from_op op2 ctx in
+    synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
   in
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
-    (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun
-    =
+let eval_binary_op (config : config) (binop : binop) (op1 : operand)
+    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | C.ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
-  | C.SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
+  | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
 
-let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
-  | E.Shared | E.TwoPhaseMut | E.Shallow ->
+  | BShared | BTwoPhaseMut | BShallow ->
       (* **REMARK**: we initially treated shallow borrows like shared borrows.
          In practice this restricted the behaviour too much, so for now we
          forbid them.
       *)
-      assert (bkind <> E.Shallow);
+      assert (bkind <> BShallow);
 
       (* Access the value *)
       let access =
         match bkind with
-        | E.Shared | E.Shallow -> Read
-        | E.TwoPhaseMut -> Write
+        | BShared | BShallow -> Read
+        | BTwoPhaseMut -> Write
         | _ -> raise (Failure "Unreachable")
       in
 
@@ -642,23 +628,21 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         access_rplace_reorganize_and_read config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
-      let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+      let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
        fun ctx ->
         (* Generate the fresh borrow id *)
-        let bid = C.fresh_borrow_id () in
+        let bid = fresh_borrow_id () in
         (* Compute the loan value, with which to replace the value at place p *)
         let nv =
-          match v.V.value with
-          | V.Loan (V.SharedLoan (bids, sv)) ->
+          match v.value with
+          | VLoan (VSharedLoan (bids, sv)) ->
               (* Shared loan: insert the new borrow id *)
-              let bids1 = V.BorrowId.Set.add bid bids in
-              { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
+              let bids1 = BorrowId.Set.add bid bids in
+              { v with value = VLoan (VSharedLoan (bids1, sv)) }
           | _ ->
               (* Not a shared loan: add a wrapper *)
-              let v' =
-                V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
-              in
-              { v with V.value = v' }
+              let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in
+              { v with value = v' }
         in
         (* Update the borrowed value in the context *)
         let ctx = write_place access p nv ctx in
@@ -666,27 +650,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
          * Note that the reference is *mutable* if we do a two-phase borrow *)
         let ref_kind =
           match bkind with
-          | E.Shared | E.Shallow -> T.Shared
-          | E.TwoPhaseMut -> T.Mut
+          | BShared | BShallow -> RShared
+          | BTwoPhaseMut -> RMut
           | _ -> raise (Failure "Unreachable")
         in
-        let rv_ty = T.Ref (T.Erased, v.ty, ref_kind) in
+        let rv_ty = TRef (RErased, v.ty, ref_kind) in
         let bc =
           match bkind with
-          | E.Shared | E.Shallow ->
+          | BShared | BShallow ->
               (* See the remark at the beginning of the match branch: we
                  handle shallow borrows like shared borrows *)
-              V.SharedBorrow bid
-          | E.TwoPhaseMut -> V.ReservedMutBorrow bid
+              VSharedBorrow bid
+          | BTwoPhaseMut -> VReservedMutBorrow bid
           | _ -> raise (Failure "Unreachable")
         in
-        let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
+        let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in
         (* Continue *)
         cf rv ctx
       in
       (* Compose and apply *)
       comp prepare eval cf ctx
-  | E.Mut ->
+  | BMut ->
       (* Access the value *)
       let access = Write in
       let expand_prim_copy = false in
@@ -694,16 +678,16 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         access_rplace_reorganize_and_read config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
-      let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+      let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
        fun ctx ->
         (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
-        let bid = C.fresh_borrow_id () in
-        let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
-        let rv : V.typed_value =
-          { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
+        let bid = fresh_borrow_id () in
+        let rv_ty = TRef (RErased, v.ty, RMut) in
+        let rv : typed_value =
+          { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty }
         in
         (* Compute the value with which to replace the value at place p *)
-        let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
+        let nv = { v with value = VLoan (VMutLoan bid) } in
         (* Update the value in the context *)
         let ctx = write_place access p nv ctx in
         (* Continue *)
@@ -712,102 +696,98 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (config : C.config)
-    (aggregate_kind : E.aggregate_kind) (ops : E.operand list)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
+    (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
   let eval_ops = eval_operands config ops in
   (* Compute the value *)
-  let compute (cf : V.typed_value -> m_fun) (values : V.typed_value list) :
-      m_fun =
+  let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
    fun ctx ->
     (* Match on the aggregate kind *)
     match aggregate_kind with
-    | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+    | AggregatedAdt (type_id, opt_variant_id, generics) -> (
         match type_id with
-        | Tuple ->
-            let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
-            let v = V.Adt { variant_id = None; field_values = values } in
-            let generics = TypesUtils.mk_generic_args [] tys [] [] in
-            let ty = T.Adt (T.Tuple, generics) in
-            let aggregated : V.typed_value = { V.value = v; ty } in
+        | TTuple ->
+            let tys = List.map (fun (v : typed_value) -> v.ty) values in
+            let v = VAdt { variant_id = None; field_values = values } in
+            let generics = mk_generic_args [] tys [] [] in
+            let ty = TAdt (TTuple, generics) in
+            let aggregated : typed_value = { value = v; ty } in
             (* Call the continuation *)
             cf aggregated ctx
-        | AdtId def_id ->
+        | TAdtId def_id ->
             (* Sanity checks *)
-            let type_decl = C.ctx_lookup_type_decl ctx def_id in
+            let type_decl = ctx_lookup_type_decl ctx def_id in
             assert (
               List.length type_decl.generics.regions
               = List.length generics.regions);
             let expected_field_types =
-              Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
-                generics
+              AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id
+                opt_variant_id generics
             in
             assert (
               expected_field_types
-              = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+              = List.map (fun (v : typed_value) -> v.ty) values);
             (* Construct the value *)
-            let av : V.adt_value =
-              { V.variant_id = opt_variant_id; V.field_values = values }
+            let av : adt_value =
+              { variant_id = opt_variant_id; field_values = values }
             in
-            let aty = T.Adt (T.AdtId def_id, generics) in
-            let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+            let aty = TAdt (TAdtId def_id, generics) in
+            let aggregated : typed_value = { value = VAdt av; ty = aty } in
             (* Call the continuation *)
             cf aggregated ctx
-        | Assumed _ -> raise (Failure "Unreachable"))
-    | E.AggregatedArray (ety, cg) -> (
+        | TAssumed _ -> raise (Failure "Unreachable"))
+    | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
+        assert (List.for_all (fun (v : typed_value) -> v.ty = ety) values);
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
         assert (len = Z.of_int (List.length values));
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
-        let ty = T.Adt (T.Assumed T.Array, generics) in
+        let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
            value equal to the array. The reason is that otherwise, the
            array we introduce here might be duplicated in the generated
            code: by introducing a symbolic value we introduce a let-binding
            in the generated code. *)
-        let saggregated =
-          mk_fresh_symbolic_typed_value_from_ety V.Aggregate ty
-        in
+        let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in
         (* Call the continuation *)
         match cf saggregated ctx with
         | None -> None
         | Some e ->
             (* Introduce the symbolic value in the AST *)
             let sv = ValuesUtils.value_as_symbolic saggregated.value in
-            Some (SymbolicAst.IntroSymbolic (ctx, None, sv, Array values, e)))
+            Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
   in
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
-    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_rvalue_not_global (config : config) (rvalue : rvalue)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
   (* Small helpers *)
-  let wrap_in_result (cf : (V.typed_value, eval_error) result -> m_fun)
-      (v : V.typed_value) : m_fun =
+  let wrap_in_result (cf : (typed_value, eval_error) result -> m_fun)
+      (v : typed_value) : m_fun =
     cf (Ok v)
   in
   let comp_wrap f = comp f wrap_in_result cf in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | E.Use op -> comp_wrap (eval_operand config op) ctx
-  | E.RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
-  | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
-  | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
-  | E.Aggregate (aggregate_kind, ops) ->
+  | Use op -> comp_wrap (eval_operand config op) ctx
+  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
+  | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
+  | Aggregate (aggregate_kind, ops) ->
       comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
-  | E.Discriminant _ ->
+  | Discriminant _ ->
       raise
         (Failure
            "Unreachable: discriminant reads should have been eliminated from \
             the AST")
-  | E.Global _ -> raise (Failure "Unreachable")
+  | Global _ -> raise (Failure "Unreachable")
 
-let eval_fake_read (config : C.config) (p : E.place) : cm_fun =
+let eval_fake_read (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   let expand_prim_copy = false in
   let cf_prepare cf =
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