Finish propagating the changes to the names and cleaning

12 files changed, 244 insertions, 179 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 41c84141..a2ae4f16 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -525,7 +525,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
-  match decl_group with Rec _ -> true | NonRec _ -> false
+  match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index aa293469..94e50a08 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -1,15 +1,10 @@
 open Aeneas.LlbcOfJson
 open Aeneas.Logging
-module T = Aeneas.Types
-module A = Aeneas.LlbcAst
-module I = Aeneas.Interpreter
+open Aeneas.LlbcAst
+open Aeneas.Interpreter
 module EL = Easy_logging.Logging
-module TA = Aeneas.TypesAnalysis
-module Micro = Aeneas.PureMicroPasses
-module Print = Aeneas.Print
-module PrePasses = Aeneas.PrePasses
-module Translate = Aeneas.Translate
 open Aeneas.Config
+open Aeneas
 
 (** The local logger *)
 let log = main_log
@@ -227,7 +222,9 @@ let () =
       if
         !backend = Lean && !extract_decreases_clauses
         && List.exists
-             (function Aeneas.LlbcAst.Fun (Rec (_ :: _)) -> true | _ -> false)
+             (function
+               | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true
+               | _ -> false)
              m.declarations
       then (
         log#error
@@ -237,15 +234,15 @@ let () =
         fail ());
 
       (* Apply the pre-passes *)
-      let m = PrePasses.apply_passes m in
+      let m = Aeneas.PrePasses.apply_passes m in
 
       (* Some options for the execution *)
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_unit_functions then I.Test.test_unit_functions m;
+      if !test_unit_functions then Test.test_unit_functions m;
 
       (* Translate the functions *)
-      Translate.translate_crate filename dest_dir m;
+      Aeneas.Translate.translate_crate filename dest_dir m;
 
       (* Print total elapsed time *)
       log#linfo
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 04f6c2c3..cd62c15c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -27,7 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
       let builtin =
         let open ExtractBuiltin in
         let funs_map = builtin_funs_map () in
-        let sname = name_to_simple_name def.fwd.f.basename in
+        let sname = name_to_simple_name def.fwd.f.llbc_name in
         SimpleNameMap.find_opt sname funs_map
       in
       (* Use the builtin names if necessary *)
@@ -65,7 +65,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
                   raise
                     (Failure
                        ("Not found: "
-                       ^ Names.name_to_string f.basename
+                       ^ name_to_string ctx f.llbc_name
                        ^ ", "
                        ^ Print.option_to_string Pure.show_loop_id f.loop_id
                        ^ Print.option_to_string Pure.show_region_group_id
@@ -212,7 +212,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
         let decl = FunDeclId.Map.find id ctx.trans_funs in
         let err =
           "Ill-formed builtin information for function "
-          ^ Names.name_to_string decl.fwd.f.basename
+          ^ name_to_string ctx decl.fwd.f.llbc_name
           ^ ": "
           ^ string_of_int (List.length filter)
           ^ " filtering arguments provided for "
@@ -1137,7 +1137,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt
-    [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause" ];
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ];
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1199,7 +1199,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt
-    [ "[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure" ];
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ];
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1253,7 +1253,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
   extract_comment fmt
-    [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases_by tactic" ];
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ];
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
   F.pp_print_string fmt "syntax \"";
@@ -1289,7 +1289,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
       (Pure.FunId (FRegular def.def_id), def.loop_id, def.back_id)
       ctx.fun_name_info
   in
-  let comment_pre = "[" ^ Print.fun_name_to_string def.basename ^ "]: " in
+  let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]: " in
   let comment =
     let loop_comment =
       match def.loop_id with
@@ -1766,13 +1766,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
-  extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ];
+  extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ];
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
   let body_name =
     ctx_get_function
-      (FromLlbc (Pure.FunId (FRegular global.body_id), None, None))
+      (FromLlbc (Pure.FunId (FRegular global.body), None, None))
       ctx
   in
 
@@ -1958,8 +1958,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
               =
             (* We do something special to reuse the [ctx_compute_fun_decl]
                function. TODO: make it cleaner. *)
-            let basename : name = [ Ident item_name ] in
-            let f = { f with basename } in
+            let llbc_name : Types.name =
+              [ Types.PeIdent (item_name, Disambiguator.zero) ]
+            in
+            let f = { f with llbc_name } in
             let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in
             let name = ctx_compute_fun_name trans f ctx in
             (* Add a prefix if necessary *)
@@ -1991,7 +1993,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
               | None ->
                   let err =
                     "Ill-formed builtin information for trait decl \""
-                    ^ Names.name_to_string trait_decl.name
+                    ^ name_to_string ctx trait_decl.llbc_name
                     ^ "\", method \"" ^ item_name
                     ^ "\": could not find name for region "
                     ^ Print.option_to_string Pure.show_region_group_id
