Extraction: use correct key to manage collision of record field names.

Fixes coq#14843
Fixes coq#16677
Fixes coq#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 coq#17321.)

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 =

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

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)

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
 
 

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

test-suite/bugs/bug_14843.v

@@ -0,0 +1,47 @@
+(* 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'.
+
+(* The same in a functor *)
+
+Module Type Nop. End Nop.
+Module Empty. End Empty.
+Module P (N : Nop).
+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 N.
+  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 N.
+End P.
+Module P' := P Empty.
+Require Import Coq.extraction.Extraction.
+Extraction Language OCaml.
+Recursive Extraction P'.N.cf P'.N.cf'.
+Extraction TestCompile P'.N.cf P'.N.cf'.