Extraction: handling modules (not functors) in Haskell by name mangling

 Module types are ignored, functors and module ident raise an error
 When dealing with simple modules, even nested, the structure
 hierarchy is removed, and names are arranged in the following way:
  - For the monolithic extraction, we simply use next_ident_away
    on short names, as we do when the same name appears in two .v.
  - For modular extraction, A.B.t become A__B__t or _A__B__t
    depending whether t is a type, a constructor or a constant.

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

1 files changed, 19 insertions, 5 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bde54e1d80..ebaa05b532 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -68,6 +68,12 @@ let rec dottify = function
   | s::[""] -> s
   | s::l -> (dottify l)^"."^s
 
+let rec pseudo_qualify up = function
+  | [] -> assert false
+  | [s] -> s
+  | s::[""] -> s
+  | s::l -> (if up then "" else "_")^(pseudo_qualify true l)^"__"^s
+
 (*s Uppercase/lowercase renamings. *)
 
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
@@ -303,6 +309,7 @@ and mp_renaming =
 let ref_renaming_fun (k,r) =
   let mp = subst_mp (modpath_of_r r) in
   let l = mp_renaming mp in
+  let l = if lang () = Haskell && not (modular ()) then [""] else l in
   let s =
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
@@ -370,7 +377,7 @@ let opened_libraries () =
    contains the label of the reference to print.
    Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
 
-let pp_gen k mp ls olab =
+let pp_ocaml_gen k mp ls olab =
   try (* what is the largest prefix of [mp] that belongs to [visible]? *)
     let prefix = common_prefix_from_list mp (get_visible_mps ()) in
     let delta = mp_length mp - mp_length prefix in
@@ -411,6 +418,14 @@ let pp_gen k mp ls olab =
       error_module_clash base_s
     else dottify ls
 
+let pp_haskell_gen k mp ls =
+  if not (modular ()) then List.hd ls
+  else match List.rev ls with
+    | [] -> assert false
+    | s::ls' ->
+	(if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
+	  (pseudo_qualify (upperkind k) (List.rev ls'))
+
 let pp_global k r =
   let ls = ref_renaming (k,r) in
   assert (List.length ls > 1);
@@ -422,9 +437,8 @@ let pp_global k r =
     (add_visible (k,s); unquote s)
   else match lang () with
     | Scheme -> unquote s (* no modular Scheme extraction... *)
-    | Haskell -> if modular () then dottify ls else s
-	(* for the moment we always qualify in modular Haskell... *)
-    | Ocaml -> pp_gen k mp ls (Some (label_of_r r))
+    | Haskell -> pp_haskell_gen k mp ls
+    | Ocaml -> pp_ocaml_gen k mp ls (Some (label_of_r r))
 
 (* The next function is used only in Ocaml extraction...*)
 let pp_module mp =
@@ -437,6 +451,6 @@ let pp_module mp =
 	(* we update the visible environment *)
 	let s = List.hd ls in
 	add_visible (Mod,s); s
-    | _ -> pp_gen Mod mp ls None
+    | _ -> pp_ocaml_gen Mod mp ls None