essai d'extraction sous un module

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

4 files changed, 39 insertions, 28 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 63b12abfb2..972c8931c1 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -229,7 +229,8 @@ let mono_environment refs =
     (List.rev l)
 
 let extraction qid = 
-  if is_something_opened () then error_section (); 
+  check_inside_section (); 
+  check_inside_module ();
   let r = Nametab.global qid in 
   if is_custom r then
     msgnl (str "User defined extraction:" ++ spc () ++ 
@@ -248,9 +249,10 @@ let extraction qid =
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
     to get the saturated environment to extract. *)
 
-let mono_extraction (f,m) vl = 
-  if is_something_opened () then error_section (); 
-  let refs = List.map Nametab.global vl in
+let mono_extraction (f,m) qualids = 
+  check_inside_section (); 
+  check_inside_module ();
+  let refs = List.map Nametab.global qualids in
   let prm = {modular=false; mod_name = m; to_appear= refs} in
   let struc = optimize_struct prm None (mono_environment refs) in 
   print_structure_to_file f prm struc; 
@@ -282,7 +284,8 @@ let extraction_file f vl =
 (*s Extraction of a module at the toplevel. *)
 
 let extraction_module m = 
-  if is_something_opened () then error_section (); 
+  check_inside_section (); 
+  check_inside_module ();
   match lang () with 
     | Toplevel -> error_toplevel ()
     | Scheme -> error_scheme ()
@@ -323,7 +326,8 @@ let dir_module_of_id m =
   try Nametab.full_name_module q with Not_found -> error_unknown_module q
 
 let extraction_library is_rec m =
-  if is_something_opened () then error_section (); 
+  check_inside_section (); 
+  check_inside_module ();  
   match lang () with 
     | Toplevel -> error_toplevel ()
     | Scheme -> error_scheme ()
@@ -359,4 +363,3 @@ let extraction_library is_rec m =
 
 
 
-
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 99ce08cd94..7d8bfa9ec5 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -18,7 +18,3 @@ val extraction_rec : reference list -> unit
 val extraction_file : string -> reference list -> unit
 val extraction_module : reference -> unit
 val extraction_library : bool -> identifier -> unit
-
-
-
-
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 529a8e3396..b503ba202b 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -30,10 +30,6 @@ let kn_of_r r = match r with
 
 let current_toplevel () = fst (Lib.current_prefix ())
 
-let is_something_opened () = 
-  try ignore (Lib.what_is_opened ()); true
-  with Not_found -> false
-
 let rec base_mp = function 
   | MPdot (mp,l) -> base_mp mp 
   | mp -> mp 
@@ -147,10 +143,20 @@ let warning_axiom r =
      pr_global r ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
      spc () ++ str "may lead to incorrect or non-terminating ML terms.")
-    
-let error_section () = 
-  err (str "You can't do that within a module or a section." ++ fnl () ++
-       str "Close it and try again.")
+
+let check_inside_module () = 
+  try 
+    ignore (Lib.what_is_opened ()); 
+    Options.if_verbose warning
+      ("Extraction inside an opened module is experimental.\n"^
+       "In case of problem, close it first.\n"); 
+    Pp.flush_all ()
+  with Not_found -> ()
+
+let check_inside_section () = 
+  if Lib.sections_are_opened () then 
+    err (str "You can't do that within a section." ++ fnl () ++
+	 str "Close it and try again.")
 
 let error_constant r = 
   err (Printer.pr_global r ++ str " is not a constant.") 
@@ -236,7 +242,7 @@ let _ = declare_summary "Extraction Lang"
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_module = false;
 	    survive_section = true }  
-
+	  
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 
@@ -254,8 +260,8 @@ let add_inline_entries b l =
   let f b = if b then Refset.add else Refset.remove in 
   let i,k = !inline_table in 
   inline_table := 
-     (List.fold_right (f b) l i), 
-     (List.fold_right (f (not b)) l k)
+  (List.fold_right (f b) l i), 
+  (List.fold_right (f (not b)) l k)
 
 (* Registration of operations for rollback. *)
 
@@ -264,7 +270,9 @@ let (inline_extraction,_) =
     {(default_object "Extraction Inline") with 
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x)}
+       export_function = (fun x -> Some x); 
+       classify_function = (fun (_,o) -> Substitute o); 
+       subst_function = (fun (_,s,(b,l)) -> (b,(List.map (subst_global s) l))) }
 
 let _ = declare_summary "Extraction Inline"
 	  { freeze_function = (fun () -> !inline_table);
@@ -276,7 +284,8 @@ let _ = declare_summary "Extraction Inline"
 (* Grammar entries. *)
 
 let extraction_inline b l =
-  if is_something_opened () then error_section (); 
+  check_inside_section (); 
+  check_inside_module ();
   let refs = List.map Nametab.global l in 
   List.iter 
     (fun r -> match r with 
@@ -348,7 +357,8 @@ let _ = declare_summary "ML extractions"
 (* Grammar entries. *)
 
 let extract_constant_inline inline r ids s =
-  if is_something_opened () then error_section (); 
+  check_inside_section ();
+  check_inside_module ();
   let g = Nametab.global r in 
   match g with 
     | ConstRef kn -> 
@@ -366,7 +376,8 @@ let extract_constant_inline inline r ids s =
 
 
 let extract_inductive r (s,l) =
-  if is_something_opened () then error_section (); 
+  check_inside_section ();
+  check_inside_module ();
   let g = Nametab.global r in 
   match g with
     | IndRef ((kn,i) as ip) ->
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 32aecd6135..5c6029e3e1 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -19,7 +19,6 @@ val id_of_global : global_reference -> identifier
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_axiom : global_reference -> 'a
 val warning_axiom : global_reference -> unit
-val error_section : unit -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
@@ -30,12 +29,14 @@ val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
 val error_unqualified_name : string -> string -> 'a 
 
+val check_inside_module : unit -> unit
+val check_inside_section : unit -> unit
+
 (*s utilities concerning [module_path]. *)
 
 val kn_of_r : global_reference -> kernel_name
 
 val current_toplevel : unit -> module_path
-val is_something_opened : unit -> bool
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool 
 val is_toplevel : module_path -> bool