suite et fin (?) de haskell: gestion des modules, mise en place du'un test

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

15 files changed, 627 insertions, 87 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index be8c6948d..4b95ba410 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -21,9 +21,7 @@ open Declare
 
 (*s Modules considerations *)
 
-let current_module = ref None
-
-let used_modules = ref Idset.empty
+let current_module = ref (id_of_string "")
 
 let is_construct = function ConstructRef _ -> true | _ -> false 
 
@@ -54,14 +52,6 @@ let is_long_module d r =
 let short_module r = 
   snd (split_dirpath (library_part r))
 
-let module_option r = 
-  let m = short_module r in
-  if Some m = !current_module then ""
-  else begin 
-    used_modules := Idset.add m !used_modules;
-    (String.capitalize (string_of_id m)) ^ "."
-  end
-
 let check_ml r d = 
   if to_inline r then 
     try 
@@ -69,6 +59,75 @@ let check_ml r d =
     with Not_found -> d
   else d
 
+(*s Get all modules names used in one [ml_decl] list. *)
+
+let ast_get_modules m a = 
+  let rec get_rec a =
+    ast_iter get_rec a;
+    match a with 
+      | MLglob r -> m := Idset.add (short_module r) !m
+      | MLcons (r,l) as a -> 
+	  m := Idset.add (short_module r) !m; 
+      | MLcase (_,v) as a -> 
+	  let r,_,_ = v.(0) in
+	  m := Idset.add (short_module r) !m;
+      | _ -> ()
+  in get_rec a
+
+let mltype_get_modules m t = 
+  let rec get_rec = function 
+    | Tglob r -> m := Idset.add (short_module r) !m
+    | Tapp l -> List.iter get_rec l
+    | Tarr (a,b) -> get_rec a; get_rec b 
+    | _ -> () 
+  in get_rec t
+
+let decl_get_modules ld = 
+  let m = ref Idset.empty in 
+  let one_decl = function 
+    | Dtype (l,_) -> 
+	List.iter (fun (_,_,l) -> 
+		     List.iter (fun (_,l) -> 
+				  List.iter (mltype_get_modules m) l) l) l
+    | Dabbrev (_,_,t) -> mltype_get_modules m t 
+    | Dglob (_,a) -> ast_get_modules m a
+    | _ -> ()
+  in 
+  List.iter one_decl ld; 
+  !m
+
+(*s Does [prop] or [arity] occur ? *)
+
+exception Print_prop
+
+let ast_print_prop a = 
+  let rec get_rec = function 
+    | MLprop | MLarity -> raise Print_prop
+    | a -> ast_iter get_rec a
+  in get_rec a
+
+let mltype_print_prop t = 
+  let rec get_rec = function 
+    | Tprop | Tarity -> raise Print_prop
+    | Tapp l -> List.iter get_rec l
+    | Tarr (a,b) -> get_rec a; get_rec b 
+    | _ -> () 
+  in get_rec t
+
+let decl_print_prop ld = 
+  let one_decl = function 
+    | Dtype (l,_) -> 
+	List.iter (fun (_,_,l) -> 
+		     List.iter (fun (_,l) -> 
+				  List.iter mltype_print_prop l) l) l
+    | Dabbrev (_,_,t) -> mltype_print_prop t 
+    | Dglob (_,a) -> ast_print_prop a
+    | _ -> ()
+  in 
+  try 
+    List.iter one_decl ld; false 
+  with Print_prop -> true
+
 (*s Tables of global renamings *)
 
 let keywords = ref Idset.empty
@@ -86,7 +145,7 @@ module ToplevelParams = struct
   let toplevel = true
   let globals () = Idset.empty
   let rename_global r _ = Termops.id_of_global (Global.env()) r
-  let pp_global r _ = Printer.pr_global r
+  let pp_global r _ _ = Printer.pr_global r
 end
 
 (*s Renaming issues for a monolithic extraction. *)
@@ -110,7 +169,7 @@ module MonoParams = struct
 	   (if upper || (is_construct r) 
 	    then uppercase_id id else lowercase_id id))
       
-  let pp_global r upper = 
+  let pp_global r upper _ = 
     str (check_ml r (string_of_id (rename_global r upper)))
       
 end
@@ -135,7 +194,10 @@ module ModularParams = struct
       if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
 	id_of_string (prefix^(string_of_id id))
       else id'
-    in global_ids := Idset.add id' !global_ids; id'
+    in 
+    if (short_module r) = !current_module then 
+      global_ids := Idset.add id' !global_ids; 
+    id'
 
   let rename_global r upper =
     cache r 
@@ -145,9 +207,16 @@ module ModularParams = struct
 	   rename_global_id r id (uppercase_id id) "Coq_"
 	 else rename_global_id r id (lowercase_id id) "coq_")
 
