Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

1 files changed, 136 insertions, 145 deletions

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index b267bb51..d7f5fcd5 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -3,26 +3,20 @@
  * some path utilities for replacement. We might change that in the future (by
  * using indices to identify the values for instance). *)
 
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module L = Logging
+open Types
+open Values
+open Contexts
 open TypesUtils
-module Inv = Invariants
-module S = SynthesizeSymbolic
 module SA = SymbolicAst
 open Cps
 open ValuesUtils
 open InterpreterUtils
 open InterpreterProjectors
-open InterpreterBorrows
+open Print.EvalCtx
+module S = SynthesizeSymbolic
 
 (** The local logger *)
-let log = L.expansion_log
+let log = Logging.expansion_log
 
 (** Projector kind *)
 type proj_kind = LoanProj | BorrowProj
@@ -53,10 +47,10 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (config : C.config)
+let apply_symbolic_expansion_to_target_avalues (config : config)
     (allow_reborrows : bool) (proj_kind : proj_kind)
-    (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+    (original_sv : symbolic_value) (expansion : symbolic_expansion)
+    (ctx : eval_ctx) : eval_ctx =
   (* Symbolic values contained in the expansion might contain already ended regions *)
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
@@ -66,7 +60,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
   (* Visitor to apply the expansion *)
   let obj =
     object (self)
-      inherit [_] C.map_eval_ctx as super
+      inherit [_] map_eval_ctx as super
 
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
@@ -94,12 +88,12 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
         (* Explore in depth first - we won't update anything: we simply
          * want to check we don't have to expand inner symbolic value *)
         match (aproj, proj_kind) with
-        | V.AEndedProjBorrows _, _ -> V.ASymbolic aproj
-        | V.AEndedProjLoans _, _ ->
+        | AEndedProjBorrows _, _ -> ASymbolic aproj
+        | AEndedProjLoans _, _ ->
             (* Explore the given back values to make sure we don't have to expand
              * anything in there *)
-            V.ASymbolic (self#visit_aproj (Some current_abs) aproj)
-        | V.AProjLoans (sv, given_back), LoanProj ->
+            ASymbolic (self#visit_aproj (Some current_abs) aproj)
+        | AProjLoans (sv, given_back), LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
@@ -107,14 +101,14 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion proj_regions
-                  ancestors_regions expansion original_sv.V.sv_ty
+                  ancestors_regions expansion original_sv.sv_ty
               in
               (* Replace *)
-              projected_value.V.value)
+              projected_value.value)
             else
               (* Not the searched symbolic value: nothing to do *)
               super#visit_ASymbolic (Some current_abs) aproj
-        | V.AProjBorrows (sv, proj_ty), BorrowProj ->
+        | AProjBorrows (sv, proj_ty), BorrowProj ->
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then
               (* Convert the symbolic expansion to a value on which we can
@@ -132,15 +126,15 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
                   proj_regions ancestors_regions expansion proj_ty
               in
               (* Replace *)
-              projected_value.V.value
+              projected_value.value
             else
               (* Not the searched symbolic value: nothing to do *)
               super#visit_ASymbolic (Some current_abs) aproj
-        | V.AProjLoans _, BorrowProj
-        | V.AProjBorrows (_, _), LoanProj
-        | V.AIgnoredProjBorrows, _ ->
+        | AProjLoans _, BorrowProj
+        | AProjBorrows (_, _), LoanProj
+        | AIgnoredProjBorrows, _ ->
             (* Nothing to do *)
-            V.ASymbolic aproj
+            ASymbolic aproj
     end
   in
   (* Apply the expansion *)
@@ -151,9 +145,9 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
 (** Auxiliary function.
     Apply a symbolic expansion to avalues in a context.
 *)
-let apply_symbolic_expansion_to_avalues (config : C.config)
-    (allow_reborrows : bool) (original_sv : V.symbolic_value)
-    (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
+let apply_symbolic_expansion_to_avalues (config : config)
+    (allow_reborrows : bool) (original_sv : symbolic_value)
+    (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
     apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
       original_sv expansion ctx
@@ -168,9 +162,8 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
     Simply replace the symbolic values (*not avalues*) in the context with
     a given value. Will break invariants if not used properly.
 *)
-let replace_symbolic_values (at_most_once : bool)
-    (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) :
-    C.eval_ctx =
+let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
+    (nv : value) (ctx : eval_ctx) : eval_ctx =
   (* Count *)
   let replaced = ref false in
   let replace () =
@@ -181,11 +174,11 @@ let replace_symbolic_values (at_most_once : bool)
   (* Visitor to apply the substitution *)
   let obj =
     object
-      inherit [_] C.map_eval_ctx as super
+      inherit [_] map_eval_ctx as super
 
-      method! visit_Symbolic env spc =
+      method! visit_VSymbolic env spc =
         if same_symbolic_id spc original_sv then replace ()
-        else super#visit_Symbolic env spc
+        else super#visit_VSymbolic env spc
     end
   in
   (* Apply the substitution *)
@@ -193,13 +186,13 @@ let replace_symbolic_values (at_most_once : bool)
   (* Return *)
   ctx
 
-let apply_symbolic_expansion_non_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+let apply_symbolic_expansion_non_borrow (config : config)
+    (original_sv : symbolic_value) (expansion : symbolic_expansion)
+    (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
   let at_most_once = false in
-  let ctx = replace_symbolic_values at_most_once original_sv nv.V.value ctx in
+  let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
   apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
@@ -211,51 +204,52 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     The function might return a list of values if the symbolic value to expand
     is an enumeration.
     
+    [generics]: mustn't contain erased regions.
     [expand_enumerations] controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (generics : T.rgeneric_args)
-    (ctx : C.eval_ctx) : V.symbolic_expansion list =
+    (kind : sv_kind) (def_id : TypeDeclId.id) (generics : generic_args)
+    (ctx : eval_ctx) : symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
-  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);
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
-    Assoc.type_decl_get_inst_norm_variants_fields_rtypes ctx def generics
+    AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
+      generics
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
     raise (Failure "Not allowed to expand enumerations with several variants");
   (* Initialize the expanded value for a given variant *)
-  let initialize
-      ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
-      V.symbolic_expansion =
+  let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
+      symbolic_expansion =
     let field_values =
-      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types
+      List.map (fun (ty : rty) -> mk_fresh_symbolic_value kind ty) field_types
     in
-    let see = V.SeAdt (variant_id, field_values) in
+    let see = SeAdt (variant_id, field_values) in
     see
   in
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
-    (field_types : T.rty list) : V.symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (kind : sv_kind)
+    (field_types : rty list) : symbolic_expansion =
   (* Generate the field values *)
   let field_values =
     List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
   in
   let variant_id = None in
-  let see = V.SeAdt (variant_id, field_values) in
+  let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
-    V.symbolic_expansion =
+let compute_expanded_symbolic_box_value (kind : sv_kind) (boxed_ty : rty) :
+    symbolic_expansion =
   (* Introduce a fresh symbolic value *)
   let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
-  let see = V.SeAdt (None, [ boxed_value ]) in
+  let see = SeAdt (None, [ boxed_value ]) in
   see
 
 (** Compute the expansion of an adt value.
@@ -263,55 +257,56 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
     The function might return a list of values if the symbolic value to expand
     is an enumeration.
 
+    [generics]: the regions shouldn't have been erased.
     [expand_enumerations] controls the expansion of enumerations: if [false], it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (adt_id : T.type_id) (generics : T.rgeneric_args)
-    (ctx : C.eval_ctx) : V.symbolic_expansion list =
+    (kind : sv_kind) (adt_id : type_id) (generics : generic_args)
+    (ctx : eval_ctx) : symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
-  | T.AdtId def_id, _, _ ->
+  | TAdtId def_id, _, _ ->
       compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
         def_id generics ctx
-  | T.Tuple, [], _ ->
+  | TTuple, [], _ ->
       [ compute_expanded_symbolic_tuple_value kind generics.types ]
-  | T.Assumed T.Box, [], [ boxed_ty ] ->
+  | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value kind boxed_ty ]
   | _ ->
       raise
         (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
 
-let expand_symbolic_value_shared_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
-    (ref_ty : T.rty) : cm_fun =
+let expand_symbolic_value_shared_borrow (config : config)
+    (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
+    (ref_ty : rty) : cm_fun =
  fun cf ctx ->
   (* First, replace the projectors on borrows.
    * The important point is that the symbolic value to expand may appear
    * several times, if it has been copied. In this case, we need to introduce
    * one fresh borrow id per instance.
    *)
-  let borrows = ref V.BorrowId.Set.empty in
+  let borrows = ref BorrowId.Set.empty in
   let fresh_borrow () =
-    let bid' = C.fresh_borrow_id () in
-    borrows := V.BorrowId.Set.add bid' !borrows;
+    let bid' = fresh_borrow_id () in
+    borrows := BorrowId.Set.add bid' !borrows;
     bid'
   in
   (* Small utility used on shared borrows in abstractions (regular borrow
    * projector and asb).
    * Returns [Some] if the symbolic value has been expanded to an asb list,
    * [None] otherwise *)
-  let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) :
-      V.abstract_shared_borrows option =
+  let reborrow_ashared proj_regions (sv : symbolic_value) (proj_ty : rty) :
+      abstract_shared_borrows option =
     if same_symbolic_id sv original_sv then
       match proj_ty with
-      | T.Ref (r, ref_ty, T.Shared) ->
+      | TRef (r, ref_ty, RShared) ->
           (* Projector over the shared value *)
-          let shared_asb = V.AsbProjReborrows (sv, ref_ty) in
+          let shared_asb = AsbProjReborrows (sv, ref_ty) in
           (* Check if the region is in the set of projected regions *)
           if region_in_set r proj_regions then
             (* In the set: we need to reborrow *)
             let bid = fresh_borrow () in
-            Some [ V.AsbBorrow bid; shared_asb ]
+            Some [ AsbBorrow bid; shared_asb ]
           else (* Not in the set: ignore *)
             Some [ shared_asb ]
       | _ -> raise (Failure "Unexpected")
@@ -322,31 +317,31 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   (* Visitor to replace the projectors on borrows *)
   let obj =
     object (self)
-      inherit [_] C.map_eval_ctx as super
+      inherit [_] map_eval_ctx as super
 
-      method! visit_Symbolic env sv =
+      method! visit_VSymbolic env sv =
         if same_symbolic_id sv original_sv then
           let bid = fresh_borrow () in
-          V.Borrow (V.SharedBorrow bid)
-        else super#visit_Symbolic env sv
+          VBorrow (VSharedBorrow bid)
+        else super#visit_VSymbolic env sv
 
-      method! visit_Abs proj_regions abs =
+      method! visit_EAbs proj_regions abs =
         assert (Option.is_none proj_regions);
-        let proj_regions = Some abs.V.regions in
-        super#visit_Abs proj_regions abs
+        let proj_regions = Some abs.regions in
+        super#visit_EAbs proj_regions abs
 
       method! visit_AProjSharedBorrow proj_regions asb =
-        let expand_asb (asb : V.abstract_shared_borrow) :
-            V.abstract_shared_borrows =
+        let expand_asb (asb : abstract_shared_borrow) : abstract_shared_borrows
+            =
           match asb with
-          | V.AsbBorrow _ -> [ asb ]
-          | V.AsbProjReborrows (sv, proj_ty) -> (
+          | AsbBorrow _ -> [ asb ]
+          | AsbProjReborrows (sv, proj_ty) -> (
               match reborrow_ashared (Option.get proj_regions) sv proj_ty with
               | None -> [ asb ]
               | Some asb -> asb)
         in
         let asb = List.concat (List.map expand_asb asb) in
-        V.AProjSharedBorrow asb
+        AProjSharedBorrow asb
 
       (** We carefully updated {!visit_ASymbolic} so that {!visit_aproj} is called
           only on child projections (i.e., projections which appear in {!AEndedProjLoans}).
@@ -363,27 +358,27 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       method! visit_ASymbolic proj_regions aproj =
         match aproj with
         | AEndedProjBorrows _ | AIgnoredProjBorrows ->
-            (* We ignore borrows *) V.ASymbolic aproj
+            (* We ignore borrows *) ASymbolic aproj
         | AProjLoans _ ->
             (* Loans are handled later *)
-            V.ASymbolic aproj
+            ASymbolic aproj
         | AProjBorrows (sv, proj_ty) -> (
             (* Check if we need to reborrow *)
             match reborrow_ashared (Option.get proj_regions) sv proj_ty with
             | None -> super#visit_ASymbolic proj_regions aproj
-            | Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
+            | Some asb -> ABorrow (AProjSharedBorrow asb))
         | AEndedProjLoans _ ->
             (* Sanity check: make sure there is nothing to expand inside the
              * children projections *)
-            V.ASymbolic (self#visit_aproj proj_regions aproj)
+            ASymbolic (self#visit_aproj proj_regions aproj)
     end
   in
   (* Call the visitor *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  assert (not (V.BorrowId.Set.is_empty bids));
-  let see = V.SeSharedRef (bids, shared_sv) in
+  assert (not (BorrowId.Set.is_empty bids));
+  let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
     apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
@@ -396,28 +391,26 @@ let expand_symbolic_value_shared_borrow (config : C.config)
     expr
 
 (** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
-    (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
-    cm_fun =
+let expand_symbolic_value_borrow (config : config)
+    (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
+    (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
+  assert (region <> RErased);
   (* Check that we are allowed to expand the reference *)
   assert (not (region_in_set region ctx.ended_regions));
   (* Match on the reference kind *)
   match rkind with
-  | T.Mut ->
+  | RMut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
       let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
-      let bid = C.fresh_borrow_id () in
-      let see = V.SeMutRef (bid, sv) in
+      let bid = fresh_borrow_id () in
+      let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
        * check that we perform exactly one substitution) *)
       let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
       let at_most_once = true in
-      let ctx =
-        replace_symbolic_values at_most_once original_sv nv.V.value ctx
-      in
+      let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
@@ -429,7 +422,7 @@ let expand_symbolic_value_borrow (config : C.config)
       (* Update the synthesized program *)
       S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
         see expr
-  | T.Shared ->
+  | RShared ->
       expand_symbolic_value_shared_borrow config original_sv original_sv_place
         ref_ty cf ctx
 
@@ -449,9 +442,9 @@ let expand_symbolic_value_borrow (config : C.config)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (config : C.config)
-    (sv : V.symbolic_value) (sv_place : SA.mplace option)
-    (see_cf_l : (V.symbolic_expansion option * st_cm_fun) list)
+let apply_branching_symbolic_expansions_non_borrow (config : config)
+    (sv : symbolic_value) (sv_place : SA.mplace option)
+    (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
   assert (see_cf_l <> []);
@@ -492,25 +485,25 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
   let seel = List.map fst see_cf_l in
   S.synthesize_symbolic_expansion sv sv_place seel subterms
 
-let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value)
+let expand_symbolic_bool (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
   (* Compute the expanded value *)
   let original_sv = sv in
   let original_sv_place = sv_place in
-  let rty = original_sv.V.sv_ty in
-  assert (rty = T.Literal PV.Bool);
+  let rty = original_sv.sv_ty in
+  assert (rty = TLiteral TBool);
   (* Expand the symbolic value to true or false and continue execution *)
-  let see_true = V.SeLiteral (PV.Bool true) in
-  let see_false = V.SeLiteral (PV.Bool false) in
+  let see_true = SeLiteral (VBool true) in
+  let see_false = SeLiteral (VBool false) in
   let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
   (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
   apply_branching_symbolic_expansions_non_borrow config original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (config : C.config)
-    (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
+let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
+    (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
@@ -522,12 +515,12 @@ let expand_symbolic_value_no_branching (config : C.config)
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sv in
   let original_sv_place = sv_place in
-  let rty = original_sv.V.sv_ty in
+  let rty = original_sv.sv_ty in
   let cc : cm_fun =
    fun cf ctx ->
     match rty with
     (* ADTs *)
-    | T.Adt (adt_id, generics) ->
+    | TAdt (adt_id, generics) ->
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
@@ -546,14 +539,14 @@ let expand_symbolic_value_no_branching (config : C.config)
         S.synthesize_symbolic_expansion_no_branching original_sv
           original_sv_place see expr
     (* Borrows *)
-    | T.Ref (region, ref_ty, rkind) ->
+    | TRef (region, ref_ty, rkind) ->
         expand_symbolic_value_borrow config original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
         raise
           (Failure
              ("expand_symbolic_value_no_branching: unexpected type: "
-            ^ T.show_rty rty))
+            ^ show_rty rty))
   in
   (* Debug *)
   let cc =
@@ -565,12 +558,12 @@ let expand_symbolic_value_no_branching (config : C.config)
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)))
+        assert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)))
   in
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
+let expand_symbolic_adt (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -580,11 +573,11 @@ let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sv in
   let original_sv_place = sv_place in
-  let rty = original_sv.V.sv_ty in
+  let rty = original_sv.sv_ty in
   (* Execute *)
   match rty with
   (* ADTs *)
-  | T.Adt (adt_id, generics) ->
+  | TAdt (adt_id, generics) ->
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
@@ -596,15 +589,14 @@ let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
       apply_branching_symbolic_expansions_non_borrow config original_sv
         original_sv_place seel cf_after_join ctx
   | _ ->
-      raise
-        (Failure ("expand_symbolic_adt: unexpected type: " ^ T.show_rty rty))
+      raise (Failure ("expand_symbolic_adt: unexpected type: " ^ show_rty rty))
 
-let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
-    (sv_place : SA.mplace option) (int_type : T.integer_type)
-    (tgts : (V.scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
+let expand_symbolic_int (config : config) (sv : symbolic_value)
+    (sv_place : SA.mplace option) (int_type : integer_type)
+    (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  assert (sv.V.sv_ty = T.Literal (PV.Integer int_type));
+  assert (sv.sv_ty = TLiteral (TInteger int_type));
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
@@ -615,7 +607,7 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
    * (optional expansion, statement to execute)
    *)
   let seel =
-    List.map (fun (v, cf) -> (Some (V.SeLiteral (PV.Scalar v)), cf)) tgts
+    List.map (fun (v, cf) -> (Some (SeLiteral (VScalar v)), cf)) tgts
   in
   let seel = List.append seel [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
@@ -630,15 +622,15 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
     object
-      inherit [_] C.iter_eval_ctx
+      inherit [_] iter_eval_ctx
 
-      method! visit_Symbolic _ sv =
-        if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then
+      method! visit_VSymbolic _ sv =
+        if ty_has_borrows ctx.type_context.type_infos sv.sv_ty then
           raise (FoundSymbolicValue sv)
         else ()
 
@@ -662,42 +654,41 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
           ("greedy_expand_symbolics_with_borrows: about to expand: "
           ^ symbolic_value_to_string ctx sv));
       let cc : cm_fun =
-        match sv.V.sv_ty with
-        | T.Adt (AdtId def_id, _) ->
+        match sv.sv_ty with
+        | TAdt (TAdtId def_id, _) ->
             (* {!expand_symbolic_value_no_branching} checks if there are branchings,
              * but we prefer to also check it here - this leads to cleaner messages
              * and debugging *)
-            let def = C.ctx_lookup_type_decl ctx def_id in
+            let def = ctx_lookup_type_decl ctx def_id in
             (match def.kind with
-            | T.Struct _ | T.Enum ([] | [ _ ]) -> ()
-            | T.Enum (_ :: _) ->
+            | Struct _ | Enum ([] | [ _ ]) -> ()
+            | Enum (_ :: _) ->
                 raise
                   (Failure
                      ("Attempted to greedily expand a symbolic enumeration \
                        with > 1 variants (option \
                        [greedy_expand_symbolics_with_borrows] of [config]): "
-                     ^ Print.name_to_string def.name))
-            | T.Opaque ->
+                     ^ name_to_string ctx def.name))
+            | Opaque ->
                 raise (Failure "Attempted to greedily expand an opaque type"));
             (* Also, we need to check if the definition is recursive *)
-            if C.ctx_type_decl_is_rec ctx def_id then
+            if ctx_type_decl_is_rec ctx def_id then
               raise
                 (Failure
                    ("Attempted to greedily expand a recursive definition \
                      (option [greedy_expand_symbolics_with_borrows] of \
                      [config]): "
-                   ^ Print.name_to_string def.name))
+                   ^ name_to_string ctx def.name))
             else expand_symbolic_value_no_branching config sv None
-        | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
+        | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config sv None
-        | T.Adt (Assumed (Array | Slice | Str), _) ->
+        | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
             raise
               (Failure
                  "Attempted to greedily expand an ADT which can't be expanded ")
-        | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ | T.Arrow _
-        | T.RawPtr _ ->
+        | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
             raise (Failure "Unreachable")
       in
       (* Compose and continue *)
@@ -706,7 +697,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (config : C.config) : cm_fun =
+let greedy_expand_symbolic_values (config : config) : cm_fun =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");