Major reorganisation of the extraction "backend".

Initial Idea: getting rid of nasty renaming issues in modules, in
 particular bugs #820 (part d) #1340 #1526 #1654

Final effect: lots of changes, simplifications, cleanups, unrelated
 fixes and ehancements, and also probably some regressions (time will 
 tell). 

A few details:

* no more experimental "Toplevel" language. 
* no more functors Make in Ocaml/Haskell/Scheme. The spirit of these
  functors and Mlpp_params was already not followed much, and this 
  framework was more a nuisance that anything else. 
* instead, some records language_descr regrouping the specific 
  features of the different output languages. 
* Common now comes before Ocaml/Haskell/Scheme, these ones are now 
  independant from each others. print_structure_to_file is now 
  in Extract_env. 
* A nice detail: no more duplications of warnings concerning axioms. 
* In modular extraction, the clashes due to the opened modules 
  are now computed once and for all thanks to record_contents_fstlev, 
  instead of re-asking Coq each time about these opened modules and 
  using Extraction.constant_kind 
* some utilities about modules_path added and/or moved from Modutil 
  to Table. 
* using a .v file as a module, e.g. in a functor application should 
  now works in modular extraction. 

Now concerning renaming issues themselves: 

* printing is done twice, the first time toward /dev/null, in order
  to encounter the naming issues unsolvable by a simple qualification. 
  On the second run, we create artificial modules Coq__123 for 
  allowing qualification of these hidden objects. 
* names are now fully separated into their syntaxic categories: 
  terms/types/constructors/modules
* Only one last unsupported situation (but at least detected and 
  signaled by an error): an object M.t from an external file-module
  M.v can't be printed when a local module M is in the way. 
  This situation is really unlikely (in Coq you must use _long_
  file-module name, e.g. Init.Datatypes.nat). It could be solved
  by inserting "module Coq_123 = M" at the beginning of the file, 
  but then the signature of Coq_123 (that is, the one of M) should 
  be written explicitely in the .mli, which is _really_ not nice. 





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

1 files changed, 389 insertions, 365 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 6db146b1e..855990d25 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -17,42 +17,218 @@ open Nameops
 open Libnames
 open Table
 open Miniml
+open Mlutil
 open Modutil
-open Ocaml
+open Mod_subst
 
