Fin d'optimisation (cas modules) + warning pour coind & ocaml

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

5 files changed, 33 insertions, 15 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e25fa7165b..807c7d4484 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -78,7 +78,7 @@ and visit_inductive eenv inds =
   List.iter visit_ind inds
 
 and visit_decl eenv = function
-  | Dtype inds ->
+  | Dtype (inds,_) ->
       visit_inductive eenv inds
   | Dabbrev (_,_,t) ->
       visit_type eenv t
@@ -191,9 +191,11 @@ let _ =
        | VARG_VARGLIST o :: VARG_STRING f :: vl ->
 	   let refs = refs_of_vargl vl in
 	   let prm = interp_options refs false o in
-	   (fun () -> Ocaml.extract_to_file f prm (decl_of_refs refs))
+	   (fun () -> 
+	      let decls = decl_of_refs refs in 
+	      let decls = optimize prm decls in
+	      Ocaml.extract_to_file 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
@@ -209,12 +211,13 @@ let extract_module m =
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
   in
-  let rl = Util.map_succeed get_reference seg in
-  let rl = 
-    let mlset = ml_extractions () in 
-    List.filter (fun r -> not (Refset.mem r mlset)) rl 
-  in
-  List.map extract_declaration rl
+  Util.map_succeed get_reference seg
+
+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
 
 let _ = 
   vinterp_add "ExtractionModule"
@@ -225,5 +228,8 @@ let _ =
 	      Ocaml.current_module := m;
 	      let f = (String.uncapitalize m) ^ ".ml" in
 	      let prm = interp_options [] true o in
-	      Ocaml.extract_to_file f prm (extract_module m))
+	      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)
        | _ -> assert false)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index e068842579..3ef949550d 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -815,7 +815,7 @@ and extract_inductive_declaration sp =
 		 :: acc )
 	[] mib.mind_packets 
     in
-    Dtype (List.rev l)
+    Dtype (List.rev l, not (mind_type_finite mib 0))
 
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 9c9ad8fe85..26fa7ded81 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -49,7 +49,7 @@ type ml_ast =
 (*s ML declarations. *)
 
 type ml_decl = 
-  | Dtype   of ml_ind list
+  | Dtype   of ml_ind list * bool
   | Dabbrev of global_reference * identifier list * ml_type
   | Dglob   of global_reference * ml_ast
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index aed1285c25..0945b79cb6 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -16,6 +16,7 @@ open Names
 open Term
 open Miniml
 open Mlutil
+open Options
 
 (*s Some utility functions. *)
 
@@ -332,10 +333,19 @@ let pp_inductive il =
 
 (*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." >])
+
+
 let pp_decl = function
-  | Dtype [] -> 
+  | Dtype ([], _) -> 
       [< >]
-  | Dtype i -> 
+  | Dtype ((_,r,_)::_ as i, cofix) -> 
+      if cofix && P.cofix_warning then if_verbose warning_coinductive r; 
       hOV 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
@@ -447,7 +457,6 @@ let ocaml_preamble () =
      'sTR "let arity = ()"; 'fNL; 'fNL >]
 
 let extract_to_file f prm decls =
-  let decls = optimize prm decls in
   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
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 9d91de87b6..14fdf6fdfd 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -47,6 +47,7 @@ $(ML): ml2v
 clean: 
 	rm -f theories/*/*.ml theories/*/*.cm*
 
+
 #
 #	Extraction of Reals
 #
@@ -77,6 +78,7 @@ $(REALSML): realsml
 #	Utilities
 #
 
+	
 ml2v: ml2v.ml
 	ocamlc -o $@ $<
 
@@ -84,6 +86,7 @@ v2ml: v2ml.ml
 	ocamlc -o $@ $< 
 	$(MAKE)
 
+
 #
 #	The End
 #