@@ -2022,7 +2024,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
     (trait_decl : trait_decl) : extraction_ctx =
   (* Lookup the information if this is a builtin trait *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name trait_decl.name in
+  let sname = name_to_simple_name trait_decl.llbc_name in
   let builtin_info =
     SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
   in
@@ -2059,8 +2061,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
   (* Check if the trait implementation is builtin *)
   let builtin_info =
     let open ExtractBuiltin in
-    let type_sname = name_to_simple_name trait_impl.name in
-    let trait_sname = name_to_simple_name trait_decl.name in
+    let type_sname = name_to_simple_name trait_impl.llbc_name in
+    let trait_sname = name_to_simple_name trait_decl.llbc_name in
     SimpleNamePairMap.find_opt (type_sname, trait_sname)
       (builtin_trait_impls_map ())
   in
@@ -2185,7 +2187,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt
-    [ "Trait declaration: [" ^ Print.name_to_string decl.name ^ "]" ];
+    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ];
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
      one line and indents are correct.
@@ -2466,14 +2468,14 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
 (** Extract a trait implementation *)
 let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
-  log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name));
+  log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
   (* Retrieve the impl name *)
   let impl_name = ctx_get_trait_impl impl.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt
-    [ "Trait implementation: [" ^ Print.name_to_string impl.name ^ "]" ];
+    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ];
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
@@ -2640,7 +2642,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_break fmt 0 0;
     (* Print a comment *)
     extract_comment fmt
-      [ "Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]" ];
+      [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ];
     F.pp_print_space fmt ();
     (* Open a box for the test *)
     F.pp_open_hovbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 553d5863..e4617d2c 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -309,7 +309,6 @@ let assumed_llbc_functions () :
         (SliceIndexShared, None, "slice_index_usize");
         (SliceIndexMut, None, "slice_index_usize");
         (SliceIndexMut, rg0, "slice_update_usize");