-(*S Renamings. *)
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+let pr_binding = function
+  | [] -> mt ()
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+let fnl2 () = fnl () ++ fnl () 
+
+let space_if = function true -> str " " | false -> mt ()
+
+let sec_space_if = function true -> spc () | false -> mt ()
+
+let is_digit = function 
+  | '0'..'9' -> true
+  | _ -> false
+
+let begins_with_CoqXX s = 
+  let n = String.length s in 
+  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+  let i = ref 3 in 
+  try while !i < n do
+    if s.[!i] = '_' then i:=n (*Stop*)
+    else if is_digit s.[!i] then incr i 
+    else raise Not_found
+  done; true
+  with Not_found -> false
+  
+let unquote s = 
+  if lang () <> Scheme then s 
+  else 
+    let s = String.copy s in 
+    for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+    s
+      
+let rec dottify = function 
+  | [] -> assert false 
+  | [s] -> unquote s 
+  | s::[""] -> unquote s 
+  | s::l -> (dottify l)^"."^(unquote s)
+
+(*s Uppercase/lowercase renamings. *) 
+
+let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+
+let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+
+(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
+let pr_upper_id id = str (String.capitalize (string_of_id id))
+
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+(*s Generic renaming issues for local variable names. *)
+
+let rec rename_id id avoid = 
+  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+
+let rec rename_vars avoid = function
+  | [] -> 
+      [], avoid
+  | id :: idl when id == dummy_name ->
+      (* we don't rename dummy binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
+  | id :: idl ->
+      let (idl, avoid) = rename_vars avoid idl in
+      let id = rename_id (lowercase_id id) avoid in
+      (id :: idl, Idset.add id avoid)
+
+let rename_tvars avoid l = 
+  let rec rename avoid = function 
+    | [] -> [],avoid 
+    | id :: idl -> 
+	let id = rename_id (lowercase_id id) avoid in 
+	let idl, avoid = rename (Idset.add id avoid) idl in 
+	(id :: idl, avoid) in
+  fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (ids' @ db, avoid')
+
+let get_db_name n (db,_) = 
+  let id = List.nth db (pred n) in 
+  if id = dummy_name then id_of_string "__" else id
+
+
+(*S Renamings of global objects. *)
 
 (*s Tables of global renamings *)
 
 let keywords = ref Idset.empty
+let set_keywords kws = keywords := kws
+
 let global_ids = ref Idset.empty
-let modular = ref false
+let add_global_ids s = global_ids := Idset.add s !global_ids
+let global_ids_list () = Idset.elements !global_ids
+
+let empty_env () = [], !global_ids
+
+let mktable () = 
+  let h = Hashtbl.create 97 in 
+  (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+
+let mkset () = 
+  let h = Hashtbl.create 97 in 
+  (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h)
+
+let mktriset () = 
+  let h = Hashtbl.create 97 in
+  (fun x y z -> Hashtbl.add h (x,y,z) ()), 
+  (fun x y z -> Hashtbl.mem h (x,y,z)), 
+  (fun () -> Hashtbl.clear h)
 
 (* For each [global_reference], this table will contain the different parts 
-   of its renamings, in [string list] form. *)
-let renamings = Hashtbl.create 97
-let rename r l = Hashtbl.add renamings r l
-let get_renamings r = Hashtbl.find renamings r 
+   of its renaming, in [string list] form. *)
+let add_renaming, get_renaming, clear_renaming = mktable ()
 
 (* Idem for [module_path]. *)
-let mp_renamings = Hashtbl.create 97
-let mp_rename mp l = Hashtbl.add mp_renamings mp l
-let mp_get_renamings mp = Hashtbl.find mp_renamings mp 
+let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable ()
 
-let modvisited = ref MPset.empty
-let modcontents = ref Gset.empty
-let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents
-let module_contents mp s = Gset.mem (mp,s) !modcontents
+(* A table for function modfstlev_rename *)
+let add_modfstlev, get_modfstlev, clear_modfstlev = mktable ()
 
-let to_qualify = ref Refset.empty
+(* A set of all external objects that will have to be fully qualified *)
+let add_static_clash, static_clash, clear_static_clash = mkset ()
 
-let mod_1st_level = ref Idmap.empty
+(* Two tables of triplets [kind * module_path * string]. The first one 
+   will record the first level of all MPfile, not only the current one. 
+   The second table will contains local renamings. *)
 
-(*s Uppercase/lowercase renamings. *) 
+type kind = Term | Type | Cons | Mod
 
-let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset ()
+let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset ()
 
-let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+(* The list of external modules that will be opened initially *)
+let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles = 
+  let m = ref MPset.empty in 
+  (fun mp -> m:= MPset.add mp !m), 
+  (fun mp -> MPset.mem mp !m),
+  (fun () -> MPset.elements !m),
+  (fun () -> m:= MPset.empty)
+
+(*s table containing the visible horizon at a precise moment *)
+
+let visible = ref ([] : module_path list)
+let pop_visible () = visible := List.tl !visible
+let push_visible mp = visible := mp :: !visible
+let top_visible_mp () = List.hd !visible
+
+(*s substitutions for printing signatures *)
+
+let substs = ref empty_subst
+let add_subst msid mp = substs := add_msid msid mp !substs
+let subst_mp mp = subst_mp !substs mp
+let subst_kn kn = subst_kn !substs kn
+let subst_con c = fst (subst_con !substs c)
+let subst_ref = function 
+  | ConstRef con -> ConstRef (subst_con con)
+  | IndRef (kn,i) -> IndRef (subst_kn kn,i)
+  | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j)
+  | _ -> assert false
+
+
+let duplicate_index = ref 0
+let to_duplicate = ref Gmap.empty
+let add_duplicate mp l = 
+  incr duplicate_index; 
+  let ren = "Coq__" ^ string_of_int (!duplicate_index) in 
+  to_duplicate := Gmap.add (mp,l) ren !to_duplicate
+let check_duplicate mp l = 
+  let mp' = subst_mp mp in 
+  Gmap.find (mp',l) !to_duplicate
+
+type reset_kind = OnlyLocal | AllButExternal | Everything
+
+let reset_allbutext () = 
+  clear_loc_mpmem (); 
+  global_ids := !keywords; 
+  clear_renaming (); 
+  clear_mp_renaming (); 
+  clear_modfstlev (); 
+  clear_static_clash (); 
+  clear_mpfiles (); 
+  duplicate_index := 0; 
+  to_duplicate := Gmap.empty; 
+  visible := []; 
+  substs := empty_subst
+ 
+let reset_everything () = reset_allbutext (); clear_ext_mpmem ()
+
+let reset_renaming_tables = function 
+  | OnlyLocal -> clear_loc_mpmem ()
+  | AllButExternal -> reset_allbutext ()
+  | Everything -> reset_everything ()
+
+(*S Renaming functions *)
 
 (* This function creates from [id] a correct uppercase/lowercase identifier. 
    This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes 
@@ -69,389 +245,237 @@ let modular_rename up id =
   then prefix ^ s
   else s
 
-let rename_module = modular_rename true 
-
-(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when 
-   [mpl] is the context of visible modules. More precisely, we check if 
-   there exists a mp1, module (sub-)path of an element of [mpl], such as 
-   module [mp1-l] contains [s]. 
-   The verification stops if we encounter [mp1=mp0]. *)
-
-exception Stop 
-
-let clash mp0 l s mpl = 
-  let rec clash_one mp = match mp with
-    | _ when mp = mp0 -> raise Stop
-    | MPdot (mp',_) -> 
-	(module_contents (add_labels_mp mp l) s) || (clash_one mp') 
-    | mp when is_toplevel mp -> false
-    | _ -> module_contents (add_labels_mp mp l) s
+(*s [record_contents_fstlev] finds the names of the first-level objects 
+  exported by the ground-level modules in [struc]. *)
+
+let rec record_contents_fstlev struc = 
+  let upper_type = (lang () = Haskell) in 
+  let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in
+  let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in
+  let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in
+  let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in 
+  let addfix mp r = 
+    add_ext_mpmem Term mp (modular_rename false (id_of_global r))
   in
-  let rec clash_list = function 
-    | [] -> false
-    | mp :: mpl -> (clash_one mp) || (clash_list mpl) 
-  in try clash_list mpl with Stop -> false
-
-(*s [contents_first_level mp] finds the names of the first-level objects 
-  exported by module [mp]. Nota: it might fail if [mp] isn't a directly 
-  visible module. Ex: [MPself] under functor, [MPbound], etc ... *)
-
-let contents_first_level mp = 
-  if not (MPset.mem mp !modvisited) then begin 
-    modvisited := MPset.add mp !modvisited; 
-    match (Global.lookup_module mp).mod_type with 
-      | MTBsig (msid,msb) -> 
-	  let add b id = add_module_contents mp (modular_rename b id) in 
-	  let upper_type = (lang () = Haskell) in
-	  List.iter 
-	    (function 
-	       | (l, SPBconst cb) -> 
-		   (match Extraction.constant_kind (Global.env ()) cb with 
-		      | Extraction.Logical -> () 
-		      | Extraction.Type -> add upper_type (id_of_label l)
-		      | Extraction.Term -> add false (id_of_label l))
-	       | (_, SPBmind mib) ->
-		   Array.iter 
-		     (fun mip -> if snd (Inductive.mind_arity mip) <> InProp
-		      then begin
-			add upper_type mip.mind_typename; 
-			Array.iter (add true) mip.mind_consnames
-		      end)
-		     mib.mind_packets
-	       | _ -> ())
-	    (Modops.subst_signature_msid msid mp msb)
-      | _ -> ()
-  end
+  let f mp = function 
+    | (l,SEdecl (Dind (_,ind))) -> 
+	Array.iter 
+	  (fun ip -> 
+	     addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames)
+	  ind.ind_packets
+    | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l)
+    | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l)
+    | (l,SEdecl (Dfix  (rv,_,_))) -> Array.iter (addfix mp) rv
+    | (l,SEmodule _) -> addmod mp (id_of_label l)
+    | (l,SEmodtype _) -> addmod mp (id_of_label l)
+  in
+  List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc
 
-(*s Initial renamings creation, for modular extraction. *) 
+(*s For monolithic extraction, first-level modules might have to be renamed 
+    with unique numbers *)
+
+let modfstlev_rename l =
+  let coqid = id_of_string "Coq" in 
+  let id = id_of_label l in 
+  try 
+    let coqset = get_modfstlev id in 
+    let nextcoq = next_ident_away coqid coqset in 
+    add_modfstlev id (nextcoq::coqset); 
+    (string_of_id nextcoq)^"_"^(string_of_id id) 
+  with Not_found -> 
+    let s = string_of_id id in 
+    if is_lower s || begins_with_CoqXX s then
+      (add_modfstlev id [coqid]; "Coq_"^s)
+    else
+      (add_modfstlev id []; s)
+
+(*s Creating renaming for a [module_path] *)
 
-let rec mp_create_modular_renamings mp = 
-  try mp_get_renamings mp 
+let rec mp_create_renaming mp = 
+  try get_mp_renaming mp 
   with Not_found -> 
     let ren = match mp with 
+      | _ when not (modular ()) && at_toplevel mp -> [""]
       | MPdot (mp,l) -> 
-	  (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp)
-      | MPself msid -> [rename_module (id_of_msid msid)]
-      | MPbound mbid -> [rename_module (id_of_mbid mbid)]
-      | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))]
-    in mp_rename mp ren; ren
+	  let lmp = mp_create_renaming mp in 
+	  if lmp = [""] then (modfstlev_rename l)::lmp
+	  else (modular_rename true (id_of_label l))::lmp
+      | MPself msid -> [modular_rename true (id_of_msid msid)]
+      | MPbound mbid -> [modular_rename true (id_of_mbid mbid)]
+      | MPfile _ when not (modular ()) -> assert false
+      | MPfile _ -> [string_of_modfile mp]
+    in add_mp_renaming mp ren; ren
+
+(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when 
+   [mpl] is the context of visible modules. More precisely, we check if 
+   there exists a [mp] in [mpl] that contains [s]. 
+   The verification stops if we encounter [mp=mp0]. *)
 
