From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:28:56 +0100
Subject: Remove the 'r type variable from the ty type definition

---
 compiler/SymbolicToPure.ml | 219 +++++++++++++++++++++++----------------------
 1 file changed, 113 insertions(+), 106 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

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
-- 
cgit v1.2.3


From 0a5859fbb7bcd99bfa221eaf1af029ff660bf963 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:35:24 +0100
Subject: Rename some variants

---
 compiler/SymbolicToPure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 97755438..91edbf04 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2487,7 +2487,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCGValue 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
@@ -2740,7 +2740,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
           const_generics
       in
       let trait_refs =
-- 
cgit v1.2.3


From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:04:11 +0100
Subject: Prefix variants related to types with "T"

---
 compiler/SymbolicToPure.ml | 104 ++++++++++++++++++++++-----------------------
 1 file changed, 51 insertions(+), 53 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 91edbf04..60020d9a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -397,8 +397,8 @@ let rec translate_sty (ty : T.ty) : ty =
   | T.TAdt (type_id, generics) -> (
       let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
-      | T.Tuple ->
+      | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
+      | T.TTuple ->
           assert (generics.const_generics = []);
           mk_simpl_tuple_ty generics.types
       | T.TAssumed aty -> (
@@ -412,23 +412,23 @@ let rec translate_sty (ty : T.ty) : ty =
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.TArray -> TAdt (TAssumed Array, generics)
-          | T.TSlice -> TAdt (TAssumed Slice, generics)
-          | T.TStr -> TAdt (TAssumed Str, generics)))
-  | TypeVar vid -> TypeVar vid
+          | T.TArray -> TAdt (TAssumed TArray, generics)
+          | T.TSlice -> TAdt (TAssumed TSlice, generics)
+          | T.TStr -> TAdt (TAssumed TStr, generics)))
+  | TVar vid -> TVar vid
   | TLiteral ty -> TLiteral ty
