Extraction: (yet another) rework of the renaming code

 - Add module parameters in the structure of visible_layer,
   in order for module params to be part of name clash detection,
   avoiding this way a source of potentially wrong code.
 - In case of clash, module params are alpha-renamed to something
   unique (Foo__XXX where XXX is the number contained in the mbid).
   This solves some situations that were unsupported by extraction.
   for instance the "Module F (X:T). Module X:=X. ... End F."
 - We now check in Coq identifiers the presence of the
   extraction-reserved string __. If it is found, we issue a warning
   (which might become an error someday).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 23 deletions

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 377648422..ceb2246ad 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -607,8 +607,8 @@ let rec pp_specif = function
 	 pp_alias_spec ren s
        with Not_found -> pp_spec s)
   | (l,Smodule mt) ->
-      let def = pp_module_type mt in
-      let def' = pp_module_type mt in
+      let def = pp_module_type [] mt in
+      let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
       (try
@@ -616,7 +616,7 @@ let rec pp_specif = function
 	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
        with Not_found -> Pp.mt ())
   | (l,Smodtype mt) ->
-      let def = pp_module_type mt in
+      let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
       (try
@@ -624,16 +624,16 @@ let rec pp_specif = function
 	 fnl () ++ str ("module type "^ren^" = ") ++ name
        with Not_found -> Pp.mt ())
 
-and pp_module_type = function
+and pp_module_type params = function
   | MTident kn ->
       pp_modname kn
   | MTfunsig (mbid, mt, mt') ->
-      let typ = pp_module_type mt in
+      let typ = pp_module_type [] mt in
       let name = pp_modname (MPbound mbid) in
-      let def = pp_module_type mt' in
+      let def = pp_module_type (MPbound mbid :: params) mt' in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MTsig (mp1, sign) ->
-      push_visible mp1;
+  | MTsig (mp, sign) ->
+      push_visible mp params;
       let l = map_succeed pp_specif sign in
       pop_visible ();
       str "sig " ++ fnl () ++
@@ -648,9 +648,9 @@ and pp_module_type = function
       in
       let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
       in
-      push_visible mp_mt;
+      push_visible mp_mt [];
       let s =
-	pp_module_type mt ++ str " with type " ++
+	pp_module_type [] mt ++ str " with type " ++
 	  pp_global Type r ++ ids
       in
       pop_visible();
@@ -660,9 +660,9 @@ and pp_module_type = function
       let mp_w =
 	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
       in
-      push_visible mp_mt;
+      push_visible mp_mt [];
       let s =
-	pp_module_type mt ++ str " with module " ++ pp_modname mp_w
+	pp_module_type [] mt ++ str " with module " ++ pp_modname mp_w
       in
       pop_visible ();
       s ++ str " = " ++ pp_modname mp
@@ -681,10 +681,10 @@ let rec pp_structure_elem = function
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
 	if Common.get_phase () = Pre then
-	  str ": " ++ pp_module_type m.ml_mod_type
+	  str ": " ++ pp_module_type [] m.ml_mod_type
 	else mt ()
       in
-      let def = pp_module_expr m.ml_mod_expr in
+      let def = pp_module_expr [] m.ml_mod_expr in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1
 	(str "module " ++ name ++ typ ++ str " = " ++
@@ -694,7 +694,7 @@ let rec pp_structure_elem = function
 	 fnl () ++ str ("module "^ren^" = ") ++ name
        with Not_found -> mt ())
   | (l,SEmodtype m) ->
-      let def = pp_module_type m in
+      let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
       (try
@@ -702,17 +702,17 @@ let rec pp_structure_elem = function
          fnl () ++ str ("module type "^ren^" = ") ++ name
        with Not_found -> mt ())
 
-and pp_module_expr = function
-  | MEident mp' -> pp_modname mp'
+and pp_module_expr params = function
+  | MEident mp -> pp_modname mp
+  | MEapply (me, me') ->
+      pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")"
   | MEfunctor (mbid, mt, me) ->
       let name = pp_modname (MPbound mbid) in
-      let typ = pp_module_type mt in
-      let def = pp_module_expr me in
+      let typ = pp_module_type [] mt in
+      let def = pp_module_expr (MPbound mbid :: params) me in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MEapply (me, me') ->
-      pp_module_expr me ++ str "(" ++ pp_module_expr me' ++ str ")"
   | MEstruct (mp, sel) ->
-      push_visible mp;
+      push_visible mp params;
       let l = map_succeed pp_structure_elem sel in
       pop_visible ();
       str "struct " ++ fnl () ++
@@ -723,7 +723,7 @@ let do_struct f s =
   let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
   in
   let ppl (mp,sel) =
-    push_visible mp;
+    push_visible mp [];
     let p = prlist_strict pp sel in
     (* for monolithic extraction, we try to simulate the unavailability
        of [MPfile] in names by artificially nesting these [MPfile] *)