Reorganize the "Extract" files

7 files changed, 1299 insertions, 1439 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index a487f9e2..fe110ee4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -336,3 +336,30 @@ let type_check_pure_code = ref false
 (** Shall we fail hard if we encounter an issue, or should we attempt to go
     as far as possible while leaving "holes" in the generated code? *)
 let fail_hard = ref true
+
+(** if true, add the type name as a prefix
+    to the variant names.
+    Ex.:
+    In Rust:
+      {[
+        enum List = {
+          Cons(u32, Box<List>),x
+          Nil,
+        }
+      ]}
+
+    F*, if option activated:
+      {[
+        type list =
+        | ListCons : u32 -> list -> list
+        | ListNil : list
+      ]}
+
+    F*, if option not activated:
+      {[
+        type list =
+        | Cons : u32 -> list -> list
+        | Nil : list
+      ]}
+ *)
+let variant_concatenate_type_name = ref true
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d7b4c152..16262c91 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -6,7 +6,6 @@
 open Pure
 open PureUtils
 open TranslateCore
-open ExtractBase
 open Config
 include ExtractTypes
 
@@ -236,12 +235,10 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
     (is_let : bool) (inside : bool) (v : typed_pattern) : extraction_ctx =
   match v.value with
   | PatConstant cv ->
-      ctx.fmt.extract_literal fmt inside cv;
+      extract_literal fmt inside cv;
       ctx
   | PatVar (v, _) ->
-      let vname =
-        ctx.fmt.var_basename ctx.names_maps.names_map.names_set v.basename v.ty
-      in
+      let vname = ctx_compute_var_basename ctx v.basename v.ty in
       let ctx, vname = ctx_add_var vname v.id ctx in
       F.pp_print_string fmt vname;
       ctx
@@ -274,7 +271,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
   | CVar var_id ->
       let var_name = ctx_get_const_generic_var var_id ctx in
       F.pp_print_string fmt var_name
-  | Const cv -> ctx.fmt.extract_literal fmt inside cv
+  | Const cv -> extract_literal fmt inside cv
   | App _ ->
       let app, args = destruct_apps e in
       extract_App ctx fmt inside app args
@@ -354,10 +351,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
        * Note that the way we generate the translation, we shouldn't get the
        * case where we have no argument (all functions are fully instantiated,
        * and no AST transformation introduces partial calls). *)
-      ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+      extract_unop (extract_texpression ctx fmt) fmt inside unop arg
   | Binop (binop, int_ty), [ arg0; arg1 ] ->
       (* Number of arguments: similar to unop *)
-      ctx.fmt.extract_binop
+      extract_binop
         (extract_texpression ctx fmt)
         fmt inside binop int_ty arg0 arg1
   | Fun fun_id, _ ->
@@ -1359,7 +1356,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     is_opaque_coq && def.signature.generics <> empty_generic_params
   in
   (* Print the qualifier ("assume", etc.). *)