-        (SliceLen, None, "slice_len");
       ]
   | Lean ->
       [
@@ -323,7 +322,6 @@ let assumed_llbc_functions () :
         (SliceIndexShared, None, "Slice.index_usize");
         (SliceIndexMut, None, "Slice.index_usize");
         (SliceIndexMut, rg0, "Slice.update_usize");
-        (SliceLen, None, "Slice.len");
       ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
@@ -538,6 +536,11 @@ let type_keyword () =
   | Coq | Lean -> "Type"
   | HOL4 -> raise (Failure "Unexpected")
 
+let name_last_elem_as_ident (n : llbc_name) : string =
+  match Collections.List.last n with
+  | PeIdent (s, _) -> s
+  | PeImpl _ -> raise (Failure "Unexpected")
+
 (**
    [ctx]: we use the context to lookup type definitions, to retrieve type names.
    This is used to compute variable names, when they have no basenames: in this
@@ -579,34 +582,90 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let int_name = int_name in
 
   (* Prepare a name.
-   * The first id elem is always the crate: if it is the local crate,
-   * we remove it.
-   * We also remove all the disambiguators, then convert everything to strings.
-   * **Rmk:** because we remove the disambiguators, there may be name collisions
-   * (which is ok, because we check for name collisions and fail if there is any).
-   *)
-  let get_name (name : name) : string list =
+     The first id elem is always the crate: if it is the local crate,
+     we remove it. We ignore disambiguators (there may be collisions, but we
+     check if there are).
+  *)
+  let rec name_to_simple_name (name : llbc_name) : string list =
     (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
-    let name = Names.filter_disambiguators name in
     match name with
-    | Ident crate :: name ->
-        let name = if crate = crate_name then name else Ident crate :: name in
+    | (PeIdent (crate, _) as id) :: name ->
+        let name = if crate = crate_name then name else id :: name in
+        let open Types in
         let name =
           List.map
             (function
-              | Names.Ident s -> s
-              | Disambiguator d -> Names.Disambiguator.to_string d)
+              | PeIdent (s, _) -> s
+              | PeImpl impl -> impl_elem_to_simple_name impl)
             name
         in
         name
     | _ ->
-        raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
+        raise
+          (Failure
+             ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
+  and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
+    (* We do something simple for now.
+       TODO: we might want to do something different for impl elements which are
+       actually trait implementations, in order to prevent name collisions (it
+       is possible to define several times the same trait for the same type,
+       but with different instantiations of the type, or different trait
+       requirements *)
+    ty_to_simple_name impl.generics impl.ty
+  and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
+      string =
+    (* We do something simple for now.
+       TODO: find a more principled way of converting types to names.
+       In particular, we might want to do something different for impl elements which are
+       actually trait implementations, in order to prevent name collisions (it
+       is possible to define several times the same trait for the same type,
+       but with different instantiations of the type, or different trait
+       requirements *)
+    match ty with
+    | TAdt (id, args) -> (
+        match id with
+        | TAdtId id ->
+            let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
+            name_last_elem_as_ident def.name
+        | TTuple ->
+            (* TODO *)
+            "Tuple"
+            ^ String.concat ""
+                (List.map (ty_to_simple_name generics) args.types)
+        | TAssumed id -> Types.show_assumed_ty id)
+    | TVar vid ->
+        (* Use the variable name *)
+        (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
+    | TLiteral lty ->
+        StringUtils.capitalize_first_letter
+          (Print.Types.literal_type_to_string lty)
+    | TNever -> raise (Failure "Unreachable")
+    | TRef (_, rty, rk) -> (
+        let rty = ty_to_simple_name generics rty in
+        match rk with
+        | RMut -> "MutBorrow" ^ rty
+        | RShared -> "SharedBorrow" ^ rty)
+    | TRawPtr (rty, rk) -> (
+        let rty = ty_to_simple_name generics rty in
+        match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
+    | TTraitType (tr, _, name) ->
+        (* TODO: this is way too simple *)
+        let trait_decl =
+          TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
+            ctx.trait_decls_ctx.trait_decls
+        in
+        name_last_elem_as_ident trait_decl.name ^ name
+    | TArrow (inputs, output) ->
+        "Arrow"
+        ^ String.concat ""
+            (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
   in
   let flatten_name (name : string list) : string =
     match !backend with
     | FStar | Coq | HOL4 -> String.concat "_" name
     | Lean -> String.concat "." name
   in
+  let get_name name : string list = name_to_simple_name name in
   let get_type_name = get_name in
   let get_type_name_no_suffix name =
     match !backend with
@@ -620,7 +679,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t"
     | Lean -> get_type_name_no_suffix name
   in
-  let field_name (def_name : name) (field_id : FieldId.id)
+  let field_name (def_name : llbc_name) (field_id : FieldId.id)
       (field_name : string option) : string =
     let field_name_s =
       match field_name with
@@ -639,7 +698,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
       | Lean | HOL4 -> def_name
       | Coq | FStar -> StringUtils.lowercase_first_letter def_name
   in
-  let variant_name (def_name : name) (variant : string) : string =
+  let variant_name (def_name : llbc_name) (variant : string) : string =
     match !backend with
     | FStar | Coq | HOL4 ->
         let variant = to_camel_case variant in
@@ -649,7 +708,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         else variant
     | Lean -> variant
   in
-  let struct_constructor (basename : name) : string =
+  let struct_constructor (basename : llbc_name) : string =
     let tname = type_name basename in
     ExtractBuiltin.mk_struct_constructor tname
   in
@@ -661,15 +720,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
     | Lean -> fname
   in
-  let global_name (name : global_name) : string =
+  let global_name (name : llbc_name) : string =
     (* Converting to snake case also lowercases the letters (in Rust, global
      * names are written in capital letters). *)
     let parts = List.map to_snake_case (get_name name) in
     String.concat "_" parts
   in
-  let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option)
-      (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int)
-      : string =
+  let fun_name (fname : llbc_name) (num_loops : int)
+      (loop_id : LoopId.id option) (num_rgs : int)
+      (rg : region_group_info option) (filter_info : bool * int) : string =
     let fname = get_fun_name fname in
     (* Compute the suffix *)
     let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
@@ -678,7 +737,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
 
   let trait_decl_name (trait_decl : trait_decl) : string =
-    type_name trait_decl.name
+    type_name trait_decl.llbc_name
   in
 
   let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
@@ -686,12 +745,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     (* TODO: provisional: we concatenate the trait impl name (which is its type)
        with the trait decl name *)
     let trait_decl =
-      let name = trait_decl.name in
+      let name = trait_decl.llbc_name in
       let name = get_type_name_no_suffix name ^ "Inst" in
       (* Remove the occurrences of '.' *)
       String.concat "" (String.split_on_char '.' name)
     in
-    let name = flatten_name (get_type_name trait_impl.name @ [ trait_decl ]) in
+    let name =
+      flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ])
+    in
     match !backend with
     | FStar -> StringUtils.lowercase_first_letter name
     | Coq | HOL4 | Lean -> name
@@ -745,7 +806,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     ^ TraitClauseId.to_string clause.clause_id
   in
 
-  let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name)
+  let termination_measure_name (_fid : A.FunDeclId.id) (fname : llbc_name)
       (num_loops : int) (loop_id : LoopId.id option) : string =
     let fname = get_fun_name fname in
     let lp_suffix = default_fun_loop_suffix num_loops loop_id in
@@ -760,7 +821,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ lp_suffix ^ suffix
   in
 
-  let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name)
+  let decreases_proof_name (_fid : A.FunDeclId.id) (fname : llbc_name)
       (num_loops : int) (loop_id : LoopId.id option) : string =
     let fname = get_fun_name fname in
     let lp_suffix = default_fun_loop_suffix num_loops loop_id in
@@ -815,12 +876,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             | TAdtId adt_id ->
                 let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
                 (* Derive the var name from the last ident of the type name
-                 * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
-                 *)
+                   Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
+                *)
                 (* The name shouldn't be empty, and its last element should
                  * be an ident *)
-                let cl = List.nth def.name (List.length def.name - 1) in
-                name_from_type_ident (Names.as_ident cl))
+                let cl = Collections.List.last def.name in
+                name_from_type_ident (TypesUtils.as_ident cl))
         | TVar _ -> (
             (* TODO: use "t" also for F* *)
             match !backend with
@@ -866,31 +927,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     match cv with
     | VScalar sv -> (
         match !backend with
-        | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+        | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
         | Coq | HOL4 | Lean ->
             let print_brackets = inside && !backend = HOL4 in
             if print_brackets then F.pp_print_string fmt "(";
             (match !backend with
             | Coq | Lean -> ()
             | HOL4 ->
-                F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty);
+                F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
                 F.pp_print_space fmt ()
             | _ -> raise (Failure "Unreachable"));
             (* We need to add parentheses if the value is negative *)
-            if sv.PV.value >= Z.of_int 0 then
-              F.pp_print_string fmt (Z.to_string sv.PV.value)
+            if sv.value >= Z.of_int 0 then
+              F.pp_print_string fmt (Z.to_string sv.value)
             else if !backend = Lean then
               (* TODO: parsing issues with Lean because there are ambiguous
                  interpretations between int values and nat values *)
               F.pp_print_string fmt
-                ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))")
-            else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
+                ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))")
+            else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
             (match !backend with
             | Coq ->
-                let iname = int_name sv.PV.int_ty in
+                let iname = int_name sv.int_ty in
                 F.pp_print_string fmt ("%" ^ iname)
             | Lean ->
-                let iname = String.lowercase_ascii (int_name sv.PV.int_ty) in
+                let iname = String.lowercase_ascii (int_name sv.int_ty) in
                 F.pp_print_string fmt ("#" ^ iname)
             | HOL4 -> ()
             | _ -> raise (Failure "Unreachable"));