-  | Never -> raise (Failure "Unreachable")
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TNever -> raise (Failure "Unreachable")
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (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
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (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")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_sgeneric_args (generics : T.generic_args) : generic_args =
   translate_generic_args translate_sty generics
@@ -506,20 +506,20 @@ 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.TAssumed aty ->
+  | TAdtId adt_id -> TAdtId adt_id
+  | TAssumed aty ->
       let aty =
         match aty with
-        | T.TArray -> Array
-        | T.TSlice -> Slice
-        | T.TStr -> Str
+        | T.TArray -> TArray
+        | T.TSlice -> TSlice
+        | T.TStr -> TStr
         | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
             raise (Failure "Unreachable")
       in
       TAssumed aty
-  | T.Tuple -> Tuple
+  | TTuple -> TTuple
 
 (** Translate a type, seen as an input/output of a forward function
     (preserve all borrows, etc.).
@@ -536,14 +536,14 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
           let type_id = translate_type_id type_id in
           TAdt (type_id, t_generics)
-      | Tuple ->
+      | TTuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_generics.types
-      | T.TAssumed T.TBox -> (
+      | TAssumed TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (
@@ -558,20 +558,20 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
                 (Failure
                    "Unreachable: box/vec/option receives exactly one type \
                     parameter")))
-  | TypeVar vid -> TypeVar vid
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> TVar vid
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> TLiteral lty
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (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
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (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
-      TraitType (trait_ref, generics, type_name)
-  | Arrow _ -> raise (Failure "TODO")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
     (generics : T.generic_args) : generic_args =
@@ -611,7 +611,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.TAdt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | 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
@@ -630,7 +630,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               let generics = translate_fwd_generic_args type_infos generics in
               Some (TAdt (type_id, generics))
             else None
-      | TAssumed T.TBox -> (
+      | TAssumed 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 *)
@@ -640,7 +640,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               raise
                 (Failure "Unreachable: boxes receive exactly one type parameter")
           )
-      | T.Tuple -> (
+      | TTuple -> (
           (* Tuples can contain borrows (which we eliminate) *)
           let tys_t = List.filter_map translate generics.types in
           match tys_t with
@@ -649,10 +649,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               (* Note that if there is exactly one type, [mk_simpl_tuple_ty]
                * is the identity *)
               Some (mk_simpl_tuple_ty tys_t)))
-  | TypeVar vid -> wrap (TypeVar vid)
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> wrap (TVar vid)
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> wrap (TLiteral lty)
-  | Ref (r, rty, rkind) -> (
+  | TRef (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
           (* Ignore shared references, unless we are below a mutable borrow *)
@@ -663,17 +663,17 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
-  | RawPtr _ ->
+  | TRawPtr _ ->
       (* TODO: not sure what to do here *)
       None
-  | TraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
       (* Translate the trait ref and the generics as "forward" generics -
          we do not want to filter any type *)
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
-      Some (TraitType (trait_ref, generics, type_name))
-  | Arrow _ -> raise (Failure "TODO")
+      Some (TTraitType (trait_ref, generics, type_name))
+  | TArrow _ -> raise (Failure "TODO")
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -1155,7 +1155,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
         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.TAdt (T.Tuple, _) ->
+        | TAdt (TTuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
@@ -1233,10 +1233,10 @@ 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.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             None
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             if field_values = [] then None
             else
@@ -1378,10 +1378,10 @@ 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.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             (ctx, None)
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             let variant_id = adt_v.variant_id in
             assert (variant_id = None);
@@ -2386,7 +2386,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
   let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
   let branch = translate_expression branch ctx in
   match type_id with
-  | T.AdtId adt_id ->
+  | TAdtId adt_id ->
       (* Detect if this is an enumeration or not *)
       let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
       let is_enum = TypesUtils.type_decl_is_enum tdef in
@@ -2433,14 +2433,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
             let field_proj = gen_field_proj fid var in
             mk_let monadic (mk_typed_pattern_from_var var None) field_proj e)
           id_var_pairs branch
-  | T.Tuple ->
+  | TTuple ->
       let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in
       let monadic = false in
       mk_let monadic
         (mk_simpl_tuple_pattern vars)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.TAssumed T.TBox ->
+  | TAssumed TBox ->
       (* There should be exactly one variable *)
       let var =
         match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2452,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.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+  | TAssumed (TArray | TSlice | 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
@@ -2484,7 +2484,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         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 = TAssumed Array; init = None; updates = values }
+          { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
     | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
@@ -2735,9 +2735,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        call to the loop forward function) *)
     let generics =
       let { types; const_generics; trait_clauses } = ctx.sg.generics in
-      let types =
-        List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
-      in
+      let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
           (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
-- 
cgit v1.2.3


From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:41:58 +0100
Subject: Add the "V" prefix to most variants related to values

---
 compiler/SymbolicToPure.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 60020d9a..258b1cf2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1149,7 +1149,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   (* Translate the value *)
   let value =
     match v.value with
-    | V.VLiteral cv -> { e = Const cv; ty }
+    | 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
@@ -1173,27 +1173,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
             let cons = { e = cons_e; ty = cons_ty } in
             (* Apply the constructor *)
             mk_apps cons field_values)
-    | Bottom -> raise (Failure "Unreachable")
-    | Loan lc -> (
+    | VBottom -> raise (Failure "Unreachable")
+    | VLoan lc -> (
         match lc with
-        | SharedLoan (_, v) -> translate v
-        | MutLoan _ -> raise (Failure "Unreachable"))
-    | Borrow bc -> (
+        | VSharedLoan (_, v) -> translate v
+        | VMutLoan _ -> raise (Failure "Unreachable"))
+    | VBorrow bc -> (
         match bc with
-        | V.SharedBorrow bid ->
+        | VSharedBorrow bid ->
             (* Lookup the shared value in the context, and continue *)
             let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
             translate sv
-        | V.ReservedMutBorrow bid ->
+        | VReservedMutBorrow bid ->
             (* Same as for shared borrows. However, note that we use reserved borrows
              * only in *meta-data*: a value *actually used* in the translation can't come
              * from an unpromoted reserved borrow *)
             let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
             translate sv
-        | V.MutBorrow (_, v) ->
+        | VMutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
             translate v)
-    | Symbolic sv -> symbolic_value_to_texpression ctx sv
+    | VSymbolic sv -> symbolic_value_to_texpression ctx sv
   in
   (* Debugging *)
   log#ldebug
-- 
cgit v1.2.3


From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 13:27:02 +0100
Subject: Add RegionsHierarchy.ml

---
 compiler/SymbolicToPure.ml | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 258b1cf2..922aa307 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -47,6 +47,7 @@ type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t;  (** *)
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
+  regions_hierarchies : T.region_groups FunIdMap.t;
 }
 [@@deriving show]
 
@@ -441,8 +442,8 @@ and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id
   translate_trait_instance_id translate_sty id
 
 let translate_trait_clause (clause : T.trait_clause) : trait_clause =
-  let { T.clause_id; meta = _; trait_id; generics } = clause in
-  let generics = translate_sgeneric_args generics in
+  let { T.clause_id; meta = _; trait_id; clause_generics } = clause in
+  let generics = translate_sgeneric_args clause_generics in
   { clause_id; trait_id; generics }
 
 let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
@@ -848,11 +849,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   let fun_infos = decls_ctx.fun_ctx.fun_infos in
   let type_infos = decls_ctx.type_ctx.type_infos in
   (* Retrieve the list of parent backward functions *)
+  let regions_hierarchy =
+    FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+  in
   let gid, parents =
     match bid with
     | None -> (None, T.RegionGroupId.Set.empty)
     | Some bid ->
-        let parents = list_ancestor_region_groups sg bid in
+        let parents = list_ancestor_region_groups regions_hierarchy bid in
         (Some bid, parents)
   in
   (* Is the function stateful, and can it fail? *)
@@ -865,7 +869,7 @@ 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_group) -> g.id) sg.regions_hierarchy
+      List.map (fun (g : T.region_group) -> g.id) regions_hierarchy
     in
     let ctx =
       InterpreterUtils.initialize_eval_context decls_ctx region_groups
@@ -898,7 +902,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   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.ty -> ty option =
-    let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
+    let rg = T.RegionGroupId.nth regions_hierarchy gid in
     let regions = T.RegionId.Set.of_list rg.regions in
     let keep_region r =
       match r with
@@ -2924,6 +2928,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let basename = def.name in
   (* Retrieve the signature *)
   let signature = ctx.sg in
+  let regions_hierarchy =
+    FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies
+  in
   (* Translate the body, if there is *)
   let body =
     match body with
@@ -2965,7 +2972,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
           | None -> []
           | Some back_id ->
               let parents_ids =
-                list_ordered_ancestor_region_groups def.signature back_id
+                list_ordered_ancestor_region_groups regions_hierarchy back_id
               in
               let backward_ids = List.append parents_ids [ back_id ] in
               List.concat
@@ -3069,6 +3076,10 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
   let translate_one (fun_id : A.fun_id) (input_names : string option list)
       (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list
       =
+    (* Retrieve the regions hierarchy *)
+    let regions_hierarchy =
+      FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+    in
     (* The forward function *)
     let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in
     let fwd_id = (fun_id, None) in
@@ -3081,7 +3092,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
           in
           let id = (fun_id, Some rg.id) in
           (id, tsg))
-        sg.regions_hierarchy
+        regions_hierarchy
     in
     (* Return *)
     (fwd_id, fwd_sg) :: back_sgs
-- 
cgit v1.2.3


From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 15 Nov 2023 22:03:21 +0100
Subject: Start updating the name type, cleanup the names and the module
 abbrevs

---
 compiler/SymbolicToPure.ml | 214 ++++++++++++++++++++++-----------------------
 1 file changed, 107 insertions(+), 107 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 922aa307..2460e040 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,18 +2,19 @@ open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
+open PrimitiveValues
+module T = Types
 module Id = Identifiers
 module C = Contexts
 module A = LlbcAst
 module S = SymbolicAst
 module TA = TypesAnalysis
-module L = Logging
 module PP = PrintPure
 module FA = FunsAnalysis
 module IU = InterpreterUtils
 
 (** The local logger *)
-let log = L.symbolic_to_pure_log
+let log = Logging.symbolic_to_pure_log
 
 type type_context = {
   llbc_type_decls : T.type_decl TypeDeclId.Map.t;
@@ -208,113 +209,92 @@ type bs_ctx = {
 [@@deriving show]
 
 (* TODO: move *)
-let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
-  Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
-    ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
-    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 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
+let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
+  let type_decls = ctx.type_context.llbc_type_decls in
+  let fun_decls = ctx.fun_context.llbc_fun_decls in
+  let global_decls = ctx.global_context.llbc_global_decls in
+  let trait_decls = ctx.trait_decls_ctx in
+  let trait_impls = ctx.trait_impls_ctx in
+  let generics = ctx.fun_decl.signature.generics in
+  let preds = ctx.fun_decl.signature.preds in
   {
-    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;
-    global_decl_id_to_string = ast_fmt.global_decl_id_to_string;
-    adt_variant_to_string = ast_fmt.adt_variant_to_string;
-    var_id_to_string;
-    adt_field_names = ast_fmt.adt_field_names;
-    trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
-    trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
-    trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
+    type_decls;
+    fun_decls;
+    global_decls;
+    trait_decls;
+    trait_impls;
+    generics;
+    preds;
+    locals = [];
   }
 
-let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
-  let generics = ctx.fun_decl.signature.generics in
+let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-    ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
-    generics.const_generics
+  let trait_decls = ctx.trait_decls_ctx in
+  let trait_impls = ctx.trait_impls_ctx in
+  let generics = ctx.sg.generics in
+  {
+    type_decls;
+    fun_decls;
+    global_decls;
+    trait_decls;
+    trait_impls;
+    generics;
+    locals = [];
+  }
 
 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_type_formatter fmt in
-  Print.PT.generic_args_to_string fmt args
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.generic_args_to_string env args
+
+let name_to_string (ctx : bs_ctx) =
+  Print.Types.name_to_string (bs_ctx_to_fmt_env ctx)
 
 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_type_formatter fmt in
-  Print.PV.symbolic_value_to_string fmt sv
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Values.symbolic_value_to_string env 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 env = bs_ctx_to_fmt_env ctx in
+  Print.Values.typed_value_to_string env v
 
 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 env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.ty_to_string env false ty
 
 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_type_formatter fmt in
-  Print.PT.ty_to_string fmt ty
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.ty_to_string env ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
-      ctx.trait_impls_ctx def.generics.types def.generics.const_generics
-  in
-  PrintPure.type_decl_to_string fmt def
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.type_decl_to_string env def
 
 let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
-  let fmt = bs_ctx_to_pp_ast_formatter ctx in
-  PrintPure.texpression_to_string fmt false "" "  " e
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.texpression_to_string env false "" "  " e
 
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
-  let type_params = sg.generics.types in
-  let cg_params = sg.generics.const_generics in
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
-  in
-  PrintPure.fun_sig_to_string fmt sg
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_sig_to_string env sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
-  let generics = def.signature.generics in
-  let type_params = generics.types in
-  let cg_params = generics.const_generics in
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt =
-    PrintPure.mk_ast_formatter type_decls fun_decls global_decls
-      ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
-  in
-  PrintPure.fun_decl_to_string fmt def
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_decl_to_string env def
 
 let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
-  let fmt = bs_ctx_to_pp_ast_formatter ctx in
-  PrintPure.typed_pattern_to_string fmt p
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.typed_pattern_to_string env p
 
 (* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
-  let fmt = bs_ctx_to_ast_formatter ctx in
-  let fmt = Print.Contexts.ast_to_value_formatter fmt in
+  let env = bs_ctx_to_fmt_env ctx in
   let verbose = false in
   let indent = "" in
   let indent_incr = "  " in
-  Print.Values.abs_to_string fmt verbose indent indent_incr abs
+  Print.Values.abs_to_string env verbose indent indent_incr abs
 
 let get_instantiated_fun_sig (fun_id : A.fun_id)
     (back_id : T.RegionGroupId.id option) (generics : generic_args)
@@ -421,7 +401,7 @@ let rec translate_sty (ty : T.ty) : ty =
   | TNever -> raise (Failure "Unreachable")
   | TRef (_, rty, _) -> translate rty
   | TRawPtr (ty, rkind) ->
-      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let mut = match rkind with RMut -> Mut | RShared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
@@ -481,21 +461,24 @@ let translate_variant (v : T.variant) : variant =
 let translate_variants (vl : T.variant list) : variant list =
   List.map translate_variant vl
 
-(** Translate a type def kind to IM *)
+(** Translate a type def kind from LLBC *)
 let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
   match kind with
   | T.Struct fields -> Struct (translate_fields fields)
   | T.Enum variants -> Enum (translate_variants variants)
   | T.Opaque -> Opaque
 
-(** Translate a type definition from IM 
+(** Translate a type definition from LLBC
 
-    TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
-    point of moving this definition for now.
+    Remark: this is not symbolic to pure but LLBC to pure. Still,
+    I don't see the point of moving this definition for now.
  *)
-let translate_type_decl (def : T.type_decl) : type_decl =
+let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
+    type_decl =
+  let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
-  let name = def.name in
+  let llbc_name = def.name in
+  let name = Print.Types.name_to_string env def.name in
   let { T.regions; types; const_generics; trait_clauses } = def.generics in
   (* Can't translate types with regions for now *)
   assert (regions = []);
@@ -503,7 +486,7 @@ let translate_type_decl (def : T.type_decl) : type_decl =
   let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
-  { def_id; name; generics; kind; preds }
+  { def_id; llbc_name; name; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -564,7 +547,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
   | TLiteral lty -> TLiteral lty
   | TRef (_, rty, _) -> translate rty
   | TRawPtr (ty, rkind) ->
-      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let mut = match rkind with RMut -> Mut | RShared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
@@ -655,10 +638,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   | TLiteral lty -> wrap (TLiteral lty)
   | TRef (r, rty, rkind) -> (
       match rkind with
-      | T.Shared ->
+      | RShared ->
           (* Ignore shared references, unless we are below a mutable borrow *)
           if inside_mut then translate rty else None
-      | T.Mut ->
+      | RMut ->
           (* Dive in, remembering the fact that we are inside a mutable borrow *)
           let inside_mut = true in
           if keep_region r then
@@ -1034,7 +1017,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
       effect_info;
     }
   in
-  let preds = translate_predicates sg.A.preds in
+  let preds = translate_predicates sg.preds in
   let sg = { generics; preds; inputs; output; doutputs; info } in
   { sg; output_names }
 
@@ -1795,7 +1778,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   log#ldebug
     (lazy
       ("translate_end_abstraction_synth_input:" ^ "\n- function: "
-      ^ Print.name_to_string ctx.fun_decl.name
+      ^ name_to_string ctx ctx.fun_decl.name
       ^ "\n- rg_id: "
       ^ T.RegionGroupId.to_string rg_id
       ^ "\n- loop_id: "
@@ -2109,7 +2092,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.FRegular ctx.fun_decl.A.def_id in
+      let fun_id = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
           (Some vloop_id) (Some rg_id)
@@ -2336,7 +2319,7 @@ 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.VScalar v) in
+        let pat = mk_typed_pattern_from_literal (VScalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
@@ -2569,7 +2552,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.FRegular ctx.fun_decl.A.def_id in
+      let fid = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
         get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
       in
@@ -2918,14 +2901,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   log#ldebug
     (lazy
       ("SymbolicToPure.translate_fun_decl: "
-      ^ Print.fun_name_to_string def.A.name
+      ^ name_to_string ctx def.name
       ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string bid
       ^ ")\n"));
 
   (* Translate the declaration *)
-  let def_id = def.A.def_id in
-  let basename = def.name in
+  let def_id = def.def_id in
+  let llbc_name = def.name in
+  let name = name_to_string ctx llbc_name in
   (* Retrieve the signature *)
   let signature = ctx.sg in
   let regions_hierarchy =
@@ -2999,7 +2983,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         log#ldebug
           (lazy
             ("SymbolicToPure.translate_fun_decl: "
-            ^ Print.fun_name_to_string def.A.name
+            ^ name_to_string ctx def.name
             ^ " ("
             ^ Print.option_to_string T.RegionGroupId.to_string bid
             ^ ")" ^ "\n- forward_inputs: "
@@ -3030,14 +3014,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let loop_id = None in
 
   (* Assemble the declaration *)
-  let def =
+  let def : fun_decl =
     {
       def_id;
       kind = def.kind;
       num_loops;
       loop_id;
       back_id = bid;
-      basename;
+      llbc_name;
+      name;
       signature;
       is_global_decl_body = def.is_global_decl_body;
       body;
@@ -3051,8 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* return *)
   def
 
-let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
-  List.map translate_type_decl type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx)
+    (type_decls : T.type_decl list) : type_decl list =
+  List.map (translate_type_decl ctx) type_decls
 
 (** Translates function signatures.
 
@@ -3105,11 +3091,11 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
     (fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
     RegularFunIdNotLoopMap.empty translated
 
-let translate_trait_decl (type_infos : TA.type_infos)
-    (trait_decl : A.trait_decl) : trait_decl =
+let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
+    : trait_decl =
   let {
     def_id;
-    name;
+    name = llbc_name;
     generics;
     preds;
     parent_clauses;
@@ -3120,6 +3106,12 @@ let translate_trait_decl (type_infos : TA.type_infos)
   } : A.trait_decl =
     trait_decl
   in
+  let type_infos = ctx.type_ctx.type_infos in
+  let name =
+    Print.Types.name_to_string
+      (Print.Contexts.decls_ctx_to_fmt_env ctx)
+      llbc_name
+  in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
   let parent_clauses = List.map translate_trait_clause parent_clauses in
@@ -3138,6 +3130,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
   in
   {
     def_id;
+    llbc_name;
     name;
     generics;
     preds;
@@ -3148,11 +3141,11 @@ let translate_trait_decl (type_infos : TA.type_infos)
     provided_methods;
   }
 
-let translate_trait_impl (type_infos : TA.type_infos)
-    (trait_impl : A.trait_impl) : trait_impl =
+let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
+    : trait_impl =
   let {
     A.def_id;
-    name;
+    name = llbc_name;
     impl_trait;
     generics;
     preds;
@@ -3164,9 +3157,15 @@ let translate_trait_impl (type_infos : TA.type_infos)
   } =
     trait_impl
   in
+  let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
     translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
   in
+  let name =
+    Print.Types.name_to_string
+      (Print.Contexts.decls_ctx_to_fmt_env ctx)
+      llbc_name
+  in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
   let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
@@ -3185,6 +3184,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
   in
   {
     def_id;
+    llbc_name;
     name;
     impl_trait;
     generics;
-- 
cgit v1.2.3


From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:13:28 +0100
Subject: Finish propagating the changes to the names and cleaning

---
 compiler/SymbolicToPure.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2460e040..4e12d31e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3036,9 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* return *)
   def
 
-let translate_type_decls (ctx : Contexts.decls_ctx)
-    (type_decls : T.type_decl list) : type_decl list =
-  List.map (translate_type_decl ctx) type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
+  List.map (translate_type_decl ctx)
+    (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
 (** Translates function signatures.
 
-- 
cgit v1.2.3


From 0757cdee8c6b8a8020d4b96a44a3017944c9a808 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:57:08 +0100
Subject: Do more cleanup

---
 compiler/SymbolicToPure.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4e12d31e..7dad54e1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3,6 +3,9 @@ open LlbcAstUtils
 open Pure
 open PureUtils
 open PrimitiveValues
+open InterpreterUtils
+open FunsAnalysis
+open TypesAnalysis
 module T = Types
 module Id = Identifiers
 module C = Contexts
@@ -10,8 +13,6 @@ module A = LlbcAst
 module S = SymbolicAst
 module TA = TypesAnalysis
 module PP = PrintPure
-module FA = FunsAnalysis
-module IU = InterpreterUtils
 
 (** The local logger *)
 let log = Logging.symbolic_to_pure_log
@@ -24,7 +25,7 @@ type type_context = {
           This map is empty when we translate the types, then contains all
           the translated types when we translate the functions.
        *)
-  type_infos : TA.type_infos;
+  type_infos : type_infos;
   recursive_decls : T.TypeDeclId.Set.t;
 }
 [@@deriving show]
@@ -47,7 +48,7 @@ type fun_sig_named_outputs = {
 type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t;  (** *)
-  fun_infos : FA.fun_info A.FunDeclId.Map.t;
+  fun_infos : fun_info A.FunDeclId.Map.t;
   regions_hierarchies : T.region_groups FunIdMap.t;
 }
 [@@deriving show]
@@ -513,7 +514,7 @@ let translate_type_id (id : T.type_id) : type_id =
 
     TODO: factor out the various translation functions.
 *)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
+let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
   | T.TAdt (type_id, generics) -> (
@@ -557,15 +558,15 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
       TTraitType (trait_ref, generics, type_name)
   | TArrow _ -> raise (Failure "TODO")
 
-and translate_fwd_generic_args (type_infos : TA.type_infos)
+and translate_fwd_generic_args (type_infos : type_infos)
     (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 : T.trait_ref) :
+and translate_fwd_trait_ref (type_infos : 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)
+and translate_fwd_trait_instance_id (type_infos : type_infos)
     (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id (translate_fwd_ty type_infos) id
 
@@ -586,7 +587,7 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     
     [inside_mut]: are we inside a mutable borrow?
  *)
-let rec translate_back_ty (type_infos : TA.type_infos)
+let rec translate_back_ty (type_infos : type_infos)
     (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
@@ -791,7 +792,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
   if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
 
 (** Small utility. *)
-let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+let get_fun_effect_info (fun_infos : 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
@@ -1783,8 +1784,8 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ^ T.RegionGroupId.to_string rg_id
       ^ "\n- loop_id: "
       ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
-      ^ "\n- eval_ctx:\n" ^ IU.eval_ctx_to_string ectx ^ "\n- abs:\n"
-      ^ IU.abs_to_string ectx abs ^ "\n"));
+      ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ectx ^ "\n- abs:\n"
+      ^ abs_to_string ctx abs ^ "\n"));
 
   (* When we end an input abstraction, this input abstraction gets back
    * the borrows which it introduced in the context through the input
-- 
cgit v1.2.3


From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Nov 2023 21:58:25 +0100
Subject: Use the name matcher implemented in Charon

---
 compiler/SymbolicToPure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dad54e1..69ff4df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2475,7 +2475,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCgValue 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
@@ -2726,7 +2726,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index)
           const_generics
       in
       let trait_refs =
-- 
cgit v1.2.3


From 00882b8fe6d8ef1d9b7a03cd5949f909d58a2da9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 11:30:43 +0100
Subject: Make a minor modification

---
 compiler/SymbolicToPure.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 69ff4df1..6983a0e8 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -269,7 +269,11 @@ let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
   let env = bs_ctx_to_fmt_env ctx in
   Print.Types.ty_to_string env ty
 
-let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
+let type_decl_to_string (ctx : bs_ctx) (def : T.type_decl) : string =
+  let env = bs_ctx_to_fmt_env ctx in
+  Print.Types.type_decl_to_string env def
+
+let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
   PrintPure.type_decl_to_string env def
 
@@ -476,6 +480,12 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
  *)
 let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     type_decl =
+  log#ldebug
+    (lazy
+      (let ctx = Print.Contexts.decls_ctx_to_fmt_env ctx in
+       "translate_type_decl:\n\n"
+       ^ Print.Types.type_decl_to_string ctx def
+       ^ "\n"));
   let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
   let llbc_name = def.name in
-- 
cgit v1.2.3


From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 12:15:37 +0100
Subject: Rename PrimitiveValues to Values

---
 compiler/SymbolicToPure.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6983a0e8..f25ff2f6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,16 +2,14 @@ open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
-open PrimitiveValues
 open InterpreterUtils
 open FunsAnalysis
 open TypesAnalysis
 module T = Types
-module Id = Identifiers
+module V = Values
 module C = Contexts
 module A = LlbcAst
 module S = SymbolicAst
-module TA = TypesAnalysis
 module PP = PrintPure
 
 (** The local logger *)
-- 
cgit v1.2.3


From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 13:55:46 +0100
Subject: Add an `is_local` field to declarations

---
 compiler/SymbolicToPure.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index f25ff2f6..9899a0c6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -495,7 +495,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
-  { def_id; llbc_name; name; generics; kind; preds }
+  let is_local = def.is_local in
+  { def_id; is_local; llbc_name; name; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -3026,6 +3027,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let def : fun_decl =
     {
       def_id;
+      is_local = def.is_local;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3104,6 +3106,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     : trait_decl =
   let {
     def_id;
+    is_local;
     name = llbc_name;
     generics;
     preds;
@@ -3139,6 +3142,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   in
   {
     def_id;
+    is_local;
     llbc_name;
     name;
     generics;
@@ -3154,6 +3158,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     : trait_impl =
   let {
     A.def_id;
+    is_local;
     name = llbc_name;
     impl_trait;
     generics;
@@ -3193,6 +3198,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   {
     def_id;
+    is_local;
     llbc_name;
     name;
     impl_trait;
-- 
cgit v1.2.3


From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:43:12 +0100
Subject: Add span information to the generated code

---
 compiler/SymbolicToPure.ml | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9899a0c6..5dee23db 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -496,7 +496,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
   let is_local = def.is_local in
-  { def_id; is_local; llbc_name; name; generics; kind; preds }
+  let meta = def.meta in
+  { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -1489,11 +1490,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
   (call_info.forward, abs_ancestors)
 
 (** Add meta-information to an expression *)
-let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
     (e : texpression) : texpression =
   let var_values = List.combine vars values in
   List.fold_right
-    (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+    (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
     var_values e
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1509,7 +1510,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
   | IntroSymbolic (ectx, p, sv, v, e) ->
       translate_intro_symbolic ectx p sv v e ctx
-  | Meta (meta, e) -> translate_meta meta e ctx
+  | Meta (meta, e) -> translate_emeta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
@@ -2206,7 +2207,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
                 var_values
             in
             let vars, values = List.split var_values in
-            mk_meta_symbolic_assignments vars values next_e
+            mk_emeta_symbolic_assignments vars values next_e
           else next_e
         in
 
@@ -2637,7 +2638,7 @@ and translate_forward_end (ectx : C.eval_ctx)
          We then remove all the meta information from the body *before* calling
          {!PureMicroPasses.decompose_loops}.
       *)
-      mk_meta_symbolic_assignments loop_info.input_vars org_args e
+      mk_emeta_symbolic_assignments loop_info.input_vars org_args e
 
 and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
@@ -2795,6 +2796,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       {
         fun_end;
         loop_id;
+        meta = loop.meta;
         fuel0 = ctx.fuel0;
         fuel = ctx.fuel;
         input_state;
@@ -2810,7 +2812,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let ty = fun_end.ty in
   { e = loop; ty }
 
-and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   let next_e = translate_expression e ctx in
   let meta =
@@ -3028,6 +3030,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     {
       def_id;
       is_local = def.is_local;
+      meta = def.meta;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3108,6 +3111,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     def_id;
     is_local;
     name = llbc_name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3145,6 +3149,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     llbc_name;
     name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3160,6 +3165,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     A.def_id;
     is_local;
     name = llbc_name;
+    meta;
     impl_trait;
     generics;
     preds;
@@ -3201,6 +3207,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     llbc_name;
     name;
+    meta;
     impl_trait;
     generics;
     preds;
-- 
cgit v1.2.3


From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 09:09:46 +0100
Subject: Improve further the generation of parent clause/trait clause names

---
 compiler/SymbolicToPure.ml | 44 ++++++++++++++++++++++++++++++++++----------
 1 file changed, 34 insertions(+), 10 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5dee23db..4df3ee73 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -497,7 +497,17 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let preds = translate_predicates def.preds in
   let is_local = def.is_local in
   let meta = def.meta in
-  { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
+  {
+    def_id;
+    is_local;
+    llbc_name;
+    name;
+    meta;
+    generics;
+    llbc_generics = def.generics;
+    kind;
+    preds;
+  }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -1029,7 +1039,17 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
     }
   in
   let preds = translate_predicates sg.preds in
-  let sg = { generics; preds; inputs; output; doutputs; info } in
+  let sg =
+    {
+      generics;
+      llbc_generics = sg.generics;
+      preds;
+      inputs;
+      output;
+      doutputs;
+      info;
+    }
+  in
   { sg; output_names }
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -3112,9 +3132,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     name = llbc_name;
     meta;
-    generics;
+    generics = llbc_generics;
     preds;
-    parent_clauses;
+    parent_clauses = llbc_parent_clauses;
     consts;
     types;
     required_methods;
@@ -3128,9 +3148,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params generics in
+  let generics = translate_generic_params llbc_generics in
   let preds = translate_predicates preds in
-  let parent_clauses = List.map translate_trait_clause parent_clauses in
+  let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3151,8 +3171,10 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     name;
     meta;
     generics;
+    llbc_generics;
     preds;
     parent_clauses;
+    llbc_parent_clauses;
     consts;
     types;
     required_methods;
@@ -3166,8 +3188,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     name = llbc_name;
     meta;
-    impl_trait;
-    generics;
+    impl_trait = llbc_impl_trait;
+    generics = llbc_generics;
     preds;
     parent_trait_refs;
     consts;
@@ -3179,14 +3201,14 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
-    translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
+    translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait
   in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params generics in
+  let generics = translate_generic_params llbc_generics in
   let preds = translate_predicates preds in
   let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
   let consts =
@@ -3209,7 +3231,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     name;
     meta;
     impl_trait;
+    llbc_impl_trait;
     generics;
+    llbc_generics;
     preds;
     parent_trait_refs;
     consts;
-- 
cgit v1.2.3