A new command "Separate Extraction"

 This is a mix of "Recursive Extraction" and "Extraction Library":
 - like "Extraction Library", the extracted code is splitted in
   separated files, one per coq source file.
 - unlike "Extraction Library", but similarly to "Recursive Extraction",
   not everything gets extracted, but only dependencies of some
   initially-given elements

 We prepare for a more clever dependency selection inside sub-modules.
 For the moment all needed sub-modules are still fully extracted (other we
 would need to fix signatures accordingly).

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

7 files changed, 116 insertions, 35 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 8a812664f..cb873f2e5 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -64,6 +64,9 @@ module type VISIT = sig
   (* Add the module_path and all its prefixes to the mp visit list *)
   val add_mp : module_path -> unit
 
+  (* Same, but we'll keep all fields of these modules *)
+  val add_mp_all : module_path -> unit
+
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ind : mutual_inductive -> unit
@@ -77,6 +80,7 @@ module type VISIT = sig
   val needed_ind : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
+  val needed_mp_all : module_path -> bool
 end
 
 module Visit : VISIT = struct
@@ -84,16 +88,26 @@ module Visit : VISIT = struct
      (for inductives and modules names) and a Cset_env for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
+      { mutable ind : KNset.t; mutable con : KNset.t;
+	mutable mp : MPset.t; mutable mp_all : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
+  let v = { ind = KNset.empty ; con = KNset.empty ;
+	    mp = MPset.empty; mp_all = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+  let reset () =
+    v.ind <- KNset.empty;
+    v.con <- KNset.empty;
+    v.mp <- MPset.empty;
+    v.mp_all <- MPset.empty
   let needed_ind i = KNset.mem (user_mind i) v.ind
   let needed_con c = KNset.mem (user_con c) v.con
-  let needed_mp mp = MPset.mem mp v.mp
+  let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
+  let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_mp_all mp =
+    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp;
+    v.mp_all <- MPset.add mp v.mp_all
   let add_ind i =
     let kn = user_mind i in
     v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
@@ -220,7 +234,7 @@ let rec extract_sfb_spec env mp = function
 *)
 
 and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
-  | SEBident mp -> Visit.add_mp mp; MTident mp
+  | SEBident mp -> Visit.add_mp_all mp; MTident mp
   | SEBwith(seb',With_definition_body(idl,cb))->
       let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
       let mt = extract_seb_spec env mp1 (seb,seb') in
@@ -228,7 +242,7 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
 	 | None -> mt
 	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
   | SEBwith(seb',With_module_body(idl,mp))->
-      Visit.add_mp mp;
+      Visit.add_mp_all mp;
       MTwith(extract_seb_spec env mp1 (seb,seb'),
 	     ML_With_module(idl,mp))
   | SEBfunctor (mbid, mtb, seb_alg') ->
@@ -309,7 +323,7 @@ and extract_seb env mp all = function
       extract_seb env mp all (expand_seb env mp seb)
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
-      Visit.add_mp mp; MEident mp
+      Visit.add_mp_all mp; MEident mp
   | SEBapply (meb, meb',_) ->
       MEapply (extract_seb env mp true meb,
 	       extract_seb env mp true meb')
@@ -336,11 +350,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 let mono_environment refs mpl =
   Visit.reset ();
   List.iter Visit.add_ref refs;
-  List.iter Visit.add_mp mpl;
+  List.iter Visit.add_mp_all mpl;
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
-    (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l
+    (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m))
+    l
 
 (**************************************)
 (*S Part II : Input/Output primitives *)
@@ -464,10 +479,11 @@ let print_structure_to_file (fn,si,mo) dry struc =
 let reset () =
   Visit.reset (); reset_tables (); reset_renaming_tables Everything
 
-let init modular =
+let init modular library =
   check_inside_section (); check_inside_module ();
   set_keywords (descr ()).keywords;
   set_modular modular;
+  set_library library;
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
@@ -494,23 +510,39 @@ let rec locate_ref = function
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
 let full_extr f (refs,mps) =
-  init false;
+  init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
-  let struc = optimize_struct refs (mono_environment refs mps) in
+  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
   warning_axioms ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
 let full_extraction f lr = full_extr f (locate_ref lr)
 
+(*s Separate extraction is similar to recursive extraction, with the output
+   decomposed in many files, one per Coq .v file *)
+
+let separate_extraction lr =
+  init true false;
+  let refs,mps = locate_ref lr in
+  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warning_axioms ();
+  let print = function
+    | (MPfile dir as mp, sel) as e ->
+	print_structure_to_file (module_filename mp) false [e]
+    | _ -> assert false
+  in
+  List.iter print struc;
+  reset ()
+
 (*s Simple extraction in the Coq toplevel. The vernacular command
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r = match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
-      init false;
-      let struc = optimize_struct [r] (mono_environment [r] []) in
+      init false false;
+      let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
       warning_axioms ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
@@ -523,12 +555,12 @@ let simple_extraction r = match locate_ref [r] with
   \verb!(Recursive) Extraction Library! [M]. *)
 
 let extraction_library is_rec m =
-  init true;
+  init true true;
   let dir_m =
     let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
-  Visit.add_mp (MPfile dir_m);
+  Visit.add_mp_all (MPfile dir_m);
   let env = Global.env () in
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,meb) =
@@ -537,7 +569,7 @@ let extraction_library is_rec m =
     else l
   in
   let struc = List.fold_left select [] l in
-  let struc = optimize_struct [] struc in
+  let struc = optimize_struct ([],[]) struc in
   warning_axioms ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 756069cd6..70783b4f9 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -13,6 +13,7 @@ open Libnames
 
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
+val separate_extraction : reference list -> unit
 val extraction_library : bool -> identifier -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index fb25e7d11..11a2d0e0d 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -63,6 +63,12 @@ VERNAC COMMAND EXTEND Extraction
   -> [ full_extraction (Some f) l ]
 END
 
+VERNAC COMMAND EXTEND SeparateExtraction
+(* Same, with content splitted in several files *)
+| [ "Separate" "Extraction" ne_global_list(l) ]
+  -> [ separate_extraction l ]
+END
+
 (* Modular extraction (one Coq library = one ML module) *)
 VERNAC COMMAND EXTEND ExtractionLibrary
 | [ "Extraction" "Library" ident(m) ]
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index bff28aef1..fd1693d3d 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -26,7 +26,7 @@ let rec msid_of_mt = function
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
 
-let struct_iter do_decl do_spec s =
+let se_iter do_decl do_spec =
   let rec mt_iter = function
     | MTident _ -> ()
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
@@ -56,7 +56,10 @@ let struct_iter do_decl do_spec s =
     | MEapply (me,me') -> me_iter me; me_iter me'
     | MEstruct (msid, sel) -> List.iter se_iter sel
   in
-  List.iter (function (_,sel) -> List.iter se_iter sel) s
+  se_iter
+
+let struct_iter do_decl do_spec s =
+  List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
 
 (*s Apply some fonctions upon all references in [ml_type], [ml_ast],
   [ml_decl], [ml_spec] and [ml_structure]. *)
@@ -234,7 +237,7 @@ let rec optim_se top to_appear s = function
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      if top && i && not (modular ()) && not (List.mem r to_appear)
+      if top && i && not (library ()) && not (List.mem r to_appear)
       then optim_se top to_appear s lse
       else
 	let d = match optimize_fix a with
@@ -252,7 +255,7 @@ let rec optim_se top to_appear s = function
 	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done;
-      if !all && top && not (modular ())
+      if !all && top && not (library ())
 	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
       then optim_se top to_appear s lse
       else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
@@ -269,7 +272,8 @@ and optim_me to_appear s = function
   | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
 
 (* After these optimisations, some dependencies may not be needed anymore.
-   For monolithic extraction, we recompute a minimal set of dependencies. *)
+   For non-library extraction, we recompute a minimal set of dependencies
+   for first-level objects *)
 
 exception NoDepCheck
 
@@ -279,12 +283,16 @@ let base_r = function
   | ConstructRef ((kn,_),_) -> IndRef (kn,0)
   | _ -> assert false
 
-let reset_needed, add_needed, found_needed, is_needed =
-  let needed = ref Refset'.empty in
-  ((fun l -> needed := Refset'.empty),
+let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
+  let needed = ref Refset'.empty
+  and needed_mps = ref MPset.empty in
+  ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty),
    (fun r -> needed := Refset'.add (base_r r) !needed),
+   (fun mp -> needed_mps := MPset.add mp !needed_mps),
    (fun r -> needed := Refset'.remove (base_r r) !needed),
-   (fun r -> Refset'.mem (base_r r) !needed))
+   (fun r ->
+     let r = base_r r in
+     Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps))
 
 let declared_refs = function
   | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
@@ -309,6 +317,15 @@ let compute_deps_decl = function
       (* Todo Later : avoid dependencies when Extract Constant *)
       decl_iter_references add_needed add_needed add_needed d
 
+let compute_deps_spec = function
+  | Sind (kn,ind) ->
+      (* Todo Later : avoid dependencies when Extract Inductive *)
+      ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind
+  | Stype (r,ids,t) ->
+      if not (is_custom r) then Option.iter (type_iter_references add_needed) t
+  | Sval (r,t) ->
+      type_iter_references add_needed t
+
 let rec depcheck_se = function
   | [] -> []
   | ((l,SEdecl d) as t)::se ->
@@ -318,7 +335,10 @@ let rec depcheck_se = function
 	(Array.iter remove_info_axiom rv; se')
       else
 	(Array.iter found_needed rv; compute_deps_decl d; t::se')
-  | _ -> raise NoDepCheck
+  | t :: se ->
+    let se' = depcheck_se se in
+    se_iter compute_deps_decl compute_deps_spec t;
+    t :: se'
 
 let rec depcheck_struct = function
   | [] -> []
@@ -341,13 +361,15 @@ let check_implicits = function
 let optimize_struct to_appear struc =
   let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
   let opt_struc =
-    List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
+    List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
+      struc
   in
   let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
   ignore (struct_ast_search check_implicits opt_struc);
-  try
-    if modular () then raise NoDepCheck;
+  if library () then opt_struc
+  else begin
     reset_needed ();
-    List.iter add_needed to_appear;
+    List.iter add_needed (fst to_appear);
+    List.iter add_needed_mp (snd to_appear);
     depcheck_struct opt_struc
-  with NoDepCheck -> opt_struc
+  end
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 83aea3964..0565522bf 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -36,4 +36,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    optimizations. The first argument is the list of objects we want to appear.
 *)
 
-val optimize_struct : global_reference list -> ml_structure -> ml_structure
+val optimize_struct : global_reference list * module_path list ->
+  ml_structure -> ml_structure
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b9081e286..6d4f06e14 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,13 +175,23 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
-(*s Extraction mode: modular or monolithic *)
+(*s Extraction modes: modular or monolithic, library or minimal ?
+
+Nota:
+ - Recursive Extraction : monolithic, minimal
+ - Separate Extraction : modular, minimal
+ - Extraction Library : modular, library
+*)
 
 let modular_ref = ref false
+let library_ref = ref false
 
 let set_modular b = modular_ref := b
 let modular () = !modular_ref
 
+let set_library b = library_ref := b
+let library () = !library_ref
+
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index f55ae53d8..8c009c662 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -115,11 +115,20 @@ val optims :  unit -> opt_flag
 type lang = Ocaml | Haskell | Scheme
 val lang : unit -> lang
 
-(*s Extraction mode: modular or monolithic *)
+(*s Extraction modes: modular or monolithic, library or minimal ?
+
+Nota:
+ - Recursive Extraction : monolithic, minimal
+ - Separate Extraction : modular, minimal
+ - Extraction Library : modular, library
+*)
 
 val set_modular : bool -> unit
 val modular : unit -> bool
 
+val set_library : bool -> unit
+val library : unit -> bool
+
 (*s Table for custom inlining *)
 
 val to_inline : global_reference -> bool