Merge pull request #88 from AeneasVerif/son/clashes

Improve the name generation for code extraction

12 files changed, 245 insertions, 115 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index af0e62d1..65aa7555 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -366,3 +366,6 @@ let backend_has_tuple_projectors () =
 (** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
     we use better projector syntax? *)
 let use_nested_tuple_projectors = ref false
+
+(** Generate name patterns for the external definitions we encounter *)
+let extract_external_name_patterns = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 794a1bfa..46f6a1ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -19,7 +19,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
      only use their type for the fields of the records we generate for the trait
      declarations *)
   match def.f.kind with
-  | TraitMethodDecl _ -> ctx
+  | TraitItemDecl _ -> ctx
   | _ -> (
       (* Check if the function is builtin *)
       let builtin =
@@ -48,6 +48,9 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
           ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
       | None ->
           (* Not builtin *)
+          (* If this is a trait method implementation, we prefix the name with the
+             name of the trait implementation. We need to do so because there
+             can be clashes otherwise. *)
           (* Register the decrease clauses, if necessary *)
           let register_decreases ctx def =
             if has_decreases_clause def then
@@ -1105,7 +1108,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitMethodProvided (decl_id, _) ->
+    | TraitItemProvided (decl_id, _) ->
         let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
         let ctx, _ = ctx_add_trait_self_clause ctx in
         let ctx = { ctx with is_provided_method = true } in
@@ -1204,9 +1207,14 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
-    def.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not def.is_local then
+       Some def.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+     name def.meta.span);
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1267,9 +1275,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1322,9 +1330,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
   F.pp_print_string fmt "syntax \"";
@@ -1364,7 +1372,12 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     in
     [ comment_pre ^ loop_comment ]
   in
-  extract_comment_with_span fmt comment def.meta.span
+  let name =
+    if !Config.extract_external_name_patterns && not def.is_local then
+      Some def.llbc_name
+    else None
+  in
+  extract_comment_with_span ctx fmt comment name def.meta.span
 
 (** Extract a function declaration.
 
@@ -1813,9 +1826,14 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  let name =
+    if !Config.extract_external_name_patterns && not global.is_local then
+      Some global.name
+    else None
+  in
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx global.name ^ "]" ]
-    global.meta.span;
+    name global.meta.span;
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
@@ -2207,9 +2225,14 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
-    decl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not decl.is_local then
+       Some decl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+     name decl.meta.span);
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
      one line and indents are correct.
@@ -2490,9 +2513,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
-    impl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not impl.is_local then
+       Some impl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+     name impl.meta.span);
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 591e8aab..5e97cd21 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1266,13 +1266,11 @@ let name_last_elem_as_ident (n : llbc_name) : string =
     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 =
+let ctx_prepare_name (ctx : extraction_ctx) (name : llbc_name) : llbc_name =
   (* 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
+      if crate = ctx.crate.name then name else id :: name
   | _ ->
       raise
         (Failure
@@ -1280,6 +1278,13 @@ let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
            ^ TranslateCore.name_to_string ctx.trans_ctx name))
 
 (** Helper *)
