mise en place extraction haskell

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

11 files changed, 555 insertions, 45 deletions

diff --git a/.depend b/.depend
index a276f5d11..2f9c529c1 100644
--- a/.depend
+++ b/.depend
@@ -253,11 +253,13 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
     kernel/term.cmi 
 contrib/extraction/extraction.cmi: kernel/environ.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
+contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi 
 contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     kernel/term.cmi 
 contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmi 
+    contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi 
 contrib/interface/dad.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
     proofs/tacmach.cmi 
 contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
@@ -1138,6 +1140,8 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
@@ -1392,14 +1396,16 @@ contrib/correctness/peffect.cmx: toplevel/himsg.cmx kernel/names.cmx \
     contrib/correctness/peffect.cmi 
 contrib/correctness/penv.cmo: toplevel/himsg.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/perror.cmi \
-    contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/ptype.cmi \
-    library/summary.cmi kernel/term.cmi contrib/correctness/penv.cmi 
+    lib/options.cmi contrib/correctness/past.cmi \
+    contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \
+    contrib/correctness/ptype.cmi library/summary.cmi kernel/term.cmi \
+    contrib/correctness/penv.cmi 
 contrib/correctness/penv.cmx: toplevel/himsg.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/perror.cmx \
-    contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/ptype.cmi \
-    library/summary.cmx kernel/term.cmx contrib/correctness/penv.cmi 
+    lib/options.cmx contrib/correctness/past.cmi \
+    contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx lib/pp.cmx \
+    contrib/correctness/ptype.cmi library/summary.cmx kernel/term.cmx \
+    contrib/correctness/penv.cmi 
 contrib/correctness/perror.cmo: library/declare.cmi kernel/evd.cmi \
     library/global.cmi toplevel/himsg.cmi kernel/names.cmi \
     contrib/correctness/past.cmi contrib/correctness/peffect.cmi lib/pp.cmi \
@@ -1604,6 +1610,16 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi 
+contrib/extraction/haskell.cmo: kernel/environ.cmi library/global.cmi \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
+    kernel/names.cmi contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi \
+    lib/pp_control.cmi kernel/term.cmi lib/util.cmi \
+    contrib/extraction/haskell.cmi 
+contrib/extraction/haskell.cmx: kernel/environ.cmx library/global.cmx \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
+    kernel/names.cmx contrib/extraction/ocaml.cmx lib/options.cmx lib/pp.cmx \
+    lib/pp_control.cmx kernel/term.cmx lib/util.cmx \
+    contrib/extraction/haskell.cmi 
 contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \
     library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
diff --git a/Makefile b/Makefile
index ed249fa76..6a2fabb26 100644
--- a/Makefile
+++ b/Makefile
@@ -134,6 +134,7 @@ USERTACCMO=$(USERTAC:.ml4=.cmo)
 USERTACCMX=$(USERTAC:.ml4=.cmx)
 
 EXTRACTIONCMO=contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo \
+	      contrib/extraction/haskell.cmo \
 	      contrib/extraction/extraction.cmo \
 	      contrib/extraction/extract_env.cmo
 
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index b8d295aef..bfe459b18 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -7,17 +7,31 @@
 (***********************************************************************)
 
 Grammar vernac vernac : ast :=
+
+(* Extraction in the Coq toplevel *)
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
               [ (Extraction $c) ]
 | extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
-| extr_list   
+
+(* Monolithic extraction to a file *)
+| extr_file
      [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile $o $f ($LIST $l)) ]
+  -> [ (ExtractionFile "ocaml" $o $f ($LIST $l)) ]
+| haskell_extr_file
+     [ "Haskell" "Extraction" stringarg($f) options($o) 
+       ne_qualidarg_list($l) "." ] 
+  -> [ (ExtractionFile "haskell" $o $f ($LIST $l)) ]
+
+(* Modular extraction (one Coq module = one ML module) *)
 | extr_module 
      [ "Extraction" "Module" options($o) identarg($m) "." ]
-  -> [ (ExtractionModule $o $m) ]
+  -> [ (ExtractionModule "ocaml" $o $m) ]
+| haskell_extr_module 
+     [ "Haskell" "Extraction" "Module" options($o) identarg($m) "." ]
+  -> [ (ExtractionModule "haskell" $o $m) ]
 
