Use the name matcher implemented in Charon

19 files changed, 440 insertions, 495 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 6aec626a..48b7ee2b 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -42,7 +42,7 @@ module Sig = struct
   let tvar_id_0 = TypeVarId.of_int 0
   let tvar_0 : ty = TVar tvar_id_0
   let cgvar_id_0 = ConstGenericVarId.of_int 0
-  let cgvar_0 : const_generic = CGVar cgvar_id_0
+  let cgvar_0 : const_generic = CgVar cgvar_id_0
 
   (** Region 'a of id 0 *)
   let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" }
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index cd62c15c..fb3364f4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -27,8 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
       let builtin =
         let open ExtractBuiltin in
         let funs_map = builtin_funs_map () in
-        let sname = name_to_simple_name def.fwd.f.llbc_name in
-        SimpleNameMap.find_opt sname funs_map
+        match_name_find_opt ctx.trans_ctx def.fwd.f.llbc_name funs_map
       in
       (* Use the builtin names if necessary *)
       match builtin with
@@ -2024,9 +2023,9 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
     (trait_decl : trait_decl) : extraction_ctx =
   (* Lookup the information if this is a builtin trait *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name trait_decl.llbc_name in
   let builtin_info =
-    SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
+    match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+      (builtin_trait_decls_map ())
   in
   let ctx =
     let trait_name, trait_constructor =
@@ -2061,9 +2060,14 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
   (* Check if the trait implementation is builtin *)
   let builtin_info =
     let open ExtractBuiltin in
-    let type_sname = name_to_simple_name trait_impl.llbc_name in
-    let trait_sname = name_to_simple_name trait_decl.llbc_name in
-    SimpleNamePairMap.find_opt (type_sname, trait_sname)
+    (* Lookup the original Rust impl to retrieve the original trait ref (we
+       use it to derive the name)*)
+    let trait_impl =
+      TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+    in
+    let decl_ref = trait_impl.impl_trait in
+    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+      decl_ref.decl_generics
       (builtin_trait_impls_map ())
   in
   (* Register some builtin information (if necessary) *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ae5a9a22..f1ba35a2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1085,8 +1085,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
   (* Check if the global corresponds to an assumed global that we should map
      to a custom definition in our standard library (for instance, happens
      with "core::num::usize::MAX") *)
-  let sname = name_to_simple_name def.name in
-  match SimpleNameMap.find_opt sname builtin_globals_map with
+  match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
   | Some name ->
       (* Yes: register the custom binding *)
       ctx_add decl name ctx
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index db942ff0..d15905a2 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -5,38 +5,8 @@
  *)
 
 open Config
-open Types
-
-type simple_name = string list [@@deriving show, ord]
-
-(* TODO: update *)
-let name_to_simple_name (s : name) : simple_name =
-  (* We simply ignore the disambiguators - TODO: update *)
-  List.map
-    (function
-      | PeIdent (id, _) -> id
-      | PeImpl i ->
-          (* TODO *)
-          show_impl_elem i)
-    s
-
-(** Small helper which cuts a string at the occurrences of "::" *)
-let string_to_simple_name (s : string) : simple_name =
-  (* No function to split by using string separator?? *)
-  let name = String.split_on_char ':' s in
-  List.filter (fun s -> s <> "") name
-
-module SimpleNameOrd = struct
-  type t = simple_name
-
-  let compare = compare_simple_name
-  let to_string = show_simple_name
-  let pp_t = pp_simple_name
-  let show_t = show_simple_name
-end
-
-module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
-module SimpleNameSet = Collections.MakeSet (SimpleNameOrd)
+open Charon.NameMatcher (* TODO: include? *)
+include ExtractName (* TODO: only open? *)
 
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
@@ -51,6 +21,9 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
   in
   g
 
+let split_on_separator (s : string) : string list =
+  Str.split (Str.regexp "::") s
+
 (** Switch between two values depending on the target backend.
 
     We often compute the same value (typically: a name) if the target
@@ -62,36 +35,36 @@ let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
 let builtin_globals : (string * string) list =
   [
     (* Min *)
-    ("core::num::usize::MIN", "core_usize_min");
-    ("core::num::u8::MIN", "core_u8_min");
-    ("core::num::u16::MIN", "core_u16_min");
-    ("core::num::u32::MIN", "core_u32_min");
-    ("core::num::u64::MIN", "core_u64_min");
-    ("core::num::u128::MIN", "core_u128_min");
-    ("core::num::isize::MIN", "core_isize_min");
-    ("core::num::i8::MIN", "core_i8_min");
-    ("core::num::i16::MIN", "core_i16_min");
-    ("core::num::i32::MIN", "core_i32_min");
-    ("core::num::i64::MIN", "core_i64_min");
-    ("core::num::i128::MIN", "core_i128_min");
+    ("core::num::{usize}::MIN", "core_usize_min");
+    ("core::num::{u8}::MIN", "core_u8_min");
+    ("core::num::{u16}::MIN", "core_u16_min");
+    ("core::num::{u32}::MIN", "core_u32_min");
+    ("core::num::{u64}::MIN", "core_u64_min");
+    ("core::num::{u128}::MIN", "core_u128_min");
+    ("core::num::{isize}::MIN", "core_isize_min");
+    ("core::num::{i8}::MIN", "core_i8_min");
+    ("core::num::{i16}::MIN", "core_i16_min");
+    ("core::num::{i32}::MIN", "core_i32_min");
+    ("core::num::{i64}::MIN", "core_i64_min");
+    ("core::num::{i128}::MIN", "core_i128_min");
     (* Max *)
-    ("core::num::usize::MAX", "core_usize_max");
-    ("core::num::u8::MAX", "core_u8_max");
-    ("core::num::u16::MAX", "core_u16_max");
-    ("core::num::u32::MAX", "core_u32_max");
-    ("core::num::u64::MAX", "core_u64_max");
-    ("core::num::u128::MAX", "core_u128_max");
-    ("core::num::isize::MAX", "core_isize_max");
-    ("core::num::i8::MAX", "core_i8_max");
-    ("core::num::i16::MAX", "core_i16_max");
-    ("core::num::i32::MAX", "core_i32_max");
-    ("core::num::i64::MAX", "core_i64_max");
-    ("core::num::i128::MAX", "core_i128_max");
+    ("core::num::{usize}::MAX", "core_usize_max");
+    ("core::num::{u8}::MAX", "core_u8_max");
+    ("core::num::{u16}::MAX", "core_u16_max");
+    ("core::num::{u32}::MAX", "core_u32_max");
+    ("core::num::{u64}::MAX", "core_u64_max");
+    ("core::num::{u128}::MAX", "core_u128_max");
+    ("core::num::{isize}::MAX", "core_isize_max");
+    ("core::num::{i8}::MAX", "core_i8_max");
+    ("core::num::{i16}::MAX", "core_i16_max");
+    ("core::num::{i32}::MAX", "core_i32_max");
+    ("core::num::{i64}::MAX", "core_i64_max");
+    ("core::num::{i128}::MAX", "core_i128_max");
   ]
 
-let builtin_globals_map : string SimpleNameMap.t =
-  SimpleNameMap.of_list
-    (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+let builtin_globals_map : string NameMatcherMap.t =
+  NameMatcherMap.of_list
+    (List.map (fun (x, y) -> (parse_pattern x, y)) builtin_globals)
 
 type builtin_variant_info = { fields : (string * string) list }
 [@@deriving show]
@@ -111,7 +84,7 @@ type builtin_type_body_info =
 [@@deriving show]
 
 type builtin_type_info = {
-  rust_name : string list;
+  rust_name : pattern;
   extract_name : string;
   keep_params : bool list option;
       (** We might want to filter some of the type parameters.
@@ -143,11 +116,11 @@ let mk_struct_constructor (type_name : string) : string =
     a type parameter for the allocator to use, which we want to filter.
  *)
 let builtin_types () : builtin_type_info list =
-  let mk_type (rust_name : string list) ?(keep_params : bool list option = None)
+  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 rust_name
+      String.concat sep (split_on_separator rust_name)
     in
     let body_info : builtin_type_body_info option =
       match kind with
@@ -166,17 +139,17 @@ let builtin_types () : builtin_type_info list =
           Some (Struct (constructor, fields))
       | KEnum -> raise (Failure "TODO")
     in
+    let rust_name = parse_pattern rust_name in
     { rust_name; extract_name; keep_params; body_info }
   in
 
   [
     (* Alloc *)
-    mk_type [ "alloc"; "alloc"; "Global" ] ();
+    mk_type "alloc::alloc::Global" ();
     (* Vec *)
-    mk_type [ "alloc"; "vec"; "Vec" ] ~keep_params:(Some [ true; false ]) ();
+    mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
     (* Range *)
-    mk_type
-      [ "core"; "ops"; "range"; "Range" ]
+    mk_type "core::ops::range::Range"
       ~kind:(KStruct [ ("start", "start"); ("end", "end_") ])
       ();
     (* Option
@@ -185,7 +158,7 @@ let builtin_types () : builtin_type_info list =
        the target backend.
     *)
     {
-      rust_name = [ "core"; "option"; "Option" ];
+      rust_name = parse_pattern "core::option::Option";
       extract_name =
         (match !backend with
         | Lean -> "Option"
@@ -218,7 +191,7 @@ let builtin_types () : builtin_type_info list =
   ]
 
 let mk_builtin_types_map () =
-  SimpleNameMap.of_list
+  NameMatcherMap.of_list
     (List.map (fun info -> (info.rust_name, info)) (builtin_types ()))
 
 let builtin_types_map = mk_memoized mk_builtin_types_map
@@ -235,15 +208,22 @@ type builtin_fun_info = {
     parameters. For instance, in the case of the `Vec` functions, there is
     a type parameter for the allocator to use, which we want to filter.
  *)
-let builtin_funs () :
-    (string list * bool list option * builtin_fun_info list) list =
+let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
+    =
   let rg0 = Some Types.RegionGroupId.zero in
   (* Small utility *)
-  let mk_fun (name : string list) (extract_name : string list option)
+  let mk_fun (rust_name : string) (extract_name : string option)
       (filter : bool list option) (with_back : bool) (back_no_suffix : bool) :
-      string list * bool list option * builtin_fun_info list =
+      pattern * bool list option * builtin_fun_info list =
+    let rust_name =
+      try parse_pattern rust_name
+      with Failure _ ->
+        raise (Failure ("Could not parse pattern: " ^ rust_name))
+    in
     let extract_name =
-      match extract_name with None -> name | Some name -> name
+      match extract_name with
+      | None -> pattern_to_fun_extract_name rust_name
+      | Some name -> split_on_separator name
     in
     let basename =
       match !backend with
@@ -257,103 +237,55 @@ let builtin_funs () :
       if with_back then [ { rg = rg0; extract_name = basename ^ back_suffix } ]
       else []
     in
-    (name, filter, fwd @ back)
+    (rust_name, filter, fwd @ back)
   in
   [
-    mk_fun [ "core"; "mem"; "replace" ] None None true false;
-    mk_fun [ "alloc"; "vec"; "Vec"; "new" ] None None false false;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "push" ]
-      None
+    mk_fun "core::mem::replace" None None true false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::new" None None false false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::push" None
       (Some [ true; false ])
       true true;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "insert" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" None
       (Some [ true; false ])
       true true;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "len" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::len" None
       (Some [ true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "index" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index" None
       (Some [ true; true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "index_mut" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index_mut" None
       (Some [ true; true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "boxed"; "Box"; "deref" ]
-      None
+    mk_fun "alloc::boxed::{Box<@T>}::deref" None
       (Some [ true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "boxed"; "Box"; "deref_mut" ]
-      None
+    mk_fun "alloc::boxed::{Box<@T>}::deref_mut" None
       (Some [ true; false ])
       true false;
-    (* TODO: fix the same like "[T]" below *)
-    mk_fun
-      [ "core"; "slice"; "index"; "[T]"; "index" ]
-      (Some [ "core"; "slice"; "index"; "Slice"; "index" ])
-      None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "[T]"; "index_mut" ]
-      (Some [ "core"; "slice"; "index"; "Slice"; "index_mut" ])
-      None true false;
-    mk_fun
-      [ "core"; "array"; "[T; N]"; "index" ]
-      (Some [ "core"; "array"; "Array"; "index" ])
-      None true false;
-    mk_fun
-      [ "core"; "array"; "[T; N]"; "index_mut" ]
-      (Some [ "core"; "array"; "Array"; "index_mut" ])
-      None true false;
-    mk_fun [ "core"; "slice"; "index"; "Range"; "get" ] None None true false;
-    mk_fun [ "core"; "slice"; "index"; "Range"; "get_mut" ] None None true false;
-    mk_fun [ "core"; "slice"; "index"; "Range"; "index" ] None None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "Range"; "index_mut" ]
-      None None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "Range"; "get_unchecked" ]
-      None None false false;
-    mk_fun
-      [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ]
-      None None false false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "get" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "get" ])
-      None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "get_mut" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "get_mut" ])
-      None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "get_unchecked" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked" ])
-      None false false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "get_unchecked_mut" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked_mut" ])
-      None false false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "index" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "index" ])
-      None true false;
-    mk_fun
-      [ "core"; "slice"; "index"; "usize"; "index_mut" ]
-      (Some [ "core"; "slice"; "index"; "Usize"; "index_mut" ])
-      None true false;
+    mk_fun "core::slice::index::{[@T]}::index" None None true false;
+    mk_fun "core::slice::index::{[@T]}::index_mut" None None true false;
+    mk_fun "core::array::{[@T; @C]}::index" None None true false;
+    mk_fun "core::array::{[@T; @C]}::index_mut" None None true false;
+    mk_fun "core::slice::index::{Range<@T>}::get" None None true false;
+    mk_fun "core::slice::index::{Range<@T>}::get_mut" None None true false;
+    mk_fun "core::slice::index::{Range<@T>}::index" None None true false;
+    mk_fun "core::slice::index::{Range<@T>}::index_mut" None None true false;
+    mk_fun "core::slice::index::{Range<@T>}::get_unchecked" None None false
+      false;
+    mk_fun "core::slice::index::{Range<@T>}::get_unchecked_mut" None None false
+      false;
+    mk_fun "core::slice::index::{usize}::get" None None true false;
+    mk_fun "core::slice::index::{usize}::get_mut" None None true false;
+    mk_fun "core::slice::index::{usize}::get_unchecked" None None false false;
+    mk_fun "core::slice::index::{usize}::get_unchecked_mut" None None false
+      false;
+    mk_fun "core::slice::index::{usize}::index" None None true false;
+    mk_fun "core::slice::index::{usize}::index_mut" None None true false;
   ]
 
 let mk_builtin_funs_map () =
-  SimpleNameMap.of_list
+  NameMatcherMap.of_list
     (List.map
        (fun (name, filter, info) -> (name, (filter, info)))
        (builtin_funs ()))
@@ -385,17 +317,22 @@ let builtin_fun_effects =
   let int_funs =
     List.map
       (fun int_name ->
-        List.map (fun op -> "core::num::" ^ int_name ^ "::" ^ op) int_ops)
+        List.map
+          (fun op ->
+            "core::num::" ^ "{"
+            ^ StringUtils.capitalize_first_letter int_name
+            ^ "}::" ^ op)
+          int_ops)
       int_names
   in
   let int_funs = List.concat int_funs in
   let no_fail_no_state_funs =
     [
       (* TODO: redundancy with the funs information below *)
-      "alloc::vec::Vec::new";
-      "alloc::vec::Vec::len";
-      "alloc::boxed::Box::deref";
-      "alloc::boxed::Box::deref_mut";
+      "alloc::vec::{alloc::vec::Vec<@T>}::new";
+      "alloc::vec::{alloc::vec::Vec<@T>}::len";
+      "alloc::boxed::{Box<@T>}::deref";
+      "alloc::boxed::{Box<@T>}::deref_mut";
       "core::mem::replace";
       "core::mem::take";
     ]
@@ -409,10 +346,10 @@ let builtin_fun_effects =
   let no_state_funs =
     [
       (* TODO: redundancy with the funs information below *)
-      "alloc::vec::Vec::push";
-      "alloc::vec::Vec::index";
-      "alloc::vec::Vec::index_mut";
-      "alloc::vec::Vec::index_mut_back";
+      "alloc::vec::{alloc::vec::Vec<@T>}::push";
+      "alloc::vec::{alloc::vec::Vec<@T>}::index";
+      "alloc::vec::{alloc::vec::Vec<@T>}::index_mut";
+      "alloc::vec::{alloc::vec::Vec<@T>}::index_mut_back";
     ]
   in
   let no_state_funs =
@@ -421,11 +358,11 @@ let builtin_fun_effects =
   no_fail_no_state_funs @ no_state_funs
 
 let builtin_fun_effects_map =
-  SimpleNameMap.of_list
-    (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects)
+  NameMatcherMap.of_list
+    (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects)
 
 type builtin_trait_decl_info = {
-  rust_name : string;
+  rust_name : pattern;
   extract_name : string;
   constructor : string;
   parent_clauses : string list;
@@ -441,13 +378,15 @@ type builtin_trait_decl_info = {
 
 let builtin_trait_decls_info () =
   let rg0 = Some Types.RegionGroupId.zero in
-  let mk_trait (rust_name : string list) ?(extract_name : string option = None)
+  let mk_trait (rust_name : string) ?(extract_name : string option = None)
       ?(parent_clauses : string list = []) ?(types : string list = [])
       ?(methods : (string * bool) list = []) () : builtin_trait_decl_info =
+    let rust_name = parse_pattern rust_name in
     let extract_name =
       match extract_name with
       | Some n -> n
       | 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)
@@ -487,7 +426,6 @@ let builtin_trait_decls_info () =
       in
       List.map mk_method methods
     in
-    let rust_name = String.concat "::" rust_name in
     {
       rust_name;
       extract_name;
@@ -500,34 +438,27 @@ let builtin_trait_decls_info () =
   in
   [
     (* Deref *)
-    mk_trait
-      [ "core"; "ops"; "deref"; "Deref" ]
-      ~types:[ "Target" ]
+    mk_trait "core::ops::deref::Deref" ~types:[ "Target" ]
       ~methods:[ ("deref", true) ]
       ();
     (* DerefMut *)
-    mk_trait
-      [ "core"; "ops"; "deref"; "DerefMut" ]
+    mk_trait "core::ops::deref::DerefMut"
       ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ]
       ~methods:[ ("deref_mut", true) ]
       ();
     (* Index *)
-    mk_trait
-      [ "core"; "ops"; "index"; "Index" ]
-      ~types:[ "Output" ]
+    mk_trait "core::ops::index::Index" ~types:[ "Output" ]
       ~methods:[ ("index", true) ]
       ();
     (* IndexMut *)
-    mk_trait
-      [ "core"; "ops"; "index"; "IndexMut" ]
+    mk_trait "core::ops::index::IndexMut"
       ~parent_clauses:[ backend_choice "index_inst" "indexInst" ]
       ~methods:[ ("index_mut", true) ]
       ();
     (* Sealed *)
-    mk_trait [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ();
+    mk_trait "core::slice::index::private_slice_index::Sealed" ();
     (* SliceIndex *)
-    mk_trait
-      [ "core"; "slice"; "index"; "SliceIndex" ]
+    mk_trait "core::slice::index::SliceIndex"
       ~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ]
       ~types:[ "Output" ]
       ~methods:
@@ -543,113 +474,56 @@ let builtin_trait_decls_info () =
   ]
 
 let mk_builtin_trait_decls_map () =
-  SimpleNameMap.of_list
+  NameMatcherMap.of_list
     (List.map
-       (fun info -> (string_to_simple_name info.rust_name, info))
+       (fun info -> (info.rust_name, info))
        (builtin_trait_decls_info ()))
 
 let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
 
-(* TODO: generalize this.
-
-   For now, the key is:
-   - name of the impl (ex.: "alloc.boxed.Boxed")
-   - name of the implemented trait (ex.: "core.ops.deref.Deref"
-*)
-type simple_name_pair = simple_name * simple_name [@@deriving show, ord]
-
-module SimpleNamePairOrd = struct
-  type t = simple_name_pair
-
-  let compare = compare_simple_name_pair
-  let to_string = show_simple_name_pair
-  let pp_t = pp_simple_name_pair
-  let show_t = show_simple_name_pair
-end
-
-module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
-
-let builtin_trait_impls_info () :
-    ((string list * string list) * (bool list option * string)) list =
-  let fmt (type_name : string list)
-      ?(extract_type_name : string list option = None)
-      (trait_name : string list) ?(filter : bool list option = None) () :
-      (string list * string list) * (bool list option * string) =
+let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
+  let fmt (rust_name : string) ?(filter : bool list option = None) () :
+      pattern * (bool list option * string) =
+    let rust_name = parse_pattern rust_name in
     let name =
-      let trait_name = String.concat "" trait_name ^ "Inst" in
+      let name = pattern_to_trait_impl_extract_name rust_name in
       let sep = backend_choice "_" "." in
-      let type_name =
-        match extract_type_name with
-        | Some type_name -> type_name
-        | None -> type_name
-      in
-      String.concat sep type_name ^ sep ^ trait_name
+      String.concat sep name
     in
-    ((type_name, trait_name), (filter, name))
+    (rust_name, (filter, name))
   in
-  (* TODO: fix the names like "[T]" below *)
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
-    fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "Deref" ] ();
-    (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
-    fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] ();
+    fmt "core::ops::Deref<Box<@T>>" ();
+    (* core::ops::Deref<alloc::boxed::Box<T>> *)
+    fmt "core::ops::Deref<Box<@T>>" ();
     (* core::ops::index::Index<[T], I> *)
-    fmt
-      [ "core"; "slice"; "index"; "[T]" ]
-      ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
-      [ "core"; "ops"; "index"; "Index" ]
-      ();
+    fmt "core::ops::index::Index<[@T], @I>" ();
     (* core::ops::index::IndexMut<[T], I> *)
-    fmt
-      [ "core"; "slice"; "index"; "[T]" ]
-      ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
-      [ "core"; "ops"; "index"; "IndexMut" ]
-      ();
+    fmt "core::ops::index::IndexMut<[@T], @I>" ();
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
-    fmt
-      [ "core"; "slice"; "index"; "private_slice_index"; "Range" ]
-      [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
-      ();
+    fmt "core::slice::index::private_slice_index::Sealed<Range<usize>>" ();
     (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
-    fmt
-      [ "core"; "slice"; "index"; "Range" ]
-      [ "core"; "slice"; "index"; "SliceIndex" ]
-      ();
+    fmt "core::slice::index::SliceIndex<Range<usize>, [@T]>" ();
     (* core::ops::index::Index<[T; N], I> *)
-    fmt
-      [ "core"; "array"; "[T; N]" ]
-      ~extract_type_name:(Some [ "core"; "array"; "Array" ])
-      [ "core"; "ops"; "index"; "Index" ]
-      ();
+    fmt "core::ops::index::Index<[@T; @N], @I>" ();
     (* core::ops::index::IndexMut<[T; N], I> *)
-    fmt
-      [ "core"; "array"; "[T; N]" ]
-      ~extract_type_name:(Some [ "core"; "array"; "Array" ])
-      [ "core"; "ops"; "index"; "IndexMut" ]
-      ();
+    fmt "core::ops::index::IndexMut<[@T; @N], @I>" ();
     (* core::slice::index::private_slice_index::Sealed<usize> *)
-    fmt
-      [ "core"; "slice"; "index"; "private_slice_index"; "usize" ]
-      [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
-      ();
+    fmt "core::slice::index::private_slice_index::Sealed<usize>" ();
     (* core::slice::index::SliceIndex<usize, [T]> *)
-    fmt
-      [ "core"; "slice"; "index"; "usize" ]
-      [ "core"; "slice"; "index"; "SliceIndex" ]
-      ();
-    (* core::ops::index::Index<Vec<T>, T> *)
-    fmt [ "alloc"; "vec"; "Vec" ]
-      [ "core"; "ops"; "index"; "Index" ]
+    fmt "core::slice::index::SliceIndex<usize, [@T]>" ();
+    (* core::ops::index::Index<alloc::vec::Vec<T>, T> *)
+    fmt "core::ops::index::Index<alloc::vec::Vec<@T>, @T>"
       ~filter:(Some [ true; true; false ])
       ();
-    (* core::ops::index::IndexMut<Vec<T>, T> *)
-    fmt [ "alloc"; "vec"; "Vec" ]
-      [ "core"; "ops"; "index"; "IndexMut" ]
+    (* core::ops::index::IndexMut<alloc::vec::Vec<T>, T> *)
+    fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @T>"
       ~filter:(Some [ true; true; false ])
       ();
   ]
 
 let mk_builtin_trait_impls_map () =
-  SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+  NameMatcherMap.of_list (builtin_trait_impls_info ())
 
 let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
new file mode 100644
index 00000000..4f5ca0d1
--- /dev/null
+++ b/compiler/ExtractName.ml
@@ -0,0 +1,177 @@
+(** Utilities for extracting names *)
+
+open Charon.NameMatcher
+
+module NameMatcherMap = struct
+  type 'a t = (pattern * 'a) list
+
+  let config = { map_vars_to_vars = true }
+
+  let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option =
+    match List.find_opt (fun (pat, _) -> match_name ctx config pat name) m with
+    | None -> None
+    | Some (_, v) -> Some v
+
+  let find_with_generics_opt (ctx : ctx) (name : Types.name)
+      (g : Types.generic_args) (m : 'a t) : 'a option =
+    match
+      List.find_opt
+        (fun (pat, _) -> match_name_with_generics ctx config pat name g)
+        m
+    with
+    | None -> None
+    | Some (_, v) -> Some v
+
+  let mem (ctx : ctx) (name : Types.name) (m : 'a t) : bool =
+    find_opt ctx name m <> None
+
+  let of_list (ls : (pattern * 'a) list) : 'a t = ls
+end
+
+(** Helper to convert name patterns to names for extraction.
+
+    For impl blocks, we simply use the name of the type (without its arguments)
+    if all the arguments are variables.
+ *)
+let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
+    string list =
+  let c = { tgt_kind = TkName } in
+  let is_var (g : generic_arg) : bool =
+    match g with
+    | GExpr (EVar _) -> true
+    | GRegion (RVar _) -> true
+    | _ -> false
+  in
+  let all_vars = List.for_all is_var in
+  let elem_to_string (e : pattern_elem) : string =
+    match e with
+    | PIdent _ -> pattern_elem_to_string c e
+    | PImpl ty -> (
+        match ty with
+        | EComp id -> (
+            (* Retrieve the last ident *)
+            let id = Collections.List.last id in
+            match id with
+            | PIdent (s, g) ->
+                if all_vars g then s else pattern_elem_to_string c id
+            | PImpl _ -> raise (Failure "Unreachable"))
+        | EPrimAdt (adt, g) ->
+            if all_vars g then
+              match adt with
+              | TTuple ->
+                  let l = List.length g in
+                  if l = 2 then "Pair" else expr_to_string c ty
+              | TArray -> "Array"
+              | TSlice -> "Slice"
+            else expr_to_string c ty
+        | ERef _ | EVar _ -> raise (Failure ""))
+  in
+  let rec pattern_to_string (n : pattern) : string list =
+    match n with
+    | [] -> raise (Failure "Unreachable")
+    | [ e ] ->
+        let e = elem_to_string e in
+        if is_trait_impl then [ e ^ "Inst" ] else [ e ]
+    | e :: n -> elem_to_string e :: pattern_to_string n
+  in
+  pattern_to_string name
+
+let pattern_to_fun_extract_name = pattern_to_extract_name false
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
+
+(* TODO: this is provisional. We just want to make sure that the extraction
+   names we derive from the patterns (for the builtin definitions) are
+   consistent with the extraction names we derive from the Rust names *)
+let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
+  pattern_to_extract_name false (name_to_pattern ctx n)
+
+let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name)
+    (p : Types.generic_params) (g : Types.generic_args) : string list =
+  pattern_to_extract_name true (name_with_generics_to_pattern ctx n p g)
+
+(*
+  (* 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 rec 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
+        let open Types in
+        let name =
+          List.map
+            (function
+              | PeIdent (s, _) -> s
+              | PeImpl impl -> impl_elem_to_simple_name impl)
+            name
+        in
+        name
+    | _ ->
+        raise
+          (Failure
+             ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
+  and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
+    (* We do something simple for now.
+       TODO: we might want to do something different for impl elements which are
+       actually trait implementations, in order to prevent name collisions (it
+       is possible to define several times the same trait for the same type,
+       but with different instantiations of the type, or different trait
+       requirements *)
+    ty_to_simple_name impl.generics impl.ty
+  and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
+      string =
+    (* We do something simple for now.
+       TODO: find a more principled way of converting types to names.
+       In particular, we might want to do something different for impl elements which are
+       actually trait implementations, in order to prevent name collisions (it
+       is possible to define several times the same trait for the same type,
+       but with different instantiations of the type, or different trait
+       requirements *)
+    match ty with
+    | TAdt (id, args) -> (
+        match id with
+        | TAdtId id ->
+            let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
+            name_last_elem_as_ident def.name
+        | TTuple ->
+            (* TODO *)
+            "Tuple"
+            ^ String.concat ""
+                (List.map (ty_to_simple_name generics) args.types)
+        | TAssumed id -> (
+            match id with
+            | Types.TBox -> "Box"
+            | Types.TArray -> "Array"
+            | Types.TSlice -> "Slice"
+            | Types.TStr -> "Str"))
+    | TVar vid ->
+        (* Use the variable name *)
+        (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
+    | TLiteral lty ->
+        StringUtils.capitalize_first_letter
+          (Print.Types.literal_type_to_string lty)
+    | TNever -> raise (Failure "Unreachable")
+    | TRef (_, rty, rk) -> (
+        let rty = ty_to_simple_name generics rty in
+        match rk with
+        | RMut -> "MutBorrow" ^ rty
+        | RShared -> "SharedBorrow" ^ rty)
+    | TRawPtr (rty, rk) -> (
+        let rty = ty_to_simple_name generics rty in
+        match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
+    | TTraitType (tr, _, name) ->
+        (* TODO: this is way too simple *)
+        let trait_decl =
+          TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
+            ctx.trait_decls_ctx.trait_decls
+        in
+        name_last_elem_as_ident trait_decl.name ^ name
+    | TArrow (inputs, output) ->
+        "Arrow"
+        ^ String.concat ""
+            (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
+  in
+*)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index de4ec735..a74bd532 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -586,84 +586,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
      we remove it. We ignore disambiguators (there may be collisions, but we
      check if there are).
   *)
-  let rec name_to_simple_name (name : llbc_name) : string list =
+  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
-        let open Types in
-        let name =
-          List.map
-            (function
-              | PeIdent (s, _) -> s
-              | PeImpl impl -> impl_elem_to_simple_name impl)
-            name
-        in
-        name
+        name_to_simple_name ctx name
     | _ ->
         raise
           (Failure
              ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
-  and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
-    (* We do something simple for now.
-       TODO: we might want to do something different for impl elements which are
-       actually trait implementations, in order to prevent name collisions (it
-       is possible to define several times the same trait for the same type,
-       but with different instantiations of the type, or different trait
-       requirements *)
-    ty_to_simple_name impl.generics impl.ty
-  and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
-      string =
-    (* We do something simple for now.
-       TODO: find a more principled way of converting types to names.
-       In particular, we might want to do something different for impl elements which are
-       actually trait implementations, in order to prevent name collisions (it
-       is possible to define several times the same trait for the same type,
-       but with different instantiations of the type, or different trait
-       requirements *)
-    match ty with
-    | TAdt (id, args) -> (
-        match id with
-        | TAdtId id ->
-            let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
-            name_last_elem_as_ident def.name
-        | TTuple ->
-            (* TODO *)
-            "Tuple"
-            ^ String.concat ""
-                (List.map (ty_to_simple_name generics) args.types)
-        | TAssumed id -> (
-            match id with
-            | Types.TBox -> "Box"
-            | Types.TArray -> "Array"
-            | Types.TSlice -> "Slice"
-            | Types.TStr -> "Str"))
-    | TVar vid ->
-        (* Use the variable name *)
-        (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
-    | TLiteral lty ->
-        StringUtils.capitalize_first_letter
-          (Print.Types.literal_type_to_string lty)
-    | TNever -> raise (Failure "Unreachable")
-    | TRef (_, rty, rk) -> (
-        let rty = ty_to_simple_name generics rty in
-        match rk with
-        | RMut -> "MutBorrow" ^ rty
-        | RShared -> "SharedBorrow" ^ rty)
-    | TRawPtr (rty, rk) -> (
-        let rty = ty_to_simple_name generics rty in
-        match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
-    | TTraitType (tr, _, name) ->
-        (* TODO: this is way too simple *)
-        let trait_decl =
-          TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
-            ctx.trait_decls_ctx.trait_decls
-        in
-        name_last_elem_as_ident trait_decl.name ^ name
-    | TArrow (inputs, output) ->
-        "Arrow"
-        ^ String.concat ""
-            (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
   in
   let flatten_name (name : string list) : string =
     match !backend with
@@ -747,17 +679,22 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
 
   let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
       string =
-    (* TODO: provisional: we concatenate the trait impl name (which is its type)
-       with the trait decl name *)
-    let trait_decl =
-      let name = trait_decl.llbc_name in
-      let name = get_type_name_no_suffix name ^ "Inst" in
-      (* Remove the occurrences of '.' *)
-      String.concat "" (String.split_on_char '.' name)
-    in
+    (* 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 =
-      flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ])
+      (* 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
@@ -1185,11 +1122,11 @@ let extract_arrow (fmt : F.formatter) () : unit =
 let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (cg : const_generic) : unit =
   match cg with
-  | CGGlobal id ->
+  | 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
-  | CGVar id ->
+  | CgValue v -> ctx.fmt.extract_literal fmt inside v
+  | CgVar id ->
       let s = ctx_get_const_generic_var id ctx in
       F.pp_print_string fmt s
 
@@ -1492,8 +1429,9 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     extraction_ctx =
   (* Lookup the builtin information, if there is *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name def.llbc_name in
-  let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
+  let info =
+    match_name_find_opt ctx.trans_ctx def.llbc_name (builtin_types_map ())
+  in
   (* Register the filtering information, if there is *)
   let ctx =
     match info with
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a07ad35a..9ae6ce86 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -58,6 +58,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
     let can_diverge = ref false in
     let is_rec = ref false in
     let group_has_builtin_info = ref false in
+    let name_matcher_ctx : Charon.NameMatcher.ctx =
+      {
+        type_decls = m.type_decls;
+        global_decls = m.global_decls;
+        trait_decls = m.trait_decls;
+      }
+    in
 
     (* We have some specialized knowledge of some library functions; we don't
        have any more custom treatment than this, and these functions can be modeled
@@ -65,8 +72,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
        way. *)
     let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
       let open ExtractBuiltin in
-      let name = name_to_simple_name f.name in
-      SimpleNameMap.find_opt name builtin_fun_effects_map
+      NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
     in
 
     (* JP: Why not use a reduce visitor here with a tuple of the values to be
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 5b2db90d..c2e47da9 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -80,7 +80,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
     let regions = List.map (fun _ -> RErased) regions in
     let types = List.map (fun (v : type_var) -> TVar v.index) types in
     let const_generics =
-      List.map (fun (v : const_generic_var) -> CGVar v.index) const_generics
+      List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics
     in
     (* Annoying that we have to generate this substitution here *)
     let r_subst _ = raise (Failure "Unexpected region") in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 1e28fd4b..38620be0 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                    ( ctx0,
                      None,
                      value_as_symbolic v.value,
-                     SymbolicAst.VaCGValue vid,
+                     SymbolicAst.VaCgValue vid,
                      e )))
       | CFnPtr _ -> raise (Failure "TODO"))
   | Copy p ->
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 01216157..ffdce481 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -31,21 +31,26 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
 let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     type_decl list * fun_decl list =
   let open ExtractBuiltin in
+  let ctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = k.type_decls;
+      global_decls = k.global_decls;
+      trait_decls = k.trait_decls;
+    }
+  in
   let is_opaque_fun (d : fun_decl) : bool =
-    let sname = name_to_simple_name d.name in
     d.body = None
     (* Something to pay attention to: we must ignore trait method *declarations*
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
     && ((not filter_assumed)
-       || (not (SimpleNameMap.mem sname builtin_globals_map))
-          && not (SimpleNameMap.mem sname (builtin_funs_map ())))
+       || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
+          && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
   in
   let is_opaque_type (d : type_decl) : bool =
-    let sname = name_to_simple_name d.name in
     d.kind = Opaque
     && ((not filter_assumed)
-       || not (SimpleNameMap.mem sname (builtin_types_map ())))
+       || not (NameMatcherMap.mem ctx d.name (builtin_types_map ())))
   in
   (* Note that by checking the function bodies we also the globals *)
   ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls),
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index e6686951..a7ec9336 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -128,9 +128,9 @@ let type_id_to_string (env : fmt_env) (id : type_id) : string =
 (* TODO: duplicates  Charon.PrintTypes.const_generic_to_string *)
 let const_generic_to_string (env : fmt_env) (cg : const_generic) : string =
   match cg with
-  | CGGlobal id -> global_decl_id_to_string env id
-  | CGVar id -> const_generic_var_id_to_string env id
-  | CGValue lit -> literal_to_string lit
+  | CgGlobal id -> global_decl_id_to_string env id
+  | CgVar id -> const_generic_var_id_to_string env id
+  | CgValue lit -> literal_to_string lit
 
 let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
   match ty with
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 5f92d18a..06270621 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -111,7 +111,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
     object
       inherit [_] map_ty
       method! visit_TVar _ var_id = subst.ty_subst var_id
-      method! visit_CGVar _ var_id = subst.cg_subst var_id
+      method! visit_CgVar _ var_id = subst.cg_subst var_id
       method! visit_Clause _ id = subst.tr_subst id
       method! visit_Self _ = subst.tr_self
     end
diff --git a/compiler/StringUtils.ml b/compiler/StringUtils.ml
index 161df27b..3ab4e808 100644
--- a/compiler/StringUtils.ml
+++ b/compiler/StringUtils.ml
@@ -1,111 +1 @@
-(** Utilities to work on strings, character per character.
-
-    They operate on ASCII strings, and are used by the project to convert
-    Rust names: Rust names are not fancy, so it shouldn't be a problem.
-    
-    Rk.: the poor support of OCaml for char manipulation is really annoying...
- *)
-
-let code_0 = 48
-let code_9 = 57
-let code_A = 65
-let code_Z = 90
-let code_a = 97
-let code_z = 122
-
-let is_lowercase_ascii (c : char) : bool =
-  let c = Char.code c in
-  code_a <= c && c <= code_z
-
-let is_uppercase_ascii (c : char) : bool =
-  let c = Char.code c in
-  code_A <= c && c <= code_Z
-
-let is_letter_ascii (c : char) : bool =
-  is_lowercase_ascii c || is_uppercase_ascii c
-
-let is_digit_ascii (c : char) : bool =
-  let c = Char.code c in
-  code_0 <= c && c <= code_9
-
-let lowercase_ascii = Char.lowercase_ascii
-let uppercase_ascii = Char.uppercase_ascii
-
-(** Using buffers as per:
-    {{: https://stackoverflow.com/questions/29957418/how-to-convert-char-list-to-string-in-ocaml} stackoverflow}
- *)
-let string_of_chars (chars : char list) : string =
-  let buf = Buffer.create (List.length chars) in
-  List.iter (Buffer.add_char buf) chars;
-  Buffer.contents buf
-
-let string_to_chars (s : string) : char list =
-  let length = String.length s in
-  let rec apply i =
-    if i = length then [] else String.get s i :: apply (i + 1)
-  in
-  apply 0
-
-(** This operates on ASCII *)
-let to_camel_case (s : string) : string =
-  (* Note that we rebuild the string in reverse order *)
-  let apply ((prev_is_under, acc) : bool * char list) (c : char) :
-      bool * char list =
-    if c = '_' then (true, acc)
-    else
-      let c = if prev_is_under then uppercase_ascii c else c in
-      (false, c :: acc)
-  in
-  let _, chars = List.fold_left apply (true, []) (string_to_chars s) in
-  string_of_chars (List.rev chars)
-
-(** This operates on ASCII *)
-let to_snake_case (s : string) : string =
-  (* Note that we rebuild the string in reverse order *)
-  let apply ((prev_is_low, prev_is_digit, acc) : bool * bool * char list)
-      (c : char) : bool * bool * char list =
-    let acc =
-      if c = '_' then acc
-      else if prev_is_digit then if is_letter_ascii c then '_' :: acc else acc
-      else if prev_is_low then
-        if (is_lowercase_ascii c || is_digit_ascii c) && c <> '_' then acc
-        else '_' :: acc
-      else acc
-    in
-    let prev_is_low = is_lowercase_ascii c in
-    let prev_is_digit = is_digit_ascii c in
-    let c = lowercase_ascii c in
-    (prev_is_low, prev_is_digit, c :: acc)
-  in
-  let _, _, chars =
-    List.fold_left apply (false, false, []) (string_to_chars s)
-  in
-  string_of_chars (List.rev chars)
-
-(** Applies a map operation.
-
-    This is very inefficient, but shouldn't be used much.
- *)
-let map (f : char -> string) (s : string) : string =
-  let sl = List.map f (string_to_chars s) in
-  let sl = List.map string_to_chars sl in
-  string_of_chars (List.concat sl)
-
-let capitalize_first_letter (s : string) : string =
-  let s = string_to_chars s in
-  let s = match s with [] -> s | c :: s' -> uppercase_ascii c :: s' in
-  string_of_chars s
-
-let lowercase_first_letter (s : string) : string =
-  let s = string_to_chars s in
-  let s = match s with [] -> s | c :: s' -> lowercase_ascii c :: s' in
-  string_of_chars s
-
-(** Unit tests *)
-let _ =
-  assert (to_camel_case "hello_world" = "HelloWorld");
-  assert (to_snake_case "HelloWorld36Hello" = "hello_world36_hello");
-  assert (to_snake_case "HELLO" = "hello");
-  assert (to_snake_case "T1" = "t1");
-  assert (to_camel_case "list" = "List");
-  assert (to_snake_case "is_cons" = "is_cons")
+include Charon.StringUtils
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 01509dec..73e7f71d 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
       raise (Failure "Unexpected")
 
-    method! visit_CGVar _ id = subst.cg_subst id
+    method! visit_CgVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
@@ -71,7 +71,7 @@ let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> RErased);
     ty_subst = (fun vid -> TVar vid);
-    cg_subst = (fun id -> CGVar id);
+    cg_subst = (fun id -> CgVar id);
     tr_subst = (fun id -> Clause id);
     tr_self = Self;
   }
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7c5d28a7..c9820ba5 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -240,7 +240,7 @@ and value_aggregate =
   | VaSingleValue of typed_value  (** Regular case *)
   | VaArray of typed_value list
       (** This is used when introducing array aggregates *)
-  | VaCGValue of const_generic_var_id
+  | VaCgValue of const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
   | VaTraitConstValue of trait_ref * generic_args * string
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dad54e1..69ff4df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2475,7 +2475,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -2726,7 +2726,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index)
           const_generics
       in
       let trait_refs =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index cf23fd44..271d19ad 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -477,8 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     let types_map = builtin_types_map () in
     List.map
       (fun (def : Pure.type_decl) ->
-        let sname = name_to_simple_name def.llbc_name in
-        SimpleNameMap.find_opt sname types_map <> None)
+        match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None)
       defs
   in
 
@@ -545,9 +544,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
   (* Check if it is a builtin global - if yes, we ignore it because we
      map the definition to one in the standard library *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name global.name in
   let extract =
-    extract && SimpleNameMap.find_opt sname builtin_globals_map = None
+    extract
+    && match_name_find_opt ctx.trans_ctx global.name builtin_globals_map = None
   in
   if extract then
     (* We don't wrap global declaration groups between calls to functions
@@ -661,8 +660,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
     let funs_map = builtin_funs_map () in
     List.map
       (fun (trans : pure_fun_translation) ->
-        let sname = name_to_simple_name trans.fwd.f.llbc_name in
-        SimpleNameMap.find_opt sname funs_map <> None)
+        match_name_find_opt ctx.trans_ctx trans.fwd.f.llbc_name funs_map <> None)
       pure_ls
   in
 
@@ -755,8 +753,11 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
   let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
   (* Check if the trait declaration is builtin, in which case we ignore it *)
   let open ExtractBuiltin in
-  let sname = name_to_simple_name trait_decl.llbc_name in
-  if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then (
+  if
+    match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+      (builtin_trait_decls_map ())
+    = None
+  then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
     if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl;
     if extract_extra_info then
@@ -775,9 +776,11 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
   (* Check if the trait implementation is builtin *)
   let builtin_info =
     let open ExtractBuiltin in
-    let type_sname = name_to_simple_name trait_impl.llbc_name in
-    let trait_sname = name_to_simple_name trait_decl.llbc_name in
-    SimpleNamePairMap.find_opt (type_sname, trait_sname)
+    let trait_impl =
+      TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+    in
+    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+      trait_impl.impl_trait.decl_generics
       (builtin_trait_impls_map ())
   in
   match builtin_info with
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index a974cdee..f251e169 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -1,6 +1,7 @@
 (** Some utilities for the translation *)
 
 open Contexts
+open ExtractName
 
 (** The local logger *)
 let log = Logging.translate_log
@@ -29,3 +30,50 @@ let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env =
 
 let name_to_string (ctx : trans_ctx) =
   Print.Types.name_to_string (trans_ctx_to_fmt_env ctx)
+
+let match_name_find_opt (ctx : trans_ctx) (name : Types.name)
+    (m : 'a NameMatcherMap.t) : 'a option =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  NameMatcherMap.find_opt mctx name m
+
+let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name)
+    (generics : Types.generic_args) (m : 'a NameMatcherMap.t) : 'a option =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  NameMatcherMap.find_with_generics_opt mctx name generics m
+
+let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  name_to_simple_name mctx n
+
+let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name)
+    (p : Types.generic_params) (g : Types.generic_args) : string list =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  name_with_generics_to_simple_name mctx n p g
diff --git a/compiler/dune b/compiler/dune
index 43ce86c8..39ad6260 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -10,7 +10,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix unionFind ocamlgraph)
+ (libraries charon core_unix unionFind ocamlgraph str)
  (modules
   AssociatedTypes
   Assumed
@@ -24,6 +24,7 @@
   Extract
   ExtractBase
   ExtractBuiltin
+  ExtractName
   ExtractTypes
   FunsAnalysis
   Identifiers