From c19b2cd5d2ee8df9897187bab0b96947ad666ae7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 1 Mar 2023 23:54:54 +0100
Subject: [PATCH] Extraction to OCaml: use correct key to manage collision of
 record field names.

Fixes #3846
Fixes #14843
Fixes #16677
Fixes #12813

When dealing with collisions by means of encapsulation in a Coq_XX
module, a field name should be bound to the name of the corresponding
inductive type declaration.

We use Table.repr_of_r to do that, but early enough to have the
relevant information on how to bind a field to the name of the
inductive that declares it. (In particular, we cannot rely on the
global tables in structures.ml because they are not valid when inside
a functor, see #17321.)

Note that Haskell and Scheme do not use records and it is ok on their
side.
---
 plugins/extraction/common.ml  |  7 +++++--
 plugins/extraction/common.mli |  1 +
 plugins/extraction/ocaml.ml   | 14 +++++++++++---
 plugins/extraction/table.ml   | 14 ++++++++------
 plugins/extraction/table.mli  |  2 +-
 test-suite/bugs/bug_14843.v   | 21 +++++++++++++++++++++
 6 files changed, 47 insertions(+), 12 deletions(-)
 create mode 100644 test-suite/bugs/bug_14843.v

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 26c51436caa4..d810cf78a1d5 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -587,11 +587,11 @@ let pp_haskell_gen k mp rls = match rls with
 
 (* Main name printing function for a reference *)
 
-let pp_global k r =
+let pp_global_with_key k key r =
   let ls = ref_renaming (k,r) in
   assert (List.length ls > 1);
   let s = List.hd ls in
-  let mp,l = repr_of_r r in
+  let mp,l = KerName.repr key in
   if ModPath.equal mp (top_visible_mp ()) then
     (* simplest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
@@ -604,6 +604,9 @@ let pp_global k r =
       | Haskell -> if modular () then pp_haskell_gen k mp rls else s
       | Ocaml -> pp_ocaml_gen k mp rls (Some l)
 
+let pp_global k r =
+  pp_global_with_key k (repr_of_r r) r
+
 (* Main name printing function for declaring a reference *)
 
 let pp_global_name k r =
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index a482cfc03d14..fd30132b5b61 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -54,6 +54,7 @@ val opened_libraries : unit -> ModPath.t list
 
 type kind = Term | Type | Cons | Mod
 
+val pp_global_with_key : kind -> KerName.t -> GlobRef.t -> string
 val pp_global : kind -> GlobRef.t -> string
 val pp_global_name : kind -> GlobRef.t -> string
 val pp_module : ModPath.t -> string
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 83e15dfebd1e..2b94edc907b4 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -94,8 +94,12 @@ let sig_preamble _ comment used_modules usf =
    below should not be altered since they force evaluation order.
 *)
 
-let str_global k r =
-  if is_inline_custom r then find_custom r else Common.pp_global k r
+let str_global_with_key k key r =
+  if is_inline_custom r then find_custom r else Common.pp_global_with_key k key r
+
+let str_global k r = str_global_with_key k (repr_of_r r) r
+
+let pp_global_with_key k key r = str (str_global_with_key k key r)
 
 let pp_global k r = str (str_global k r)
 
@@ -148,8 +152,12 @@ let get_ind = let open GlobRef in function
   | ConstructRef (ind,_) -> IndRef ind
   | _ -> assert false
 
+let kn_of_ind = let open GlobRef in function
+  | IndRef (kn,_) -> MutInd.user kn
+  | _ -> assert false
+
 let pp_one_field r i = function
-  | Some r -> pp_global Term r
+  | Some r' -> pp_global_with_key Term (kn_of_ind (get_ind r)) r'
   | None -> pp_global Type (get_ind r) ++ str "__" ++ int i
 
 let pp_field r fields i = pp_one_field r i (List.nth fields i)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c0639a264ccc..0d17b0cbec33 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -35,17 +35,19 @@ let occur_kn_in_ref kn = let open GlobRef in function
   | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn'
   | ConstRef _ | VarRef _ -> false
 
+(* Return the "canonical" name used for declaring a name *)
+
 let repr_of_r = let open GlobRef in function
-  | ConstRef kn -> KerName.repr (Constant.user kn)
+  | ConstRef kn -> Constant.user kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> KerName.repr (MutInd.user kn)
-  | VarRef v -> KerName.repr (Lib.make_kn v)
+  | ConstructRef ((kn,_),_) -> MutInd.user kn
+  | VarRef v -> Lib.make_kn v
 
 let modpath_of_r r =
-  let mp,_ = repr_of_r r in mp
+  KerName.modpath (repr_of_r r)
 
 let label_of_r r =
-  let _,l = repr_of_r r in l
+  KerName.label (repr_of_r r)
 
 let rec base_mp = function
   | MPdot (mp,l) -> base_mp mp
@@ -94,7 +96,7 @@ let rec parse_labels2 ll mp1 = function
 
 let labels_of_ref r =
   let mp_top = Lib.current_mp () in
-  let mp,l = repr_of_r r in
+  let mp,l = KerName.repr (repr_of_r r) in
   parse_labels2 [l] mp_top mp
 
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index d95a19cfdef4..c1fa7accb97e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
 
 val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * Label.t
+val repr_of_r : GlobRef.t -> KerName.t
 val modpath_of_r : GlobRef.t -> ModPath.t
 val label_of_r : GlobRef.t -> Label.t
 val base_mp : ModPath.t -> ModPath.t
diff --git a/test-suite/bugs/bug_14843.v b/test-suite/bugs/bug_14843.v
new file mode 100644
index 000000000000..29180f604c39
--- /dev/null
+++ b/test-suite/bugs/bug_14843.v
@@ -0,0 +1,21 @@
+(* f1 was renamed into Coq__1.f1 but Coq__1 was not defined *)
+(* similar to #12813, #16677 *)
+
+Record r : Type := mk { f1 : unit -> unit; f2: unit -> unit }.
+Set Primitive Projections.
+Record r' : Type := mk' { f1' : unit -> unit; f2': unit -> unit }.
+Unset Primitive Projections.
+
+Module M.
+Definition f1 (ti:unit) : unit := tt.
+Definition f2 (ti:unit) : unit := tt.
+Definition cf := mk f1 f2.
+
+Definition f1' (ti:unit) : unit := tt.
+Definition f2' (ti:unit) : unit := tt.
+Definition cf' := mk' f1' f2'.
+End M.
+
+Require Import Coq.extraction.Extraction.
+Recursive Extraction M.cf M.cf'.
+Extraction TestCompile M.cf M.cf'.