réparation Correctness; options Extraction (changement de syntaxe)

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

4 files changed, 21 insertions, 19 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index c4c62b3cbe..e909d45111 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -12,10 +12,10 @@ Grammar vernac vernac : ast :=
 | extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
 | extr_list   
-     [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] 
+     [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] 
   -> [ (ExtractionFile $o $f ($LIST $l)) ]
 | extr_module 
-     [ "Extraction" options($o) "Module" identarg($m) "." ]
+     [ "Extraction" "Module" options($o) identarg($m) "." ]
   -> [ (ExtractionModule $o $m) ]
 
 | extract_constant 
@@ -39,7 +39,7 @@ with idorstring : ast :=
 | ids_string [ stringarg($s) ] -> [ $s ]
 
 with options : ast :=
-| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ]
-| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> 
+| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ]
+| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> 
                 [ (VERNACARGLIST "expand" ($LIST $l)) ]
 | ext_opt_none  [ ] -> [ (VERNACARGLIST "nooption") ].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index b0bb1ad3a9..6165910487 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -161,13 +161,13 @@ let _ =
 
 let interp_options keep modular = function
   | [VARG_STRING "noopt"] ->
-      { no_opt = true; modular = modular; 
+      { optimization = false; modular = modular; 
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | [VARG_STRING "nooption"] ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | VARG_STRING "expand" :: l ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; 
 	to_expand = refs_set_of_list (refs_of_vargl l) }
   | _ -> 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 4b04c4dec1..b7a07c7060 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -202,26 +202,29 @@ module Refset =
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }
 
-let ml_subst_glob r m = 
+let subst_glob_ast r m = 
   let rec substrec = function
     | MLglob r' as t -> if r = r' then m else t
     | t -> ast_map substrec t
   in
   substrec
 
-let expand r m = function
-  | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t')
+let subst_glob_decl r m = function
+  | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
 let normalize = betared_ast
 
-let keep prm r t' = true
-  (* prm.no_opt || Refset.mem r prm.to_keep *)
+let expansion_test r t = false
+
+let expand prm r t = 
+  (not (Refset.mem r prm.to_keep)) &&
+  (Refset.mem r prm.to_expand || (prm.optimization && expansion_test r t))
 
 let warning_expansion r = 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
@@ -240,13 +243,12 @@ let rec optimize prm = function
       let t' = normalize t in [ Dglob(r,t') ]
   | Dglob(r,t) as d :: l ->
       let t' = normalize t in
-      if keep prm r t' then
-	(Dglob(r,t')) :: (optimize prm l)
-      else begin
+      if expand prm r t' then begin
 	warning_expansion r;
-	let l' = List.map (expand r t') l in
+	let l' = List.map (subst_glob_decl r t') l in
         optimize prm l'
-      end
+      end else 
+	(Dglob(r,t')) :: (optimize prm l)
 
 (*s Table for direct ML extractions. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index af931b6486..f4aae3b7fc 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -45,7 +45,7 @@ module Refset : Set.S with type elt = global_reference
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }