Fix issues with name collisions

2 files changed, 39 insertions, 13 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 864d513f..60455cd9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -655,6 +655,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | _ ->
         raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
   in
+  let flatten_name (name : string list) : string =
+    match !backend with
+    | FStar | Coq | HOL4 -> String.concat "_" name
+    | Lean -> String.concat "." name
+  in
   let get_type_name = get_name in
   let type_name_to_camel_case name =
     let name = get_type_name name in
@@ -708,9 +713,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let get_fun_name fname =
     let fname = get_name fname in
     (* TODO: don't convert to snake case for Coq, HOL4, F* *)
-    match !backend with
-    | FStar | Coq | HOL4 -> String.concat "_" (List.map to_snake_case fname)
-    | Lean -> String.concat "." fname
+    flatten_name fname
   in
   let global_name (name : global_name) : string =
     (* Converting to snake case also lowercases the letters (in Rust, global
@@ -732,8 +735,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     type_name_to_snake_case trait_decl.name
   in
 
-  let trait_impl_name (trait_impl : trait_impl) : string =
-    get_fun_name trait_impl.name
+  let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
+      string =
+    (* TODO: provisional: we concatenate the trait impl name (which is its type)
+       with the trait decl name *)
+    let inst_keyword =
+      match !backend with
+      | HOL4 | FStar | Coq -> "_instance"
+      | Lean -> "Instance"
+    in
+    flatten_name
+      (get_type_name trait_impl.name
+      @ [ trait_decl_name trait_decl ^ inst_keyword ])
   in
 
   let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause)
@@ -4017,8 +4030,9 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
     (trait_impl : trait_impl) : extraction_ctx =
   (* For now we do not support overriding provided methods *)
   assert (trait_impl.provided_methods = []);
-  (* Everything is actually taken care of by {!extract_trait_decl_register_names} *)
-  ctx
+  (* Everything is taken care of by {!extract_trait_decl_register_names} *but*
+     the name of the implementation itself *)
+  ctx_add_trait_impl trait_impl ctx
 
 (** Small helper.
 
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 612cf359..1996d38f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -245,7 +245,7 @@ type formatter = {
           - loop identifier, if this is for a loop
        *)
   trait_decl_name : trait_decl -> string;
-  trait_impl_name : trait_impl -> string;
+  trait_impl_name : trait_decl -> trait_impl -> string;
   trait_parent_clause_name : trait_decl -> trait_clause -> string;
   trait_const_name : trait_decl -> string -> string;
   trait_type_name : trait_decl -> string -> string;
@@ -523,7 +523,8 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   log#serror err;
-  raise (Failure err)
+  (* If we fail hard on errors, raise an exception *)
+  if !Config.extract_fail_hard then raise (Failure err)
 
 let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
   StringMap.find_opt name nm.name_to_id
@@ -534,15 +535,21 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      if !Config.extract_fail_hard then
-        report_name_collision id_to_string clash id name
+      report_name_collision id_to_string clash id name
 
 let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
     (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
   (* Sanity check *)
-  assert (not (StringSet.mem name nm.names_set));
+  if StringSet.mem name nm.names_set then (
+    let err =
+      "Error when registering the name for id: " ^ id_to_string id
+      ^ ":\nThe chosen name is already in the names set: " ^ name
+    in
+    log#serror err;
+    (* If we fail hard on errors, raise an exception *)
+    if !Config.extract_fail_hard then raise (Failure err));
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
   let name_to_id = StringMap.add name id nm.name_to_id in
@@ -1284,8 +1291,13 @@ let ctx_add_trait_decl (d : trait_decl) (ctx : extraction_ctx) : extraction_ctx
 
 let ctx_add_trait_impl (d : trait_impl) (ctx : extraction_ctx) : extraction_ctx
     =
+  (* We need to lookup the trait decl that is implemented by the trait impl *)
+  let decl =
+    Pure.TraitDeclId.Map.find d.impl_trait.trait_decl_id ctx.trans_trait_decls
+  in
+  (* Compute the name *)
   let is_opaque = false in
-  let name = ctx.fmt.trait_impl_name d in
+  let name = ctx.fmt.trait_impl_name decl d in
   ctx_add is_opaque (TraitImplId d.def_id) name ctx
 
 let ctx_add_trait_const (d : trait_decl) (item : string) (ctx : extraction_ctx)