Extraction: At declaration point of a global, use its declaring name.

If we need to print the name of an inlined constant (as in "let name =",
"val name :" or "type name ="), we need its name without inlining nor
qualification.

In particular, we introduce a function pp_global_name to make it
clearer that printing a name at declaration point of a global is only
about printing the basename (formerly, Common.pp_global was correctly
printing the basename without qualification thanks to the
"top_visible_mp ()" test, but OCaml.pp_global was wrongly inlining).

3 files changed, 18 insertions, 8 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4a41f4c890..d215a7673d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -604,6 +604,13 @@ 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)
 
+(* Main name printing function for declaring a reference *)
+
+let pp_global_name k r =
+  let ls = ref_renaming (k,r) in
+  assert (List.length ls > 1);
+  List.hd ls
+
 (* The next function is used only in Ocaml extraction...*)
 
 let pp_module mp =
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0bd9efd255..a482cfc03d 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -55,6 +55,7 @@ val opened_libraries : unit -> ModPath.t list
 type kind = Term | Type | Cons | Mod
 
 val pp_global : kind -> GlobRef.t -> string
+val pp_global_name : kind -> GlobRef.t -> string
 val pp_module : ModPath.t -> string
 
 val top_visible_mp : unit -> ModPath.t
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 088405da5d..6425c3111e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -99,6 +99,8 @@ let str_global k r =
 
 let pp_global k r = str (str_global k r)
 
+let pp_global_name k r = str (Common.pp_global k r)
+
 let pp_modname mp = str (Common.pp_module mp)
 
 (* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
@@ -451,7 +453,7 @@ let pp_val e typ =
 
 let pp_Dfix (rv,c,t) =
   let names = Array.map
-    (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+    (fun r -> if is_inline_custom r then mt () else pp_global_name Term r) rv
   in
   let rec pp init i =
     if i >= Array.length rv then mt ()
@@ -504,7 +506,7 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet =
-  let name = pp_global Type (GlobRef.IndRef (kn,0)) in
+  let name = pp_global_name Type (GlobRef.IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
          pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -513,7 +515,7 @@ let pp_singleton kn packet =
 
 let pp_record kn fields ip_equiv packet =
   let ind = GlobRef.IndRef (kn,0) in
-  let name = pp_global Type ind in
+  let name = pp_global_name Type ind in
   let fieldnames = pp_fields ind fields in
   let l = List.combine fieldnames packet.ip_types.(0) in
   let pl = rename_tvars keywords packet.ip_vars in
@@ -535,7 +537,7 @@ let pp_ind co kn ind =
   let nextkwd = fnl () ++ str "and " in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
-                  pp_global Type (GlobRef.IndRef (kn,i)))
+                  pp_global_name Type (GlobRef.IndRef (kn,i)))
       ind.ind_packets
   in
   let cnames =
@@ -575,7 +577,7 @@ let pp_decl = function
     | Dterm (r,_,_) when is_inline_custom r -> mt ()
     | Dind (kn,i) -> pp_mind kn i
     | Dtype (r, l, t) ->
-        let name = pp_global Type r in
+        let name = pp_global_name Type r in
         let l = rename_tvars keywords l in
         let ids, def =
           try
@@ -592,7 +594,7 @@ let pp_decl = function
           if is_custom r then str (" = " ^ find_custom r)
           else pp_function (empty_env ()) a
         in
-        let name = pp_global Term r in
+        let name = pp_global_name Term r in
         pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
     | Dfix (rv,defs,typs) ->
         pp_Dfix (rv,defs,typs)
@@ -603,10 +605,10 @@ let pp_spec = function
   | Sind (kn,i) -> pp_mind kn i
   | Sval (r,t) ->
       let def = pp_type false [] t in
-      let name = pp_global Term r in
+      let name = pp_global_name Term r in
       hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
   | Stype (r,vl,ot) ->
-      let name = pp_global Type r in
+      let name = pp_global_name Type r in
       let l = rename_tvars keywords vl in
       let ids, def =
         try