Use the name matcher implemented in Charon

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" }

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) *)

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