+let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
+    string list =
+  (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+  let name = ctx_prepare_name ctx name in
+  name_to_simple_name ctx.trans_ctx name
+
+(** Helper *)
 let ctx_compute_simple_type_name = ctx_compute_simple_name
 
 (** Helper *)
@@ -1369,10 +1374,11 @@ let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) :
 
 (** 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
+  match !Config.backend with
+  | Coq | FStar | HOL4 ->
+      let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
+      String.concat "_" parts
+  | Lean -> flatten_name (ctx_compute_simple_name ctx 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.
@@ -1426,8 +1432,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
   let name =
     let params = trait_impl.llbc_generics in
     let args = trait_impl.llbc_impl_trait.decl_generics in
-    trait_name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name
-      params args
+    let name = ctx_prepare_name ctx trait_decl.llbc_name in
+    trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
   in
   let name = flatten_name name in
   match !backend with
@@ -1506,6 +1512,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
     if !Config.record_fields_short_names then clause
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
   in
+  let clause = clause ^ "Inst" in
   match !backend with
   | FStar -> StringUtils.lowercase_first_letter clause
   | Coq | HOL4 | Lean -> clause
@@ -1715,6 +1722,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
     ctx_compute_trait_clause_name ctx current_def_name params
       params.trait_clauses clause_id
   in
+  let clause = clause ^ "Inst" in
   match !backend with
   | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
   | Lean -> clause
@@ -1882,8 +1890,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       (* Not the case: "standard" registration *)
       let name = ctx_compute_global_name ctx def.name in
       let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
-      let ctx = ctx_add decl (name ^ "_c") ctx in
-      let ctx = ctx_add body (name ^ "_body") ctx in
+      (* If this is a provided constant (i.e., the default value for a constant
+         in a trait declaration) we add a suffix. Otherwise there is a clash
+         between the name for the default constant and the name for the field
+         in the trait declaration *)
+      let suffix =
+        match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
+      in
+      let ctx = ctx_add decl (name ^ suffix) ctx in
+      let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 88de31fe..401d0137 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -253,35 +253,77 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       (Some [ true; false ]);
     mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
       (Some [ true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index" None
+    mk_fun
+      "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
+       @I>}::index"
+      (Some "alloc.vec.Vec.index")
       (Some [ true; true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut" None
+    mk_fun
+      "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
+       @I>}::index_mut"
+      (Some "alloc.vec.Vec.index_mut")
       (Some [ true; true; false ]);
-    mk_fun "alloc::boxed::{Box<@T>}::deref" None (Some [ true; false ]);
-    mk_fun "alloc::boxed::{Box<@T>}::deref_mut" None (Some [ true; false ]);
-    mk_fun "core::slice::index::{[@T]}::index" None None;
-    mk_fun "core::slice::index::{[@T]}::index_mut" None None;
-    mk_fun "core::array::{[@T; @C]}::index" None None;
-    mk_fun "core::array::{[@T; @C]}::index_mut" None None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get"
+    mk_fun "alloc::boxed::{core::ops::deref::Deref<Box<@T>>}::deref"
+      (Some "alloc.boxed.Box.deref")
+      (Some [ true; false ]);
+    mk_fun "alloc::boxed::{core::ops::deref::DerefMut<Box<@T>>}::deref_mut"
+      (Some "alloc.boxed.Box.deref_mut")
+      (Some [ true; false ]);
+    mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I>}::index"
+      (Some "core.slice.index.Slice.index") None;
+    mk_fun
+      "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut"
+      (Some "core.slice.index.Slice.index_mut") None;
+    mk_fun "core::array::{core::ops::index::Index<[@T; @N], @I>}::index"
+      (Some "core.array.Array.index") None;
+    mk_fun "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut"
+      (Some "core.array.Array.index_mut") None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get"
       (Some "core::slice::index::RangeUsize::get") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_mut"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_mut"
       (Some "core::slice::index::RangeUsize::get_mut") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::index"
       (Some "core::slice::index::RangeUsize::index") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index_mut"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::index_mut"
       (Some "core::slice::index::RangeUsize::index_mut") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_unchecked"
       (Some "core::slice::index::RangeUsize::get_unchecked") None;
     mk_fun
-      "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked_mut"
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_unchecked_mut"
       (Some "core::slice::index::RangeUsize::get_unchecked_mut") None;
-    mk_fun "core::slice::index::{usize}::get" None None;
-    mk_fun "core::slice::index::{usize}::get_mut" None None;
-    mk_fun "core::slice::index::{usize}::get_unchecked" None None;
-    mk_fun "core::slice::index::{usize}::get_unchecked_mut" None None;
-    mk_fun "core::slice::index::{usize}::index" None None;
-    mk_fun "core::slice::index::{usize}::index_mut" None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::get"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_mut"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_unchecked"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_unchecked_mut"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::index"
+      (Some "core_slice_index_Slice_index") None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::index_mut"
+      (Some "core_slice_index_Slice_index_mut") None;
   ]
 
 let mk_builtin_funs_map () =
@@ -351,9 +393,10 @@ let builtin_fun_effects =
     [
       (* 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";
+      "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
+       @I>}::index";
+      "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
+       @I>}::index_mut";
     ]
   in
   let no_state_funs =
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 4c1ffb46..80ed2ca3 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -31,69 +31,82 @@ end
     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 pattern_to_extract_name (name : pattern) : string list =
   let c = { tgt = TkName } in
-  let is_var (g : generic_arg) : bool =
-    match g with
-    | GExpr (EVar _) -> true
-    | GRegion (RVar _) -> true
-    | _ -> false
+  let all_vars =
+    let check (g : generic_arg) : bool =
+      match g with GExpr (EVar _) | GRegion (RVar _) -> true | _ -> false
+    in
+    List.for_all check
   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 -> (
+
+  (* This is a bit of a hack: we want to simplify the occurrences of
+     tuples of two variables, arrays with only variables, slices with
+     only variables, etc.
+     We explore the pattern and replace such occurrences with a specific name.
+  *)
+  let replace_option_name (id : pattern) =
+    match id with
+    | [ PIdent ("core", []); PIdent ("option", []); PIdent ("Option", g) ] ->
+        (* Option *)
+        [ PIdent ("Option", g) ]
+    | _ -> id
+  in
+  let visitor =
+    object
+      inherit [_] map_pattern as super
+
+      method! visit_PIdent _ s g =
+        if all_vars g then super#visit_PIdent () s []
+        else super#visit_PIdent () s g
+
+      method! visit_EComp _ id =
+        (* Simplify if this is [Option] *)
+        super#visit_EComp () (replace_option_name id)
+
+      method! visit_PImpl _ ty =
         match ty with
         | EComp id -> (
-            (* Retrieve the last ident *)
+            (* Only keep 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
+            | PIdent (_, _) -> super#visit_PImpl () (EComp [ 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 _ | EArrow _ | ERawPtr _ ->
-            (* We simply convert the pattern to a string. This is not very
-               satisfying but we should rarely get there. *)
-            expr_to_string c ty)
-  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
+        | _ -> super#visit_PImpl () ty
+
+      method! visit_EPrimAdt _ adt g =
+        if all_vars g then
+          match adt with
+          | TTuple ->
+              let l = List.length g in
+              if l = 2 then EComp [ PIdent ("Pair", []) ]
+              else super#visit_EPrimAdt () adt g
+          | TArray -> EComp [ PIdent ("Array", []) ]
+          | TSlice -> EComp [ PIdent ("Slice", []) ]
+        else if adt = TTuple && List.length g = 2 then
+          super#visit_EComp () [ PIdent ("Pair", g) ]
+        else super#visit_EPrimAdt () adt g
+    end
   in
-  pattern_to_string name
+  let name = visitor#visit_pattern () name in
+  List.map (pattern_elem_to_string c) name
 
-let pattern_to_type_extract_name = pattern_to_extract_name false
-let pattern_to_fun_extract_name = pattern_to_extract_name false
-let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
+let pattern_to_type_extract_name = pattern_to_extract_name
+let pattern_to_fun_extract_name = pattern_to_extract_name
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name
 
 (* 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) (is_trait_impl : bool) (n : Types.name) :
-    string list =
+let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
   let c : to_pat_config =
     { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
   in
-  pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n)
+  pattern_to_extract_name (name_to_pattern ctx c n)
 
 (** If the [prefix] is Some, we attempt to remove the common prefix
     between [prefix] and [name] from [name] *)
-let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
+let name_with_generics_to_simple_name (ctx : ctx)
     ?(prefix : Types.name option = None) (name : Types.name)
     (p : Types.generic_params) (g : Types.generic_args) : string list =
   let c : to_pat_config =
@@ -111,4 +124,4 @@ let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
         let _, _, name = pattern_common_prefix { equiv = true } prefix name in
         name
   in
-  pattern_to_extract_name is_trait_impl name
+  pattern_to_extract_name name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 05b71b9f..9d4131d2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1116,8 +1116,8 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   F.pp_print_string fmt rd;
   F.pp_close_box fmt ()
 
-let extract_comment_with_span (fmt : F.formatter) (sl : string list)
-    (span : Meta.span) : unit =
+let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
+    (sl : string list) (name : Types.name option) (span : Meta.span) : unit =
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -1126,7 +1126,13 @@ let extract_comment_with_span (fmt : F.formatter) (sl : string list)
     "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-"
     ^ loc_to_string span.end_loc
   in
-  extract_comment fmt (sl @ [ span ])
+  let name =
+    match name with
+    | None -> []
+    | Some name ->
+        [ "Name pattern: " ^ name_to_pattern_string ctx.trans_ctx name ]
+  in
+  extract_comment fmt (sl @ [ span ] @ name)
 
 let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
@@ -1359,9 +1365,14 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if !backend <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
-    def.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not def.is_local then
+       Some def.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+     name def.meta.span);
   F.pp_print_break fmt 0 0;
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fd3e334b..ccae4588 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -68,12 +68,12 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
-    (regions_hierarchy : region_var_groups) (kind : fun_kind) :
+    (regions_hierarchy : region_var_groups) (kind : item_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
-    | RegularKind | TraitMethodImpl _ -> UnknownTrait __FUNCTION__
-    | TraitMethodDecl _ | TraitMethodProvided _ -> Self
+    | RegularKind | TraitItemImpl _ -> UnknownTrait __FUNCTION__
+    | TraitItemDecl _ | TraitItemProvided _ -> Self
   in
   let generics =
     let { regions; types; const_generics; trait_clauses } = sg.generics in
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index d3fac032..1053c9ab 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -44,7 +44,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     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)
+    && (match d.kind with TraitItemDecl _ -> false | _ -> true)
     && ((not filter_assumed)
        || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
           && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 3f5e62ad..e703f1a0 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -118,6 +118,9 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
          (0, 1).1)." );
+      ( "-ext-name-pats",
+        Arg.Set extract_external_name_patterns,
+        " Generate name patterns for the external definitions we find." );
     ]
   in
 
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index dd7a4acf..33c23cc3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1063,13 +1063,13 @@ type fun_body = {
 }
 [@@deriving show]
 
-type fun_kind = A.fun_kind [@@deriving show]
+type item_kind = A.item_kind [@@deriving show]
 
 type fun_decl = {
   def_id : FunDeclId.id;
   is_local : bool;
   meta : meta;
-  kind : fun_kind;
+  kind : item_kind;
   num_loops : int;
       (** The number of loops in the parent forward function (basically the number
           of loops appearing in the original Rust functions, unless some loops are
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c12de045..48a3685b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -730,7 +730,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
         match pure_fun.f.Pure.kind with
-        | TraitMethodDecl _ -> ()
+        | TraitItemDecl _ -> ()
         | _ ->
             (* Translate *)
             export_functions_group [ pure_fun ])
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 05877b5a..3e4c7375 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -60,8 +60,7 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
       trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
-  let is_trait_impl = false in
-  name_to_simple_name mctx is_trait_impl n
+  name_to_simple_name mctx n
 
 let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
     ?(prefix : Types.name option = None) (n : Types.name)
@@ -75,5 +74,20 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
       trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
-  let is_trait_impl = true in
-  name_with_generics_to_simple_name mctx is_trait_impl ~prefix n p g
+  name_with_generics_to_simple_name mctx ~prefix n p g
+
+let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat = Charon.NameMatcher.name_to_pattern mctx c n in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat