Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

1 files changed, 195 insertions, 273 deletions

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index a54ab604..30ec7c19 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -4,32 +4,11 @@
     TODO: there misses trait **implementations**
  *)
 
-open Names
 open Config
+open Charon.NameMatcher (* TODO: include? *)
+include ExtractName (* TODO: only open? *)
 
-type simple_name = string list [@@deriving show, ord]
-
-let name_to_simple_name (s : name) : simple_name =
-  (* We simply ignore the disambiguators *)
-  List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) 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)
+let log = Logging.builtin_log
 
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
@@ -44,6 +23,18 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
   in
   g
 
+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" ])
+
 (** Switch between two values depending on the target backend.
 
     We often compute the same value (typically: a name) if the target
@@ -55,36 +46,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]
@@ -104,7 +95,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.
@@ -136,12 +127,9 @@ 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
-    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
@@ -159,17 +147,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
@@ -178,7 +166,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"
@@ -211,7 +199,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
@@ -228,21 +216,24 @@ 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 =
-    let extract_name =
-      match extract_name with None -> name | Some name -> name
+      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 basename =
-      match !backend with
-      | FStar | Coq | HOL4 -> String.concat "_" extract_name
-      | Lean -> String.concat "." extract_name
+    let extract_name =
+      match extract_name with
+      | None -> pattern_to_fun_extract_name rust_name
+      | Some name -> split_on_separator 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
@@ -250,106 +241,73 @@ 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 "core::slice::{[@T]}::len"
+      (Some (backend_choice "slice::len" "Slice::len"))
+      None true false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"
+      (Some "alloc::vec::Vec::new") None false false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None
       (Some [ true; false ])
       true true;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "insert" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None
       (Some [ true; false ])
       true true;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "len" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
       (Some [ true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "index" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index" None
       (Some [ true; true; false ])
       true false;
-    mk_fun
-      [ "alloc"; "vec"; "Vec"; "index_mut" ]
-      None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::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::{[@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::{core::ops::range::Range<usize>}::get"
+      (Some "core::slice::index::RangeUsize::get") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_mut"
+      (Some "core::slice::index::RangeUsize::get_mut") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index"
+      (Some "core::slice::index::RangeUsize::index") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index_mut"
+      (Some "core::slice::index::RangeUsize::index_mut") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked"
+      (Some "core::slice::index::RangeUsize::get_unchecked") None false 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;
+      "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked_mut"
+      (Some "core::slice::index::RangeUsize::get_unchecked_mut") 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
-    (List.map
-       (fun (name, filter, info) -> (name, (filter, info)))
-       (builtin_funs ()))
+  let m =
+    NameMatcherMap.of_list
+      (List.map
+         (fun (name, filter, info) -> (name, (filter, info)))
+         (builtin_funs ()))
+  in
+  log#ldebug
+    (lazy ("builtin_funs_map:\n" ^ NameMatcherMap.to_string (fun _ -> "...") m));
+  m
 
 let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
@@ -378,17 +336,21 @@ 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";
+      (* TODO: redundancy with the funs information above *)
+      "core::slice::{[@T]}::len";
+      "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
       "core::mem::replace";
       "core::mem::take";
     ]
@@ -401,11 +363,11 @@ let builtin_fun_effects =
   in
   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";
+      (* TODO: redundancy with the funs information above *)
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut_back";
     ]
   in
   let no_state_funs =
@@ -414,11 +376,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;
@@ -434,25 +396,29 @@ 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 -> (
-          match !backend with
-          | Coq | FStar | HOL4 -> String.concat "_" rust_name
-          | Lean -> String.concat "." rust_name)
+      | None ->
+          let rust_name = pattern_to_fun_extract_name rust_name in
+          flatten_name rust_name
     in
     let constructor = mk_struct_constructor extract_name in
     let consts = [] in
     let types =
       let mk_type item_name =
         let type_name =
+          if !record_fields_short_names then item_name
+          else extract_name ^ "_" ^ item_name
+        in
+        let type_name =
           match !backend with
-          | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name
-          | Lean -> item_name
+          | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
+          | Lean -> type_name
         in
         let clauses = [] in
         (item_name, (type_name, clauses))
@@ -463,9 +429,8 @@ let builtin_trait_decls_info () =
       let mk_method (item_name, with_back) =
         (* TODO: factor out with builtin_funs_info *)
         let basename =
-          match !backend with
-          | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name
-          | Lean -> item_name
+          if !record_fields_short_names then item_name
+          else extract_name ^ "_" ^ item_name
         in
         let back_no_suffix = false in
         let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
@@ -480,7 +445,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;
@@ -493,35 +457,25 @@ 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" ]
-      ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ]
+    mk_trait "core::ops::deref::DerefMut" ~parent_clauses:[ "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" ]
-      ~parent_clauses:[ backend_choice "index_inst" "indexInst" ]
+    mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ "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" ]
-      ~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ]
+    mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ "sealedInst" ]
       ~types:[ "Output" ]
       ~methods:
         [
@@ -536,113 +490,81 @@ 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) ?(extract_name : string option = None)
+      ?(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 sep = backend_choice "_" "." in
-      let type_name =
-        match extract_type_name with
-        | Some type_name -> type_name
-        | None -> type_name
+      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 type_name ^ sep ^ trait_name
+      flatten_name 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" ] ();
+    fmt "core::ops::deref::Deref<Box<@T>>"
+      ~extract_name:(Some "alloc::boxed::Box::coreopsDerefInst") ();
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
-    fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] ();
+    fmt "core::ops::deref::DerefMut<Box<@T>>"
+      ~extract_name:(Some "alloc::boxed::Box::coreopsDerefMutInst") ();
     (* 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>"
+      ~extract_name:(Some "core::ops::index::IndexSliceTIInst") ();
     (* 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>"
+      ~extract_name:(Some "core::ops::index::IndexMutSliceTIInst") ();
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
     fmt
-      [ "core"; "slice"; "index"; "private_slice_index"; "Range" ]
-      [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
-      ();
+      "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
+      ~extract_name:
+        (Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") ();
     (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
-    fmt
-      [ "core"; "slice"; "index"; "Range" ]
-      [ "core"; "slice"; "index"; "SliceIndex" ]
+    fmt "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T]>"
+      ~extract_name:(Some "core::slice::index::SliceIndexRangeUsizeSliceTInst")
       ();
     (* 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>"
+      ~extract_name:(Some "core::ops::index::IndexArrayInst") ();
     (* 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>"
+      ~extract_name:(Some "core::ops::index::IndexMutArrayIInst") ();
     (* 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>"
+      ~extract_name:
+        (Some "core::slice::index::private_slice_index::SealedUsizeInst") ();
     (* 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]>"
+      ~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceTInst") ();
+    (* core::ops::index::Index<alloc::vec::Vec<T>, T> *)
+    fmt "core::ops::index::Index<alloc::vec::Vec<@T, @A>, @T>"
+      ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexInst")
       ~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, @A>, @T>"
+      ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst")
       ~filter:(Some [ true; true; false ])
       ();
   ]
 
 let mk_builtin_trait_impls_map () =
-  SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+  let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
+  log#ldebug
+    (lazy
+      ("builtin_trait_impls_map:\n"
+      ^ NameMatcherMap.to_string (fun _ -> "...") m));
+  m
 
 let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map