+let rec clash mem mp0 s = function 
+  | [] -> false
+  | mp :: _ when mp = mp0 -> false
+  | mp :: mpl -> mem mp s || clash mem mp0 s mpl
+    
+(*s Initial renamings creation, for modular extraction. *) 
 
 let create_modular_renamings struc = 
   let current_module = fst (List.hd struc) in 
-  let modfiles = ref MPset.empty in 
-  let { up = u ; down = d } = struct_get_references_set struc 
+  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc 
   in 
   (* 1) creates renamings of objects *)
   let add upper r = 
     let mp = modpath_of_r r in 
-    let l = mp_create_modular_renamings mp in 
+    let l = mp_create_renaming mp in 
     let s = modular_rename upper (id_of_global r) in 
-    global_ids := Idset.add (id_of_string s) !global_ids;    
-    rename r (s::l); 
+    add_global_ids (id_of_string s);
+    add_renaming r (s::l); 
     begin try 
-      let mp = modfile_of_mp mp in 
-      if mp <> current_module then modfiles := MPset.add mp !modfiles
+      let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp
     with Not_found -> () 
     end; 
   in
-  Refset.iter (add true) u; 
-  Refset.iter (add false) d; 
+  Refset.iter (add (lang () = Haskell)) ty; 
+  Refset.iter (add true) co;
+  Refset.iter (add false) tr;
   
   (* 2) determines the opened libraries. *)
