Update the name generation and add CLI to print external pat names

7 files changed, 106 insertions, 48 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..b9c6b1b0 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -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
@@ -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..e0614af1 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 *)
@@ -1426,8 +1431,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
@@ -1715,6 +1720,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
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 4c1ffb46..b53f4cdd 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -31,8 +31,7 @@ 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
@@ -68,32 +67,26 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
             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
+    match n with [] -> [] | e :: n -> elem_to_string e :: pattern_to_string n
   in
   pattern_to_string 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 +104,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/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/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