@@ -1426,7 +1487,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     extraction_ctx =
   (* Lookup the builtin information, if there is *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name def.name in
+  let sname = name_to_simple_name def.llbc_name in
   let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
   (* Register the filtering information, if there is *)
   let ctx =
@@ -1442,7 +1503,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
   (* Compute and register the type def name *)
   let def_name =
     match info with
-    | None -> ctx.fmt.type_name def.name
+    | None -> ctx.fmt.type_name def.llbc_name
     | Some info -> info.extract_name
   in
   let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
@@ -1460,10 +1521,10 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
               let field_names =
                 FieldId.mapi
                   (fun fid (field : field) ->
-                    (fid, ctx.fmt.field_name def.name fid field.field_name))
+                    (fid, ctx.fmt.field_name def.llbc_name fid field.field_name))
                   fields
               in
-              let cons_name = ctx.fmt.struct_constructor def.name in
+              let cons_name = ctx.fmt.struct_constructor def.llbc_name in
               (field_names, cons_name)
           | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
               let field_names =
@@ -1499,12 +1560,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
               VariantId.mapi
                 (fun variant_id (variant : variant) ->
                   let name =
-                    ctx.fmt.variant_name def.name variant.variant_name
+                    ctx.fmt.variant_name def.llbc_name variant.variant_name
                   in
                   (* Add the type name prefix for Lean *)
                   let name =
                     if !Config.backend = Lean then
-                      let type_name = ctx.fmt.type_name def.name in
+                      let type_name = ctx.fmt.type_name def.llbc_name in
                       type_name ^ "." ^ name
                     else name
                   in
@@ -1648,7 +1709,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
   let print_variant _variant_id (v : variant) =
     (* We don't lookup the name, because it may have a prefix for the type
        id (in the case of Lean) *)
-    let cons_name = ctx.fmt.variant_name def.name v.variant_name in
+    let cons_name = ctx.fmt.variant_name def.llbc_name v.variant_name in
     let fields = v.fields in
     extract_type_decl_variant ctx fmt type_decl_group def_name type_params
       cg_params cons_name fields
@@ -2030,7 +2091,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if !backend <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt [ "[" ^ Print.name_to_string def.name ^ "]" ];
+  extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ];
   F.pp_print_break fmt 0 0;
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 57aa9e12..a07ad35a 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -164,7 +164,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
   let analyze_fun_decl_group (d : fun_declaration_group) : unit =
     (* Retrieve the function declarations *)