-  let pp_global r upper = 
-    str
-      (check_ml r ((module_option r)^(string_of_id (rename_global r upper))))
+  let pp_global r upper ctx = 
+    let id = rename_global r upper in 
+    let m = short_module r in
+    let mem id = match ctx with 
+      | None -> true
+      | Some ctx -> Idset.mem id ctx in 
+    let s = if (m <> !current_module) && (mem id) then 
+      (String.capitalize (string_of_id m)) ^ "." ^ (string_of_id id)
+    else (string_of_id id)
+    in str (check_ml r s)
 
 end
 
@@ -167,34 +236,36 @@ let init_global_ids lang =
   Hashtbl.clear renamings;
   keywords := 
   (match lang with 
-     | "ocaml" -> Ocaml.keywords
-     | "haskell" -> Haskell.keywords
-     | _ -> assert false);
-  global_ids := !keywords;
-  used_modules := Idset.empty
+     | Ocaml -> Ocaml.keywords
+     | Haskell -> Haskell.keywords);
+  global_ids := !keywords
 
 let extract_to_file f prm decls =
   cons_cofix := Refset.empty;
   current_module := prm.mod_name;
   init_global_ids prm.lang;
-  let preamble,pp_decl = match prm.lang,prm.mod_name with 
-    | "ocaml", None -> Ocaml.preamble, OcamlMonoPp.pp_decl
-    | "ocaml", _ -> Ocaml.preamble, OcamlModularPp.pp_decl
-    | "haskell", None -> Haskell.preamble, HaskellMonoPp.pp_decl
-    | "haskell", _ -> Haskell.preamble, HaskellModularPp.pp_decl
-    | _ -> assert false
+  let pp_decl = match prm.lang,prm.modular with 
+    | Ocaml, false -> OcamlMonoPp.pp_decl
+    | Ocaml, _ -> OcamlModularPp.pp_decl
+    | Haskell, false -> HaskellMonoPp.pp_decl
+    | Haskell, _ -> HaskellModularPp.pp_decl
   in
-  let pp = prlist_with_sep fnl pp_decl decls in 
+  let preamble,prop_decl,open_str = match prm.lang with 
+    | Ocaml -> Ocaml.preamble, Ocaml.prop_decl, "open "
+    | Haskell -> Haskell.preamble, Haskell.prop_decl, "import qualified "
+  in
+  let used_modules = if prm.modular then 
+    Idset.remove prm.mod_name (decl_get_modules decls)
+  else Idset.empty
+  in 
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
-  if decls <> [] || prm.lang = "haskell" 
-  then msgnl_with ft (hv 0 (preamble prm));
-  Idset.iter (fun m -> msgnl_with ft (str "open " ++ pr_id m)) !used_modules; 
-  msgnl_with ft pp;
-  pp_flush_with ft ();
-  close_out cout  
-
-(*
+  pp_with ft (preamble prm);
+  Idset.iter 
+    (fun m -> msgnl_with ft (str open_str ++ pr_id (uppercase_id m))) 
+    used_modules; 
+  if (decl_print_prop decls) then msgnl_with ft prop_decl
+  else msgnl_with ft (mt()); 
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
@@ -202,5 +273,4 @@ let extract_to_file f prm decls =
       pp_flush_with ft (); close_out cout; raise e
   end;
   pp_flush_with ft ();
-  close_out cout
-*)
+  close_out cout  
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 7d712ce85..361eac76f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -201,8 +201,8 @@ let decl_of_refs refs = List.map extract_declaration (extract_env refs)
 
 let local_optimize refs = 
   let prm = 
-    { lang = "ocaml" ; toplevel = true; 
-      mod_name = None; to_appear = refs} in
+    { lang = Ocaml ; toplevel = true; modular = false;
+      mod_name = id_of_string ""; to_appear = refs} in
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
@@ -262,15 +262,32 @@ let _ =
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
     We just call [extract_to_file] on the saturated environment. *)
 