-  let used_modules = MPset.elements !modfiles in 
-
-  (* [s] will contain all first-level sub-modules of [cur_mp] *)
-  let s = ref Stringset.empty in 
-  begin 
-    let add l = s := Stringset.add (rename_module (id_of_label l)) !s in 
-    match (Global.lookup_module current_module).mod_type with 
-      | MTBsig (_,msb) ->
-	  List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb
-      | _ -> ()
-  end;
-  (* We now compare [s] with the modules coming from [used_modules]. *)
-  List.iter 
-    (function 
-       | MPfile d -> 
-	   let s_mp = 
-	     String.capitalize (string_of_id (List.hd (repr_dirpath d))) in 
-	   if Stringset.mem s_mp !s then error_module_clash s_mp 
-	   else s:= Stringset.add s_mp !s 
-       | _ -> assert false)
-    used_modules;
+  let used_modules = list_mpfiles () in 
+  let used_modules' = List.rev used_modules in 
+  let str_list = List.map string_of_modfile used_modules' 
+  in
+  let rec check_elsewhere mpl sl = match mpl, sl with
+    | [], [] -> []
+    | mp::mpl, _::sl -> 
+	if List.exists (ext_mpmem Mod mp) sl then
+	  check_elsewhere mpl sl
+	else mp :: (check_elsewhere mpl sl)
+    | _ -> assert false
+  in 
+  let opened_modules = check_elsewhere used_modules' str_list in 
+  clear_mpfiles (); 
+  List.iter add_mpfiles opened_modules; 
 
   (* 3) determines the potential clashes *)