-    let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in
+    let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
     let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in
     let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in
     let fun_ids = FunDeclId.Set.of_list fun_ids in
@@ -183,7 +183,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
     | GlobalGroup id :: decls' ->
         (* Analyze a global by analyzing its body function *)
         let global = GlobalDeclId.Map.find id globals_map in
-        analyze_fun_decl_group (NonRec global.body);
+        analyze_fun_decl_group (NonRecGroup global.body);
         analyze_decl_groups decls'
   in
 
diff --git a/compiler/Print.ml b/compiler/Print.ml
index cd83a589..48a5a20b 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,6 +1,5 @@
 include Charon.PrintUtils
 include Charon.PrintLlbcAst
-open Charon.PrintPrimitiveValues
 open Charon.PrintTypes
 open Charon.PrintExpressions
 open Charon.PrintLlbcAst.Ast
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fa059499..40711e53 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -14,6 +14,7 @@ module GlobalDeclId = A.GlobalDeclId
 module TraitDeclId = T.TraitDeclId
 module TraitImplId = T.TraitImplId
 module TraitClauseId = T.TraitClauseId
+module Disambiguator = T.Disambiguator
 
 (** We redefine identifiers for loop: in {!Values}, the identifiers are global
     (they monotonically increase across functions) while in {!module:Pure} we want
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d2747a4b..2106c206 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -3,10 +3,13 @@
 open Pure
 open PureUtils
 open TranslateCore
-module V = Values
 
 (** The local logger *)
-let log = L.pure_micro_passes_log
+let log = Logging.pure_micro_passes_log
+
+let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_decl_to_string fmt def
 
 (** Small utility.
 
@@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     match
                       TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups
                     with
-                    | NonRec _ -> false
-                    | Rec _ -> true
+                    | NonRecGroup _ -> false
+                    | RecGroup _ -> true
                   in
                   (* Convert, if possible - note that for now for Lean and Coq
                      we don't support the structure syntax on recursive structures *)
@@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
 
             let loop_body = { inputs; inputs_lvs; body = loop_body } in
 
-            let loop_def =
+            let loop_def : fun_decl =
               {
                 def_id = def.def_id;
                 kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
                 back_id = def.back_id;
-                basename = def.basename;
+                llbc_name = def.llbc_name;
+                name = def.name;
                 signature = loop_sig;
                 is_global_decl_body = def.is_global_decl_body;
                 body = Some loop_body;
@@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     mk_unit_rvalue
                 | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
                     | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
-                    | ArrayRepeat | SliceLen ),
+                    | ArrayRepeat ),
                     _ ) ->
                     super#visit_texpression env e)
-            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) ->
+                failwith "TODO"
+                (*
                 (* Lookup the function name *)
                 let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
                 match
@@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       | _ -> raise (Failure "Unreachable")
                     in
                     mk_apps arg args
-                | _ -> super#visit_texpression env e)
+                | _ -> super#visit_texpression env e
+                       *)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
@@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
   (* Debug *)
   log#ldebug
     (lazy
-      ("PureMicroPasses.apply_passes_to_def: "
-      ^ Print.fun_name_to_string def.basename
-      ^ " ("
+      ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string def.back_id
       ^ ")"));
 
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.
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2aedb544..cf23fd44 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1,11 +1,11 @@
-open InterpreterStatements
 open Interpreter
-module L = Logging
-module T = Types
-module A = LlbcAst
+open Expressions
+open Types
+open Values
+open LlbcAst
+open Contexts
 module SA = SymbolicAst
 module Micro = PureMicroPasses
-module C = Contexts
 open PureUtils
 open TranslateCore
 
@@ -16,18 +16,17 @@ let log = TranslateCore.log
     - the list of symbolic values used for the input values
     - the generated symbolic AST
 *)
-type symbolic_fun_translation = V.symbolic_value list * SA.expression
+type symbolic_fun_translation = symbolic_value list * SA.expression
 
 (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
     for the forward function and the backward functions.
 *)
-let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
-    : symbolic_fun_translation option =
+let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
+    symbolic_fun_translation option =
   (* Debug *)
   log#ldebug
     (lazy
-      ("translate_function_to_symbolics: "
-      ^ Print.fun_name_to_string fdef.A.name));
+      ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name));
 
   match fdef.body with
   | None -> None
@@ -45,12 +44,11 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
 *)
 let translate_function_to_pure (trans_ctx : trans_ctx)
     (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t)
-    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
-    : pure_fun_translation_no_loops =
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) :
+    pure_fun_translation_no_loops =
   (* Debug *)
   log#ldebug
-    (lazy
-      ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
+    (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name));
 
   let def_id = fdef.def_id in
 
@@ -61,22 +59,24 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
   (* Initialize the context *)
   let forward_sig =