-  let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
+  let qualif = fun_decl_kind_to_qualif kind in
   (match qualif with
   | Some qualif ->
       F.pp_print_string fmt qualif;
@@ -1655,7 +1652,7 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "QUALIF NAME " *)
-  (match ctx.fmt.fun_decl_kind_to_qualif kind with
+  (match fun_decl_kind_to_qualif kind with
   | Some qualif ->
       F.pp_print_string fmt qualif;
       F.pp_print_space fmt ()
@@ -1824,11 +1821,11 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
     | None ->
         List.map
           (fun (c : trait_clause) ->
-            let name = ctx.fmt.trait_parent_clause_name trait_decl c in
+            let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in
             (* Add a prefix if necessary *)
             let name =
               if !Config.record_fields_short_names then name
-              else ctx.fmt.trait_decl_name trait_decl ^ name
+              else ctx_compute_trait_decl_name ctx trait_decl ^ name
             in
             (c.clause_id, name))
           trait_decl.parent_clauses
@@ -1855,11 +1852,11 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
     | None ->
         List.map
           (fun (item_name, _) ->
-            let name = ctx.fmt.trait_const_name trait_decl item_name in
+            let name = ctx_compute_trait_const_name ctx trait_decl item_name in
             (* Add a prefix if necessary *)
             let name =
               if !Config.record_fields_short_names then name
-              else ctx.fmt.trait_decl_name trait_decl ^ name
+              else ctx_compute_trait_decl_name ctx trait_decl ^ name
             in
             (item_name, name))
           consts
@@ -1887,19 +1884,21 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
     match builtin_info with
     | None ->
         let compute_type_name (item_name : string) : string =
-          let type_name = ctx.fmt.trait_type_name trait_decl item_name in
+          let type_name =
+            ctx_compute_trait_type_name ctx trait_decl item_name
+          in
           if !Config.record_fields_short_names then type_name
-          else ctx.fmt.trait_decl_name trait_decl ^ type_name
+          else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
         in
         let compute_clause_name (item_name : string) (clause : trait_clause) :
             TraitClauseId.id * string =
           let name =
-            ctx.fmt.trait_type_clause_name trait_decl item_name clause
+            ctx_compute_trait_type_clause_name ctx trait_decl item_name clause
           in
           (* Add a prefix if necessary *)
           let name =
             if !Config.record_fields_short_names then name
-            else ctx.fmt.trait_decl_name trait_decl ^ name
+            else ctx_compute_trait_decl_name ctx trait_decl ^ name
           in
           (clause.clause_id, name)
         in
@@ -1971,7 +1970,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
             (* Add a prefix if necessary *)
             let name =
               if !Config.record_fields_short_names then name
-              else ctx.fmt.trait_decl_name trait_decl ^ "_" ^ name
+              else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name
             in
             (f.back_id, name)
           in
@@ -2036,8 +2035,8 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
     let trait_name, trait_constructor =
       match builtin_info with
       | None ->
-          ( ctx.fmt.trait_decl_name trait_decl,
-            ctx.fmt.trait_decl_constructor trait_decl )
+          ( ctx_compute_trait_decl_name ctx trait_decl,
+            ctx_compute_trait_decl_constructor ctx trait_decl )
       | Some info -> (info.extract_name, info.constructor)
     in
     let ctx = ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in
@@ -2101,7 +2100,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
   (* Compute the name *)
   let name =
     match builtin_info with
-    | None -> ctx.fmt.trait_impl_name trait_decl trait_impl
+    | None -> ctx_compute_trait_impl_name ctx trait_decl trait_impl
     | Some name -> name
   in
   ctx_add (TraitImplId trait_impl.def_id) name ctx
@@ -2214,7 +2213,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open the box for the name + generics *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   let qualif =
-    Option.get (ctx.fmt.type_decl_kind_to_qualif SingleNonRec (Some Struct))
+    Option.get (type_decl_kind_to_qualif SingleNonRec (Some Struct))
   in
   (* When checking if the trait declaration is empty: we ignore the provided
      methods, because for now they are extracted separately *)
@@ -2505,7 +2504,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* `let (....) : Trait ... =` *)
   (* Open the box for the name + generics *)
   F.pp_open_hovbox fmt ctx.indent_incr;
-  (match ctx.fmt.fun_decl_kind_to_qualif SingleNonRec with
+  (match fun_decl_kind_to_qualif SingleNonRec with
   | Some qualif ->
       F.pp_print_string fmt qualif;
       F.pp_print_space fmt ()
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index f1ba35a2..0b9908b2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -2,9 +2,11 @@
 
 open Contexts
 open Pure
-open TranslateCore
+open StringUtils
+open Config
 module F = Format
 open ExtractBuiltin
+open TranslateCore
 
 (** The local logger *)
 let log = Logging.extract_log
@@ -109,225 +111,6 @@ let decl_is_not_last_from_group (kind : decl_kind) : bool =
 
 type type_decl_kind = Enum | Struct [@@deriving show]
 
-(* TODO: this should be a module we give to a functor! *)
-
-(** A formatter's role is twofold:
-    1. Come up with name suggestions.
-    For instance, provided some information about a function (its basename,
-    information about the region group, etc.) it should come up with an
-    appropriate name for the forward/backward function.
-
-    It can of course apply many transformations, like changing to camel case/
-    snake case, adding prefixes/suffixes, etc.
-
-    2. Format some specific terms, like constants.
-
-    TODO: unclear that this is useful now that all the backends are so much
-    entangled in Extract.ml
- *)
-type formatter = {
-  bool_name : string;
-  char_name : string;
-  int_name : integer_type -> string;
-  str_name : string;
-  type_decl_kind_to_qualif :
-    decl_kind -> type_decl_kind option -> string option;
-      (** Compute the qualified for a type definition/declaration.
-
-          For instance: "type", "and", etc.
-
-          Remark: can return [None] for some backends like HOL4.
-       *)
-  fun_decl_kind_to_qualif : decl_kind -> string option;
-      (** Compute the qualified for a function definition/declaration.
-
-          For instance: "let", "let rec", "and", etc.
-
-          Remark: can return [None] for some backends like HOL4.
-       *)
-  field_name : llbc_name -> FieldId.id -> string option -> string;
-      (** Inputs:
-          - type name
-          - field id
-          - field name
-
-          Note that fields don't always have names, but we still need to
-          generate some names if we want to extract the structures to records...
-          We might want to extract such structures to tuples, later, but field
-          access then causes trouble because not all provers accept syntax like
-          [x.3] where [x] is a tuple.
-       *)
-  variant_name : llbc_name -> string -> string;
-      (** Inputs:
-          - type name
-          - variant name
-       *)
-  struct_constructor : llbc_name -> string;
-      (** Structure constructors are used when constructing structure values.
-
-          For instance, in F*:
-          {[
-            type pair = { x : nat; y : nat }
-            let p : pair = Mkpair 0 1
-          ]}
-
-          Inputs:
-          - type name
-      *)
-  type_name : llbc_name -> string;
-      (** Provided a basename, compute a type name. *)
-  global_name : llbc_name -> string;
-      (** Provided a basename, compute a global name. *)
-  fun_name :
-    llbc_name ->
-    int ->
-    LoopId.id option ->
-    int ->
-    region_group_info option ->
-    bool * int ->
-    string;
-      (** Compute the name of a regular (non-assumed) function.
-
-          Inputs:
-          - function basename (TODO: shouldn't appear for assumed functions?...)
-          - number of loops in the function (useful to check if we need to use
-            indices to derive unique names for the loops for instance - if there is
-            exactly one loop, we don't need to use indices)
-          - loop id (if pertinent)
-          - number of region groups
-          - region group information in case of a backward function
-            ([None] if forward function)
-          - pair:
-            - do we generate the forward function (it may have been filtered)?
-            - the number of *extracted backward functions* (same comment as for
-              the number of loops)
-              The number of extracted backward functions if not necessarily
-              equal to the number of region groups, because we may have
-              filtered some of them.
-          TODO: use the fun id for the assumed functions.
-       *)
-  termination_measure_name :
-    A.FunDeclId.id -> llbc_name -> int -> LoopId.id option -> string;
-      (** Generates the name of the termination measure used to prove/reason about
-          termination. The generated code uses this clause where needed,
-          but its body must be defined by the user.
-
-          F* and Lean only.
-
-          Inputs:
-          - function id: this is especially useful to identify whether the
-            function is an assumed function or a local function
-          - function basename
-          - the number of loops in the parent function. This is used for
-            the same purpose as in {!field:llbc_name}.
-          - loop identifier, if this is for a loop
-       *)
-  decreases_proof_name :
-    A.FunDeclId.id -> llbc_name -> int -> LoopId.id option -> string;
-      (** Generates the name of the proof used to prove/reason about
-          termination. The generated code uses this clause where needed,
-          but its body must be defined by the user.
-
-          Lean only.
-
-          Inputs:
-          - function id: this is especially useful to identify whether the
-            function is an assumed function or a local function
-          - function basename
-          - the number of loops in the parent function. This is used for
-            the same purpose as in {!field:llbc_name}.
-          - loop identifier, if this is for a loop
-       *)
-  trait_decl_name : trait_decl -> string;
-  trait_impl_name : trait_decl -> trait_impl -> string;
-  trait_decl_constructor : trait_decl -> string;
-  trait_parent_clause_name : trait_decl -> trait_clause -> string;
-  trait_const_name : trait_decl -> string -> string;
-  trait_type_name : trait_decl -> string -> string;
-  trait_method_name : trait_decl -> string -> string;
-  trait_type_clause_name : trait_decl -> string -> trait_clause -> string;
-  var_basename : StringSet.t -> string option -> ty -> string;
-      (** Generates a variable basename.
-
-          Inputs:
-          - the set of names used in the context so far
-          - the basename we got from the symbolic execution, if we have one
-          - the type of the variable (can be useful for heuristics, in order
-            not to always use "x" for instance, whenever naming anonymous
-            variables)
-
-          Note that once the formatter generated a basename, we add an index
-          if necessary to prevent name clashes: the burden of name clashes checks
-          is thus on the caller's side.
-       *)
-  type_var_basename : StringSet.t -> string -> string;
-      (** Generates a type variable basename. *)
-  const_generic_var_basename : StringSet.t -> string -> string;
-      (** Generates a const generic variable basename. *)
-  trait_self_clause_basename : string;
-  trait_clause_basename : StringSet.t -> trait_clause -> string;
-      (** Return a base name for a trait clause. We might add a suffix to prevent
-          collisions.
-
-          In the traduction we explicitely manipulate the trait clause instances,
-          that is we introduce one input variable for each trait clause.
-       *)
-  append_index : string -> int -> string;
-      (** Appends an index to a name - we use this to generate unique
-          names: when doing so, the role of the formatter is just to concatenate
-          indices to names, the responsability of finding a proper index is
-          delegated to helper functions.
-       *)
-  extract_literal : F.formatter -> bool -> literal -> unit;
-      (** Format a constant value.
-
-          Inputs:
-          - formatter
-          - [inside]: if [true], the value should be wrapped in parentheses
-            if it is made of an application (ex.: [U32 3])
-          - the constant value
-       *)
-  extract_unop :
-    (bool -> texpression -> unit) ->
-    F.formatter ->
-    bool ->
-    unop ->
-    texpression ->
-    unit;
-      (** Format a unary operation
-
-          Inputs:
-          - a formatter for expressions (called on the argument of the unop)
-          - extraction context (see below)
-          - formatter
-          - expression formatter
-          - [inside]
-          - unop
-          - argument
-       *)
-  extract_binop :
-    (bool -> texpression -> unit) ->
-    F.formatter ->
-    bool ->
-    E.binop ->
-    integer_type ->
-    texpression ->
-    texpression ->
-    unit;
-      (** Format a binary operation
-
-          Inputs:
-          - a formatter for expressions (called on the arguments of the binop)
-          - extraction context (see below)
-          - formatter
-          - expression formatter
-          - [inside]
-          - binop
-          - argument 0
-          - argument 1
-       *)
-}
-
 (** We use identifiers to look for name clashes *)
 type id =
   | GlobalId of A.GlobalDeclId.id
@@ -590,6 +373,152 @@ type names_maps = {
        *)
 }
 
+(** Return [true] if we are strict on collisions for this id (i.e., we forbid
+    collisions even with the ids in the unsafe names map) *)
+let strict_collisions (id : id) : bool =
+  match id with UnknownId | TypeId _ -> true | _ -> false
+
+(** We might not check for collisions for some specific ids (ex.: field names) *)
+let allow_collisions (id : id) : bool =
+  match id with
+  | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
+  | TraitMethodId _ ->
+      !Config.record_fields_short_names
+  | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _, _)) ->
+      (* We map several assumed functions to the same id *)
+      true
+  | _ -> false
+
+(** The [id_to_string] function to print nice debugging messages if there are
+    collisions *)
+let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+    (nm : names_maps) : names_maps =
+  (* We do not use the same name map if we allow/disallow collisions.
+     We notably use it for field names: some backends like Lean can use the
+     type information to disambiguate field projections.
+
+     Remark: we still need to check that those "unsafe" ids don't collide with
+     the ids that we mark as "strict on collision".
+
+     For instance, we don't allow naming a field "let". We enforce this by
+     not checking collision between ids for which we permit collisions (ex.:
+     between fields), but still checking collisions between those ids and the
+     others (ex.: fields and keywords).
+  *)
+  if allow_collisions id then (
+    (* Check with the ids which are considered to be strict on collisions *)
+    names_map_check_collision id_to_string id name nm.strict_names_map;
+    {
+      nm with
+      unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
+    })
+  else
+    (* Remark: if we are strict on collisions:
+       - we add the id to the strict collisions map
+       - we check that the id doesn't collide with the unsafe map
+       TODO: we might not check that:
+       - a user defined function doesn't collide with an assumed function
+       - two trait decl items don't collide with each other
+    *)
+    let strict_names_map =
+      if strict_collisions id then
+        names_map_add id_to_string id name nm.strict_names_map
+      else nm.strict_names_map
+    in
+    let names_map = names_map_add id_to_string id name nm.names_map in
+    { nm with strict_names_map; names_map }
+
+(** The [id_to_string] function to print nice debugging messages if there are
+    collisions *)
+let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
+    string =
+  (* We do not use the same name map if we allow/disallow collisions *)
+  let map_to_string (m : string IdMap.t) : string =
+    "[\n"
+    ^ String.concat ","
+        (List.map
+           (fun (id, n) -> "\n  " ^ id_to_string id ^ " -> " ^ n)
+           (IdMap.bindings m))
+    ^ "\n]"
+  in
+  if allow_collisions id then (
+    let m = nm.unsafe_names_map.id_to_name in
+    match IdMap.find_opt id m with
+    | Some s -> s
+    | None ->
+        let err =
+          "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
+          ^ map_to_string m
+        in
+        log#serror err;
+        if !Config.fail_hard then raise (Failure err)
+        else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
+  else
+    let m = nm.names_map.id_to_name in
+    match IdMap.find_opt id m with
+    | Some s -> s
+    | None ->
+        let err =
+          "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
+          ^ map_to_string m
+        in
+        log#serror err;
+        if !Config.fail_hard then raise (Failure err)
+        else "(ERROR: \"" ^ id_to_string id ^ "\")"
+
+type names_map_init = {
+  keywords : string list;
+  assumed_adts : (assumed_ty * string) list;
+  assumed_structs : (assumed_ty * string) list;
+  assumed_variants : (assumed_ty * VariantId.id * string) list;
+  assumed_llbc_functions :
+    (A.assumed_fun_id * RegionGroupId.id option * string) list;
+  assumed_pure_functions : (pure_assumed_fun_id * string) list;
+}
+
+let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
+    (name : string) (nm : names_maps) : names_maps =
+  names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+
+let names_maps_add_assumed_struct (id_to_string : id -> string)
+    (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
+  names_maps_add id_to_string (StructId (TAssumed id)) name nm
+
+let names_maps_add_assumed_variant (id_to_string : id -> string)
+    (id : assumed_ty) (variant_id : VariantId.id) (name : string)
+    (nm : names_maps) : names_maps =
+  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+
+let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+    (name : string) (nm : names_maps) : names_maps =
+  names_maps_add id_to_string (FunId fid) name nm
+
+let bool_name () = if !backend = Lean then "Bool" else "bool"
+let char_name () = if !backend = Lean then "Char" else "char"
+let str_name () = if !backend = Lean then "String" else "string"
+
+(** Small helper to compute the name of an int type *)
+let int_name (int_ty : integer_type) =
+  let isize, usize, i_format, u_format =
+    match !backend with
+    | FStar | Coq | HOL4 ->
+        ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
+    | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
+  in
+  match int_ty with
+  | Isize -> isize
+  | I8 -> Printf.sprintf i_format 8
+  | I16 -> Printf.sprintf i_format 16
+  | I32 -> Printf.sprintf i_format 32
+  | I64 -> Printf.sprintf i_format 64
+  | I128 -> Printf.sprintf i_format 128
+  | Usize -> usize
+  | U8 -> Printf.sprintf u_format 8
+  | U16 -> Printf.sprintf u_format 16
+  | U32 -> Printf.sprintf u_format 32
+  | U64 -> Printf.sprintf u_format 64
+  | U128 -> Printf.sprintf u_format 128
+
 (** Extraction context.
 
     Note that the extraction context contains information coming from the
@@ -601,7 +530,6 @@ type extraction_ctx = {
   crate : A.crate;
   trans_ctx : trans_ctx;
   names_maps : names_maps;
-  fmt : formatter;
   indent_incr : int;
       (** The indent increment we insert whenever we need to indent more *)
   use_dep_ite : bool;
@@ -741,125 +669,15 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       ^ ", method name (" ^ fwd_back_kind ^ "): " ^ fun_name
   | TraitSelfClauseId -> "trait_self_clause"
 
-(** Return [true] if we are strict on collisions for this id (i.e., we forbid
-    collisions even with the ids in the unsafe names map) *)
-let strict_collisions (id : id) : bool =
-  match id with UnknownId | TypeId _ -> true | _ -> false
-
-(** We might not check for collisions for some specific ids (ex.: field names) *)
-let allow_collisions (id : id) : bool =
-  match id with
-  | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
-  | TraitMethodId _ ->
-      !Config.record_fields_short_names
-  | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _, _)) ->
-      (* We map several assumed functions to the same id *)
-      true
-  | _ -> false
-
-(** The [id_to_string] function to print nice debugging messages if there are
-    collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
-    (nm : names_maps) : names_maps =
-  (* We do not use the same name map if we allow/disallow collisions.
-     We notably use it for field names: some backends like Lean can use the
-     type information to disambiguate field projections.
-
-     Remark: we still need to check that those "unsafe" ids don't collide with
-     the ids that we mark as "strict on collision".
-
-     For instance, we don't allow naming a field "let". We enforce this by
-     not checking collision between ids for which we permit collisions (ex.:
-     between fields), but still checking collisions between those ids and the
-     others (ex.: fields and keywords).
-  *)
-  if allow_collisions id then (
-    (* Check with the ids which are considered to be strict on collisions *)
-    names_map_check_collision id_to_string id name nm.strict_names_map;
-    {
-      nm with
-      unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
-    })
-  else
-    (* Remark: if we are strict on collisions:
-       - we add the id to the strict collisions map
-       - we check that the id doesn't collide with the unsafe map
-       TODO: we might not check that:
-       - a user defined function doesn't collide with an assumed function
-       - two trait decl items don't collide with each other
-    *)
-    let strict_names_map =
-      if strict_collisions id then
-        names_map_add id_to_string id name nm.strict_names_map
-      else nm.strict_names_map
-    in
-    let names_map = names_map_add id_to_string id name nm.names_map in
-    { nm with strict_names_map; names_map }
-
 let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string id ctx in
   let names_maps = names_maps_add id_to_string id name ctx.names_maps in
   { ctx with names_maps }
 
-(** The [id_to_string] function to print nice debugging messages if there are
-    collisions *)
-let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
-    string =
-  (* We do not use the same name map if we allow/disallow collisions *)
-  let map_to_string (m : string IdMap.t) : string =
-    "[\n"
-    ^ String.concat ","
-        (List.map
-           (fun (id, n) -> "\n  " ^ id_to_string id ^ " -> " ^ n)
-           (IdMap.bindings m))
-    ^ "\n]"
-  in
-  if allow_collisions id then (
-    let m = nm.unsafe_names_map.id_to_name in
-    match IdMap.find_opt id m with
-    | Some s -> s
-    | None ->
-        let err =
-          "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
-          ^ map_to_string m
-        in
-        log#serror err;
-        if !Config.fail_hard then raise (Failure err)
-        else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
-  else
-    let m = nm.names_map.id_to_name in
-    match IdMap.find_opt id m with
-    | Some s -> s
-    | None ->
-        let err =
-          "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
-          ^ map_to_string m
-        in
-        log#serror err;
-        if !Config.fail_hard then raise (Failure err)
-        else "(ERROR: \"" ^ id_to_string id ^ "\")"
-
 let ctx_get (id : id) (ctx : extraction_ctx) : string =
   let id_to_string (id : id) : string = id_to_string id ctx in
   names_maps_get id_to_string id ctx.names_maps
 
-let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
-    (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (TypeId (TAssumed id)) name nm
-
-let names_maps_add_assumed_struct (id_to_string : id -> string)
-    (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (StructId (TAssumed id)) name nm
-
-let names_maps_add_assumed_variant (id_to_string : id -> string)
-    (id : assumed_ty) (variant_id : VariantId.id) (name : string)
-    (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
-
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
-    (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (FunId fid) name nm
-
 let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
   ctx_get (GlobalId id) ctx
 
@@ -950,15 +768,970 @@ let ctx_get_termination_measure (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
   ctx_get (TerminationMeasureId (FRegular def_id, loop_id)) ctx
 
+(** Small helper to compute the name of a unary operation *)
+let unop_name (unop : unop) : string =
+  match unop with
+  | Not -> (
+      match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
+  | Neg (int_ty : integer_type) -> (
+      match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
+  | Cast _ ->
+      (* We never directly use the unop name in this case *)
+      raise (Failure "Unsupported")
+
+(** Small helper to compute the name of a binary operation (note that many
+    binary operations like "less than" are extracted to primitive operations,
+    like [<]).
+ *)
+let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
+  let binop =
+    match binop with
+    | Div -> "div"
+    | Rem -> "rem"
+    | Add -> "add"
+    | Sub -> "sub"
+    | Mul -> "mul"
+    | Lt -> "lt"
+    | Le -> "le"
+    | Ge -> "ge"
+    | Gt -> "gt"
+    | BitXor -> "xor"
+    | BitAnd -> "and"
+    | BitOr -> "or"
+    | Shl -> "lsl"
+    | Shr ->
+        "asr"
+        (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
+    | _ -> raise (Failure "Unreachable")
+  in
+  (* Remark: the Lean case is actually not used *)
+  match !backend with
+  | Lean -> int_name int_ty ^ "." ^ binop
+  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
+
+(** A list of keywords/identifiers used by the backend and with which we
+    want to check collision.
+
+    Remark: this is useful mostly to look for collisions when generating
+    names for *variables*.
+ *)
+let keywords () =
+  let named_unops =
+    unop_name Not
+    :: List.map (fun it -> unop_name (Neg it)) T.all_signed_int_types
+  in
+  let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
+  let named_binops =
+    List.concat_map
+      (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
+      named_binops
+  in
+  let misc =
+    match !backend with
+    | FStar ->
+        [
+          "assert";
+          "assert_norm";
+          "assume";
+          "else";
+          "fun";
+          "fn";
+          "FStar";
+          "FStar.Mul";
+          "if";
+          "in";
+          "include";
+          "int";
+          "let";
+          "list";
+          "match";
+          "open";
+          "rec";
+          "scalar_cast";
+          "then";
+          "type";
+          "Type0";
+          "Type";
+          "unit";
+          "val";
+          "with";
+        ]
+    | Coq ->
+        [
+          "assert";
+          "Arguments";
+          "Axiom";
+          "char_of_byte";
+          "Check";
+          "Declare";
+          "Definition";
+          "else";
+          "End";
+          "fun";
+          "Fixpoint";
+          "if";
+          "in";
+          "int";
+          "Inductive";
+          "Import";
+          "let";
+          "Lemma";
+          "match";
+          "Module";
+          "not";
+          "Notation";
+          "Proof";
+          "Qed";
+          "rec";
+          "Record";
+          "Require";
+          "Scope";
+          "Search";
+          "SearchPattern";
+          "Set";
+          "then";
+          (* [tt] is unit *)
+          "tt";
+          "type";
+          "Type";
+          "unit";
+          "with";
+        ]
+    | Lean ->
+        [
+          "by";
+          "class";
+          "decreasing_by";
+          "def";
+          "deriving";
+          "do";
+          "else";
+          "end";
+          "for";
+          "have";
+          "if";
+          "inductive";
+          "instance";
+          "import";
+          "let";
+          "macro";
+          "match";
+          "namespace";
+          "opaque";
+          "open";
+          "run_cmd";
+          "set_option";
+          "simp";
+          "structure";
+          "syntax";
+          "termination_by";
+          "then";
+          "Type";
+          "unsafe";
+          "where";
+          "with";
+          "opaque_defs";
+        ]
+    | HOL4 ->
+        [
+          "Axiom";
+          "case";
+          "Definition";
+          "else";
+          "End";
+          "fix";
+          "fix_exec";
+          "fn";
+          "fun";
+          "if";
+          "in";
+          "int";
+          "Inductive";
+          "let";
+          "of";
+          "Proof";
+          "QED";
+          "then";
+          "Theorem";
+        ]
+  in
+  List.concat [ named_unops; named_binops; misc ]
+
+let assumed_adts () : (assumed_ty * string) list =
+  match !backend with
+  | Lean ->
+      [
+        (TState, "State");
+        (TResult, "Result");
+        (TError, "Error");
+        (TFuel, "Nat");
+        (TArray, "Array");
+        (TSlice, "Slice");
+        (TStr, "Str");
+        (TRawPtr Mut, "MutRawPtr");
+        (TRawPtr Const, "ConstRawPtr");
+      ]
+  | Coq | FStar | HOL4 ->
+      [
+        (TState, "state");
+        (TResult, "result");
+        (TError, "error");
+        (TFuel, if !backend = HOL4 then "num" else "nat");
+        (TArray, "array");
+        (TSlice, "slice");
+        (TStr, "str");
+        (TRawPtr Mut, "mut_raw_ptr");
+        (TRawPtr Const, "const_raw_ptr");
+      ]
+
+let assumed_struct_constructors () : (assumed_ty * string) list =
+  match !backend with
+  | Lean -> [ (TArray, "Array.make") ]
+  | Coq -> [ (TArray, "mk_array") ]
+  | FStar -> [ (TArray, "mk_array") ]
+  | HOL4 -> [ (TArray, "mk_array") ]
+
+let assumed_variants () : (assumed_ty * VariantId.id * string) list =
+  match !backend with
+  | FStar ->
+      [
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail");
+        (TError, error_failure_id, "Failure");
+        (TError, error_out_of_fuel_id, "OutOfFuel");
+        (* No Fuel::Zero on purpose *)
+        (* No Fuel::Succ on purpose *)
+      ]
+  | Coq ->
+      [
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail_");
+        (TError, error_failure_id, "Failure");
+        (TError, error_out_of_fuel_id, "OutOfFuel");
+        (TFuel, fuel_zero_id, "O");
+        (TFuel, fuel_succ_id, "S");
+      ]
+  | Lean ->
+      [
+        (TResult, result_return_id, "ret");
+        (TResult, result_fail_id, "fail");
+        (TError, error_failure_id, "panic");
+        (* No Fuel::Zero on purpose *)
+        (* No Fuel::Succ on purpose *)
+      ]
+  | HOL4 ->
+      [
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail");
+        (TError, error_failure_id, "Failure");
+        (* No Fuel::Zero on purpose *)
+        (* No Fuel::Succ on purpose *)
+      ]
+
+let assumed_llbc_functions () :
+    (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+  let rg0 = Some T.RegionGroupId.zero in
+  match !backend with
+  | FStar | Coq | HOL4 ->
+      [
+        (ArrayIndexShared, None, "array_index_usize");
+        (ArrayIndexMut, None, "array_index_usize");
+        (ArrayIndexMut, rg0, "array_update_usize");
+        (ArrayToSliceShared, None, "array_to_slice");
+        (ArrayToSliceMut, None, "array_to_slice");
+        (ArrayToSliceMut, rg0, "array_from_slice");
+        (ArrayRepeat, None, "array_repeat");
+        (SliceIndexShared, None, "slice_index_usize");
+        (SliceIndexMut, None, "slice_index_usize");
+        (SliceIndexMut, rg0, "slice_update_usize");
+      ]
+  | Lean ->
+      [
+        (ArrayIndexShared, None, "Array.index_usize");
+        (ArrayIndexMut, None, "Array.index_usize");
+        (ArrayIndexMut, rg0, "Array.update_usize");
+        (ArrayToSliceShared, None, "Array.to_slice");
+        (ArrayToSliceMut, None, "Array.to_slice");
+        (ArrayToSliceMut, rg0, "Array.from_slice");
+        (ArrayRepeat, None, "Array.repeat");
+        (SliceIndexShared, None, "Slice.index_usize");
+        (SliceIndexMut, None, "Slice.index_usize");
+        (SliceIndexMut, rg0, "Slice.update_usize");
+      ]
+
+let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
+  match !backend with
+  | FStar ->
+      [
+        (Return, "return");
+        (Fail, "fail");
+        (Assert, "massert");
+        (FuelDecrease, "decrease");
+        (FuelEqZero, "is_zero");
+      ]
+  | Coq ->
+      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+      [ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
+  | Lean ->
+      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+      [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ]
+  | HOL4 ->
+      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+      [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+
+let names_map_init () : names_map_init =
+  {
+    keywords = keywords ();
+    assumed_adts = assumed_adts ();
+    assumed_structs = assumed_struct_constructors ();
+    assumed_variants = assumed_variants ();
+    assumed_llbc_functions = assumed_llbc_functions ();
+    assumed_pure_functions = assumed_pure_functions ();
+  }
+
+(** Initialize names maps with a proper set of keywords/names coming from the
+    target language/prover. *)
+let initialize_names_maps () : names_maps =
+  let init = names_map_init () in
+  let int_names = List.map int_name T.all_int_types in
+  let keywords =
+    List.concat
+      [ [ bool_name (); char_name (); str_name () ]; int_names; init.keywords ]
+  in
+  let names_set = StringSet.empty in
+  let name_to_id = StringMap.empty in
+  (* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId].
+   * Also note that we don't need this mapping for keywords: we insert keywords only
+   * to check collisions. *)
+  let id_to_name = IdMap.empty in
+  let names_map = { id_to_name; name_to_id; names_set } in
+  let unsafe_names_map = empty_unsafe_names_map in
+  let strict_names_map = empty_names_map in
+  (* For debugging - we are creating bindings for assumed types and functions, so
+   * it is ok if we simply use the "show" function (those aren't simply identified
+   * by numbers) *)
+  let id_to_string = show_id in
+  (* Add the keywords as strict collisions *)
+  let strict_names_map =
+    List.fold_left
+      (fun nm name ->
+        (* There is duplication in the keywords so we don't check the collisions
+           while registering them (what is important is that there are no collisions
+           between keywords and user-defined identifiers) *)
+        names_map_add_unchecked UnknownId name nm)
+      strict_names_map keywords
+  in
+  let nm = { names_map; unsafe_names_map; strict_names_map } in
+  (* Then we add:
+   * - the assumed types
+   * - the assumed struct constructors
+   * - the assumed variants
+   * - the assumed functions
+   *)
+  let nm =
+    List.fold_left
+      (fun nm (type_id, name) ->
+        names_maps_add_assumed_type id_to_string type_id name nm)
+      nm init.assumed_adts
+  in
+  let nm =
+    List.fold_left
+      (fun nm (type_id, name) ->
+        names_maps_add_assumed_struct id_to_string type_id name nm)
+      nm init.assumed_structs
+  in
+  let nm =
+    List.fold_left
+      (fun nm (type_id, variant_id, name) ->
+        names_maps_add_assumed_variant id_to_string type_id variant_id name nm)
+      nm init.assumed_variants
+  in
+  let assumed_functions =
+    List.map
+      (fun (fid, rg, name) ->
+        (FromLlbc (Pure.FunId (FAssumed fid), None, rg), name))
+      init.assumed_llbc_functions
+    @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+  in
+  let nm =
+    List.fold_left
+      (fun nm (fid, name) -> names_maps_add_function id_to_string fid name nm)
+      nm assumed_functions
+  in
+  (* Return *)
+  nm
+
+(** Compute the qualified for a type definition/declaration.
+
+    For instance: "type", "and", etc.
+
+    Remark: can return [None] for some backends like HOL4.
+ *)
+let type_decl_kind_to_qualif (kind : decl_kind)
+    (type_kind : type_decl_kind option) : string option =
+  match !backend with
+  | FStar -> (
+      match kind with
+      | SingleNonRec -> Some "type"
+      | SingleRec -> Some "type"
+      | MutRecFirst -> Some "type"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "assume type"
+      | Declared -> Some "val")
+  | Coq -> (
+      match (kind, type_kind) with
+      | SingleNonRec, Some Enum -> Some "Inductive"
+      | SingleNonRec, Some Struct -> Some "Record"
+      | (SingleRec | MutRecFirst), Some _ -> Some "Inductive"
+      | (MutRecInner | MutRecLast), Some _ ->
+          (* Coq doesn't support groups of mutually recursive definitions which mix
+           * records and inducties: we convert everything to records if this happens
+           *)
+          Some "with"
+      | (Assumed | Declared), None -> Some "Axiom"
+      | SingleNonRec, None ->
+          (* This is for traits *)
+          Some "Record"
+      | _ ->
+          raise
+            (Failure
+               ("Unexpected: (" ^ show_decl_kind kind ^ ", "
+               ^ Print.option_to_string show_type_decl_kind type_kind
+               ^ ")")))
+  | Lean -> (
+      match kind with
+      | SingleNonRec ->
+          if type_kind = Some Struct then Some "structure" else Some "inductive"
+      | SingleRec -> Some "inductive"
+      | MutRecFirst -> Some "inductive"
+      | MutRecInner -> Some "inductive"
+      | MutRecLast -> Some "inductive"
+      | Assumed -> Some "axiom"
+      | Declared -> Some "axiom")
+  | HOL4 -> None
+
+(** Compute the qualified for a function definition/declaration.
+
+    For instance: "let", "let rec", "and", etc.
+
+    Remark: can return [None] for some backends like HOL4.
+ *)
+let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
+  match !backend with
+  | FStar -> (
+      match kind with
+      | SingleNonRec -> Some "let"
+      | SingleRec -> Some "let rec"
+      | MutRecFirst -> Some "let rec"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "assume val"
+      | Declared -> Some "val")
+  | Coq -> (
+      match kind with
+      | SingleNonRec -> Some "Definition"
+      | SingleRec -> Some "Fixpoint"
+      | MutRecFirst -> Some "Fixpoint"
+      | MutRecInner -> Some "with"
+      | MutRecLast -> Some "with"
+      | Assumed -> Some "Axiom"
+      | Declared -> Some "Axiom")
+  | Lean -> (
+      match kind with
+      | SingleNonRec -> Some "def"
+      | SingleRec -> Some "divergent def"
+      | MutRecFirst -> Some "mutual divergent def"
+      | MutRecInner -> Some "divergent def"
+      | MutRecLast -> Some "divergent def"
+      | Assumed -> Some "axiom"
+      | Declared -> Some "axiom")
+  | HOL4 -> None
+
+(** The type of types.
+
+    TODO: move inside the formatter?
+ *)
+let type_keyword () =
+  match !backend with
+  | FStar -> "Type0"
+  | Coq | Lean -> "Type"
+  | HOL4 -> raise (Failure "Unexpected")
+
+(** Helper *)
+let name_last_elem_as_ident (n : llbc_name) : string =
+  match Collections.List.last n with
+  | PeIdent (s, _) -> s
+  | PeImpl _ -> raise (Failure "Unexpected")
+
+(** Helper
+
+    Prepare a name.
+    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 ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
+    string list =
+  (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+  match name with
+  | (PeIdent (crate, _) as id) :: name ->
+      let name = if crate = ctx.crate.name then name else id :: name in
+      name_to_simple_name ctx.trans_ctx name
+  | _ ->
+      raise
+        (Failure
+           ("Unexpected name shape: "
+           ^ TranslateCore.name_to_string ctx.trans_ctx name))
+
+(** Helper *)
+let ctx_compute_simple_type_name = ctx_compute_simple_name
+
+(** Helper *)
+let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) (name : llbc_name) :
+    string =
+  flatten_name (ctx_compute_simple_type_name ctx name)
+
+(** Provided a basename, compute a type name. *)
+let ctx_compute_type_name (ctx : extraction_ctx) (name : llbc_name) =
+  let name = ctx_compute_type_name_no_suffix ctx name in
+  match !backend with
+  | FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
+  | Coq | HOL4 -> name ^ "_t"
+  | Lean -> name
+
+(** Inputs:
+    - type name
+    - field id
+    - field name
+
+    Note that fields don't always have names, but we still need to
+    generate some names if we want to extract the structures to records...
+    We might want to extract such structures to tuples, later, but field
+    access then causes trouble because not all provers accept syntax like
+    [x.3] where [x] is a tuple.
+ *)
+let ctx_compute_field_name (ctx : extraction_ctx) (def_name : llbc_name)
+    (field_id : FieldId.id) (field_name : string option) : string =
+  let field_name_s =
+    match field_name with
+    | Some field_name -> field_name
+    | None ->
+        (* TODO: extract structs with no field names to tuples *)
+        FieldId.to_string field_id
+  in
+  if !Config.record_fields_short_names then
+    if field_name = None then (* TODO: this is a bit ugly *)
+      "_" ^ field_name_s
+    else field_name_s
+  else
+    let def_name =
+      ctx_compute_type_name_no_suffix ctx def_name ^ "_" ^ field_name_s
+    in
+    match !backend with
+    | Lean | HOL4 -> def_name
+    | Coq | FStar -> StringUtils.lowercase_first_letter def_name
+
+(** Inputs:
+    - type name
+    - variant name
+ *)
+let ctx_compute_variant_name (ctx : extraction_ctx) (def_name : llbc_name)
+    (variant : string) : string =
+  match !backend with
+  | FStar | Coq | HOL4 ->
+      let variant = to_camel_case variant in
+      if !variant_concatenate_type_name then
+        StringUtils.capitalize_first_letter
+          (ctx_compute_type_name_no_suffix ctx def_name ^ "_" ^ variant)
+      else variant
+  | Lean -> variant
+
+(** Structure constructors are used when constructing structure values.
+
+    For instance, in F*:
+    {[
+      type pair = { x : nat; y : nat }
+      let p : pair = Mkpair 0 1
+    ]}
+
+    Inputs:
+    - type name
+*)
+let ctx_compute_struct_constructor (ctx : extraction_ctx) (basename : llbc_name)
+    : string =
+  let tname = ctx_compute_type_name ctx basename in
+  ExtractBuiltin.mk_struct_constructor tname
+
+let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) :
+    string =
+  let fname = ctx_compute_simple_name ctx fname in
+  (* TODO: don't convert to snake case for Coq, HOL4, F* *)
+  let fname = flatten_name fname in
+  match !backend with
+  | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
+  | Lean -> fname
+
+(** Provided a basename, compute the name of a global declaration. *)
+let ctx_compute_global_name (ctx : extraction_ctx) (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 (ctx_compute_simple_name ctx name) in
+  String.concat "_" parts
+
+(** Helper function: generate a suffix for a function name, i.e., generates
+    a suffix like "_loop", "loop1", etc. to append to a function name.
+ *)
+let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
+    string =
+  match loop_id with
+  | None -> ""
+  | Some loop_id ->
+      (* If this is for a loop, generally speaking, we append the loop index.
+         If this function admits only one loop, we omit it. *)
+      if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
+
+(** A helper function: generates a function suffix from a region group
+    information.
+    TODO: move all those helpers.
+*)
+let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
+    (num_region_groups : int) (rg : region_group_info option)
+    ((keep_fwd, num_backs) : bool * int) : string =
+  let lp_suff = default_fun_loop_suffix num_loops loop_id in
+
+  (* There are several cases:
+     - [rg] is [Some]: this is a forward function:
+       - we add "_fwd"
+     - [rg] is [None]: this is a backward function:
+       - this function has one extracted backward function:
+         - if the forward function has been filtered, we add "_fwd_back":
+           the forward function is useless, so the unique backward function
+           takes its place, in a way
+         - otherwise we add "_back"
+       - this function has several backward functions: we add "_back" and an
+         additional suffix to identify the precise backward function
+     Note that we always add a suffix (in case there are no region groups,
+     we could not add the "_fwd" suffix) to prevent name clashes between
+     definitions (in particular between type and function definitions).
+  *)
+  let rg_suff =
+    (* TODO: make all the backends match what is done for Lean *)
+    match rg with
+    | None ->
+        if
+          (* In order to avoid name conflicts:
+           * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
+           * - otherwise, no suffix (because the backward functions will have a suffix)
+           *)
+          num_backs = 1 && not keep_fwd
+        then "_fwd"
+        else ""
+    | Some rg ->
+        assert (num_region_groups > 0 && num_backs > 0);
+        if num_backs = 1 then
+          (* Exactly one backward function *)
+          if not keep_fwd then "" else "_back"
+        else if
+          (* Several region groups/backward functions:
+             - if all the regions in the group have names, we use those names
+             - otherwise we use an index
+          *)
+          List.for_all Option.is_some rg.region_names
+        then
+          (* Concatenate the region names *)
+          "_back" ^ String.concat "" (List.map Option.get rg.region_names)
+        else (* Use the region index *)
+          "_back" ^ RegionGroupId.to_string rg.id
+  in
+  lp_suff ^ rg_suff
+
+(** Compute the name of a regular (non-assumed) function.
+
+    Inputs:
+    - function basename (TODO: shouldn't appear for assumed functions?...)
+    - number of loops in the function (useful to check if we need to use
+      indices to derive unique names for the loops for instance - if there is
+      exactly one loop, we don't need to use indices)
+    - loop id (if pertinent)
+    - number of region groups
+    - region group information in case of a backward function
+      ([None] if forward function)
+    - pair:
+      - do we generate the forward function (it may have been filtered)?
+      - the number of *extracted backward functions* (same comment as for
+        the number of loops)
+        The number of extracted backward functions if not necessarily
+        equal to the number of region groups, because we may have
+        filtered some of them.
+    TODO: use the fun id for the assumed functions.
+ *)
+let ctx_compute_fun_name (ctx : extraction_ctx) (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 = ctx_compute_fun_name_no_suffix ctx fname in
+  (* Compute the suffix *)
+  let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
+  (* Concatenate *)
+  fname ^ suffix
+
+let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+    : string =
+  ctx_compute_type_name ctx trait_decl.llbc_name
+
+let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+    (trait_impl : trait_impl) : string =
+  (* We derive the trait impl name from the implemented trait.
+     For instance, if this implementation is an instance of `trait::Trait`
+     for `<foo::Foo, u32>`, we generate the name: "trait.TraitFooFooU32Inst".
+     Importantly, it is to be noted that the name is independent of the place
+     where the instance has been defined (it is indepedent of the file, etc.).
+  *)
+  let name =
+    (* We need to lookup the LLBC definitions, to have the original instantiation *)
+    let trait_impl =
+      TraitImplId.Map.find trait_impl.def_id
+        ctx.trans_ctx.trait_impls_ctx.trait_impls
+    in
+    let params = trait_impl.generics in
+    let args = trait_impl.impl_trait.decl_generics in
+    name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name params
+      args
+  in
+  let name = flatten_name name in
+  match !backend with
+  | FStar -> StringUtils.lowercase_first_letter name
+  | Coq | HOL4 | Lean -> name
+
+let ctx_compute_trait_decl_constructor (ctx : extraction_ctx)
+    (trait_decl : trait_decl) : string =
+  let name = ctx_compute_trait_decl_name ctx trait_decl in
+  ExtractBuiltin.mk_struct_constructor name
+
+let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
+    (trait_decl : trait_decl) (clause : trait_clause) : string =
+  (* TODO: improve - it would be better to not use indices *)
+  let clause = "parent_clause_" ^ TraitClauseId.to_string clause.clause_id in
+  if !Config.record_fields_short_names then clause
+  else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
+
+let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+    (item : string) : string =
+  let name =
+    if !Config.record_fields_short_names then item
+    else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+  in
+  (* Constants are usually all capital letters.
+     Some backends do not support field names starting with a capital letter,
+     and it may be weird to lowercase everything (especially as it may lead
+     to more name collisions): we add a prefix when necessary.
+     For instance, it gives: "U" -> "tU"
+     Note that for some backends we prepend the type name (because those backends
+     can't disambiguate fields coming from different ADTs if they have the same
+     names), and thus don't need to add a prefix starting with a lowercase.
+  *)
+  match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+
+let ctx_compute_trait_const_name (ctx : extraction_ctx)
+    (trait_decl : trait_decl) (item : string) : string =
+  let name =
+    if !Config.record_fields_short_names then item
+    else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+  in
+  (* See [trait_type_name] *)
+  match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+
+let ctx_compute_trait_method_name (ctx : extraction_ctx)
+    (trait_decl : trait_decl) (item : string) : string =
+  if !Config.record_fields_short_names then item
+  else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+
+let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
+    (trait_decl : trait_decl) (item : string) (clause : trait_clause) : string =
+  (* TODO: improve - it would be better to not use indices *)
+  ctx_compute_trait_type_name ctx trait_decl item
+  ^ "_clause_"
+  ^ TraitClauseId.to_string clause.clause_id
+
+(** Generates the name of the termination measure used to prove/reason about
+    termination. The generated code uses this clause where needed,
+    but its body must be defined by the user.
+
+    F* and Lean only.
+
+    Inputs:
+    - function id: this is especially useful to identify whether the
+      function is an assumed function or a local function
+    - function basename
+    - the number of loops in the parent function. This is used for
+      the same purpose as in {!field:llbc_name}.
+    - loop identifier, if this is for a loop
+ *)
+let ctx_compute_termination_measure_name (ctx : extraction_ctx)
+    (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
+    (loop_id : LoopId.id option) : string =
+  let fname = ctx_compute_fun_name_no_suffix ctx fname in
+  let lp_suffix = default_fun_loop_suffix num_loops loop_id in
+  (* Compute the suffix *)
+  let suffix =
+    match !Config.backend with
+    | FStar -> "_decreases"
+    | Lean -> "_terminates"
+    | Coq | HOL4 -> raise (Failure "Unexpected")
+  in
+  (* Concatenate *)
+  fname ^ lp_suffix ^ suffix
+
+(** Generates the name of the proof used to prove/reason about
+    termination. The generated code uses this clause where needed,
+    but its body must be defined by the user.
+
+    Lean only.
+
+    Inputs:
+    - function id: this is especially useful to identify whether the
+      function is an assumed function or a local function
+    - function basename
+    - the number of loops in the parent function. This is used for
+      the same purpose as in {!field:llbc_name}.
+    - loop identifier, if this is for a loop
+ *)
+let ctx_compute_decreases_proof_name (ctx : extraction_ctx)
+    (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
+    (loop_id : LoopId.id option) : string =
+  let fname = ctx_compute_fun_name_no_suffix ctx fname in
+  let lp_suffix = default_fun_loop_suffix num_loops loop_id in
+  (* Compute the suffix *)
+  let suffix =
+    match !Config.backend with
+    | Lean -> "_decreases"
+    | FStar | Coq | HOL4 -> raise (Failure "Unexpected")
+  in
+  (* Concatenate *)
+  fname ^ lp_suffix ^ suffix
+
+(** Generates a variable basename.
+
+    Inputs:
+    - the set of names used in the context so far
+    - the basename we got from the symbolic execution, if we have one
+    - the type of the variable (can be useful for heuristics, in order
+      not to always use "x" for instance, whenever naming anonymous
+      variables)
+
+    Note that once the formatter generated a basename, we add an index
+    if necessary to prevent name clashes: the burden of name clashes checks
+    is thus on the caller's side.
+ *)
+let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option)
+    (ty : ty) : string =
+  (* Small helper to derive var names from ADT type names.
+
+     We do the following:
+     - convert the type name to snake case
+     - take the first letter of every "letter group"
+     Ex.: "HashMap" -> "hash_map" -> "hm"
+  *)
+  let name_from_type_ident (name : string) : string =
+    let cl = to_snake_case name in
+    let cl = String.split_on_char '_' cl in
+    let cl = List.filter (fun s -> String.length s > 0) cl in
+    assert (List.length cl > 0);
+    let cl = List.map (fun s -> s.[0]) cl in
+    StringUtils.string_of_chars cl
+  in
+  (* If there is a basename, we use it *)
+  match basename with
+  | Some basename ->
+      (* This should be a no-op *)
+      to_snake_case basename
+  | None -> (
+      (* No basename: we use the first letter of the type *)
+      match ty with
+      | TAdt (type_id, generics) -> (
+          match type_id with
+          | TTuple ->
+              (* The "pair" case is frequent enough to have its special treatment *)
+              if List.length generics.types = 2 then "p" else "t"
+          | TAssumed TResult -> "r"
+          | TAssumed TError -> ConstStrings.error_basename
+          | TAssumed TFuel -> ConstStrings.fuel_basename
+          | TAssumed TArray -> "a"
+          | TAssumed TSlice -> "s"
+          | TAssumed TStr -> "s"
+          | TAssumed TState -> ConstStrings.state_basename
+          | TAssumed (TRawPtr _) -> "p"
+          | TAdtId adt_id ->
+              let def =
+                TypeDeclId.Map.find adt_id ctx.trans_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"
+              *)
+              (* The name shouldn't be empty, and its last element should
+               * be an ident *)
+              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
+          | FStar -> "x" (* lacking inspiration here... *)
+          | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
+      | TLiteral lty -> (
+          match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
+      | TArrow _ -> "f"
+      | TTraitType (_, _, name) -> name_from_type_ident name)
+
+(** Generates a type variable basename. *)
+let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
+    string =
+  (* Rust type variables are snake-case and start with a capital letter *)
+  match !backend with
+  | FStar ->
+      (* This is *not* a no-op: this removes the capital letter *)
+      to_snake_case basename
+  | HOL4 ->
+      (* In HOL4, type variable names must start with "'" *)
+      "'" ^ to_snake_case basename
+  | Coq | Lean -> basename
+
+(** Generates a const generic variable basename. *)
+let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
+    (basename : string) : string =
+  (* Rust type variables are snake-case and start with a capital letter *)
+  match !backend with
+  | FStar | HOL4 ->
+      (* This is *not* a no-op: this removes the capital letter *)
+      to_snake_case basename
+  | Coq | Lean -> basename
+
+(** Return a base name for a trait clause. We might add a suffix to prevent
+    collisions.
+
+    In the traduction we explicitely manipulate the trait clause instances,
+    that is we introduce one input variable for each trait clause.
+ *)
+let ctx_compute_trait_clause_basename (_ctx : extraction_ctx)
+    (_clause : trait_clause) : string =
+  (* TODO: actually use the clause to derive the name *)
+  "inst"
+
+let trait_self_clause_basename = "self_clause"
+
+(** Appends an index to a name - we use this to generate unique
+    names: when doing so, the role of the formatter is just to concatenate
+    indices to names, the responsability of finding a proper index is
+    delegated to helper functions.
+ *)
+let name_append_index (basename : string) (i : int) : string =
+  basename ^ string_of_int i
+
 (** Generate a unique type variable name and add it to the context *)
 let ctx_add_type_var (basename : string) (id : TypeVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
+  let name = ctx_compute_type_var_basename ctx basename in
   let name =
-    ctx.fmt.type_var_basename ctx.names_maps.names_map.names_set basename
-  in
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
-      name
+    basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
   in
   let ctx = ctx_add (TypeVarId id) name ctx in
   (ctx, name)
@@ -966,13 +1739,9 @@ let ctx_add_type_var (basename : string) (id : TypeVarId.id)
 (** Generate a unique const generic variable name and add it to the context *)
 let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
+  let name = ctx_compute_const_generic_var_basename ctx basename in
   let name =
-    ctx.fmt.const_generic_var_basename ctx.names_maps.names_map.names_set
-      basename
-  in
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
-      name
+    basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
   in
   let ctx = ctx_add (ConstGenericVarId id) name ctx in
   (ctx, name)
@@ -988,7 +1757,7 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
 let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
     extraction_ctx * string =
   let name =
-    basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
   let ctx = ctx_add (VarId id) name ctx in
@@ -996,9 +1765,9 @@ let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
 
 (** Generate a unique variable name for the trait self clause and add it to the context *)
 let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
-  let basename = ctx.fmt.trait_self_clause_basename in
+  let basename = trait_self_clause_basename in
   let name =
-    basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
   let ctx = ctx_add TraitSelfClauseId name ctx in
@@ -1008,7 +1777,7 @@ let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
 let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
   let name =
-    basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
       basename
   in
   let ctx = ctx_add (LocalTraitClauseId id) name ctx in
@@ -1019,9 +1788,7 @@ let ctx_add_vars (vars : var list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (v : var) ->
-      let name =
-        ctx.fmt.var_basename ctx.names_maps.names_map.names_set v.basename v.ty
-      in
+      let name = ctx_compute_var_basename ctx v.basename v.ty in
       ctx_add_var name v.id ctx)
     ctx vars
 
@@ -1042,9 +1809,7 @@ let ctx_add_local_trait_clauses (clauses : trait_clause list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (c : trait_clause) ->
-      let basename =
-        ctx.fmt.trait_clause_basename ctx.names_maps.names_map.names_set c
-      in
+      let basename = ctx_compute_trait_clause_basename ctx c in
       ctx_add_local_trait_clause basename c.clause_id ctx)
     ctx clauses
 
@@ -1064,7 +1829,7 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx.fmt.decreases_proof_name def.def_id def.llbc_name def.num_loops
+    ctx_compute_decreases_proof_name ctx def.def_id def.llbc_name def.num_loops
       def.loop_id
   in
   ctx_add (DecreasesProofId (FRegular def.def_id, def.loop_id)) name ctx
@@ -1072,8 +1837,8 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
 let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx.fmt.termination_measure_name def.def_id def.llbc_name def.num_loops
-      def.loop_id
+    ctx_compute_termination_measure_name ctx def.def_id def.llbc_name
+      def.num_loops def.loop_id
   in
   ctx_add (TerminationMeasureId (FRegular def.def_id, def.loop_id)) name ctx
 
@@ -1091,7 +1856,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       ctx_add decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
-      let name = ctx.fmt.global_name def.name in
+      let name = ctx_compute_global_name ctx def.name in
       let body = FunId (FromLlbc (FunId (FRegular def.body), None, None)) in
       let ctx = ctx_add decl (name ^ "_c") ctx in
       let ctx = ctx_add body (name ^ "_body") ctx in
@@ -1123,8 +1888,8 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
         Some { id = rg_id; region_names }
   in
   (* Add the function name *)
-  ctx.fmt.fun_name def.llbc_name def.num_loops def.loop_id num_rgs rg_info
-    (keep_fwd, num_backs)
+  ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id num_rgs
+    rg_info (keep_fwd, num_backs)
 
 (* TODO: move to Extract *)
 let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
@@ -1148,156 +1913,6 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
         ctx.fun_name_info;
   }
 
-type names_map_init = {
-  keywords : string list;
-  assumed_adts : (assumed_ty * string) list;
-  assumed_structs : (assumed_ty * string) list;
-  assumed_variants : (assumed_ty * VariantId.id * string) list;
-  assumed_llbc_functions :
-    (A.assumed_fun_id * RegionGroupId.id option * string) list;
-  assumed_pure_functions : (pure_assumed_fun_id * string) list;
-}
-
-(** Initialize names maps with a proper set of keywords/names coming from the
-    target language/prover. *)
-let initialize_names_maps (fmt : formatter) (init : names_map_init) : names_maps
+let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
     =
-  let int_names = List.map fmt.int_name T.all_int_types in
-  let keywords =
-    List.concat
-      [
-        [ fmt.bool_name; fmt.char_name; fmt.str_name ]; int_names; init.keywords;
-      ]
-  in
-  let names_set = StringSet.empty in
-  let name_to_id = StringMap.empty in
-  (* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId].
-   * Also note that we don't need this mapping for keywords: we insert keywords only
-   * to check collisions. *)
-  let id_to_name = IdMap.empty in
-  let names_map = { id_to_name; name_to_id; names_set } in
-  let unsafe_names_map = empty_unsafe_names_map in
-  let strict_names_map = empty_names_map in
-  (* For debugging - we are creating bindings for assumed types and functions, so
-   * it is ok if we simply use the "show" function (those aren't simply identified
-   * by numbers) *)
-  let id_to_string = show_id in
-  (* Add the keywords as strict collisions *)
-  let strict_names_map =
-    List.fold_left
-      (fun nm name ->
-        (* There is duplication in the keywords so we don't check the collisions
-           while registering them (what is important is that there are no collisions
-           between keywords and user-defined identifiers) *)
-        names_map_add_unchecked UnknownId name nm)
-      strict_names_map keywords
-  in
-  let nm = { names_map; unsafe_names_map; strict_names_map } in
-  (* Then we add:
-   * - the assumed types
-   * - the assumed struct constructors
-   * - the assumed variants
-   * - the assumed functions
-   *)
-  let nm =
-    List.fold_left
-      (fun nm (type_id, name) ->
-        names_maps_add_assumed_type id_to_string type_id name nm)
-      nm init.assumed_adts
-  in
-  let nm =
-    List.fold_left
-      (fun nm (type_id, name) ->
-        names_maps_add_assumed_struct id_to_string type_id name nm)
-      nm init.assumed_structs
-  in
-  let nm =
-    List.fold_left
-      (fun nm (type_id, variant_id, name) ->
-        names_maps_add_assumed_variant id_to_string type_id variant_id name nm)
-      nm init.assumed_variants
-  in
-  let assumed_functions =
-    List.map
-      (fun (fid, rg, name) ->
-        (FromLlbc (Pure.FunId (FAssumed fid), None, rg), name))
-      init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
-  in
-  let nm =
-    List.fold_left
-      (fun nm (fid, name) -> names_maps_add_function id_to_string fid name nm)
-      nm assumed_functions
-  in
-  (* Return *)
-  nm
-
-let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
-  fmt.type_name def.llbc_name
-
-(** Helper function: generate a suffix for a function name, i.e., generates
-    a suffix like "_loop", "loop1", etc. to append to a function name.
- *)
-let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
-    string =
-  match loop_id with
-  | None -> ""
-  | Some loop_id ->
-      (* If this is for a loop, generally speaking, we append the loop index.
-         If this function admits only one loop, we omit it. *)
-      if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
-
-(** A helper function: generates a function suffix from a region group
-    information.
-    TODO: move all those helpers.
-*)
-let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
-    (num_region_groups : int) (rg : region_group_info option)
-    ((keep_fwd, num_backs) : bool * int) : string =
-  let lp_suff = default_fun_loop_suffix num_loops loop_id in
-
-  (* There are several cases:
-     - [rg] is [Some]: this is a forward function:
-       - we add "_fwd"
-     - [rg] is [None]: this is a backward function:
-       - this function has one extracted backward function:
-         - if the forward function has been filtered, we add "_fwd_back":
-           the forward function is useless, so the unique backward function
-           takes its place, in a way
-         - otherwise we add "_back"
-       - this function has several backward functions: we add "_back" and an
-         additional suffix to identify the precise backward function
-     Note that we always add a suffix (in case there are no region groups,
-     we could not add the "_fwd" suffix) to prevent name clashes between
-     definitions (in particular between type and function definitions).
-  *)
-  let rg_suff =
-    (* TODO: make all the backends match what is done for Lean *)
-    match rg with
-    | None ->
-        if
-          (* In order to avoid name conflicts:
-           * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
-           * - otherwise, no suffix (because the backward functions will have a suffix)
-           *)
-          num_backs = 1 && not keep_fwd
-        then "_fwd"
-        else ""
-    | Some rg ->
-        assert (num_region_groups > 0 && num_backs > 0);
-        if num_backs = 1 then
-          (* Exactly one backward function *)
-          if not keep_fwd then "" else "_back"
-        else if
-          (* Several region groups/backward functions:
-             - if all the regions in the group have names, we use those names
-             - otherwise we use an index
-          *)
-          List.for_all Option.is_some rg.region_names
-        then
-          (* Concatenate the region names *)
-          "_back" ^ String.concat "" (List.map Option.get rg.region_names)
-        else (* Use the region index *)
-          "_back" ^ RegionGroupId.to_string rg.id
-  in
-  lp_suff ^ rg_suff
+  ctx_compute_type_name ctx def.llbc_name
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index b0a5159f..ef746ddf 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -26,6 +26,11 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
 let split_on_separator (s : string) : string list =
   Str.split (Str.regexp "\\(::\\|\\.\\)") s
 
+let flatten_name (name : string list) : string =
+  match !backend with
+  | FStar | Coq | HOL4 -> String.concat "_" name
+  | Lean -> String.concat "." name
+
 let () =
   assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
   assert (split_on_separator "x.y.z" = [ "x"; "y"; "z" ])
@@ -124,10 +129,7 @@ let mk_struct_constructor (type_name : string) : string =
 let builtin_types () : builtin_type_info list =
   let mk_type (rust_name : string) ?(keep_params : bool list option = None)
       ?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
-    let extract_name =
-      let sep = backend_choice "_" "." in
-      String.concat sep (split_on_separator rust_name)
-    in
+    let extract_name = flatten_name (split_on_separator rust_name) in
     let body_info : builtin_type_body_info option =
       match kind with
       | KOpaque -> None
@@ -231,11 +233,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
       | None -> pattern_to_fun_extract_name rust_name
       | Some name -> split_on_separator name
     in
-    let basename =
-      match !backend with
-      | FStar | Coq | HOL4 -> String.concat "_" extract_name
-      | Lean -> String.concat "." extract_name
-    in
+    let basename = flatten_name extract_name in
     let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
     let fwd = [ { rg = None; extract_name = basename ^ fwd_suffix } ] in
     let back_suffix = if with_back && back_no_suffix then "" else "_back" in
@@ -400,11 +398,9 @@ let builtin_trait_decls_info () =
     let extract_name =
       match extract_name with
       | Some n -> n
-      | None -> (
+      | None ->
           let rust_name = pattern_to_fun_extract_name rust_name in
-          match !backend with
-          | Coq | FStar | HOL4 -> String.concat "_" rust_name
-          | Lean -> String.concat "." rust_name)
+          flatten_name rust_name
     in
     let constructor = mk_struct_constructor extract_name in
     let consts = [] in
@@ -502,13 +498,12 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
       pattern * (bool list option * string) =
     let rust_name = parse_pattern rust_name in
     let name =
-      let sep = backend_choice "_" "." in
       let name =
         match extract_name with
         | None -> pattern_to_trait_impl_extract_name rust_name
         | Some name -> split_on_separator name
       in
-      String.concat sep name
+      flatten_name name
     in
     (rust_name, (filter, name))
   in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 3a81e6fe..c9be5abe 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -6,354 +6,88 @@
 open Pure
 open PureUtils
 open TranslateCore
-open ExtractBase
-open StringUtils
 open Config
-module F = Format
+include ExtractBase
 
-(** Small helper to compute the name of an int type *)
-let int_name (int_ty : integer_type) =
-  let isize, usize, i_format, u_format =
-    match !backend with
-    | FStar | Coq | HOL4 ->
-        ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
-    | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
-  in
-  match int_ty with
-  | Isize -> isize
-  | I8 -> Printf.sprintf i_format 8
-  | I16 -> Printf.sprintf i_format 16
-  | I32 -> Printf.sprintf i_format 32
-  | I64 -> Printf.sprintf i_format 64
-  | I128 -> Printf.sprintf i_format 128
-  | Usize -> usize
-  | U8 -> Printf.sprintf u_format 8
-  | U16 -> Printf.sprintf u_format 16
-  | U32 -> Printf.sprintf u_format 32
-  | U64 -> Printf.sprintf u_format 64
-  | U128 -> Printf.sprintf u_format 128
-
-(** Small helper to compute the name of a unary operation *)
-let unop_name (unop : unop) : string =
-  match unop with
-  | Not -> (
-      match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
-  | Neg (int_ty : integer_type) -> (
-      match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
-  | Cast _ ->
-      (* We never directly use the unop name in this case *)
-      raise (Failure "Unsupported")
-
-(** Small helper to compute the name of a binary operation (note that many
-    binary operations like "less than" are extracted to primitive operations,
-    like [<]).
- *)
-let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
-  let binop =
-    match binop with
-    | Div -> "div"
-    | Rem -> "rem"
-    | Add -> "add"
-    | Sub -> "sub"
-    | Mul -> "mul"
-    | Lt -> "lt"
-    | Le -> "le"
-    | Ge -> "ge"
-    | Gt -> "gt"
-    | BitXor -> "xor"
-    | BitAnd -> "and"
-    | BitOr -> "or"
-    | Shl -> "lsl"
-    | Shr ->
-        "asr"
-        (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
-    | _ -> raise (Failure "Unreachable")
-  in
-  (* Remark: the Lean case is actually not used *)
-  match !backend with
-  | Lean -> int_name int_ty ^ "." ^ binop
-  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
+(** Format a constant value.
 
-(** A list of keywords/identifiers used by the backend and with which we
-    want to check collision.
-
-    Remark: this is useful mostly to look for collisions when generating
-    names for *variables*.
+    Inputs:
+    - formatter
+    - [inside]: if [true], the value should be wrapped in parentheses
+      if it is made of an application (ex.: [U32 3])
+    - the constant value
  *)
-let keywords () =
-  let named_unops =
-    unop_name Not
-    :: List.map (fun it -> unop_name (Neg it)) T.all_signed_int_types
-  in
-  let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
-  let named_binops =
-    List.concat_map
-      (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
-      named_binops
-  in
-  let misc =
-    match !backend with
-    | FStar ->
-        [
-          "assert";
-          "assert_norm";
-          "assume";
-          "else";
-          "fun";
-          "fn";
-          "FStar";
-          "FStar.Mul";
-          "if";
-          "in";
-          "include";
-          "int";
-          "let";
-          "list";
-          "match";
-          "open";
-          "rec";
-          "scalar_cast";
-          "then";
-          "type";
-          "Type0";
-          "Type";
-          "unit";
-          "val";
-          "with";
-        ]
-    | Coq ->
-        [
-          "assert";
-          "Arguments";
-          "Axiom";
-          "char_of_byte";
-          "Check";
-          "Declare";
-          "Definition";
-          "else";
-          "End";
-          "fun";
-          "Fixpoint";
-          "if";
-          "in";
-          "int";
-          "Inductive";
-          "Import";
-          "let";
-          "Lemma";
-          "match";
-          "Module";
-          "not";
-          "Notation";
-          "Proof";
-          "Qed";
-          "rec";
-          "Record";
-          "Require";
-          "Scope";
-          "Search";
-          "SearchPattern";
-          "Set";
-          "then";
-          (* [tt] is unit *)
-          "tt";
-          "type";
-          "Type";
-          "unit";
-          "with";
-        ]
-    | Lean ->
-        [
-          "by";
-          "class";
-          "decreasing_by";
-          "def";
-          "deriving";
-          "do";
-          "else";
-          "end";
-          "for";
-          "have";
-          "if";
-          "inductive";
-          "instance";
-          "import";
-          "let";
-          "macro";
-          "match";
-          "namespace";
-          "opaque";
-          "open";
-          "run_cmd";
-          "set_option";
-          "simp";
-          "structure";
-          "syntax";
-          "termination_by";
-          "then";
-          "Type";
-          "unsafe";
-          "where";
-          "with";
-          "opaque_defs";
-        ]
-    | HOL4 ->
-        [
-          "Axiom";
-          "case";
-          "Definition";
-          "else";
-          "End";
-          "fix";
-          "fix_exec";
-          "fn";
-          "fun";
-          "if";
-          "in";
-          "int";
-          "Inductive";
-          "let";
-          "of";
-          "Proof";
-          "QED";
-          "then";
-          "Theorem";
-        ]
-  in
-  List.concat [ named_unops; named_binops; misc ]
+let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit =
+  match cv with
+  | VScalar sv -> (
+      match !backend with
+      | 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.int_ty);
+              F.pp_print_space fmt ()
+          | _ -> raise (Failure "Unreachable"));
+          (* We need to add parentheses if the value is negative *)
+          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.value) ^ ":Int))")
+          else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
+          (match !backend with
+          | Coq ->
+              let iname = int_name sv.int_ty in
+              F.pp_print_string fmt ("%" ^ iname)
+          | Lean ->
+              let iname = String.lowercase_ascii (int_name sv.int_ty) in
+              F.pp_print_string fmt ("#" ^ iname)
+          | HOL4 -> ()
+          | _ -> raise (Failure "Unreachable"));
+          if print_brackets then F.pp_print_string fmt ")")
+  | VBool b ->
+      let b =
+        match !backend with
+        | HOL4 -> if b then "T" else "F"
+        | Coq | FStar | Lean -> if b then "true" else "false"
+      in
+      F.pp_print_string fmt b
+  | VChar c -> (
+      match !backend with
+      | HOL4 ->
+          (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
+          F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
+      | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+      | Coq ->
+          if inside then F.pp_print_string fmt "(";
+          F.pp_print_string fmt "char_of_byte";
+          F.pp_print_space fmt ();
+          (* Convert the the char to ascii *)
+          let c =
+            let i = Char.code c in
+            let x0 = i / 16 in
+            let x1 = i mod 16 in
+            "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
+          in
+          F.pp_print_string fmt c;
+          if inside then F.pp_print_string fmt ")")
 
-let assumed_adts () : (assumed_ty * string) list =
-  match !backend with
-  | Lean ->
-      [
-        (TState, "State");
-        (TResult, "Result");
-        (TError, "Error");
-        (TFuel, "Nat");
-        (TArray, "Array");
-        (TSlice, "Slice");
-        (TStr, "Str");
-        (TRawPtr Mut, "MutRawPtr");
-        (TRawPtr Const, "ConstRawPtr");
-      ]
-  | Coq | FStar | HOL4 ->
-      [
-        (TState, "state");
-        (TResult, "result");
-        (TError, "error");
-        (TFuel, if !backend = HOL4 then "num" else "nat");
-        (TArray, "array");
-        (TSlice, "slice");
-        (TStr, "str");
-        (TRawPtr Mut, "mut_raw_ptr");
-        (TRawPtr Const, "const_raw_ptr");
-      ]
-
-let assumed_struct_constructors () : (assumed_ty * string) list =
-  match !backend with
-  | Lean -> [ (TArray, "Array.make") ]
-  | Coq -> [ (TArray, "mk_array") ]
-  | FStar -> [ (TArray, "mk_array") ]
-  | HOL4 -> [ (TArray, "mk_array") ]
-
-let assumed_variants () : (assumed_ty * VariantId.id * string) list =
-  match !backend with
-  | FStar ->
-      [
-        (TResult, result_return_id, "Return");
-        (TResult, result_fail_id, "Fail");
-        (TError, error_failure_id, "Failure");
-        (TError, error_out_of_fuel_id, "OutOfFuel");
-        (* No Fuel::Zero on purpose *)
-        (* No Fuel::Succ on purpose *)
-      ]
-  | Coq ->
-      [
-        (TResult, result_return_id, "Return");
-        (TResult, result_fail_id, "Fail_");
-        (TError, error_failure_id, "Failure");
-        (TError, error_out_of_fuel_id, "OutOfFuel");
-        (TFuel, fuel_zero_id, "O");
-        (TFuel, fuel_succ_id, "S");
-      ]
-  | Lean ->
-      [
-        (TResult, result_return_id, "ret");
-        (TResult, result_fail_id, "fail");
-        (TError, error_failure_id, "panic");
-        (* No Fuel::Zero on purpose *)
-        (* No Fuel::Succ on purpose *)
-      ]
-  | HOL4 ->
-      [
-        (TResult, result_return_id, "Return");
-        (TResult, result_fail_id, "Fail");
-        (TError, error_failure_id, "Failure");
-        (* No Fuel::Zero on purpose *)
-        (* No Fuel::Succ on purpose *)
-      ]
-
-let assumed_llbc_functions () :
-    (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
-  let rg0 = Some T.RegionGroupId.zero in
-  match !backend with
-  | FStar | Coq | HOL4 ->
-      [
-        (ArrayIndexShared, None, "array_index_usize");
-        (ArrayIndexMut, None, "array_index_usize");
-        (ArrayIndexMut, rg0, "array_update_usize");
-        (ArrayToSliceShared, None, "array_to_slice");
-        (ArrayToSliceMut, None, "array_to_slice");
-        (ArrayToSliceMut, rg0, "array_from_slice");
-        (ArrayRepeat, None, "array_repeat");
-        (SliceIndexShared, None, "slice_index_usize");
-        (SliceIndexMut, None, "slice_index_usize");
-        (SliceIndexMut, rg0, "slice_update_usize");
-      ]
-  | Lean ->
-      [
-        (ArrayIndexShared, None, "Array.index_usize");
-        (ArrayIndexMut, None, "Array.index_usize");
-        (ArrayIndexMut, rg0, "Array.update_usize");
-        (ArrayToSliceShared, None, "Array.to_slice");
-        (ArrayToSliceMut, None, "Array.to_slice");
-        (ArrayToSliceMut, rg0, "Array.from_slice");
-        (ArrayRepeat, None, "Array.repeat");
-        (SliceIndexShared, None, "Slice.index_usize");
-        (SliceIndexMut, None, "Slice.index_usize");
-        (SliceIndexMut, rg0, "Slice.update_usize");
-      ]
-
-let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
-  match !backend with
-  | FStar ->
-      [
-        (Return, "return");
-        (Fail, "fail");
-        (Assert, "massert");
-        (FuelDecrease, "decrease");
-        (FuelEqZero, "is_zero");
-      ]
-  | Coq ->
-      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
-      [ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
-  | Lean ->
-      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
-      [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ]
-  | HOL4 ->
-      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
-      [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
-
-let names_map_init () : names_map_init =
-  {
-    keywords = keywords ();
-    assumed_adts = assumed_adts ();
-    assumed_structs = assumed_struct_constructors ();
-    assumed_variants = assumed_variants ();
-    assumed_llbc_functions = assumed_llbc_functions ();
-    assumed_pure_functions = assumed_pure_functions ();
-  }
+(** Format a unary operation
 
+    Inputs:
+    - a formatter for expressions (called on the argument of the unop)
+    - extraction context (see below)
+    - formatter
+    - expression formatter
+    - [inside]
+    - unop
+    - argument
+ *)
 let extract_unop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
     =
@@ -409,7 +143,18 @@ let extract_unop (extract_expr : bool -> texpression -> unit)
           extract_expr true arg;
           if inside then F.pp_print_string fmt ")")
 
-(** [extract_expr] : the boolean argument is [inside] *)
+(** Format a binary operation
+
+    Inputs:
+    - a formatter for expressions (called on the arguments of the binop)
+    - extraction context (see below)
+    - formatter
+    - expression formatter
+    - [inside]
+    - binop
+    - argument 0
+    - argument 1
+ *)
 let extract_binop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (binop : E.binop)
     (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
@@ -451,523 +196,6 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
       extract_expr true arg1);
   if inside then F.pp_print_string fmt ")"
 
-let type_decl_kind_to_qualif (kind : decl_kind)
-    (type_kind : type_decl_kind option) : string option =
-  match !backend with
-  | FStar -> (
-      match kind with
-      | SingleNonRec -> Some "type"
-      | SingleRec -> Some "type"
-      | MutRecFirst -> Some "type"
-      | MutRecInner -> Some "and"
-      | MutRecLast -> Some "and"
-      | Assumed -> Some "assume type"
-      | Declared -> Some "val")
-  | Coq -> (
-      match (kind, type_kind) with
-      | SingleNonRec, Some Enum -> Some "Inductive"
-      | SingleNonRec, Some Struct -> Some "Record"
-      | (SingleRec | MutRecFirst), Some _ -> Some "Inductive"
-      | (MutRecInner | MutRecLast), Some _ ->
-          (* Coq doesn't support groups of mutually recursive definitions which mix
-           * records and inducties: we convert everything to records if this happens
-           *)
-          Some "with"
-      | (Assumed | Declared), None -> Some "Axiom"
-      | SingleNonRec, None ->
-          (* This is for traits *)
-          Some "Record"
-      | _ ->
-          raise
-            (Failure
-               ("Unexpected: (" ^ show_decl_kind kind ^ ", "
-               ^ Print.option_to_string show_type_decl_kind type_kind
-               ^ ")")))
-  | Lean -> (
-      match kind with
-      | SingleNonRec ->
-          if type_kind = Some Struct then Some "structure" else Some "inductive"
-      | SingleRec -> Some "inductive"
-      | MutRecFirst -> Some "inductive"
-      | MutRecInner -> Some "inductive"
-      | MutRecLast -> Some "inductive"
-      | Assumed -> Some "axiom"
-      | Declared -> Some "axiom")
-  | HOL4 -> None
-
-let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
-  match !backend with
-  | FStar -> (
-      match kind with
-      | SingleNonRec -> Some "let"
-      | SingleRec -> Some "let rec"
-      | MutRecFirst -> Some "let rec"
-      | MutRecInner -> Some "and"
-      | MutRecLast -> Some "and"
-      | Assumed -> Some "assume val"
-      | Declared -> Some "val")
-  | Coq -> (
-      match kind with
-      | SingleNonRec -> Some "Definition"
-      | SingleRec -> Some "Fixpoint"
-      | MutRecFirst -> Some "Fixpoint"
-      | MutRecInner -> Some "with"
-      | MutRecLast -> Some "with"
-      | Assumed -> Some "Axiom"
-      | Declared -> Some "Axiom")
-  | Lean -> (
-      match kind with
-      | SingleNonRec -> Some "def"
-      | SingleRec -> Some "divergent def"
-      | MutRecFirst -> Some "mutual divergent def"
-      | MutRecInner -> Some "divergent def"
-      | MutRecLast -> Some "divergent def"
-      | Assumed -> Some "axiom"
-      | Declared -> Some "axiom")
-  | HOL4 -> None
-
-(** The type of types.
-
-    TODO: move inside the formatter?
- *)
-let type_keyword () =
-  match !backend with
-  | FStar -> "Type0"
-  | 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
-   case we use the first letter of the type name.
-
-   [variant_concatenate_type_name]: if true, add the type name as a prefix
-   to the variant names.
-   Ex.:
-   In Rust:
-     {[
-       enum List = {
-         Cons(u32, Box<List>),x
-         Nil,
-       }
-     ]}
-
-   F*, if option activated:
-     {[
-       type list =
-       | ListCons : u32 -> list -> list
-       | ListNil : list
-     ]}
-
-   F*, if option not activated:
-     {[
-       type list =
-       | Cons : u32 -> list -> list
-       | Nil : list
-     ]}
-
-   Rk.: this should be true by default, because in Rust all the variant names
-   are actively uniquely identifier by the type name [List::Cons(...)], while
-   in other languages it is not necessarily the case, and thus clashes can mess
-   up type checking. Note that some languages actually forbids the name clashes
-   (it is the case of F* ).
- *)
-let mk_formatter (ctx : trans_ctx) (crate_name : string)
-    (variant_concatenate_type_name : bool) : formatter =
-  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 ignore disambiguators (there may be collisions, but we
-     check if there are).
-  *)
-  let name_to_simple_name (name : llbc_name) : string list =
-    (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
-    match name with
-    | (PeIdent (crate, _) as id) :: name ->
-        let name = if crate = crate_name then name else id :: name in
-        name_to_simple_name ctx name
-    | _ ->
-        raise
-          (Failure
-             ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
-  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
-    | FStar | Coq | HOL4 -> String.concat "_" (get_type_name name)
-    | Lean -> String.concat "." (get_type_name name)
-  in
-  let type_name name =
-    match !backend with
-    | FStar ->
-        StringUtils.lowercase_first_letter (get_type_name_no_suffix name ^ "_t")
-    | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t"
-    | Lean -> get_type_name_no_suffix name
-  in
-  let field_name (def_name : llbc_name) (field_id : FieldId.id)
-      (field_name : string option) : string =
-    let field_name_s =
-      match field_name with
-      | Some field_name -> field_name
-      | None ->
-          (* TODO: extract structs with no field names to tuples *)
-          FieldId.to_string field_id
-    in
-    if !Config.record_fields_short_names then
-      if field_name = None then (* TODO: this is a bit ugly *)
-        "_" ^ field_name_s
-      else field_name_s
-    else
-      let def_name = get_type_name_no_suffix def_name ^ "_" ^ field_name_s in
-      match !backend with
-      | Lean | HOL4 -> def_name
-      | Coq | FStar -> StringUtils.lowercase_first_letter def_name
-  in
-  let variant_name (def_name : llbc_name) (variant : string) : string =
-    match !backend with
-    | FStar | Coq | HOL4 ->
-        let variant = to_camel_case variant in
-        if variant_concatenate_type_name then
-          StringUtils.capitalize_first_letter
-            (get_type_name_no_suffix def_name ^ "_" ^ variant)
-        else variant
-    | Lean -> variant
-  in
-  let struct_constructor (basename : llbc_name) : string =
-    let tname = type_name basename in
-    ExtractBuiltin.mk_struct_constructor tname
-  in
-  let get_fun_name fname =
-    let fname = get_name fname in
-    (* TODO: don't convert to snake case for Coq, HOL4, F* *)
-    let fname = flatten_name fname in
-    match !backend with
-    | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
-    | Lean -> fname
-  in
-  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 : 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
-    (* Concatenate *)
-    fname ^ suffix
-  in
-
-  let trait_decl_name (trait_decl : trait_decl) : string =
-    type_name trait_decl.llbc_name
-  in
-
-  let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
-      string =
-    (* We derive the trait impl name from the implemented trait.
-       For instance, if this implementation is an instance of `trait::Trait`
-       for `<foo::Foo, u32>`, we generate the name: "trait.TraitFooFooU32Inst".
-       Importantly, it is to be noted that the name is independent of the place
-       where the instance has been defined (it is indepedent of the file, etc.).
-    *)
-    let name =
-      (* We need to lookup the LLBC definitions, to have the original instantiation *)
-      let trait_impl =
-        TraitImplId.Map.find trait_impl.def_id ctx.trait_impls_ctx.trait_impls
-      in
-      let params = trait_impl.generics in
-      let args = trait_impl.impl_trait.decl_generics in
-      name_with_generics_to_simple_name ctx trait_decl.llbc_name params args
-    in
-    let name = flatten_name name in
-    match !backend with
-    | FStar -> StringUtils.lowercase_first_letter name
-    | Coq | HOL4 | Lean -> name
-  in
-
-  let trait_decl_constructor (trait_decl : trait_decl) : string =
-    let name = trait_decl_name trait_decl in
-    ExtractBuiltin.mk_struct_constructor name
-  in
-
-  let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause)
-      : string =
-    (* TODO: improve - it would be better to not use indices *)
-    let clause = "parent_clause_" ^ TraitClauseId.to_string clause.clause_id in
-    if !Config.record_fields_short_names then clause
-    else trait_decl_name trait_decl ^ "_" ^ clause
-  in
-  let trait_type_name (trait_decl : trait_decl) (item : string) : string =
-    let name =
-      if !Config.record_fields_short_names then item
-      else trait_decl_name trait_decl ^ "_" ^ item
-    in
-    (* Constants are usually all capital letters.
-       Some backends do not support field names starting with a capital letter,
-       and it may be weird to lowercase everything (especially as it may lead
-       to more name collisions): we add a prefix when necessary.
-       For instance, it gives: "U" -> "tU"
-       Note that for some backends we prepend the type name (because those backends
-       can't disambiguate fields coming from different ADTs if they have the same
-       names), and thus don't need to add a prefix starting with a lowercase.
-    *)
-    match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
-  in
-  let trait_const_name (trait_decl : trait_decl) (item : string) : string =
-    let name =
-      if !Config.record_fields_short_names then item
-      else trait_decl_name trait_decl ^ "_" ^ item
-    in
-    (* See [trait_type_name] *)
-    match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
-  in
-  let trait_method_name (trait_decl : trait_decl) (item : string) : string =
-    if !Config.record_fields_short_names then item
-    else trait_decl_name trait_decl ^ "_" ^ item
-  in
-  let trait_type_clause_name (trait_decl : trait_decl) (item : string)
-      (clause : trait_clause) : string =
-    (* TODO: improve - it would be better to not use indices *)
-    trait_type_name trait_decl item
-    ^ "_clause_"
-    ^ TraitClauseId.to_string clause.clause_id
-  in
-
-  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
-    (* Compute the suffix *)
-    let suffix =
-      match !Config.backend with
-      | FStar -> "_decreases"
-      | Lean -> "_terminates"
-      | Coq | HOL4 -> raise (Failure "Unexpected")
-    in
-    (* Concatenate *)
-    fname ^ lp_suffix ^ suffix
-  in
-
-  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
-    (* Compute the suffix *)
-    let suffix =
-      match !Config.backend with
-      | Lean -> "_decreases"
-      | FStar | Coq | HOL4 -> raise (Failure "Unexpected")
-    in
-    (* Concatenate *)
-    fname ^ lp_suffix ^ suffix
-  in
-
-  let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
-      : string =
-    (* Small helper to derive var names from ADT type names.
-
-       We do the following:
-       - convert the type name to snake case
-       - take the first letter of every "letter group"
-       Ex.: "HashMap" -> "hash_map" -> "hm"
-    *)
-    let name_from_type_ident (name : string) : string =
-      let cl = to_snake_case name in
-      let cl = String.split_on_char '_' cl in
-      let cl = List.filter (fun s -> String.length s > 0) cl in
-      assert (List.length cl > 0);
-      let cl = List.map (fun s -> s.[0]) cl in
-      StringUtils.string_of_chars cl
-    in
-    (* If there is a basename, we use it *)
-    match basename with
-    | Some basename ->
-        (* This should be a no-op *)
-        to_snake_case basename
-    | None -> (
-        (* No basename: we use the first letter of the type *)
-        match ty with
-        | TAdt (type_id, generics) -> (
-            match type_id with
-            | TTuple ->
-                (* The "pair" case is frequent enough to have its special treatment *)
-                if List.length generics.types = 2 then "p" else "t"
-            | TAssumed TResult -> "r"
-            | TAssumed TError -> ConstStrings.error_basename
-            | TAssumed TFuel -> ConstStrings.fuel_basename
-            | TAssumed TArray -> "a"
-            | TAssumed TSlice -> "s"
-            | TAssumed TStr -> "s"
-            | TAssumed TState -> ConstStrings.state_basename
-            | TAssumed (TRawPtr _) -> "p"
-            | 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"
-                *)
-                (* The name shouldn't be empty, and its last element should
-                 * be an ident *)
-                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
-            | FStar -> "x" (* lacking inspiration here... *)
-            | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
-        | TLiteral lty -> (
-            match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
-        | TArrow _ -> "f"
-        | TTraitType (_, _, name) -> name_from_type_ident name)
-  in
-  let type_var_basename (_varset : StringSet.t) (basename : string) : string =
-    (* Rust type variables are snake-case and start with a capital letter *)
-    match !backend with
-    | FStar ->
-        (* This is *not* a no-op: this removes the capital letter *)
-        to_snake_case basename
-    | HOL4 ->
-        (* In HOL4, type variable names must start with "'" *)
-        "'" ^ to_snake_case basename
-    | Coq | Lean -> basename
-  in
-  let const_generic_var_basename (_varset : StringSet.t) (basename : string) :
-      string =
-    (* Rust type variables are snake-case and start with a capital letter *)
-    match !backend with
-    | FStar | HOL4 ->
-        (* This is *not* a no-op: this removes the capital letter *)
-        to_snake_case basename
-    | Coq | Lean -> basename
-  in
-  let trait_clause_basename (_varset : StringSet.t) (_clause : trait_clause) :
-      string =
-    (* TODO: actually use the clause to derive the name *)
-    "inst"
-  in
-  let trait_self_clause_basename = "self_clause" in
-  let append_index (basename : string) (i : int) : string =
-    basename ^ string_of_int i
-  in
-
-  let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit
-      =
-    match cv with
-    | VScalar sv -> (
-        match !backend with
-        | 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.int_ty);
-                F.pp_print_space fmt ()
-            | _ -> raise (Failure "Unreachable"));
-            (* We need to add parentheses if the value is negative *)
-            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.value) ^ ":Int))")
-            else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
-            (match !backend with
-            | Coq ->
-                let iname = int_name sv.int_ty in
-                F.pp_print_string fmt ("%" ^ iname)
-            | Lean ->
-                let iname = String.lowercase_ascii (int_name sv.int_ty) in
-                F.pp_print_string fmt ("#" ^ iname)
-            | HOL4 -> ()
-            | _ -> raise (Failure "Unreachable"));
-            if print_brackets then F.pp_print_string fmt ")")
-    | VBool b ->
-        let b =
-          match !backend with
-          | HOL4 -> if b then "T" else "F"
-          | Coq | FStar | Lean -> if b then "true" else "false"
-        in
-        F.pp_print_string fmt b
-    | VChar c -> (
-        match !backend with
-        | HOL4 ->
-            (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
-            F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
-        | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
-        | Coq ->
-            if inside then F.pp_print_string fmt "(";
-            F.pp_print_string fmt "char_of_byte";
-            F.pp_print_space fmt ();
-            (* Convert the the char to ascii *)
-            let c =
-              let i = Char.code c in
-              let x0 = i / 16 in
-              let x1 = i mod 16 in
-              "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
-            in
-            F.pp_print_string fmt c;
-            if inside then F.pp_print_string fmt ")")
-  in
-  let bool_name = if !backend = Lean then "Bool" else "bool" in
-  let char_name = if !backend = Lean then "Char" else "char" in
-  let str_name = if !backend = Lean then "String" else "string" in
-  {
-    bool_name;
-    char_name;
-    int_name;
-    str_name;
-    type_decl_kind_to_qualif;
-    fun_decl_kind_to_qualif;
-    field_name;
-    variant_name;
-    struct_constructor;
-    type_name;
-    global_name;
-    fun_name;
-    termination_measure_name;
-    decreases_proof_name;
-    trait_decl_name;
-    trait_impl_name;
-    trait_decl_constructor;
-    trait_parent_clause_name;
-    trait_const_name;
-    trait_type_name;
-    trait_method_name;
-    trait_type_clause_name;
-    var_basename;
-    type_var_basename;
-    const_generic_var_basename;
-    trait_self_clause_basename;
-    trait_clause_basename;
-    append_index;
-    extract_literal;
-    extract_unop;
-    extract_binop;
-  }
-
-let mk_formatter_and_names_maps (ctx : trans_ctx) (crate_name : string)
-    (variant_concatenate_type_name : bool) : formatter * names_maps =
-  let fmt = mk_formatter ctx crate_name variant_concatenate_type_name in
-  let names_maps = initialize_names_maps fmt (names_map_init ()) in
-  (fmt, names_maps)
-
 let is_single_opaque_fun_decl_group (dg : Pure.fun_decl list) : bool =
   match dg with [ d ] -> d.body = None | _ -> false
 
@@ -1125,17 +353,17 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
   | CgGlobal id ->
       let s = ctx_get_global id ctx in
       F.pp_print_string fmt s
-  | CgValue v -> ctx.fmt.extract_literal fmt inside v
+  | CgValue v -> extract_literal fmt inside v
   | CgVar id ->
       let s = ctx_get_const_generic_var id ctx in
       F.pp_print_string fmt s
 
-let extract_literal_type (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
     (ty : literal_type) : unit =
   match ty with
-  | TBool -> F.pp_print_string fmt ctx.fmt.bool_name
-  | TChar -> F.pp_print_string fmt ctx.fmt.char_name
-  | TInteger int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+  | TBool -> F.pp_print_string fmt (bool_name ())
+  | TChar -> F.pp_print_string fmt (char_name ())
+  | TInteger int_ty -> F.pp_print_string fmt (int_name int_ty)
 
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
@@ -1446,7 +674,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.llbc_name
+    | None -> ctx_compute_type_name ctx def.llbc_name
     | Some info -> info.extract_name
   in
   let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
@@ -1464,10 +692,14 @@ 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.llbc_name fid field.field_name))
+                    ( fid,
+                      ctx_compute_field_name ctx def.llbc_name fid
+                        field.field_name ))
                   fields
               in
-              let cons_name = ctx.fmt.struct_constructor def.llbc_name in
+              let cons_name =
+                ctx_compute_struct_constructor ctx def.llbc_name
+              in
               (field_names, cons_name)
           | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
               let field_names =
@@ -1503,12 +735,13 @@ 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.llbc_name variant.variant_name
+                    ctx_compute_variant_name ctx 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.llbc_name in
+                      let type_name = ctx_compute_type_name ctx def.llbc_name in
                       type_name ^ "." ^ name
                     else name
                   in
@@ -1570,8 +803,7 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
           | Some field_name ->
               let var_id = VarId.of_int (FieldId.to_int fid) in
               let field_name =
-                ctx.fmt.var_basename ctx.names_maps.names_map.names_set
-                  (Some field_name) f.field_ty
+                ctx_compute_var_basename ctx (Some field_name) f.field_ty
               in
               let ctx, field_name = ctx_add_var field_name var_id ctx in
               F.pp_print_string fmt (field_name ^ " :");
@@ -1652,7 +884,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.llbc_name v.variant_name in
+    let cons_name = ctx_compute_variant_name ctx 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
@@ -2059,7 +1291,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "type TYPE_NAME" *)
-  let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
+  let qualif = type_decl_kind_to_qualif kind type_kind in
   (match qualif with
   | Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name)
   | None -> F.pp_print_string fmt def_name);
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 0daf454d..e350da8a 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -178,7 +178,10 @@ let () =
           log#error "The Lean backend doesn't support the -use-fuel option";
           fail ());
         (* Lean can disambiguate the field names *)
-        record_fields_short_names := true
+        record_fields_short_names := true;
+        (* We exploit the fact that the variant name should always be
+           prefixed with the type name to prevent collisions *)
+        variant_concatenate_type_name := false
     | HOL4 ->
         (* We don't support fuel for the HOL4 backend *)
         if !use_fuel then (
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 271d19ad..05e48af5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -993,20 +993,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     translate_crate_to_pure crate
   in
 
-  (* Initialize the extraction context - for now we extract only to F*.
-   * We initialize the names map by registering the keywords used in the
-   * language, as well as some primitive names ("u32", etc.) *)
-  let variant_concatenate_type_name =
-    (* For Lean, we exploit the fact that the variant name should always be
-       prefixed with the type name to prevent collisions *)
-    match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false
-  in
-  (* Initialize the names map (we insert the names of the "primitives"
-     declarations, and insert the names of the local declarations later) *)
-  let fmt, names_maps =
-    Extract.mk_formatter_and_names_maps trans_ctx crate.name
-      variant_concatenate_type_name
-  in
+  (* Initialize the names map by registering the keywords used in the
+     language, as well as some primitive names ("u32", etc.).
+     We insert the names of the local declarations later. *)
+  let names_maps = Extract.initialize_names_maps () in
 
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
@@ -1061,7 +1051,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       ExtractBase.crate;
       trans_ctx;
       names_maps;
-      fmt;
       indent_incr = 2;
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
       fun_name_info = PureUtils.RegularFunIdMap.empty;