aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 15:37:46 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 15:37:46 +0000
commit695bf462bba223c8870634bac7cb149ffb0b28b6 (patch)
tree5ace99c11a8dc151e48fd6dc61e6c8bb9494ad98 /plugins
parent8c376b71eb6ebc72ec44fd980dc282b8796299c7 (diff)
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
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extract_env.ml66
-rw-r--r--plugins/extraction/extract_env.mli1
-rw-r--r--plugins/extraction/g_extraction.ml46
-rw-r--r--plugins/extraction/modutil.ml52
-rw-r--r--plugins/extraction/modutil.mli3
-rw-r--r--plugins/extraction/table.ml12
-rw-r--r--plugins/extraction/table.mli11
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