+let lang_to_lang = function 
+  | "ocaml" -> Ocaml 
+  | "haskell" -> Haskell 
+  | _ -> assert false
+
+let lang_suffix = function 
+  | Ocaml -> "ml"
+  | Haskell -> "hs"
+
+let filename f lang = 
+  let s = lang_suffix lang in 
+  if Filename.check_suffix f s then f,id_of_string (Filename.chop_suffix f s) 
+  else f^"."^s,id_of_string f
+
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
        | VARG_STRING lang :: VARG_STRING f :: vl ->
 	   (fun () -> 
+	      let lang = lang_to_lang lang in 
+	      let f,m = filename f lang in 
 	      let refs = refs_of_vargl vl in
 	      let prm = {lang=lang;
 			 toplevel=false;
-			 mod_name = None;
+			 modular=false; 
+			 mod_name = m;
 			 to_appear= refs} in 
 	      let decls = decl_of_refs refs in 
 	      let decls = add_ml_decls prm decls in 
@@ -289,20 +306,21 @@ let decl_in_m m = function
   | Dcustom (r,_) ->  is_long_module m r
 
 let module_file_name m = function
-  | "ocaml" -> (String.uncapitalize (string_of_id m)) ^ ".ml"
-  | "haskell" -> (String.capitalize (string_of_id m)) ^ ".hs"
-  | _ -> assert false
+  | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
+  | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
 
 let _ = 
   vinterp_add "ExtractionModule"
     (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
+	      let lang = lang_to_lang lang in 
 	      let dir_m = module_of_id m in 
 	      let f = module_file_name m lang in
 	      let prm = {lang=lang;
 			 toplevel=false;
-			 mod_name= Some m;
+			 modular=true;
+			 mod_name= m;
 			 to_appear= []} in 
 	      let rl = extract_module dir_m in 
 	      let decls = optimize prm (decl_of_refs rl) in
@@ -320,13 +338,15 @@ let _ =
         (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
+	      let lang = lang_to_lang lang in 
 	      let dir_m = module_of_id m in 
 	      let modules,refs = 
 		modules_extract_env dir_m in
 	      check_modules modules; 
 	      let dummy_prm = {lang=lang;
 			      toplevel=false;
-			      mod_name= Some m;
+			      modular=true;
+			      mod_name=m;
 			      to_appear= []} in
 	      let decls = optimize dummy_prm (decl_of_refs refs) in
 	      let decls = add_ml_decls dummy_prm decls in
@@ -336,7 +356,8 @@ let _ =
 		   let f = module_file_name short_m lang in 
 		   let prm = {lang=lang;
 			      toplevel=false;
-			      mod_name= Some short_m;
+			      modular=true;
+			      mod_name=short_m;
 			      to_appear= []} in 
 		   let decls = List.filter (decl_in_m m) decls in
 		   if decls <> [] then extract_to_file f prm decls)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index cb3dd32e3..4970a0791 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -32,15 +32,16 @@ let keywords =
   Idset.empty
 
 let preamble prm =
-  let m = match prm.mod_name with 
-    | None -> "Main" 
-    | Some m -> String.capitalize (string_of_id m) 
-  in 
-  (str "module " ++ str m ++ str " where" ++ fnl () ++ fnl () ++
-     str "type Prop = Unit.Unit" ++ fnl () ++
-     str "prop = Unit.unit" ++ fnl () ++ fnl () ++
-     str "data Arity = Unit.Unit" ++ fnl () ++
-     str "arity = Unit.unit" ++ fnl () ++ fnl ())
+  let m = String.capitalize (string_of_id prm.mod_name)   in 
+  str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
+  str "import qualified Prelude" ++ fnl()
+
+let prop_decl = 
+  str "import qualified Unit" ++ fnl () ++ fnl () ++
+  str "type Prop = Unit.Unit" ++ fnl () ++
+  str "prop = Unit.unit" ++ fnl () ++ fnl () ++
+  str "data Arity = Unit.Unit" ++ fnl () ++
+  str "arity = Unit.unit" ++ fnl ()
 
 let pp_abst = function
   | [] -> (mt ())
@@ -52,8 +53,9 @@ let pp_abst = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global r = P.pp_global r true
-let pp_global r = P.pp_global r false
+let pp_type_global r = P.pp_global r true None
+let pp_global r = P.pp_global r false None
+
 let rename_global r = P.rename_global r false
 
 let pr_lower_id id = pr_id (lowercase_id id)
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index beed696d4..73e9e974a 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -17,4 +17,6 @@ val keywords : Idset.t
 
 val preamble : extraction_params -> std_ppcmds
 
+val prop_decl : std_ppcmds
+
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index f4fef3df1..7c72bde37 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -56,15 +56,20 @@ type ml_decl =
   | Dglob   of global_reference * ml_ast
   | Dcustom of global_reference * string
 
+(*s Target language. *)
+
+type lang = Ocaml | Haskell
+
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
     The resulting pretty-printer is a module of type [Mlpp] providing
     functions to print types, terms and declarations. *)
 
 type extraction_params =  
-  { lang : string; 
+  { lang : lang; 
     toplevel : bool; 
-    mod_name : identifier option; 
+    modular : bool; 
+    mod_name : identifier; 
     to_appear : global_reference list }
 
 module type Mlpp_param = sig
@@ -72,7 +77,7 @@ module type Mlpp_param = sig
   val globals : unit -> Idset.t
       (* the bool arg is: should we rename in uppercase or not ? *)
   val rename_global : global_reference -> bool -> identifier
-  val pp_global : global_reference -> bool -> std_ppcmds
+  val pp_global : global_reference -> bool -> Idset.t option -> std_ppcmds
 end
 
 module type Mlpp = sig
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index dd21564ce..d516bb369 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -178,6 +178,21 @@ let ast_map_lift f n = function
   | MLmagic a -> MLmagic (f n a)
   | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a	
 
+(* Iter over asts. *) 
+
+let ast_iter_case f (c,ids,a) = f a
+
+let ast_iter f = function
+  | MLlam (i,a) -> f a
+  | MLletin (i,a,b) -> f a; f b
+  | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v
+  | MLfix (i,ids,v) -> Array.iter f v
+  | MLapp (a,l) -> f a; List.iter f l
+  | MLcons (c,l) -> List.iter f l
+  | MLcast (a,t) -> f a
+  | MLmagic a -> f a
+  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> ()
+
 (*s [occurs k t] returns true if [(Rel k)] occurs in [t]. *)
 
 let occurs k t = 
@@ -763,10 +778,7 @@ let add_ml_decls prm decls =
   let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
   (List.rev l @ decls)
 
-let strict_language = function
-  | "ocaml" -> true
-  | "haskell" -> false
-  | _ -> assert false
+let strict_language = (=) Ocaml
 
 let rec empty_ind = function 
   | [] -> [],[]
@@ -804,7 +816,7 @@ let rec optim prm = function
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
-      if (not b || prm.mod_name <> None || List.mem r prm.to_appear) then 
+      if (not b || prm.modular || List.mem r prm.to_appear) then 
  	  let t = optimize_fix t in
 	  Dglob (r,t) :: (optim prm l)
       else 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index abec7a65d..1b8166b58 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -41,6 +41,8 @@ val clear_singletons : unit -> unit
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn
     lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *)
 
+val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+
 val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 60b0b9689..db64c1e72 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -117,18 +117,22 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "prop" ; "arity" ] 
   Idset.empty
 
