Remove the 'r type variable from the ty type definition

1 files changed, 113 insertions, 106 deletions

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2ce8c706..97755438 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -213,14 +213,12 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
 
 let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
-  let rvar_to_string = Print.Types.region_var_id_to_string in
-  let r_to_string = Print.Types.region_id_to_string in
+  let region_id_to_string = Print.Types.region_id_to_string in
   let type_var_id_to_string = Print.Types.type_var_id_to_string in
   let var_id_to_string = Print.Expressions.var_id_to_string in
   let ast_fmt = bs_ctx_to_ast_formatter ctx in
   {
-    Print.Values.rvar_to_string;
-    r_to_string;
+    Print.Values.region_id_to_string;
     type_var_id_to_string;
     type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
     const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
@@ -242,30 +240,29 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
     generics.const_generics
 
-let ctx_egeneric_args_to_string (ctx : bs_ctx) (args : T.egeneric_args) : string
-    =
+let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_etype_formatter fmt in
-  Print.PT.egeneric_args_to_string fmt args
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
+  Print.PT.generic_args_to_string fmt args
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_rtype_formatter fmt in
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
   Print.PV.symbolic_value_to_string fmt sv
 
 let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
   Print.PV.typed_value_to_string fmt v
 
-let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
+let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
   let fmt = PrintPure.ast_to_type_formatter fmt in
   PrintPure.ty_to_string fmt false ty
 
-let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
+let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
-  let fmt = Print.PC.ctx_to_rtype_formatter fmt in
-  Print.PT.rty_to_string fmt ty
+  let fmt = Print.PC.ctx_to_type_formatter fmt in
+  Print.PT.ty_to_string fmt ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let type_decls = ctx.type_context.llbc_type_decls in
@@ -343,13 +340,13 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
 (* TODO: move *)
 let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
     (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
-  let id = (E.Regular def_id, back_id) in
+  let id = (E.FRegular def_id, back_id) in
   (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
 
 (* Some generic translation functions (we need to translate different "flavours"
-   of types: sty, forward types, backward types, etc.) *)
-let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
-    (generics : 'r T.generic_args) : generic_args =
+   of types: forward types, backward types, etc.) *)
+let rec translate_generic_args (translate_ty : T.ty -> ty)
+    (generics : T.generic_args) : generic_args =
   (* We ignore the regions: if they didn't cause trouble for the symbolic execution,
      then everything's fine *)
   let types = List.map translate_ty generics.types in
@@ -359,7 +356,7 @@ let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
   in
   { types; const_generics; trait_refs }
 
-and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
+and translate_trait_ref (translate_ty : T.ty -> ty) (tr : T.trait_ref) :
     trait_ref =
   let trait_id = translate_trait_instance_id translate_ty tr.trait_id in
   let generics = translate_generic_args translate_ty tr.generics in
@@ -368,13 +365,13 @@ and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
   in
   { trait_id; generics; trait_decl_ref }
 
-and translate_trait_decl_ref (translate_ty : 'r T.ty -> ty)
-    (tr : 'r T.trait_decl_ref) : trait_decl_ref =
+and translate_trait_decl_ref (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref)
+    : trait_decl_ref =
   let decl_generics = translate_generic_args translate_ty tr.decl_generics in
   { trait_decl_id = tr.trait_decl_id; decl_generics }
 
-and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
-    (id : 'r T.trait_instance_id) : trait_instance_id =
+and translate_trait_instance_id (translate_ty : T.ty -> ty)
+    (id : T.trait_instance_id) : trait_instance_id =
   let translate_trait_instance_id = translate_trait_instance_id translate_ty in
   match id with
   | T.Self -> Self
@@ -393,19 +390,20 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
   | FnPointer _ -> raise (Failure "TODO")
   | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
 
-let rec translate_sty (ty : T.sty) : ty =
+(** Translate a signature type - TODO: factor out the different translation functions *)
+let rec translate_sty (ty : T.ty) : ty =
   let translate = translate_sty in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> Adt (AdtId adt_id, generics)
+      | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
       | T.Tuple ->
           assert (generics.const_generics = []);
           mk_simpl_tuple_ty generics.types
-      | T.Assumed aty -> (
+      | T.TAssumed aty -> (
           match aty with
-          | T.Box -> (
+          | T.TBox -> (
               (* Eliminate the boxes *)
               match generics.types with
               | [ ty ] -> ty
@@ -414,31 +412,31 @@ let rec translate_sty (ty : T.sty) : ty =
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.Array -> Adt (Assumed Array, generics)
-          | T.Slice -> Adt (Assumed Slice, generics)
-          | T.Str -> Adt (Assumed Str, generics)))
+          | T.TArray -> TAdt (TAssumed Array, generics)
+          | T.TSlice -> TAdt (TAssumed Slice, generics)
+          | T.TStr -> TAdt (TAssumed Str, generics)))
   | TypeVar vid -> TypeVar vid
-  | Literal ty -> Literal ty
+  | TLiteral ty -> TLiteral ty
   | Never -> raise (Failure "Unreachable")
   | Ref (_, rty, _) -> translate rty
   | RawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      Adt (Assumed (RawPtr mut), generics)
+      TAdt (TAssumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
       TraitType (trait_ref, generics, type_name)
   | Arrow _ -> raise (Failure "TODO")
 
-and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args =
+and translate_sgeneric_args (generics : T.generic_args) : generic_args =
   translate_generic_args translate_sty generics
 
-and translate_strait_ref (tr : T.strait_ref) : trait_ref =
+and translate_strait_ref (tr : T.trait_ref) : trait_ref =
   translate_trait_ref translate_sty tr
 
-and translate_strait_instance_id (id : T.strait_instance_id) : trait_instance_id
+and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id
     =
   translate_trait_instance_id translate_sty id
 
@@ -447,7 +445,7 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause =
   let generics = translate_sgeneric_args generics in
   { clause_id; trait_id; generics }
 
-let translate_strait_type_constraint (ttc : T.strait_type_constraint) :
+let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
     trait_type_constraint =
   let { T.trait_ref; generics; type_name; ty } = ttc in
   let trait_ref = translate_strait_ref trait_ref in
@@ -509,38 +507,43 @@ let translate_type_decl (def : T.type_decl) : type_decl =
 let translate_type_id (id : T.type_id) : type_id =
   match id with
   | AdtId adt_id -> AdtId adt_id
-  | T.Assumed aty ->
+  | T.TAssumed aty ->
       let aty =
         match aty with
-        | T.Array -> Array
-        | T.Slice -> Slice
-        | T.Str -> Str
-        | T.Box ->
+        | T.TArray -> Array
+        | T.TSlice -> Slice
+        | T.TStr -> Str
+        | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
             raise (Failure "Unreachable")
       in
-      Assumed aty
+      TAssumed aty
   | T.Tuple -> Tuple
 
 (** Translate a type, seen as an input/output of a forward function
-    (preserve all borrows, etc.)
+    (preserve all borrows, etc.).
+
+    Remark: it doesn't matter whether the types has regions or erased regions
+    (both cases happen, actually).
+
+    TODO: factor out the various translation functions.
 *)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
+let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
+      | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
           let type_id = translate_type_id type_id in
-          Adt (type_id, t_generics)
+          TAdt (type_id, t_generics)
       | Tuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_generics.types
-      | T.Assumed T.Box -> (
+      | T.TAssumed T.TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (
@@ -557,13 +560,13 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
                     parameter")))
   | TypeVar vid -> TypeVar vid
   | Never -> raise (Failure "Unreachable")
-  | Literal lty -> Literal lty
+  | TLiteral lty -> TLiteral lty
   | Ref (_, rty, _) -> translate rty
   | RawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      Adt (Assumed (RawPtr mut), generics)
+      TAdt (TAssumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
@@ -571,25 +574,25 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   | Arrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
-    (generics : 'r T.generic_args) : generic_args =
+    (generics : T.generic_args) : generic_args =
   translate_generic_args (translate_fwd_ty type_infos) generics
 
-and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : 'r T.trait_ref) :
+and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : T.trait_ref) :
     trait_ref =
   translate_trait_ref (translate_fwd_ty type_infos) tr
 
 and translate_fwd_trait_instance_id (type_infos : TA.type_infos)
-    (id : 'r T.trait_instance_id) : trait_instance_id =
+    (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id (translate_fwd_ty type_infos) id
 
 (** Simply calls [translate_fwd_ty] *)
-let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty =
+let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
   let type_infos = ctx.type_context.type_infos in
   translate_fwd_ty type_infos ty
 
 (** Simply calls [translate_fwd_generic_args] *)
-let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
-    : generic_args =
+let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
+    generic_args =
   let type_infos = ctx.type_context.type_infos in
   translate_fwd_generic_args type_infos generics
 
@@ -600,20 +603,21 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
     [inside_mut]: are we inside a mutable borrow?
  *)
 let rec translate_back_ty (type_infos : TA.type_infos)
-    (keep_region : 'r -> bool) (inside_mut : bool) (ty : 'r T.ty) : ty option =
+    (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option
+    =
   let translate = translate_back_ty type_infos keep_region inside_mut in
   (* A small helper for "leave" types *)
   let wrap ty = if inside_mut then Some ty else None in
   match ty with
-  | T.Adt (type_id, generics) -> (
+  | T.TAdt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
+      | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
           let type_id = translate_type_id type_id in
           if inside_mut then
             (* We do not want to filter anything, so we translate the generics
                as "forward" types *)
             let generics = translate_fwd_generic_args type_infos generics in
-            Some (Adt (type_id, generics))
+            Some (TAdt (type_id, generics))
           else
             (* If not inside a mutable reference: check if at least one
                of the generics contains a mutable reference (i.e., is not
@@ -624,9 +628,9 @@ let rec translate_back_ty (type_infos : TA.type_infos)
             let types = List.filter_map translate generics.types in
             if types <> [] then
               let generics = translate_fwd_generic_args type_infos generics in
-              Some (Adt (type_id, generics))
+              Some (TAdt (type_id, generics))
             else None
-      | Assumed T.Box -> (
+      | TAssumed T.TBox -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           (* Eliminate the box *)
@@ -647,7 +651,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               Some (mk_simpl_tuple_ty tys_t)))
   | TypeVar vid -> wrap (TypeVar vid)
   | Never -> raise (Failure "Unreachable")
-  | Literal lty -> wrap (Literal lty)
+  | TLiteral lty -> wrap (TLiteral lty)
   | Ref (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
@@ -673,7 +677,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
-    (inside_mut : bool) (ty : 'r T.ty) : ty option =
+    (inside_mut : bool) (ty : T.ty) : ty option =
   let type_infos = ctx.type_context.type_infos in
   translate_back_ty type_infos keep_region inside_mut ty
 
@@ -682,7 +686,7 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
     T.ConstGenericVarId.Map.of_list
       (List.map
          (fun (cg : T.const_generic_var) ->
-           (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+           (cg.index, ctx_translate_fwd_ty ctx (T.TLiteral cg.ty)))
          ctx.sg.generics.const_generics)
   in
   let env = VarId.Map.empty in
@@ -807,7 +811,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
-  | TraitMethod (_, _, fid) | FunId (Regular fid) ->
+  | TraitMethod (_, _, fid) | FunId (FRegular fid) ->
       let info = A.FunDeclId.Map.find fid fun_infos in
       let stateful_group = info.stateful in
       let stateful =
@@ -820,7 +824,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         can_diverge = info.can_diverge;
         is_rec = info.is_rec || Option.is_some lid;
       }
-  | FunId (Assumed aid) ->
+  | FunId (FAssumed aid) ->
       assert (lid = None);
       {
         can_fail = Assumed.assumed_fun_can_fail aid;
@@ -861,21 +865,21 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   (* Create the context *)
   let ctx =
     let region_groups =
-      List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
+      List.map (fun (g : T.region_group) -> g.id) sg.regions_hierarchy
     in
     let ctx =
       InterpreterUtils.initialize_eval_context decls_ctx region_groups
         sg.generics.types sg.generics.const_generics
     in
     (* Compute the normalization map for the *sty* types and add it to the context *)
-    AssociatedTypes.ctx_add_norm_trait_stypes_from_preds ctx
+    AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
       sg.preds.trait_type_constraints
   in
 
   (* Normalize the signature *)
   let sg =
     let ({ A.inputs; output; _ } : A.fun_sig) = sg in
-    let norm = AssociatedTypes.ctx_normalize_sty ctx in
+    let norm = AssociatedTypes.ctx_normalize_ty ctx in
     let inputs = List.map norm inputs in
     let output = norm output in
     { sg with A.inputs; output }
@@ -893,14 +897,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
    * so just check that there aren't parent regions *)
   assert (T.RegionGroupId.Set.is_empty parents);
   (* Small helper to translate types for backward functions *)
-  let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.sty -> ty option
-      =
+  let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option =
     let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
-    let regions = T.RegionVarId.Set.of_list rg.regions in
+    let regions = T.RegionId.Set.of_list rg.regions in
     let keep_region r =
       match r with
-      | T.Static -> raise Unimplemented
-      | T.Var r -> T.RegionVarId.Set.mem r regions
+      | T.RStatic -> raise Unimplemented
+      | T.RErased -> raise (Failure "Unexpected erased region")
+      | T.RVar r -> T.RegionId.Set.mem r regions
     in
     let inside_mut = false in
     translate_back_ty type_infos keep_region inside_mut
@@ -1042,7 +1046,7 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
   (* Return *)
   (ctx, state_pat)
 
-let fresh_var_llbc_ty (basename : string option) (ty : 'r T.ty) (ctx : bs_ctx) :
+let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) :
     bs_ctx * var =
   (* Generate the fresh variable *)
   let id, var_counter = VarId.fresh ctx.var_counter in
@@ -1106,7 +1110,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
 (** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
   match (v.value, v.ty) with
-  | V.Adt av, T.Adt (T.Assumed T.Box, _) -> (
+  | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> (
       match av.field_values with
       | [ bv ] -> unbox_typed_value bv
       | _ -> raise (Failure "Unreachable"))
@@ -1145,13 +1149,13 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   (* Translate the value *)
   let value =
     match v.value with
-    | V.Literal cv -> { e = Const cv; ty }
-    | Adt av -> (
+    | V.VLiteral cv -> { e = Const cv; ty }
+    | VAdt av -> (
         let variant_id = av.variant_id in
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.Adt (T.Tuple, _) ->
+        | T.TAdt (T.Tuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
@@ -1229,7 +1233,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1374,7 +1378,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -1645,7 +1649,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   log#ldebug
     (lazy
       ("translate_function_call:\n"
-      ^ ctx_egeneric_args_to_string ctx call.generics));
+      ^ ctx_generic_args_to_string ctx call.generics));
   (* Translate the function call *)
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   let args =
@@ -1845,11 +1849,12 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ("translate_end_abstraction_synth_input:"
      ^ "\n\n- given back variables types:\n"
       ^ Print.list_to_string
-          (fun (v : var) -> ty_to_string ctx v.ty)
+          (fun (v : var) -> pure_ty_to_string ctx v.ty)
           given_back_variables
       ^ "\n\n- consumed values:\n"
       ^ Print.list_to_string
-          (fun e -> texpression_to_string ctx e ^ " : " ^ ty_to_string ctx e.ty)
+          (fun e ->
+            texpression_to_string ctx e ^ " : " ^ pure_ty_to_string ctx e.ty)
           consumed_values
       ^ "\n"));
 
@@ -1948,7 +1953,8 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
              ^ "\n- inst_sg.inputs ("
              ^ string_of_int (List.length inst_sg.inputs)
              ^ "): "
-             ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
+             ^ String.concat ", "
+                 (List.map (pure_ty_to_string ctx) inst_sg.inputs)));
          List.iter
            (fun (x, ty) -> assert ((x : texpression).ty = ty))
            (List.combine inputs inst_sg.inputs);
@@ -2070,8 +2076,9 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
       log#ldebug
         (lazy
           ("\n- given_back ty: "
-          ^ ty_to_string ctx given_back.ty
-          ^ "\n- sig input ty: " ^ ty_to_string ctx input.ty));
+          ^ pure_ty_to_string ctx given_back.ty
+          ^ "\n- sig input ty: "
+          ^ pure_ty_to_string ctx input.ty));
       assert (given_back.ty = input.ty))
     given_back_inputs;
   (* Translate the next expression *)
@@ -2098,7 +2105,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       (* Actually the same case as [SynthInput] *)
       translate_end_abstraction_synth_input ectx abs e ctx rg_id
   | V.LoopCall ->
-      let fun_id = E.Regular ctx.fun_decl.A.def_id in
+      let fun_id = E.FRegular ctx.fun_decl.A.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
           (Some vloop_id) (Some rg_id)
@@ -2229,7 +2236,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   let func =
     { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args }
   in
-  let func_ty = mk_arrow (Literal Bool) mk_unit_ty in
+  let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
   let func = { e = Qualif func; ty = func_ty } in
   let assertion = mk_apps func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
@@ -2325,12 +2332,12 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
         (* We don't need to update the context: we don't introduce any
            * new values/variables *)
         let branch = translate_expression branch_e ctx in
-        let pat = mk_typed_pattern_from_literal (PV.Scalar v) in
+        let pat = mk_typed_pattern_from_literal (PV.VScalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
       let otherwise = translate_expression otherwise ctx in
-      let pat_ty = Literal (Integer int_ty) in
+      let pat_ty = TLiteral (TInteger int_ty) in
       let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
       let otherwise : match_branch =
         { pat = otherwise_pat; branch = otherwise }
@@ -2433,7 +2440,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_simpl_tuple_pattern vars)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed T.Box ->
+  | T.TAssumed T.TBox ->
       (* There should be exactly one variable *)
       let var =
         match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2445,7 +2452,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed (T.Array | T.Slice | T.Str) ->
+  | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
@@ -2469,19 +2476,19 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
   *)
   let v =
     match v with
-    | SingleValue v -> typed_value_to_texpression ctx ectx v
-    | Array values ->
+    | VaSingleValue v -> typed_value_to_texpression ctx ectx v
+    | VaArray values ->
         (* We use a struct update to encode the array aggregate, in order
            to preserve the structure and allow generating code of the shape
            `[x0, ...., xn]` *)
         let values = List.map (typed_value_to_texpression ctx ectx) values in
         let values = FieldId.mapi (fun fid v -> (fid, v)) values in
         let su : struct_update =
-          { struct_id = Assumed Array; init = None; updates = values }
+          { struct_id = TAssumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
-    | TraitConstValue (trait_ref, generics, const_name) ->
+    | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
         let generics = translate_fwd_generic_args type_infos generics in
@@ -2558,7 +2565,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let org_args = args in
 
       (* Lookup the effect info for the loop function *)
-      let fid = E.Regular ctx.fun_decl.A.def_id in
+      let fid = E.FRegular ctx.fun_decl.A.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
       in
@@ -2661,7 +2668,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         ^ T.RegionGroupId.Map.show
             (fun (rids, tys) ->
               "(" ^ T.RegionId.Set.show rids ^ ", "
-              ^ Print.list_to_string (rty_to_string ctx) tys
+              ^ Print.list_to_string (ty_to_string ctx) tys
               ^ ")")
             loop.rg_to_given_back_tys
         ^ "\n"));
@@ -2925,8 +2932,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     | None -> None
     | Some body ->
         let effect_info =
-          get_fun_effect_info ctx.fun_context.fun_infos (FunId (Regular def_id))
-            None bid
+          get_fun_effect_info ctx.fun_context.fun_infos
+            (FunId (FRegular def_id)) None bid
         in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
@@ -2999,8 +3006,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
             ^ "\n- back_state: "
             ^ String.concat ", " (List.map show_var back_state)
             ^ "\n- signature.inputs: "
-            ^ String.concat ", " (List.map (ty_to_string ctx) signature.inputs)
-            ));
+            ^ String.concat ", "
+                (List.map (pure_ty_to_string ctx) signature.inputs)));
         (* TODO: we need to normalize the types *)
         if !Config.type_check_pure_code then
           assert (
@@ -3070,7 +3077,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
     (* The backward functions *)
     let back_sgs =
       List.map
-        (fun (rg : T.region_var_group) ->
+        (fun (rg : T.region_group) ->
           let tsg =
             translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id)
           in