-    RegularFunIdNotLoopMap.find (E.FRegular def_id, None) fun_sigs
+    RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs
   in
-  let sv_to_var = V.SymbolicValueId.Map.empty in
+  let sv_to_var = SymbolicValueId.Map.empty in
   let var_counter = Pure.VarId.generator_zero in
   let state_var, var_counter = Pure.VarId.fresh var_counter in
   let back_state_var, var_counter = Pure.VarId.fresh var_counter in
   let fuel0, var_counter = Pure.VarId.fresh var_counter in
   let fuel, var_counter = Pure.VarId.fresh var_counter in
-  let calls = V.FunCallId.Map.empty in
-  let abstractions = V.AbstractionId.Map.empty in
+  let calls = FunCallId.Map.empty in
+  let abstractions = AbstractionId.Map.empty in
   let recursive_type_decls =
-    T.TypeDeclId.Set.of_list
+    TypeDeclId.Set.of_list
       (List.filter_map
          (fun (tid, g) ->
-           match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid)
-         (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
+           match g with
+           | Charon.GAst.NonRecGroup _ -> None
+           | RecGroup _ -> Some tid)
+         (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
   in
   let type_context =
     {
@@ -104,9 +104,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   *)
   let loop_ids_map =
     match symbolic_trans with
-    | None -> V.LoopId.Map.empty
+    | None -> LoopId.Map.empty
     | Some (_, ast) ->
-        let m = ref V.LoopId.Map.empty in
+        let m = ref LoopId.Map.empty in
         let _, fresh_loop_id = Pure.LoopId.fresh_stateful_generator () in
 
         let visitor =
@@ -115,10 +115,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
             method! visit_loop env loop =
               let _ =
-                match V.LoopId.Map.find_opt loop.loop_id !m with
+                match LoopId.Map.find_opt loop.loop_id !m with
                 | Some _ -> ()
-                | None ->
-                    m := V.LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
+                | None -> m := LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
               in
               super#visit_loop env loop
           end
@@ -148,9 +147,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       fun_decl = fdef;
       forward_inputs = [];
       (* Empty for now *)
-      backward_inputs = T.RegionGroupId.Map.empty;
+      backward_inputs = RegionGroupId.Map.empty;
       (* Empty for now *)
-      backward_outputs = T.RegionGroupId.Map.empty;
+      backward_outputs = RegionGroupId.Map.empty;
       loop_backward_outputs = None;
       (* Empty for now *)
       calls;
@@ -171,7 +170,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     | Some body, Some (input_svs, _) ->
         let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in
         let forward_input_varnames =
-          List.map (fun (v : A.var) -> v.name) forward_input_vars
+          List.map (fun (v : var) -> v.name) forward_input_vars
         in
         let input_svs = List.combine forward_input_varnames input_svs in
         let ctx, forward_inputs =
@@ -189,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   in
 
   (* Translate the backward functions *)
-  let translate_backward (rg : T.region_group) : Pure.fun_decl =
+  let translate_backward (rg : region_group) : Pure.fun_decl =
     (* For the backward inputs/outputs initialization: we use the fact that
      * there are no nested borrows for now, and so that the region groups
      * can't have parents *)
@@ -244,10 +243,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
           SymbolicToPure.fresh_vars backward_outputs ctx
         in
         let backward_inputs =
-          T.RegionGroupId.Map.singleton back_id backward_inputs
+          RegionGroupId.Map.singleton back_id backward_inputs
         in
         let backward_outputs =
-          T.RegionGroupId.Map.singleton back_id backward_outputs
+          RegionGroupId.Map.singleton back_id backward_outputs
         in
 
         (* Put everything in the context *)
@@ -274,7 +273,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   (pure_forward, pure_backwards)
 
 (* TODO: factor out the return type *)
-let translate_crate_to_pure (crate : A.crate) :
+let translate_crate_to_pure (crate : crate) :
     trans_ctx
     * Pure.type_decl list
     * pure_fun_translation list
@@ -287,9 +286,7 @@ let translate_crate_to_pure (crate : A.crate) :
   let trans_ctx = compute_contexts crate in
 
   (* Translate all the type definitions *)
-  let type_decls =
-    SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
-  in
+  let type_decls = SymbolicToPure.translate_type_decls trans_ctx in
 
   (* Compute the type definition map *)
   let type_decls_map =
@@ -301,24 +298,24 @@ let translate_crate_to_pure (crate : A.crate) :
   let assumed_sigs =
     List.map
       (fun (info : Assumed.assumed_fun_info) ->
-        ( E.FAssumed info.fun_id,
+        ( FAssumed info.fun_id,
           List.map (fun _ -> None) info.fun_sig.inputs,
           info.fun_sig ))
       Assumed.assumed_fun_infos
   in
   let local_sigs =
     List.map
-      (fun (fdef : A.fun_decl) ->
+      (fun (fdef : fun_decl) ->
         let input_names =
           match fdef.body with
           | None -> List.map (fun _ -> None) fdef.signature.inputs
           | Some body ->
               List.map
-                (fun (v : A.var) -> v.name)
+                (fun (v : var) -> v.name)
                 (LlbcAstUtils.fun_body_get_input_vars body)
         in
-        (E.FRegular fdef.def_id, input_names, fdef.signature))
-      (A.FunDeclId.Map.values crate.functions)
+        (FRegular fdef.def_id, input_names, fdef.signature))
+      (FunDeclId.Map.values crate.fun_decls)
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in
@@ -327,22 +324,21 @@ let translate_crate_to_pure (crate : A.crate) :
   let pure_translations =
     List.map
       (translate_function_to_pure trans_ctx fun_sigs type_decls_map)
-      (A.FunDeclId.Map.values crate.functions)
+      (FunDeclId.Map.values crate.fun_decls)
   in
 
   (* Translate the trait declarations *)
-  let type_infos = trans_ctx.type_ctx.type_infos in
   let trait_decls =
     List.map
-      (SymbolicToPure.translate_trait_decl type_infos)
-      (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
+      (SymbolicToPure.translate_trait_decl trans_ctx)
+      (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
 
   (* Translate the trait implementations *)
   let trait_impls =
     List.map
-      (SymbolicToPure.translate_trait_impl type_infos)
-      (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
+      (SymbolicToPure.translate_trait_impl trans_ctx)
+      (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
   (* Apply the micro-passes *)
@@ -401,9 +397,9 @@ let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) :
   log#ldebug
     (lazy
       ("Opaque decls:" ^ "\n- types:\n"
-      ^ String.concat ",\n" (List.map T.show_type_decl types)
+      ^ String.concat ",\n" (List.map show_type_decl types)
       ^ "\n- functions:\n"
-      ^ String.concat ",\n" (List.map A.show_fun_decl funs)));
+      ^ String.concat ",\n" (List.map show_fun_decl funs)));
   (types <> [], funs <> [])
 
 (** Export a type declaration.
@@ -481,7 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     let types_map = builtin_types_map () in
     List.map
       (fun (def : Pure.type_decl) ->
-        let sname = name_to_simple_name def.name in
+        let sname = name_to_simple_name def.llbc_name in
         SimpleNameMap.find_opt sname types_map <> None)
       defs
   in
@@ -531,10 +527,10 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     TODO: check correct behavior with opaque globals.
  *)
 let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
-    (id : A.GlobalDeclId.id) : unit =
+    (id : GlobalDeclId.id) : unit =
   let global_decls = ctx.trans_ctx.global_ctx.global_decls in
-  let global = A.GlobalDeclId.Map.find id global_decls in
-  let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+  let global = GlobalDeclId.Map.find id global_decls in
+  let trans = FunDeclId.Map.find global.body ctx.trans_funs in
   assert (trans.fwd.loops = []);
   assert (trans.backs = []);
   let body = trans.fwd.f in
@@ -665,7 +661,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
     let funs_map = builtin_funs_map () in
     List.map
       (fun (trans : pure_fun_translation) ->
-        let sname = name_to_simple_name trans.fwd.f.basename in
+        let sname = name_to_simple_name trans.fwd.f.llbc_name in
         SimpleNameMap.find_opt sname funs_map <> None)
       pure_ls
   in
@@ -756,10 +752,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool)
     (extract_extra_info : bool) : unit =
-  let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
+  let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
   (* Check if the trait declaration is builtin, in which case we ignore it *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name trait_decl.name in
+  let sname = name_to_simple_name trait_decl.llbc_name in
   if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
     if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl;
@@ -771,7 +767,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
   (* Lookup the definition *)
-  let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
+  let trait_impl = TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
   let trait_decl =
     Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
       ctx.trans_trait_decls
@@ -779,8 +775,8 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
   (* Check if the trait implementation is builtin *)
   let builtin_info =
     let open ExtractBuiltin in
-    let type_sname = name_to_simple_name trait_impl.name in
-    let trait_sname = name_to_simple_name trait_decl.name in
+    let type_sname = name_to_simple_name trait_impl.llbc_name in
+    let trait_sname = name_to_simple_name trait_decl.llbc_name in
     SimpleNamePairMap.find_opt (type_sname, trait_sname)
       (builtin_trait_impls_map ())
   in
@@ -817,14 +813,15 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     Extract.extract_state_type fmt ctx kind
   in
 
-  let export_decl_group (dg : A.declaration_group) : unit =
+  let export_decl_group (dg : declaration_group) : unit =
     match dg with
-    | Type (NonRec id) ->
+    | TypeGroup (NonRecGroup id) ->
         if config.extract_types then export_types_group false [ id ]
-    | Type (Rec ids) -> if config.extract_types then export_types_group true ids
-    | Fun (NonRec id) -> (
+    | TypeGroup (RecGroup ids) ->
+        if config.extract_types then export_types_group true ids
+    | FunGroup (NonRecGroup id) -> (
         (* Lookup *)
-        let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
+        let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
         (* Special case: we skip trait method *declarations* (we will
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
@@ -834,21 +831,21 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         | _ ->
             (* Translate *)
             export_functions_group [ pure_fun ])
-    | Fun (Rec ids) ->
+    | FunGroup (RecGroup ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids
+          List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
         in
         (* Translate *)
         export_functions_group pure_funs
-    | Global id -> export_global id
-    | TraitDecl id ->
+    | GlobalGroup id -> export_global id
+    | TraitDeclGroup id ->
         (* TODO: update to extract groups *)
         if config.extract_trait_decls && config.extract_transparent then (
           export_trait_decl_group id;
           export_trait_decl_group_extra_info id)
-    | TraitImpl id ->
+    | TraitImplGroup id ->
         if config.extract_trait_impls && config.extract_transparent then
           export_trait_impl id
   in
@@ -986,7 +983,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   close_out out
 
 (** Translate a crate and write the synthesized code to an output file. *)
-let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
+let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     unit =
   (* Translate the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
@@ -1036,8 +1033,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
   in
-  let trans_funs : pure_fun_translation A.FunDeclId.Map.t =
-    A.FunDeclId.Map.of_list
+  let trans_funs : pure_fun_translation FunDeclId.Map.t =
+    FunDeclId.Map.of_list
       (List.map
          (fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans))
          trans_funs)
@@ -1046,13 +1043,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   (* Put everything in the context *)
   let ctx =
     let trans_trait_decls =
-      T.TraitDeclId.Map.of_list
+      TraitDeclId.Map.of_list
         (List.map
            (fun (d : Pure.trait_decl) -> (d.def_id, d))
            trans_trait_decls)
     in
     let trans_trait_impls =
-      T.TraitImplId.Map.of_list
+      TraitImplId.Map.of_list
         (List.map
            (fun (d : Pure.trait_impl) -> (d.def_id, d))
            trans_trait_impls)
@@ -1107,12 +1104,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         if is_global then ctx
         else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans)
       ctx
-      (A.FunDeclId.Map.values trans_funs)
+      (FunDeclId.Map.values trans_funs)
   in
 
   let ctx =
     List.fold_left Extract.extract_global_decl_register_names ctx
-      (A.GlobalDeclId.Map.values crate.globals)
+      (GlobalDeclId.Map.values crate.global_decls)
   in
 
   let ctx =
@@ -1291,7 +1288,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          namespace;
          in_namespace = true;
          crate_name;
-         rust_module_name = crate.A.name;
+         rust_module_name = crate.name;
          module_name = types_module;
          custom_msg = ": type definitions";
          custom_imports = [];
@@ -1319,7 +1316,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
             namespace;
             in_namespace = true;
             crate_name;
-            rust_module_name = crate.A.name;
+            rust_module_name = crate.name;
             module_name = template_clauses_module;
             custom_msg = ": templates for the decreases clauses";
             custom_imports = [ types_module ];
@@ -1369,7 +1366,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
              namespace;
              in_namespace = false;
              crate_name;
-             rust_module_name = crate.A.name;
+             rust_module_name = crate.name;
              module_name = opaque_module;
              custom_msg;
              custom_imports = [];
@@ -1408,7 +1405,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          namespace;
          in_namespace = true;
          crate_name;
-         rust_module_name = crate.A.name;
+         rust_module_name = crate.name;
          module_name = fun_module;
          custom_msg = ": function definitions";
          custom_imports = [];
@@ -1441,7 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          namespace;
          in_namespace = true;
          crate_name;
-         rust_module_name = crate.A.name;
+         rust_module_name = crate.name;
          module_name = crate_name;
          custom_msg = "";
          custom_imports = [];
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index a148175d..a974cdee 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -26,3 +26,6 @@ let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env =
 
 let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env =
   PrintPure.decls_ctx_to_fmt_env ctx
+
+let name_to_string (ctx : trans_ctx) =
+  Print.Types.name_to_string (trans_ctx_to_fmt_env ctx)
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 659eac59..5371a3d7 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -283,7 +283,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
 let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
     (infos : type_infos) (decl : A.type_declaration_group) : type_infos =
   (* Collect the identifiers used in the declaration group *)
-  let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in
+  let ids = match decl with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
   (* Retrieve the type definitions *)
   let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in
   (* Initialize the type information for the current definitions *)