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

2 files changed, 30 insertions, 11 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bde54e1d8..ebaa05b53 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
 
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index c1ed62b34..c199225e4 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -251,7 +251,7 @@ let pp_one_ind ip pl cv =
   if Array.length cv = 0 then str "= () -- empty inductive"
   else
     (v 0 (str "= " ++
-	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor
+	  prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
 	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
 
 let rec pp_ind first kn i ind =
@@ -311,12 +311,17 @@ let pp_decl = function
 	  else
 	    hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
 
-let pp_structure_elem = function
+let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) ->
-      failwith "TODO: Haskell extraction of modules not implemented yet"
-  | (l,SEmodtype m) ->
-      failwith "TODO: Haskell extraction of modules not implemented yet"
+  | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
+  | (l,SEmodtype m) -> mt ()
+      (* for the moment we simply discard module type *)
+
+and pp_module_expr = function
+  | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel
+  | MEident _ -> failwith "Not Implemented: Module Ident"
+  | MEfunctor _ -> failwith "Not Implemented: Module Functor"
+  | MEapply _ -> failwith "Not Implemented: Module Application"
 
 let pp_struct =
   let pp_sel (mp,sel) =