Improve the name generation for code extraction

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

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

compiler/ExtractBase.ml

@@ -1266,19 +1266,24 @@ 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
            ("Unexpected name shape: "
            ^ 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
 
@@ -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 =

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 =