-let preamble _ =
-  (str "type prop = unit" ++ fnl () ++
-     str "let prop = ()" ++ fnl () ++ fnl () ++
-     str "type arity = unit" ++ fnl () ++
-     str "let arity = ()" ++ fnl () ++ fnl ())
+let preamble _ = mt()
+
+let prop_decl = 
+  fnl () ++
+  str "type prop = unit" ++ fnl () ++
+  str "let prop = ()" ++ fnl () ++ fnl () ++
+  str "type arity = unit" ++ fnl () ++
+  str "let arity = ()" ++ fnl ()
 
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global r = P.pp_global r false
-let pp_global r = P.pp_global r false
+let pp_type_global r = P.pp_global r false (Some (P.globals()))
+let pp_global r env = P.pp_global r false (Some (snd env))
+let pp_global' r = P.pp_global r false None
 let rename_global r = P.rename_global r false 
 
 let empty_env () = [], P.globals()
@@ -194,28 +198,28 @@ let rec pp_expr par env args =
 			 ++ pp_expr false env [] a1 ++ spc () ++ str "in") ++ 
 		  spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
     | MLglob r -> 
-	apply (pp_global r)
+	apply (pp_global r env )
     | MLcons (r,[]) ->
 	assert (args=[]);
 	if Refset.mem r !cons_cofix then 
-	  (open_par par ++ str "lazy " ++ pp_global r ++ close_par par)
-	else pp_global r
+	  (open_par par ++ str "lazy " ++ pp_global r env ++ close_par par)
+	else pp_global r env
     | MLcons (r,[a]) ->
 	assert (args=[]);
 	if Refset.mem r !cons_cofix then 
 	  (open_par par ++ str "lazy (" ++
-	   pp_global r ++ spc () ++
+	   pp_global r env ++ spc () ++
 	   pp_expr true env [] a ++ str ")" ++ close_par par)
 	else
