Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

2 files changed, 145 insertions, 158 deletions

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 2a277c91..729a3577 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -1,10 +1,7 @@
-module T = Types
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module L = Logging
+open Types
+open Values
+open Expressions
+open Contexts
 open Cps
 open ValuesUtils
 open InterpreterUtils
@@ -14,7 +11,7 @@ open InterpreterExpansion
 module Synth = SynthesizeSymbolic
 
 (** The local logger *)
-let log = L.paths_log
+let log = Logging.paths_log
 
 (** Paths *)
 
@@ -25,26 +22,26 @@ let log = L.paths_log
     TODO: compare with borrow_lres?
 *)
 type path_fail_kind =
-  | FailSharedLoan of V.BorrowId.Set.t
+  | FailSharedLoan of BorrowId.Set.t
       (** Failure because we couldn't go inside a shared loan *)
-  | FailMutLoan of V.BorrowId.id
+  | FailMutLoan of BorrowId.id
       (** Failure because we couldn't go inside a mutable loan *)
-  | FailReservedMutBorrow of V.BorrowId.id
+  | FailReservedMutBorrow of BorrowId.id
       (** Failure because we couldn't go inside a reserved mutable borrow
           (which should get activated) *)
-  | FailSymbolic of int * V.symbolic_value
+  | FailSymbolic of int * symbolic_value
       (** Failure because we need to enter a symbolic value (and thus need to
           expand it).
           We return the number of elements which remained in the path when we
           reached the error - this allows to retrieve the path prefix, which
           is useful for the synthesis. *)
-  | FailBottom of int * E.projection_elem * T.ety
+  | FailBottom of int * projection_elem * ety
       (** Failure because we need to enter an any value - we can expand Bottom
           values if they are left values. We return the number of elements which
           remained in the path when we reached the error - this allows to
           properly update the Bottom value, if needs be.
        *)
-  | FailBorrow of V.borrow_content
+  | FailBorrow of borrow_content
       (** We got stuck because we couldn't enter a borrow *)
 [@@deriving show]
 
@@ -56,7 +53,7 @@ type path_fail_kind =
 type 'a path_access_result = ('a, path_fail_kind) result
 (** The result of reading from/writing to a place *)
 
-type updated_read_value = { read : V.typed_value; updated : V.typed_value }
+type updated_read_value = { read : typed_value; updated : typed_value }
 
 type projection_access = {
   enter_shared_loans : bool;
@@ -71,10 +68,10 @@ type projection_access = {
     
     TODO: use exceptions?
  *)
-let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
+let rec access_projection (access : projection_access) (ctx : eval_ctx)
     (* Function to (eventually) update the value we find *)
-      (update : V.typed_value -> V.typed_value) (p : E.projection)
-    (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result =
+      (update : typed_value -> typed_value) (p : projection) (v : typed_value) :
+    (eval_ctx * updated_read_value) path_access_result =
   (* For looking up/updating shared loans *)
   let ek : exploration_kind =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -86,8 +83,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       if nv.ty <> v.ty then (
         log#lerror
           (lazy
-            ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
-           ^ T.show_ety v.ty));
+            ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
+           ^ show_ety v.ty));
         raise
           (Failure
              "Assertion failed: new value doesn't have the same type as its \
@@ -95,55 +92,55 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       Ok (ctx, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
-      match (pe, v.V.value, v.V.ty) with
+      match (pe, v.value, v.ty) with
       | ( Field ((ProjAdt (_, _) as proj_kind), field_id),
-          V.Adt adt,
-          T.Adt (type_id, _) ) -> (
+          VAdt adt,
+          TAdt (type_id, _) ) -> (
           (* Check consistency *)
           (match (proj_kind, type_id) with
-          | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
+          | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
               assert (def_id = def_id');
               assert (opt_variant_id = adt.variant_id)
           | _ -> raise (Failure "Unreachable"));
           (* Actually project *)
-          let fv = T.FieldId.nth adt.field_values field_id in
+          let fv = FieldId.nth adt.field_values field_id in
           match access_projection access ctx update p' fv with
           | Error err -> Error err
           | Ok (ctx, res) ->
               (* Update the field value *)
               let nvalues =
-                T.FieldId.update_nth adt.field_values field_id res.updated
+                FieldId.update_nth adt.field_values field_id res.updated
               in
-              let nadt = V.Adt { adt with V.field_values = nvalues } in
+              let nadt = VAdt { adt with field_values = nvalues } in
               let updated = { v with value = nadt } in
               Ok (ctx, { res with updated }))
       (* Tuples *)
-      | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _) -> (
+      | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
           assert (arity = List.length adt.field_values);
-          let fv = T.FieldId.nth adt.field_values field_id in
+          let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
           match access_projection access ctx update p' fv with
           | Error err -> Error err
           | Ok (ctx, res) ->
               (* Update the field value *)
               let nvalues =
-                T.FieldId.update_nth adt.field_values field_id res.updated
+                FieldId.update_nth adt.field_values field_id res.updated
               in
-              let ntuple = V.Adt { adt with field_values = nvalues } in
+              let ntuple = VAdt { adt with field_values = nvalues } in
               let updated = { v with value = ntuple } in
               Ok (ctx, { res with updated })
           (* If we reach Bottom, it may mean we need to expand an uninitialized
            * enumeration value *))
-      | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
+      | Field ((ProjAdt (_, _) | ProjTuple _), _), VBottom, _ ->
           Error (FailBottom (1 + List.length p', pe, v.ty))
       (* Symbolic value: needs to be expanded *)
-      | _, Symbolic sp, _ ->
+      | _, VSymbolic sp, _ ->
           (* Expand the symbolic value *)
           Error (FailSymbolic (1 + List.length p', sp))
       (* Box dereferencement *)
       | ( DerefBox,
-          Adt { variant_id = None; field_values = [ bv ] },
-          T.Adt (T.Assumed T.Box, _) ) -> (
+          VAdt { variant_id = None; field_values = [ bv ] },
+          TAdt (TAssumed TBox, _) ) -> (
           (* We allow moving outside of boxes. In practice, this kind of
            * manipulations should happen only inside unsafe code, so
            * it shouldn't happen due to user code, and we leverage it
@@ -156,20 +153,20 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                 {
                   v with
                   value =
-                    V.Adt { variant_id = None; field_values = [ res.updated ] };
+                    VAdt { variant_id = None; field_values = [ res.updated ] };
                 }
               in
               Ok (ctx, { res with updated = nv }))
       (* Borrows *)
-      | Deref, V.Borrow bc, _ -> (
+      | Deref, VBorrow bc, _ -> (
           match bc with
-          | V.SharedBorrow bid ->
+          | VSharedBorrow bid ->
               (* Lookup the loan content, and explore from there *)
               if access.lookup_shared_borrows then
                 match lookup_loan ek bid ctx with
-                | _, Concrete (V.MutLoan _) ->
+                | _, Concrete (VMutLoan _) ->
                     raise (Failure "Expected a shared loan")
-                | _, Concrete (V.SharedLoan (bids, sv)) -> (
+                | _, Concrete (VSharedLoan (bids, sv)) -> (
                     (* Explore the shared value *)
                     match access_projection access ctx update p' sv with
                     | Error err -> Error err
@@ -178,23 +175,23 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                            by {!access_projection} *)
                         let ctx =
                           update_loan ek bid
-                            (V.SharedLoan (bids, res.updated))
+                            (VSharedLoan (bids, res.updated))
                             ctx
                         in
                         (* Return - note that we don't need to update the borrow itself *)
                         Ok (ctx, { res with updated = v }))
                 | ( _,
                     Abstract
-                      ( V.AMutLoan (_, _)
-                      | V.AEndedMutLoan
+                      ( AMutLoan (_, _)
+                      | AEndedMutLoan
                           { given_back = _; child = _; given_back_meta = _ }
-                      | V.AEndedSharedLoan (_, _)
-                      | V.AIgnoredMutLoan (_, _)
-                      | V.AEndedIgnoredMutLoan
+                      | AEndedSharedLoan (_, _)
+                      | AIgnoredMutLoan (_, _)
+                      | AEndedIgnoredMutLoan
                           { given_back = _; child = _; given_back_meta = _ }
-                      | V.AIgnoredSharedLoan _ ) ) ->
+                      | AIgnoredSharedLoan _ ) ) ->
                     raise (Failure "Expected a shared (abstraction) loan")
-                | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> (
+                | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
                     (* Explore the shared value *)
                     match access_projection access ctx update p' sv with
                     | Error err -> Error err
@@ -202,37 +199,34 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                         (* Relookup the child avalue *)
                         let av =
                           match lookup_loan ek bid ctx with
-                          | _, Abstract (V.ASharedLoan (_, _, av)) -> av
+                          | _, Abstract (ASharedLoan (_, _, av)) -> av
                           | _ -> raise (Failure "Unexpected")
                         in
                         (* Update the shared loan with the new value returned
                              by {!access_projection} *)
                         let ctx =
                           update_aloan ek bid
-                            (V.ASharedLoan (bids, res.updated, av))
+                            (ASharedLoan (bids, res.updated, av))
                             ctx
                         in
                         (* Return - note that we don't need to update the borrow itself *)
                         Ok (ctx, { res with updated = v }))
               else Error (FailBorrow bc)
-          | V.ReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
-          | V.MutBorrow (bid, bv) ->
+          | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
+          | VMutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
                 match access_projection access ctx update p' bv with
                 | Error err -> Error err
                 | Ok (ctx, res) ->
                     let nv =
-                      {
-                        v with
-                        value = V.Borrow (V.MutBorrow (bid, res.updated));
-                      }
+                      { v with value = VBorrow (VMutBorrow (bid, res.updated)) }
                     in
                     Ok (ctx, { res with updated = nv })
               else Error (FailBorrow bc))
-      | _, V.Loan lc, _ -> (
+      | _, VLoan lc, _ -> (
           match lc with
-          | V.MutLoan bid -> Error (FailMutLoan bid)
-          | V.SharedLoan (bids, sv) ->
+          | VMutLoan bid -> Error (FailMutLoan bid)
+          | VSharedLoan (bids, sv) ->
               (* If we can enter shared loan, we ignore the loan. Pay attention
                  to the fact that we need to reexplore the *whole* place (i.e,
                  we mustn't ignore the current projection element *)
@@ -241,18 +235,15 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                 | Error err -> Error err
                 | Ok (ctx, res) ->
                     let nv =
-                      {
-                        v with
-                        value = V.Loan (V.SharedLoan (bids, res.updated));
-                      }
+                      { v with value = VLoan (VSharedLoan (bids, res.updated)) }
                     in
                     Ok (ctx, { res with updated = nv })
               else Error (FailSharedLoan bids))
-      | (_, (V.Literal _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
+      | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r ->
           let pe, v, ty = r in
-          let pe = "- pe: " ^ E.show_projection_elem pe in
-          let v = "- v:\n" ^ V.show_value v in
-          let ty = "- ty:\n" ^ T.show_ety ty in
+          let pe = "- pe: " ^ show_projection_elem pe in
+          let v = "- v:\n" ^ show_value v in
+          let ty = "- ty:\n" ^ show_ety ty in
           log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
           raise (Failure "Inconsistent projection"))
 
@@ -264,16 +255,16 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
  *)
 let access_place (access : projection_access)
     (* Function to (eventually) update the value we find *)
-      (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx)
-    : (C.eval_ctx * V.typed_value) path_access_result =
+      (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
+    (eval_ctx * typed_value) path_access_result =
   (* Lookup the variable's value *)
-  let value = C.ctx_lookup_var_value ctx p.var_id in
+  let value = ctx_lookup_var_value ctx p.var_id in
   (* Apply the projection *)
   match access_projection access ctx update p.projection value with
   | Error err -> Error err
   | Ok (ctx, res) ->
       (* Update the value *)
-      let ctx = C.ctx_update_var_value ctx p.var_id res.updated in
+      let ctx = ctx_update_var_value ctx p.var_id res.updated in
       (* Return *)
       Ok (ctx, res.read)
 
@@ -309,8 +300,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
-    V.typed_value path_access_result =
+let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
+    typed_value path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
   let update v = v in
@@ -324,22 +315,21 @@ let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
         if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
-            ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
-            ^ C.show_env ctx.env
+            ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
           in
           log#serror msg;
           raise (Failure "Unexpected environment update"));
       Ok read_value
 
-let read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
-    V.typed_value =
+let read_place (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value
+    =
   match try_read_place access p ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
-let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
-    (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
+let try_write_place (access : access_kind) (p : place) (nv : typed_value)
+    (ctx : eval_ctx) : eval_ctx path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
   let update _ = nv in
@@ -349,41 +339,42 @@ let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
       (* We ignore the read value *)
       Ok ctx
 
-let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+let write_place (access : access_kind) (p : place) (nv : typed_value)
+    (ctx : eval_ctx) : eval_ctx =
   match try_write_place access p nv ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok ctx -> ctx
 
-let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
-    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (generics : T.egeneric_args) : V.typed_value =
+let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id)
+    (opt_variant_id : VariantId.id option) (generics : generic_args) :
+    typed_value =
+  assert (TypesUtils.generic_args_only_erased_regions generics);
   (* Lookup the definition and check if it is an enumeration - it
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
-  let def = C.ctx_lookup_type_decl ctx def_id in
-  assert (List.length generics.regions = List.length def.T.generics.regions);
+  let def = ctx_lookup_type_decl ctx def_id in
+  assert (List.length generics.regions = List.length def.generics.regions);
   (* Compute the field types *)
   let field_types =
-    Assoc.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id generics
+    AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id
+      generics
   in
   (* Initialize the expanded value *)
   let fields = List.map mk_bottom field_types in
-  let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
-  let ty = T.Adt (T.AdtId def_id, generics) in
-  { V.value = av; V.ty }
+  let av = VAdt { variant_id = opt_variant_id; field_values = fields } in
+  let ty = TAdt (TAdtId def_id, generics) in
+  { value = av; ty }
 
-let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
-    V.typed_value =
+let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value =
   (* Generate the field values *)
   let fields = List.map mk_bottom field_types in
-  let v = V.Adt { variant_id = None; field_values = fields } in
+  let v = VAdt { variant_id = None; field_values = fields } in
   let generics = TypesUtils.mk_generic_args [] field_types [] [] in
-  let ty = T.Adt (T.Tuple, generics) in
-  { V.value = v; V.ty }
+  let ty = TAdt (TTuple, generics) in
+  { value = v; ty }
 
-(** Auxiliary helper to expand {!V.Bottom} values.
+(** Auxiliary helper to expand {!Bottom} values.
 
     During compilation, rustc desaggregates the ADT initializations. The
     consequence is that the following rust code:
@@ -399,19 +390,19 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     ]}
 
     The consequence is that we may sometimes need to write fields to values
-    which are currently {!V.Bottom}. When doing this, we first expand the value
+    which are currently {!Bottom}. When doing this, we first expand the value
     to, say, [Cons Bottom Bottom] (note that field projection contains information
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
 *)
-let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
-    (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+let expand_bottom_value_from_projection (access : access_kind) (p : place)
+    (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) :
+    eval_ctx =
   (* Debugging *)
   log#ldebug
     (lazy
       ("expand_bottom_value_from_projection:\n" ^ "pe: "
-     ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));
+     ^ show_projection_elem pe ^ "\n" ^ "ty: " ^ show_ety ty));
   (* Prepare the update: we need to take the proper prefix of the place
      during whose evaluation we got stuck *)
   let projection' =
@@ -421,41 +412,40 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
   in
   let p' = { p with projection = projection' } in
   (* Compute the expanded value.
-     The type of the {!V.Bottom} value should be a tuple or an ADT.
+     The type of the {!Bottom} value should be a tuple or an AD
      Note that the projection element we got stuck at should be a
-     field projection, and gives the variant id if the {!V.Bottom} value
+     field projection, and gives the variant id if the {!Bottom} value
      is an enumeration value.
      Also, the expanded value should be the proper ADT variant or a tuple
-     with the proper arity, with all the fields initialized to {!V.Bottom}
+     with the proper arity, with all the fields initialized to {!Bottom}
   *)
   let nv =
     match (pe, ty) with
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
-        T.Adt (T.AdtId def_id', generics) ) ->
+        TAdt (TAdtId def_id', generics) ) ->
         assert (def_id = def_id');
         compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
-        T.Adt
-          ( T.Tuple,
-            { T.regions = []; types; const_generics = []; trait_refs = [] } ) )
-      ->
+        TAdt
+          (TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
+      ) ->
         assert (arity = List.length types);
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value types
     | _ ->
         raise
           (Failure
-             ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
+             ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty))
   in
   (* Update the context by inserting the expanded value at the proper place *)
   match try_write_place access p' nv ctx with
   | Ok ctx -> ctx
   | Error _ -> raise (Failure "Unreachable")
 
-let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
-    (p : E.place) : cm_fun =
+let rec update_ctx_along_read_place (config : config) (access : access_kind)
+    (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
   match try_read_place access p ctx with
@@ -476,14 +466,14 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
             expand_symbolic_value_no_branching config sp
               (Some (Synth.mk_mplace prefix ctx))
         | FailBottom (_, _, _) ->
-            (* We can't expand {!V.Bottom} values while reading them *)
+            (* We can't expand {!Bottom} values while reading them *)
             raise (Failure "Found [Bottom] while reading a place")
         | FailBorrow _ -> raise (Failure "Could not read a borrow")
       in
       comp cc (update_ctx_along_read_place config access p) cf ctx
 
-let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
-    (p : E.place) : cm_fun =
+let rec update_ctx_along_write_place (config : config) (access : access_kind)
+    (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
@@ -501,7 +491,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
             expand_symbolic_value_no_branching config sp
               (Some (Synth.mk_mplace p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
-            (* Expand the {!V.Bottom} value *)
+            (* Expand the {!Bottom} value *)
             fun cf ctx ->
              let ctx =
                expand_bottom_value_from_projection access p remaining_pes pe ty
@@ -516,8 +506,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-let rec end_loans_at_place (config : C.config) (access : access_kind)
-    (p : E.place) : cm_fun =
+let rec end_loans_at_place (config : config) (access : access_kind) (p : place)
+    : cm_fun =
  fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
    * loans.
@@ -526,28 +516,28 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
    * *)
   let obj =
     object
-      inherit [_] V.iter_typed_value as super
+      inherit [_] iter_typed_value as super
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow _ | V.MutBorrow (_, _) ->
+        | VSharedBorrow _ | VMutBorrow (_, _) ->
             (* Nothing special to do *) super#visit_borrow_content env bc
-        | V.ReservedMutBorrow bid ->
+        | VReservedMutBorrow bid ->
             (* We need to activate reserved borrows *)
             let cc = promote_reserved_mut_borrow config bid in
             raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
         match lc with
-        | V.SharedLoan (bids, v) -> (
+        | VSharedLoan (bids, v) -> (
             (* End the loans if we need a modification access, otherwise dive into
                the shared value *)
             match access with
-            | Read -> super#visit_SharedLoan env bids v
+            | Read -> super#visit_VSharedLoan env bids v
             | Write | Move ->
                 let cc = end_borrows config bids in
                 raise (UpdateCtx cc))
-        | V.MutLoan bid ->
+        | VMutLoan bid ->
             (* We always need to end mutable borrows *)
             let cc = end_borrow config bid in
             raise (UpdateCtx cc)
@@ -571,20 +561,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
      * a recursive call to reinspect the value *)
     comp cc (end_loans_at_place config access p) cf ctx
 
-let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
+let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
   let v = read_place access p ctx in
-  let ctx = write_place access p (mk_bottom v.V.ty) ctx in
-  let dummy_id = C.fresh_dummy_var_id () in
-  let ctx = C.ctx_push_dummy_var ctx dummy_id v in
+  let ctx = write_place access p (mk_bottom v.ty) ctx in
+  let dummy_id = fresh_dummy_var_id () in
+  let ctx = ctx_push_dummy_var ctx dummy_id v in
   (* Auxiliary function *)
   let rec drop : cm_fun =
    fun cf ctx ->
     (* Read the value *)
-    let v = C.ctx_lookup_dummy_var ctx dummy_id in
+    let v = ctx_lookup_dummy_var ctx dummy_id in
     (* Check if there are loans or borrows to end *)
     let with_borrows = false in
     match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -595,8 +585,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
         (* There are: end them then retry *)
         let cc =
           match c with
-          | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids
-          | LoanContent (V.MutLoan bid) -> end_borrow config bid
+          | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids
+          | LoanContent (VMutLoan bid) -> end_borrow config bid
           | BorrowContent _ -> raise (Failure "Unreachable")
         in
         (* Retry *)
@@ -608,7 +598,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
   let cc =
     comp cc (fun cf ctx ->
         (* Pop *)
-        let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
+        let ctx, v = ctx_remove_dummy_var ctx dummy_id in
         (* Reinsert *)
         let ctx = write_place access p v ctx in
         (* Sanity check *)
@@ -619,8 +609,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
   (* Continue *)
   cc cf ctx
 
-let prepare_lplace (config : C.config) (p : E.place)
-    (cf : V.typed_value -> m_fun) : m_fun =
+let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) :
+    m_fun =
  fun ctx ->
   log#ldebug
     (lazy
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 0ff8063f..3e29b810 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -1,13 +1,8 @@
-module T = Types
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module L = Logging
+open Types
+open Values
+open Expressions
+open Contexts
 open Cps
-open InterpreterExpansion
-module Synth = SynthesizeSymbolic
 
 type access_kind = Read | Write | Move
 
@@ -18,13 +13,13 @@ type access_kind = Read | Write | Move
     updates the environment (by ending borrows, expanding symbolic values, etc.)
     until it manages to fully access the provided place.
  *)
-val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun
+val update_ctx_along_read_place : config -> access_kind -> place -> cm_fun
 
 (** Update the environment to be able to write to a place.
 
     See {!update_ctx_along_read_place}.
 *)
-val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
+val update_ctx_along_write_place : config -> access_kind -> place -> cm_fun
 
 (** Read the value at a given place.
 
@@ -34,7 +29,7 @@ val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value
+val read_place : access_kind -> place -> eval_ctx -> typed_value
 
 (** Update the value at a given place.
 
@@ -45,23 +40,25 @@ val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value
     the overwritten value contains borrows, loans, etc. and will simply
     overwrite it.
  *)
-val write_place :
-  access_kind -> E.place -> V.typed_value -> C.eval_ctx -> C.eval_ctx
+val write_place : access_kind -> place -> typed_value -> eval_ctx -> eval_ctx
 
 (** Compute an expanded tuple ⊥ value.
 
     [compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns
     [(⊥:ty0, ..., ⊥:tyn)]
  *)
-val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
+val compute_expanded_bottom_tuple_value : ety list -> typed_value
 
-(** Compute an expanded ADT ⊥ value *)
+(** Compute an expanded ADT ⊥ value.
+
+    The types in the generics should use erased regions.
+  *)
 val compute_expanded_bottom_adt_value :
-  C.eval_ctx ->
-  T.TypeDeclId.id ->
-  T.VariantId.id option ->
-  T.egeneric_args ->
-  V.typed_value
+  eval_ctx ->
+  TypeDeclId.id ->
+  VariantId.id option ->
+  generic_args ->
+  typed_value
 
 (** Drop (end) outer loans at a given place, which should be seen as an l-value
     (we will write to it later, but need to drop the loans before writing).
@@ -76,7 +73,7 @@ val compute_expanded_bottom_adt_value :
     that the place is *inside* a borrow, if we end the borrow, we won't be able
     to reinsert the value back).
  *)
-val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
+val drop_outer_loans_at_lplace : config -> place -> cm_fun
 
 (** End the loans at a given place: read the value, if it contains a loan,
     end this loan, repeat.
@@ -87,7 +84,7 @@ val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
     when moving values, we can't move a value which contains loans and thus need
     to end them, etc.
  *)
-val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
+val end_loans_at_place : config -> access_kind -> place -> cm_fun
 
 (** Small utility.
 
@@ -98,4 +95,4 @@ val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
     place. This value should not contain any outer loan (and we check it is the
     case). Note that this value is very likely to contain ⊥ subvalues.
   *)
-val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun
+val prepare_lplace : config -> place -> (typed_value -> m_fun) -> m_fun