From 695bf462bba223c8870634bac7cb149ffb0b28b6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 7 Mar 2011 15:37:46 +0000 Subject: 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 --- plugins/extraction/extract_env.ml | 66 +++++++++++++++++++++++++++---------- plugins/extraction/extract_env.mli | 1 + plugins/extraction/g_extraction.ml4 | 6 ++++ plugins/extraction/modutil.ml | 52 ++++++++++++++++++++--------- plugins/extraction/modutil.mli | 3 +- plugins/extraction/table.ml | 12 ++++++- plugins/extraction/table.mli | 11 ++++++- 7 files changed, 116 insertions(+), 35 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3