+(* Overriding of a Coq object by an ML one *)
 | extract_constant 
      [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
   -> [ (EXTRACT_CONSTANT $x $y) ]
@@ -26,6 +40,7 @@ Grammar vernac vernac : ast :=
      [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
   -> [ (EXTRACT_INDUCTIVE $x $y) ]
 
+(* Utility entries *)
 with mindnames : ast :=
   mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
         -> [(VERNACARGLIST $id ($LIST $idl))]
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index f08e69161..da3d464bb 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -167,15 +167,22 @@ let _ =
 
 (*s Extraction parameters. *)
 
-let interp_options keep modular = function
+let strict_language = function
+  | "ocaml" -> true
+  | "haskell" -> false
+  | _ -> assert false
+
+let interp_options lang keep modular m = function
   | [VARG_STRING "noopt"] ->
-      { optimization = false; modular = modular; 
+      { optimization = false; modular = modular; module_name = m;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | [VARG_STRING "nooption"] ->
-      { optimization = true; modular = modular;
+      { optimization = strict_language lang; 
+	modular = modular; module_name = m;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | VARG_STRING "expand" :: l ->
-      { optimization = true; modular = modular;
+      { optimization = strict_language lang; 
+	modular = modular; module_name = m;
 	to_keep = refs_set_of_list keep; 
 	to_expand = refs_set_of_list (refs_of_vargl l) }
   | _ -> 
@@ -185,17 +192,23 @@ let interp_options keep modular = function
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
     We just call [extract_to_file] on the saturated environment. *)
 
+let extract_to_file = function
+  | "ocaml" -> Ocaml.extract_to_file 
+  | "haskell" -> Haskell.extract_to_file
+  | _ -> assert false
+
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
-       | VARG_VARGLIST o :: VARG_STRING f :: vl ->
+       | VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl ->
 	   let refs = refs_of_vargl vl in
-	   let prm = interp_options refs false o in
+	   let prm = interp_options lang refs false "" o in
 	   (fun () -> 
 	      let decls = decl_of_refs refs in 
 	      let decls = optimize prm decls in
-	      Ocaml.extract_to_file f prm decls)
+	      extract_to_file lang f prm decls)
        | _ -> assert false)
+
 (*s Extraction of a module. The vernacular command is \verb!Extraction Module!
     [M]. We build the environment to extract by traversing the segment of
     module [M]. We just keep constants and inductives, and we remove
@@ -216,20 +229,25 @@ let extract_module m =
 let decl_mem rl = function 
   | Dglob (r,_) -> List.mem r rl 
   | Dabbrev (r,_,_) -> List.mem r rl 
-  | Dtype((_,r,_)::_, _) -> List.mem r rl
-  | Dtype([],_) -> false
+  | Dtype ((_,r,_)::_, _) -> List.mem r rl
+  | Dtype ([],_) -> false
+
+let file_suffix = function
+  | "ocaml" -> ".ml"
+  | "haskell" -> ".hs"
+  | _ -> assert false
 
 let _ = 
   vinterp_add "ExtractionModule"
     (function 
-       | [VARG_VARGLIST o; VARG_IDENTIFIER m] ->
+       | [VARG_STRING lang; VARG_VARGLIST o; VARG_IDENTIFIER m] ->
 	   (fun () -> 
 	      let m = Names.string_of_id m in
 	      Ocaml.current_module := m;
-	      let f = (String.uncapitalize m) ^ ".ml" in
-	      let prm = interp_options [] true o in
+	      let f = (String.uncapitalize m) ^ (file_suffix lang) in
+	      let prm = interp_options lang [] true m o in
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
 	      let decls = List.filter (decl_mem rl) decls in
-	      Ocaml.extract_to_file f prm decls)
+	      extract_to_file lang f prm decls)
        | _ -> assert false)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
new file mode 100644
index 000000000..827381d1c
--- /dev/null
+++ b/contrib/extraction/haskell.ml
@@ -0,0 +1,430 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Production of Haskell syntax. *)
+
+open Pp
+open Util
+open Names
+open Term
+open Miniml
+open Mlutil
+open Options
+open Ocaml
+
+let rec collapse_type_app = function
+  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
+  | l -> l
+
+let space_if = function true -> [< 'sTR " " >] | false -> [< >]
+
+let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
+
+(*s Haskell renaming issues. *)
+
+let haskell_keywords =     
+  List.fold_right (fun s -> Idset.add (id_of_string s))
+  [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
+    "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
+    "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
+    "as"; "qualified"; "hiding" ]
+  Idset.empty
+
+let current_ids = ref haskell_keywords
+
+let rec rename_id id avoid = 
+  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+
+let rename_global id = 
+  let id' = rename_id id !current_ids in
+  current_ids := Idset.add id' !current_ids; 
+  id'
+
+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))
+
+let rename_lower_global id = rename_global (lowercase_id id)
+let rename_upper_global id = rename_global (uppercase_id id)
+
+let pr_lower_id id = pr_id (lowercase_id id)
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+let rec rename_vars avoid = function
+  | [] -> 
+      [], avoid
+  | id :: idl when id == prop_name ->
+      (* we don't rename propositions binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
+  | id :: idl ->
+      let id' = rename_id (lowercase_id id) avoid in
+      let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in
+      (id' :: idl', avoid')
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (ids' @ db, avoid')
+
+let empty_env () = ([], !current_ids)
+
+let get_db_name n (db,_) = List.nth db (pred n)
+
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+    the list [id1;...;idn] and the term [t]. *)
+
+let collect_lambda = 
+  let rec collect acc = function
+    | MLlam(id,t) -> collect (id::acc) t
+    | x           -> acc,x
+  in 
+  collect []
+
+let abst = function
+  | [] -> [< >]
+  | l  -> [< 'sTR "\\ ";
+             prlist_with_sep (fun  ()-> [< 'sTR " " >]) pr_id l;
+             'sTR " ->"; 'sPC >]
+
+let pr_binding = function
+  | [] -> [< >]
+  | l  -> [< 'sTR " "; prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l >]
+
+(*s The pretty-printing functor. *)
+
+module Make = functor(P : Mlpp_param) -> struct
+
+let pp_reference f r = 
+  try let s = find_ml_extraction r in [< 'sTR s >]
+  with Not_found -> f r
+ 
+let pp_type_global = pp_reference P.pp_type_global
+let pp_global = pp_reference P.pp_global
+
+(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
+    are needed or not. *)
+
+let rec pp_type par t =
+  let rec pp_rec par = function
+    | Tvar id -> 
+	pr_id (lowercase_id id) (* TODO: possible clash with Haskell kw *)
+    | Tapp l ->
+	(match collapse_type_app l with
+	   | [] -> assert false
+	   | [t] -> pp_rec par t
+	   | t::l -> 
+	       [< open_par par;
+		  pp_rec false t; 'sPC;
+		  prlist_with_sep (fun () -> [< 'sPC >]) (pp_type true) l; 
+		  close_par par >])
+    | Tarr (t1,t2) ->
+	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
+	   pp_rec false t2; close_par par >]
+    | Tglob r -> 
+	pp_type_global r
+    | Tprop ->
+	string "Prop"
+    | Tarity ->
+	string "Arity"
+  in 
+  hOV 0 (pp_rec par t)
+
+(*s Pretty-printing of expressions. [par] indicates whether
+    parentheses are needed or not. [env] is the list of names for the
+    de Bruijn variables. [args] is the list of collected arguments
+    (already pretty-printed). *)
+
+let expr_needs_par = function
+  | MLlam _  -> true
+  | MLcase _ -> true
+  | _        -> false 
+
+let rec pp_expr par env args = 
+  let apply st = match args with
+    | [] -> st
+    | _  -> hOV 2 [< open_par par; st; 'sPC;
+                     prlist_with_sep (fun () -> [< 'sPC >]) (fun s -> s) args;
+                     close_par par >] 
+  in
+  function
+    | MLrel n -> 
+	apply (pr_id (get_db_name n env))
+    | MLapp (f,args') ->
+	let stl = List.map (pp_expr true env []) args' in
+        pp_expr par env (stl @ args) f
+    | MLlam _ as a -> 
+      	let fl,a' = collect_lambda a in
+	let fl,env' = push_vars fl env in
+	let st = [< abst (List.rev fl); pp_expr false env' [] a' >] in
+	if args = [] then
+          [< open_par par; st; close_par par >]
+        else
+          apply [< 'sTR "("; st; 'sTR ")" >]
+    | MLletin (id,a1,a2) ->
+	let id',env' = push_vars [id] env in
+	let par' = par || args <> [] in
+	let par2 = not par' && expr_needs_par a2 in
+	apply 
+	  (hOV 0 [< open_par par';
+		    hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
+			     pp_expr false env [] a1; 'sPC; 'sTR "in" >];
+		    'sPC;
+		    pp_expr par2 env' [] a2;
+		    close_par par' >])
+    | MLglob r -> 
+	apply (pp_global r)
+    | MLcons (r,[]) ->
+	pp_global r
+    | MLcons (r,[a]) ->
+	[< open_par par; pp_global r; 'sPC;
+	   pp_expr true env [] a; close_par par >]
+    | MLcons (r,args') ->
+	[< open_par par; pp_global r; 'sPC;
+	   prlist_with_sep (fun () -> [< 'sPC >]) (pp_expr true env []) args';
+	   close_par par >]
+    | MLcase (t, pv) ->
+      	apply
+      	  [< if args <> [] then [< 'sTR "(" >]  else open_par par;
+      	     v 0 [< 'sTR "case "; pp_expr false env [] t; 'sTR " of";
+		    'fNL; 'sTR "  "; pp_pat env pv >];
+	     if args <> [] then [< 'sTR ")" >] else close_par par >]
+    | MLfix (i,ids,defs) ->
+	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+      	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
+    | MLexn id -> 
+	[< open_par par; 'sTR "error"; 'sPC; 
+	   'qS (string_of_id id); close_par par >]
+    | MLprop ->
+	string "prop"
+    | MLarity ->
+	string "arity"
+    | MLcast (a,t) ->
+	[< open_par true; pp_expr false env args a; 'sPC; 'sTR "::"; 'sPC; 
+	   pp_type false t; close_par true >]
+    | MLmagic a ->
+	[< open_par true; 'sTR "Obj.magic"; 'sPC; 
+	   pp_expr false env args a; close_par true >]
+
+and pp_pat env pv = 
+  let pp_one_pat (name,ids,t) =
+    let ids,env' = push_vars (List.rev ids) env in
+    let par = expr_needs_par t in
+    hOV 2 [< pp_global name;
+	     begin match ids with 
+	       | [] -> [< >]
+	       | _  -> [< 'sTR " "; 
+			  prlist_with_sep 
+			    (fun () -> [< 'sPC >]) pr_id (List.rev ids) >]
+	     end;
+	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
+  in 
+  if pv = [||] then
+    [< 'sTR "_ -> error \"shouldn't happen\" -- empty inductive" >]
+  else
+    [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "  " >]) pp_one_pat pv >]
+
+(*s names of the functions ([ids]) are already pushed in [env],
+    and passed here just for convenience. *)
+
+and pp_fix par env in_p (ids,bl) args =
+  [< open_par par; 
+     v 0 [< 'sTR "let { " ;
+	    prvect_with_sep
+      	      (fun () -> [< 'sTR "; "; 'fNL >])
+	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	      (array_map2 (fun id b -> (id,b)) ids bl);
+	    'sTR " }";'fNL;
+	    match in_p with
+	      | Some j -> 
+      		  hOV 2 [< 'sTR "in "; pr_id ids.(j);
+			   if args <> [] then
+			     [< 'sTR " "; 
+				prlist_with_sep (fun () -> [<'sTR " ">])
+				  (fun s -> s) args >]
+			   else
+			     [< >] >]
+	      | None -> 
+		  [< >] >];
+     close_par par >]
+
+and pp_function env f t =
+  let bl,t' = collect_lambda t in
+  let bl,env' = push_vars bl env in
+  [< f; pr_binding (List.rev bl);
+     'sTR " ="; 'fNL; 'sTR "  ";
+     hOV 2 (pp_expr false env' [] t') >]
+	
+let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let pp_one_inductive (pl,name,cl) =
+  let pp_constructor (id,l) =
+    [< pp_global id;
+       match l with
+         | [] -> [< >] 
+	 | _  -> [< 'sTR " " ;
+      	       	    prlist_with_sep 
+		      (fun () -> [< 'sTR " " >]) (pp_type true) l >] >]
+  in
+  [< 'sTR (if cl = [] then "type " else "data "); 
+     pp_type_global name; 'sTR " ";
+     prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id pl;
+     if pl = [] then [< >] else [< 'sTR " " >];
+     if cl = [] then
+       [< 'sTR "= () -- empty inductive" >]
+     else
+       [< v 0 [< 'sTR "= ";
+		 prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
+                   pp_constructor cl >] >] >]
+
+let pp_inductive il =
+  [< prlist_with_sep (fun () -> [< 'fNL >]) pp_one_inductive il; 'fNL >]
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+  | Dtype ([], _) -> 
+      [< >]
+  | Dtype (i, _) -> 
+      hOV 0 (pp_inductive i)
+  | Dabbrev (r, l, t) ->
+      hOV 0 [< 'sTR "type "; pp_type_global r; 'sPC; 
+	       prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id l;
+	       if l <> [] then [< 'sTR " " >] else [< >]; 'sTR "="; 'sPC;
+	       pp_type false t; 'fNL >]
+  | Dglob (r, MLfix (i,ids,defs)) ->
+      let env = empty_env () in
+      let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+      [< prlist_with_sep (fun () -> [< 'fNL >])
+	   (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
+	   (List.combine (List.rev ids') (Array.to_list defs));
+	 'fNL;
+	 let id = P.rename_global r in
+	 let idi = List.nth (List.rev ids') i in
+	 if id <> idi then
+	   [< 'fNL; pr_id id; 'sTR " = "; pr_id idi; 'fNL >]
+	 else
+	   [< >] >]
+  | Dglob (r, a) ->
+      hOV 0 [< pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+
+let pp_type = pp_type false
+
+end
+
+(*s Renaming issues for a monolithic extraction. *)
+
+module MonoParams = struct
+
+let renamings = Hashtbl.create 97
+
+let cache r f = 
+  try Hashtbl.find renamings r 
+  with Not_found -> let id = f r in Hashtbl.add renamings r id; id
+
+let rename_type_global r =  
+  cache r
+    (fun r -> 
+       let id = Environ.id_of_global (Global.env()) r in
+       rename_upper_global id)
+
+let pp_type_global r = pr_id (rename_type_global r)
+
+let rename_global r = 
+  cache r
+    (fun r -> 
+       let id = Environ.id_of_global (Global.env()) r in
+       match r with
+	 | ConstructRef _ -> rename_upper_global id
+	 | _ -> rename_lower_global id)
+
+let pp_global r = pr_id (rename_global r)
+
+let cofix_warning = true
+
+end
+
+module MonoPp = Make(MonoParams)
+
+(*s Renaming issues in a modular extraction. *)
+
+module ModularParams = struct
+
+  let avoid = 
+    Idset.add (id_of_string "prop")
+      (Idset.add (id_of_string "arity") haskell_keywords)
+
+  let rename_lower id = 
+    if Idset.mem id avoid || id <> lowercase_id id then 
+      "coq_" ^ string_of_id id 
+    else 
+      string_of_id id
+
+  let rename_upper id = 
+    if Idset.mem id avoid || id <> uppercase_id id then 
+      "Coq_" ^ string_of_id id 
+    else 
+      string_of_id id
+
+  let id_of_global r s =
+    let sp = match r with
+      | ConstRef sp -> sp
+      | IndRef (sp,_) -> sp
+      | ConstructRef ((sp,_),_) -> sp
+      | _ -> assert false
+    in
+    let m = list_last (dirpath sp) in
+    id_of_string 
+      (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+
+  let rename_type_global r = 
+    let id = Environ.id_of_global (Global.env()) r in 
+    id_of_global r (rename_upper id)
+
+  let rename_global r = 
+    let id = Environ.id_of_global (Global.env()) r in 
+    match r with
+      | ConstructRef _ -> id_of_global r (rename_upper id)
+      | _ -> id_of_global r (rename_lower id)
+
+  let pp_type_global r = pr_id (rename_type_global r)
+  let pp_global r = pr_id (rename_global r)
+
+  let cofix_warning = true
+end
+
+module ModularPp = Make(ModularParams)
+
+(*s Extraction to a file. *)
+
+let haskell_preamble prm =
+  let m = if prm.modular then String.capitalize prm.module_name else "Main" in
+  [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
+     'sTR "type Prop = ()"; 'fNL;
+     'sTR "prop = ()"; 'fNL; 'fNL;
+     'sTR "type Arity = ()"; 'fNL;
+     'sTR "arity = ()"; 'fNL; 'fNL >]
+
+let extract_to_file f prm decls =
+  let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
+  let cout = open_out f in
+  let ft = Pp_control.with_output_to cout in
+  pP_with ft (hV 0 (haskell_preamble prm));
+  begin 
+    try
+      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
+    with e ->
+      pp_flush_with ft (); close_out cout; raise e
+  end;
+  pp_flush_with ft ();
+  close_out cout
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
new file mode 100644
index 000000000..8e09da5c4
--- /dev/null
+++ b/contrib/extraction/haskell.mli
@@ -0,0 +1,16 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Production of Haskell syntax. *)
+
+open Miniml
+open Mlutil
+
+val extract_to_file : string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index fafdcdd01..6413e1ec4 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -227,6 +227,7 @@ module Refset =
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
+  module_name : string; (* module name if [modular] *)
   optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index abfccc36b..381033a01 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -50,6 +50,7 @@ module Refset : Set.S with type elt = global_reference
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
+  module_name : string; (* module name if [modular] *)
   optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2fdc8c8ac..750afc782 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -115,7 +115,7 @@ let collect_lambda =
 let abst = function
   | [] -> [< >]
   | l  -> [< 'sTR "fun ";
-             prlist_with_sep (fun  ()-> [< 'sTR " " >]) pr_id l;
+             prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l;
              'sTR " ->"; 'sPC >]
 
 let pr_binding = function
@@ -311,35 +311,31 @@ let pp_one_inductive (pl,name,cl) =
          | [] -> [< >] 
 	 | _  -> [< 'sTR " of " ;
       	       	    prlist_with_sep 
-		      (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >]
-    >]
+		      (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >] >]
   in
-    [< pp_parameters pl; pp_global name; 'sTR " ="; 
-       if cl = [] then
-	 [< 'sTR " unit (* empty inductive *)" >]
-       else
-	 [< 'fNL;
-	    v 0 [< 'sTR "    ";
-		   prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
-                     (fun c -> hOV 2 (pp_constructor c)) cl >] >] >]
+  [< pp_parameters pl; pp_type_global name; 'sTR " ="; 
+     if cl = [] then
+       [< 'sTR " unit (* empty inductive *)" >]
+     else
+       [< 'fNL;
+	  v 0 [< 'sTR "    ";
+		 prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
+                   (fun c -> hOV 2 (pp_constructor c)) cl >] >] >]
 
 let pp_inductive il =
   [< 'sTR "type ";
-     prlist_with_sep 
-       (fun () -> [< 'fNL; 'sTR "and " >])
-       (fun i -> pp_one_inductive i)
-       il;
+     prlist_with_sep (fun () -> [< 'fNL; 'sTR "and " >]) pp_one_inductive il;
      'fNL >]
 
 (*s Pretty-printing of a declaration. *)
 
 let warning_coinductive r = 
-  wARN (hOV 0 [< 'sTR "You are trying to extract the CoInductive definition"; 'sPC;
-		 Printer.pr_global r; 'sPC; 'sTR "in Ocaml."; 'sPC; 
-		 'sTR "This is in general NOT a good idea,"; 'sPC; 
-		 'sTR "since Ocaml is not lazy."; 'sPC;
-		 'sTR "You should consider using Haskell instead." >])
-
+  wARN (hOV 0 
+	  [< 'sTR "You are trying to extract the CoInductive definition"; 'sPC;
+	     Printer.pr_global r; 'sPC; 'sTR "in Ocaml."; 'sPC; 
+	     'sTR "This is in general NOT a good idea,"; 'sPC; 
+	     'sTR "since Ocaml is not lazy."; 'sPC;
+	     'sTR "You should consider using Haskell instead." >])
 
 let pp_decl = function
   | Dtype ([], _) -> 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 74d751051..057d909fa 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -8,11 +8,26 @@
 
 (*i $Id$ i*)
 
+(*s Some utility functions to be reused in module [Haskell]. *)
+
+open Pp
+open Miniml
+open Names
+
+val string : string -> std_ppcmds
+val open_par : bool -> std_ppcmds
+val close_par : bool -> std_ppcmds
+
+val collect_lambda : ml_ast -> identifier list * ml_ast
+val push_vars : identifier list -> identifier list * Idset.t ->
+  identifier list * (identifier list * Idset.t)
+
+val current_module : string ref
+
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
     declarations to a file. *)
 
-open Miniml
 open Mlutil
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
index 042418cd3..087fa7d9d 100644
--- a/contrib/extraction/test/.cvsignore
+++ b/contrib/extraction/test/.cvsignore
@@ -3,3 +3,4 @@ ml2v
 v2ml
 log
 
+*.h*