-  List.iter contents_first_level used_modules; 
-  let used_modules' = List.rev used_modules in 
-  let needs_qualify r = 
+  let needs_qualify k r = 
     let mp = modpath_of_r r in 
     if (is_modfile mp) && mp <> current_module && 
-      (clash mp [] (List.hd (get_renamings r)) used_modules')
-    then to_qualify := Refset.add r !to_qualify
+      (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
+    then add_static_clash r
   in
-  Refset.iter needs_qualify u;
-  Refset.iter needs_qualify d; 
-  used_modules
+  Refset.iter (needs_qualify Type) ty;
+  Refset.iter (needs_qualify Term) tr;
+  Refset.iter (needs_qualify Cons) co;
+  List.rev opened_modules
 
 (*s Initial renamings creation, for monolithic extraction. *)
 
-let begins_with_CoqXX s = 
-  (String.length s >= 4) && 
-  (String.sub s 0 3 = "Coq") &&
-  (try 
-     for i = 4 to (String.index s '_')-1 do 
-       match s.[i] with 
-	 | '0'..'9' -> () 
-	 | _ -> raise Not_found
-     done; 
-     true
-   with Not_found -> false)
-
-let mod_1st_level_rename l =
-  let coqid = id_of_string "Coq" in 
-  let id = id_of_label l in 
-  try 
-    let coqset = Idmap.find id !mod_1st_level in 
-    let nextcoq = next_ident_away coqid coqset in 
-    mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level; 
-    (string_of_id nextcoq)^"_"^(string_of_id id) 
-  with Not_found -> 
-    let s = string_of_id id in 
-    if is_lower s || begins_with_CoqXX s then
-      (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s)
-    else
-      (mod_1st_level := Idmap.add id [] !mod_1st_level; s)
-
-let rec mp_create_mono_renamings mp = 
-  try mp_get_renamings mp 
-  with Not_found -> 
-    let ren = match mp with 
-       | _ when (at_toplevel mp) -> [""]
-       | MPdot (mp,l) -> 
-	   let lmp = mp_create_mono_renamings mp in
-	   if lmp = [""] then (mod_1st_level_rename l)::lmp
-	   else (rename_module (id_of_label l))::lmp
-       | MPself msid -> [rename_module (id_of_msid msid)]
-       | MPbound mbid -> [rename_module (id_of_mbid mbid)]
-       | _ -> assert false
-    in mp_rename mp ren; ren
-
 let create_mono_renamings struc = 
-  let { up = u ; down = d } = struct_get_references_list struc in 
+  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in
   let add upper r = 
     let mp = modpath_of_r r in 
-    let l = mp_create_mono_renamings mp in
+    let l = mp_create_renaming mp in
     let mycase = if upper then uppercase_id else lowercase_id in 
     let id = 
       if l = [""] then 
-	next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids)
+	next_ident_away (mycase (id_of_global r)) (global_ids_list ())
       else id_of_string (modular_rename upper (id_of_global r))
     in 
-    global_ids := Idset.add id !global_ids;    
-    rename r ((string_of_id id)::l) 
+    add_global_ids id; 
+    add_renaming r ((string_of_id id)::l) 
   in
-  List.iter (add true) (List.rev u); 
-  List.iter (add false) (List.rev d)
-		    
-(*s Renaming issues at toplevel *)
-
-module TopParams = struct
-  let globals () = Idset.empty
-  let pp_global _ r = pr_id (id_of_global r)
-  let pp_module _ mp = str (string_of_mp mp)
-end
-
-(*s Renaming issues for a monolithic or modular extraction. *)
-
-module StdParams = struct
-
-  let globals () = !global_ids
-
-  let unquote s = 
-    if lang () <> Scheme then s 
-    else 
-      let s = String.copy s in 
-      for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
-      s
-
-  let rec dottify = function 
-    | [] -> assert false 
-    | [s] -> unquote s 
-    | s::[""] -> unquote s 
-    | s::l -> (dottify l)^"."^(unquote s)
-
-  let pp_global mpl r = 
-    let ls = get_renamings r in 
-    let s = List.hd ls in 
-    let mp = modpath_of_r r in 
-    let ls = 
-      if mp = List.hd mpl then [s] (* simpliest situation *)
-      else match lang () with 
-	| Scheme -> [s] (* no modular Scheme extraction... *)
-	| Toplevel -> [s] (* idem *)
-	| Haskell -> 
-	    if !modular then 
-	      ls (* for the moment we always qualify in modular Haskell *)
-	    else [s]
-	| Ocaml -> 
-	    try (* has [mp] something in common with one of those in [mpl] ? *)
-	      let pref = common_prefix_from_list mp mpl in 
-	      (*i TODO: possibilité de clash i*)
-	      list_firstn ((mp_length mp)-(mp_length pref)+1) ls
-	    with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
-	      let base = base_mp mp in 
-	      if !modular &&  
-		(at_toplevel mp) && 
-		not (Refset.mem r !to_qualify) && 
-		not (clash base [] s mpl) 
-	      then snd (list_sep_last ls)
-	      else ls
-    in 
-    add_module_contents mp s; (* update the visible environment *)
-    str (dottify ls)
-
-  (* The next function is used only in Ocaml extraction...*)
-  let pp_module mpl mp = 
-    let ls = 
-      if !modular 
-      then mp_create_modular_renamings mp 
-      else mp_create_mono_renamings mp 
-    in 
-    let ls = 
-      try (* has [mp] something in common with one of those in [mpl] ? *)
-	let pref = common_prefix_from_list mp mpl in 
-	(*i TODO: clash possible i*)
-	list_firstn ((mp_length mp)-(mp_length pref)) ls
-      with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
-	if !modular && (at_toplevel mp) 
-	then snd (list_sep_last ls)
-	else ls
-    in str (dottify ls) 
-
-end
-
-module ToplevelPp = Ocaml.Make(TopParams)
-module OcamlPp = Ocaml.Make(StdParams)
-module HaskellPp = Haskell.Make(StdParams)
-module SchemePp = Scheme.Make(StdParams)
-
-let pp_decl mp d = match lang () with 
-  | Ocaml -> OcamlPp.pp_decl mp d 
-  | Haskell -> HaskellPp.pp_decl mp d
-  | Scheme -> SchemePp.pp_decl mp d 
-  | Toplevel -> ToplevelPp.pp_decl mp d 
-
-let pp_struct s = match lang () with 
-  | Ocaml -> OcamlPp.pp_struct s 
-  | Haskell -> HaskellPp.pp_struct s
-  | Scheme -> SchemePp.pp_struct s
-  | Toplevel -> ToplevelPp.pp_struct s
-
-let pp_signature s = match lang () with 
-  | Ocaml -> OcamlPp.pp_signature s 
-  | Haskell -> HaskellPp.pp_signature s
-  | _ -> assert false
-
-let set_keywords () =
-  (match lang () with 
-    | Ocaml -> keywords := Ocaml.keywords
-    | Haskell -> keywords := Haskell.keywords
-    | Scheme -> keywords := Scheme.keywords
-    | Toplevel -> keywords := Idset.empty);
-  global_ids := !keywords; 
-  to_qualify := Refset.empty
+  List.iter (add (lang () = Haskell)) (List.rev ty); 
+  List.iter (add false) (List.rev tr);
+  List.iter (add true) (List.rev co);
+  []
+
+let create_renamings struc = 
+  if modular () then create_modular_renamings struc
+  else create_mono_renamings struc
     
-let preamble prm = match lang () with 
-  | Ocaml -> Ocaml.preamble prm   
-  | Haskell -> Haskell.preamble prm
-  | Scheme -> Scheme.preamble prm
-  | Toplevel -> (fun _ _ _ -> mt ())
-
-let preamble_sig prm = match lang () with 
-  | Ocaml -> Ocaml.preamble_sig prm   
-  | _ -> assert false
-
-(*S Extraction of one decl to stdout. *)
-
-let print_one_decl struc mp decl = 
-  set_keywords (); 
-  modular := false; 
-  create_mono_renamings struc;
-  msgnl (pp_decl [mp] decl)
-
-(*S Extraction to a file. *)
-
-let info f = 
-  Options.if_verbose msgnl 
-    (str ("The file "^f^" has been created by extraction."))
-
-let print_structure_to_file f prm struc =
-  Hashtbl.clear renamings;
-  mod_1st_level := Idmap.empty; 
-  modcontents := Gset.empty;
-  modvisited := MPset.empty; 
-  set_keywords ();
-  modular := prm.modular; 
-  let used_modules =
-    if lang () = Toplevel then []
-    else if prm.modular then create_modular_renamings struc
-    else (create_mono_renamings struc; [])
-  in 
-  let print_dummys =
-    (struct_ast_search ((=) MLdummy) struc, 
-     struct_type_search Mlutil.isDummy struc, 
-     struct_type_search ((=) Tunknown) struc)
-  in 
-  let print_magic = 
-    if lang () <> Haskell then false 
-    else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
-  in
-  (* print the implementation *)
-  let cout = option_map (fun (f,_) -> open_out f) f in 
-  let ft = match cout with 
-    | None -> !Pp_control.std_ft
-    | Some cout -> Pp_control.with_output_to cout in 
-  begin try 
-    msg_with ft (preamble prm used_modules print_dummys print_magic);
-    msg_with ft (pp_struct struc);
-    option_iter close_out cout; 
-  with e -> 
-    option_iter close_out cout; raise e
-  end;
-  option_iter (fun (f,_) -> info f) f;
-  (* print the signature *)
-  match f with 
-    | Some (_,f) when lang () = Ocaml -> 
-	let cout = open_out f in
-	let ft = Pp_control.with_output_to cout in
-	begin try 
-	  msg_with ft (preamble_sig prm used_modules print_dummys);
-	  msg_with ft (pp_signature (signature_of_structure struc));
-	  close_out cout;
-	with e -> 
-	  close_out cout; raise e 
-	end; 
-	info f 
-    | _ -> ()
-	  
-
-(*i 
-  (* DO NOT REMOVE: used when making names resolution *)
-  let cout = open_out (f^".ren") in 
-  let ft = Pp_control.with_output_to cout in
-  Hashtbl.iter 
-    (fun r id -> 
-       if short_module r = !current_module then 
-	 msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
-    renamings;
-  pp_flush_with ft ();
-  close_out cout;
-i*)    
-
-
-
-
-
-
+		    
+(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
+
+let pp_global k r = 
+  let ls = get_renaming r in 
+  assert (List.length ls > 1); 
+  let s = List.hd ls in 
+  let mp = modpath_of_r r in 
+  if mp = top_visible_mp () then 
+    (* simpliest situation: definition of r (or use in the same context) *)
+    (* we update the visible environment *)
+    (add_loc_mpmem k mp s; unquote s)
+  else match lang () with 
+    | Scheme -> unquote s (* no modular Scheme extraction... *)
+    | Haskell -> 
+	(* for the moment we always qualify in modular Haskell *)
+	if modular () then dottify ls else s
+    | Ocaml -> 
+	try (* has [mp] something in common with one of [!visible] ? *)
+	  let prefix = common_prefix_from_list mp !visible in 
+	  let delta = mp_length mp - mp_length prefix in 
+	  let ls = list_firstn (delta+1) ls in 
+	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
+             but this (not-so-long) name can in fact be hidden. Solution: 
+	     duplication of the _definition_ of r in a Coq__XXX module *)
+	  let s,ls' = list_sep_last ls in 
+	  let k' = if ls' = [] then k else Mod in 
+	  if clash (loc_mpmem k') prefix s !visible then 
+	    let front = if ls' = [] then [s] else ls' in 
+	    let l = get_nth_label delta r in 
+	    try dottify (front @ [check_duplicate prefix l])
+	    with Not_found -> add_duplicate prefix l; dottify ls
+	  else dottify ls 
+	with Not_found -> 
+	  (* [mp] belongs to a closed module, not one of [!visible]. *)
+	  let base = base_mp mp in 
+	  let base_s,ls1 = list_sep_last ls in 
+	  let s,ls2 = list_sep_last ls1 in  
+	  let k' = if ls2 = [] then k else Mod in 
+	  if modular () && (mem_mpfiles base) && 
+	    not (static_clash r) && 
+	    (* k' = Mod can't clash in an opened module, see earlier check *)
+	    not (clash (loc_mpmem k') base s !visible)
+	  then (* Standard situation of an object in another file: *)
+	    (* Thanks to the "open" of this file we remove its name *) 
+	    dottify ls1
+	  else if clash (loc_mpmem Mod) base base_s !visible then 
+	    error_module_clash base_s
+	  else dottify ls 
+	    
+(* The next function is used only in Ocaml extraction...*)
+let pp_module mp = 
+  let ls = mp_create_renaming mp in
+  if List.length ls = 1 then dottify ls 
+  else match mp with 
+    | MPdot (mp0,_) when mp0 = top_visible_mp () -> 
+	(* simpliest situation: definition of mp (or use in the same context) *)
+	(* we update the visible environment *)
+	let s = List.hd ls in 
+	add_loc_mpmem Mod mp0 s; s
+    | _ ->
+	try (* has [mp] something in common with one of those in [!visible] ? *)
+	  let prefix = common_prefix_from_list mp !visible in 
+	  assert (mp <> prefix); (* no use of mp as whole module from itself *)
+	  let delta = mp_length mp - mp_length prefix in 
+	  let ls = list_firstn delta ls in
+	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
+	     but this (not-so-long) name can in fact be hidden. Solution: 
+	     duplication of the _definition_ of mp via a Coq__XXX module *)
+	  let s,ls' = list_sep_last ls in 
+	  if clash (loc_mpmem Mod) prefix s !visible then 
+	    let l = get_nth_label_mp delta mp in 
+	    try dottify (ls' @ [check_duplicate prefix l])
+	    with Not_found -> add_duplicate prefix l; dottify ls
+	  else dottify ls
+	with Not_found -> 
+	  (* [mp] belongs to a closed module, not one of [!visible]. *)
+	  let base = base_mp mp in 
+	  let base_s,ls' = list_sep_last ls in 
+	  let s = fst (list_sep_last ls) in 
+	  if modular () && (mem_mpfiles base) &&
+	    not (clash (loc_mpmem Mod) base s !visible)
+	  then dottify ls'
+	  else if clash (loc_mpmem Mod) base base_s !visible then 
+	    error_module_clash base_s
+	  else dottify ls