-	  (open_par par ++ pp_global r ++ spc () ++
+	  (open_par par ++ pp_global r env ++ spc () ++
 	   pp_expr true env [] a ++ close_par par)
     | MLcons (r,args') ->
 	assert (args=[]);
 	if Refset.mem r !cons_cofix then 
-	  (open_par par ++ str "lazy (" ++ pp_global r ++ spc () ++
+	  (open_par par ++ str "lazy (" ++ pp_global r env ++ spc () ++
 	   pp_tuple (pp_expr true env []) args' ++ str ")" ++ close_par par)
 	else
-	  (open_par par ++ pp_global r ++ spc () ++
+	  (open_par par ++ pp_global r env ++ spc () ++
 	   pp_tuple (pp_expr true env []) args' ++ close_par par)
     | MLcase (t,[|(r,_,_) as x|])->
 	let expr = if Refset.mem r !cons_cofix then 
@@ -265,7 +269,7 @@ and pp_one_pat s env (r,ids,t) =
   let args = 
     if ids = [] then (mt ()) 
     else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
-  pp_global r ++ args ++ s ++ spc () ++ pp_expr par env' [] t
+  pp_global r env ++ args ++ s ++ spc () ++ pp_expr par env' [] t
   
 and pp_pat env pv = 
   prvect_with_sep (fun () -> (fnl () ++ str "| ")) 
@@ -330,7 +334,7 @@ let pp_parameters l =
 let pp_one_ind prefix (pl,name,cl) =
   let pl,ren = rename_tvars keywords pl in 
   let pp_constructor (id,l) =
-    (pp_global id ++
+    (pp_global' id ++
        match l with
          | [] -> (mt ()) 
 	 | _  -> (str " of " ++
@@ -387,9 +391,9 @@ let pp_decl = function
       (hov 2 (pp_fix false env' None ([|id|],[|def|]) []))
   | Dglob (r, a) ->
       hov 0 (str "let " ++ 
-	       pp_function (empty_env ()) (pp_global r) a ++ fnl ())
+	       pp_function (empty_env ()) (pp_global' r) a ++ fnl ())
   | Dcustom (r,s) -> 
-      hov 0 (str "let " ++ pp_global r ++ 
+      hov 0 (str "let " ++ pp_global' r ++ 
 	       str " =" ++ spc () ++ str s ++ fnl ())
 
 let pp_type = pp_type false Idmap.empty
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 6a797d15b..7c5855d13 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -44,6 +44,8 @@ val keywords : Idset.t
 
 val preamble : extraction_params -> std_ppcmds
 
+val prop_decl : std_ppcmds
+
 (*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. *)
diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
index 087fa7d9d..fa307db73 100644
--- a/contrib/extraction/test/.cvsignore
+++ b/contrib/extraction/test/.cvsignore
@@ -1,6 +1,7 @@
 theories
 ml2v 
 v2ml
+hs2v
+v2hs
 log
-
-*.h*
+*.hi
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
new file mode 100644
index 000000000..8dc8d0166
--- /dev/null
+++ b/contrib/extraction/test/Makefile.haskell
@@ -0,0 +1,378 @@
+# 
+#	General variables
+#
+
+TOPDIR=../../..
+
+# Files with axioms to be realized: can't be extracted directly
+
+AXIOMSVO:= \
+theories/Init/Prelude.vo \
+theories/Arith/Arith.vo \
+theories/Lists/List.vo \
+theories/Reals/% \
+theories/Reals/Rsyntax.vo \
+theories/Num/% \
+theories/ZArith/Zsyntax.vo
+
+DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
+
+INCL:= $(patsubst %,-i%,$(DIRS))
+
+VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
+
+VO:= $(filter-out $(AXIOMSVO),$(VO))
+
+HS:= $(shell test -x v2hs && ./v2hs $(VO))
+
+O:= $(patsubst %.hs,%.o,$(HS))
+
+#
+#	General rules 
+#
+
+all: v2hs hs Unit.o $(O)
+
+hs: $(HS)
+
+tree:
+	mkdir -p $(DIRS)
+
+%.o:%.hs
+	hbc $(INCL) -c $<
+
+$(HS): hs2v
+	./extract.haskell $@
+
+clean: 
+	rm -f theories/*/*.*
+
+
+#
+#	Utilities
+#
+
+hs2v: hs2v.ml
+	ocamlc -o $@ $<
+
+v2hs: v2hs.ml
+	ocamlc -o $@ $< 
+	$(MAKE) -f Makefile.haskell
+
+
+#
+#	The End
+#
+
+.PHONY: all tree clean depend
+
+# DO NOT DELETE: Beginning of Haskell dependencies
+theories/Arith/Between.o : theories/Arith/Between.hs
+theories/Arith/Compare.o : theories/Arith/Compare.hs
+theories/Arith/Compare.o : theories/Arith/Compare_dec.o
+theories/Arith/Compare.o : theories/Init/Specif.o
+theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs
+theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
+theories/Arith/Compare_dec.o : theories/Init/Logic.o
+theories/Arith/Compare_dec.o : theories/Init/Specif.o
+theories/Arith/Div2.o : theories/Arith/Div2.hs
+theories/Arith/Div2.o : theories/Init/Datatypes.o
+theories/Arith/Div2.o : theories/Init/Peano.o
+theories/Arith/EqNat.o : theories/Arith/EqNat.hs
+theories/Arith/EqNat.o : theories/Init/Datatypes.o
+theories/Arith/EqNat.o : theories/Init/Specif.o
+theories/Arith/Euclid.o : theories/Arith/Compare_dec.o
+theories/Arith/Euclid.o : theories/Arith/Euclid.hs
+theories/Arith/Euclid.o : theories/Arith/Minus.o
+theories/Arith/Euclid.o : theories/Arith/Wf_nat.o
+theories/Arith/Euclid.o : theories/Init/Datatypes.o
+theories/Arith/Euclid.o : theories/Init/Specif.o
+theories/Arith/Even.o : theories/Arith/Even.hs
+theories/Arith/Even.o : theories/Init/Datatypes.o
+theories/Arith/Even.o : theories/Init/Specif.o
+theories/Arith/Gt.o : theories/Arith/Gt.hs
+theories/Arith/Le.o : theories/Arith/Le.hs
+theories/Arith/Lt.o : theories/Arith/Lt.hs
+theories/Arith/Max.o : theories/Arith/Max.hs
+theories/Arith/Max.o : theories/Init/Datatypes.o
+theories/Arith/Max.o : theories/Init/Logic.o
+theories/Arith/Max.o : theories/Init/Specif.o
+theories/Arith/Min.o : theories/Arith/Min.hs
+theories/Arith/Min.o : theories/Init/Datatypes.o
+theories/Arith/Min.o : theories/Init/Logic.o
+theories/Arith/Min.o : theories/Init/Specif.o
+theories/Arith/Minus.o : theories/Arith/Minus.hs
+theories/Arith/Minus.o : theories/Init/Datatypes.o
+theories/Arith/Mult.o : theories/Arith/Mult.hs
+theories/Arith/Mult.o : theories/Arith/Plus.o
+theories/Arith/Mult.o : theories/Init/Datatypes.o
+theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs
+theories/Arith/Peano_dec.o : theories/Init/Datatypes.o
+theories/Arith/Peano_dec.o : theories/Init/Specif.o
+theories/Arith/Plus.o : theories/Arith/Plus.hs
+theories/Arith/Plus.o : theories/Init/Datatypes.o
+theories/Arith/Plus.o : theories/Init/Logic.o
+theories/Arith/Plus.o : theories/Init/Specif.o
+theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs
+theories/Arith/Wf_nat.o : theories/Init/Datatypes.o
+theories/Arith/Wf_nat.o : theories/Init/Logic.o
+theories/Arith/Wf_nat.o : theories/Init/Wf.o
+theories/Bool/Bool.o : theories/Bool/Bool.hs
+theories/Bool/Bool.o : theories/Init/Datatypes.o
+theories/Bool/Bool.o : theories/Init/Specif.o
+theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs
+theories/Bool/BoolEq.o : theories/Init/Datatypes.o
+theories/Bool/BoolEq.o : theories/Init/Specif.o
+theories/Bool/DecBool.o : theories/Bool/DecBool.hs
+theories/Bool/DecBool.o : theories/Init/Specif.o
+theories/Bool/IfProp.o : theories/Bool/IfProp.hs
+theories/Bool/IfProp.o : theories/Init/Datatypes.o
+theories/Bool/IfProp.o : theories/Init/Specif.o
+theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs
+theories/Bool/Sumbool.o : theories/Init/Datatypes.o
+theories/Bool/Sumbool.o : theories/Init/Specif.o
+theories/Bool/Zerob.o : theories/Bool/Zerob.hs
+theories/Bool/Zerob.o : theories/Init/Datatypes.o
+theories/Init/Datatypes.o : theories/Init/Datatypes.hs
+theories/Init/DatatypesSyntax.o : theories/Init/DatatypesSyntax.hs
+theories/Init/Logic.o : theories/Init/Logic.hs
+theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs
+theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs
+theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs
+theories/Init/Peano.o : theories/Init/Datatypes.o
+theories/Init/Peano.o : theories/Init/Peano.hs
+theories/Init/Specif.o : theories/Init/Datatypes.o
+theories/Init/Specif.o : theories/Init/Logic.o
+theories/Init/Specif.o : theories/Init/Specif.hs
+theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs
+theories/Init/Wf.o : theories/Init/Wf.hs
+theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o
+theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
+theories/IntMap/Adalloc.o : theories/Init/Logic.o
+theories/IntMap/Adalloc.o : theories/Init/Specif.o
+theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
+theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
+theories/IntMap/Adalloc.o : theories/IntMap/Map.o
+theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Addec.o : theories/Bool/Sumbool.o
+theories/IntMap/Addec.o : theories/Init/Datatypes.o
+theories/IntMap/Addec.o : theories/Init/Specif.o
+theories/IntMap/Addec.o : theories/IntMap/Addec.hs
+theories/IntMap/Addec.o : theories/IntMap/Addr.o
+theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Addr.o : theories/Bool/Bool.o
+theories/IntMap/Addr.o : theories/Init/Datatypes.o
+theories/IntMap/Addr.o : theories/Init/Specif.o
+theories/IntMap/Addr.o : theories/IntMap/Addr.hs
+theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Adist.o : theories/Arith/Min.o
+theories/IntMap/Adist.o : theories/Init/Datatypes.o
+theories/IntMap/Adist.o : theories/IntMap/Addr.o
+theories/IntMap/Adist.o : theories/IntMap/Adist.hs
+theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs
+theories/IntMap/Fset.o : theories/Init/Datatypes.o
+theories/IntMap/Fset.o : theories/Init/Logic.o
+theories/IntMap/Fset.o : theories/Init/Specif.o
+theories/IntMap/Fset.o : theories/IntMap/Addec.o
+theories/IntMap/Fset.o : theories/IntMap/Addr.o
+theories/IntMap/Fset.o : theories/IntMap/Fset.hs
+theories/IntMap/Fset.o : theories/IntMap/Map.o
+theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Lsort.o : theories/Bool/Sumbool.o
+theories/IntMap/Lsort.o : theories/Init/Datatypes.o
+theories/IntMap/Lsort.o : theories/Init/Logic.o
+theories/IntMap/Lsort.o : theories/Init/Specif.o
+theories/IntMap/Lsort.o : theories/IntMap/Addec.o
+theories/IntMap/Lsort.o : theories/IntMap/Addr.o
+theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
+theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o
+theories/IntMap/Lsort.o : theories/Lists/PolyList.o
+theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Map.o : theories/Init/Datatypes.o
+theories/IntMap/Map.o : theories/Init/Peano.o
+theories/IntMap/Map.o : theories/Init/Specif.o
+theories/IntMap/Map.o : theories/IntMap/Addec.o
+theories/IntMap/Map.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Map.hs
+theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs
+theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
+theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
+theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs
+theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
+theories/IntMap/Mapcard.o : theories/Arith/Plus.o
+theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o
+theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
+theories/IntMap/Mapcard.o : theories/Init/Logic.o
+theories/IntMap/Mapcard.o : theories/Init/Peano.o
+theories/IntMap/Mapcard.o : theories/Init/Specif.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
+theories/IntMap/Mapcard.o : theories/IntMap/Map.o
+theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
+theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
+theories/IntMap/Mapfold.o : theories/Init/Logic.o
+theories/IntMap/Mapfold.o : theories/Init/Specif.o
+theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
+theories/IntMap/Mapfold.o : theories/IntMap/Map.o
+theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs
+theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o
+theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
+theories/IntMap/Mapiter.o : theories/Init/Logic.o
+theories/IntMap/Mapiter.o : theories/Init/Specif.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
+theories/IntMap/Mapiter.o : theories/IntMap/Map.o
+theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
+theories/IntMap/Mapiter.o : theories/Lists/PolyList.o
+theories/IntMap/Maplists.o : theories/Bool/Bool.o
+theories/IntMap/Maplists.o : theories/Bool/Sumbool.o
+theories/IntMap/Maplists.o : theories/Init/Datatypes.o
+theories/IntMap/Maplists.o : theories/Init/Logic.o
+theories/IntMap/Maplists.o : theories/Init/Specif.o
+theories/IntMap/Maplists.o : theories/IntMap/Addec.o
+theories/IntMap/Maplists.o : theories/IntMap/Map.o
+theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o
+theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
+theories/IntMap/Maplists.o : theories/Lists/PolyList.o
+theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
+theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs
+theories/Lists/ListSet.o : theories/Init/Datatypes.o
+theories/Lists/ListSet.o : theories/Init/Logic.o
+theories/Lists/ListSet.o : theories/Init/Specif.o
+theories/Lists/ListSet.o : theories/Lists/ListSet.hs
+theories/Lists/ListSet.o : theories/Lists/PolyList.o
+theories/Lists/PolyList.o : theories/Init/Datatypes.o
+theories/Lists/PolyList.o : theories/Init/Specif.o
+theories/Lists/PolyList.o : theories/Lists/PolyList.hs
+theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs
+theories/Lists/Streams.o : theories/Init/Datatypes.o
+theories/Lists/Streams.o : theories/Lists/Streams.hs
+theories/Lists/TheoryList.o : theories/Bool/DecBool.o
+theories/Lists/TheoryList.o : theories/Init/Datatypes.o
+theories/Lists/TheoryList.o : theories/Init/Specif.o
+theories/Lists/TheoryList.o : theories/Lists/PolyList.o
+theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
+theories/Logic/Berardi.o : theories/Logic/Berardi.hs
+theories/Logic/Classical.o : theories/Logic/Classical.hs
+theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs
+theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs
+theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs
+theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs
+theories/Logic/Decidable.o : theories/Logic/Decidable.hs
+theories/Logic/Elimdep.o : theories/Logic/Elimdep.hs
+theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs
+theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs
+theories/Logic/JMeq.o : theories/Logic/JMeq.hs
+theories/Relations/Newman.o : theories/Relations/Newman.hs
+theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs
+theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs
+theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs
+theories/Relations/Relations.o : theories/Relations/Relations.hs
+theories/Relations/Rstar.o : theories/Relations/Rstar.hs
+theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs
+theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs
+theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs
+theories/Sets/Cpo.o : theories/Sets/Cpo.hs
+theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs
+theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs
+theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs
+theories/Sets/Image.o : theories/Sets/Image.hs
+theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs
+theories/Sets/Integers.o : theories/Sets/Integers.hs
+theories/Sets/Integers.o : theories/Sets/Partial_Order.o
+theories/Sets/Multiset.o : theories/Init/Datatypes.o
+theories/Sets/Multiset.o : theories/Init/Peano.o
+theories/Sets/Multiset.o : theories/Init/Specif.o
+theories/Sets/Multiset.o : theories/Sets/Multiset.hs
+theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs
+theories/Sets/Permut.o : theories/Sets/Permut.hs
+theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
+theories/Sets/Powerset.o : theories/Sets/Powerset.hs
+theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs
+theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs
+theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs
+theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs
+theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs
+theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs
+theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs
+theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs
+theories/Sets/Uniset.o : theories/Bool/Bool.o
+theories/Sets/Uniset.o : theories/Init/Datatypes.o
+theories/Sets/Uniset.o : theories/Init/Specif.o
+theories/Sets/Uniset.o : theories/Sets/Uniset.hs
+theories/Sorting/Heap.o : theories/Init/Logic.o
+theories/Sorting/Heap.o : theories/Init/Specif.o
+theories/Sorting/Heap.o : theories/Lists/PolyList.o
+theories/Sorting/Heap.o : theories/Sets/Multiset.o
+theories/Sorting/Heap.o : theories/Sorting/Heap.hs
+theories/Sorting/Heap.o : theories/Sorting/Sorting.o
+theories/Sorting/Permutation.o : theories/Lists/PolyList.o
+theories/Sorting/Permutation.o : theories/Sets/Multiset.o
+theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
+theories/Sorting/Sorting.o : theories/Init/Logic.o
+theories/Sorting/Sorting.o : theories/Init/Specif.o
+theories/Sorting/Sorting.o : theories/Lists/PolyList.o
+theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs
+theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs
+theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs
+theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs
+theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexicographic_Exponentiation.hs
+theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs
+theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs
+theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs
+theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
+theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
+theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
+theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs
+theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs
+theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o
+theories/ZArith/Fast_integer.o : theories/Init/Peano.o
+theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs
+theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
+theories/ZArith/Wf_Z.o : theories/Init/Logic.o
+theories/ZArith/Wf_Z.o : theories/Init/Peano.o
+theories/ZArith/Wf_Z.o : theories/Init/Specif.o
+theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs
+theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
+theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o
+theories/ZArith/ZArith_dec.o : theories/Init/Logic.o
+theories/ZArith/ZArith_dec.o : theories/Init/Specif.o
+theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
+theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
+theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
+theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
+theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
+theories/ZArith/Zcomplements.o : theories/Init/Logic.o
+theories/ZArith/Zcomplements.o : theories/Init/Specif.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o
+theories/ZArith/Zcomplements.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
+theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs
+theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs
+theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
+theories/ZArith/Zmisc.o : theories/Init/Specif.o
+theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs
+theories/ZArith/Zpower.o : theories/Init/Datatypes.o
+theories/ZArith/Zpower.o : theories/Init/Logic.o
+theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
+# DO NOT DELETE: End of Haskell dependencies
diff --git a/contrib/extraction/test/Unit.hs b/contrib/extraction/test/Unit.hs
new file mode 100644
index 000000000..2001dfa1b
--- /dev/null
+++ b/contrib/extraction/test/Unit.hs
@@ -0,0 +1,5 @@
+module Unit where 
+
+type Unit = ()
+unit = ()
+
diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell
new file mode 100755
index 000000000..ef98a62ed
--- /dev/null
+++ b/contrib/extraction/test/extract.haskell
@@ -0,0 +1,13 @@
+#!/bin/sh
+rm -f /tmp/extr$$.v 
+vfile=`./hs2v $1`
+d=`dirname $vfile`
+n=`basename $vfile .v`
+cat custom/all > /tmp/extr$$.v
+if [ -e custom/$n ]; then cat custom/$n >> /tmp/extr$$.v; fi  
+echo "Cd \"$d\". Haskell Extraction Module $n. " >> /tmp/extr$$.v
+../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
+out=$?
+rm -f /tmp/extr$$.v
+exit $out
+
diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml
new file mode 100644
index 000000000..fd8b9b269
--- /dev/null
+++ b/contrib/extraction/test/hs2v.ml
@@ -0,0 +1,14 @@
+let _ =
+  for j = 1 to ((Array.length Sys.argv)-1) do
+    let fml = Sys.argv.(j) in
+    let f = Filename.chop_extension fml in 
+    let fv = f ^ ".v" in
+    if Sys.file_exists ("../../../" ^ fv) then
+      print_string (fv^" ") 
+    else
+      let d = Filename.dirname f in
+      let b = String.uncapitalize (Filename.basename f) in
+      let fv = Filename.concat d (b ^ ".v ") in
+      print_string fv
+  done;
+  print_newline()
diff --git a/contrib/extraction/test/v2hs.ml b/contrib/extraction/test/v2hs.ml
new file mode 100644
index 000000000..886328754
--- /dev/null
+++ b/contrib/extraction/test/v2hs.ml
@@ -0,0 +1,9 @@
+let _ = 
+  for j = 1 to ((Array.length Sys.argv) -1) do 
+    let s = Sys.argv.(j) in
+    let b = Filename.chop_extension (Filename.basename s) in 
+    let b = String.capitalize b in
+    let d = Filename.dirname s in 
+    print_string (Filename.concat d (b ^ ".hs "))
+  done;	
+  print_newline()