diff options
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/extract_env.ml | 9 | ||||
-rw-r--r-- | contrib/extraction/g_extraction.ml4 | 17 | ||||
-rw-r--r-- | contrib/extraction/table.ml | 56 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 7 |
4 files changed, 87 insertions, 2 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index aac44a6ff..e59c5811f 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -348,8 +348,13 @@ let mono_filename f = let module_filename m = let d = descr () in - let f = if d.capital_file then String.capitalize else String.uncapitalize in - let fn = f (string_of_id m) in + let fc = String.capitalize (string_of_id m) in + let fn = + if is_blacklisted fc then + if d.capital_file then "Coq_"^fc else "coq_"^fc + else + if d.capital_file then fc else String.uncapitalize fc + in Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m (*s Extraction of one decl to stdout. *) diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index d89d855b3..2b561616b 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -89,6 +89,23 @@ VERNAC COMMAND EXTEND ResetExtractionInline -> [ reset_extraction_inline () ] END +VERNAC COMMAND EXTEND ExtractionBlacklist +(* Force Extraction to not use some filenames *) +| [ "Extraction" "Blacklist" ne_ident_list(l) ] + -> [ extraction_blacklist l ] +END + +VERNAC COMMAND EXTEND PrintExtractionBlacklist +| [ "Print" "Extraction" "Blacklist" ] + -> [ print_extraction_blacklist () ] +END + +VERNAC COMMAND EXTEND ResetExtractionBlacklist +| [ "Reset" "Extraction" "Blacklist" ] + -> [ reset_extraction_blacklist () ] +END + + (* Overriding of a Coq object by an ML one *) VERNAC COMMAND EXTEND ExtractionConstant | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 1612c8dd8..f653b3a48 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -507,6 +507,62 @@ let (reset_inline,_) = let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) +(*s Extraction Blacklist of filenames not to use while extracting *) + +let blacklist_table = ref Stringset.empty + +let is_blacklisted s = + (Stringset.mem (String.capitalize s) !blacklist_table) || + (Stringset.mem (String.uncapitalize s) !blacklist_table) + +let string_of_modfile mp = + let s = string_of_modfile mp in + if is_blacklisted s then "Coq_"^s else s + +let add_blacklist_entries l = + blacklist_table := List.fold_right Stringset.add l !blacklist_table + +(* Registration of operations for rollback. *) + +let (blacklist_extraction,_) = + declare_object + {(default_object "Extraction Blacklist") with + cache_function = (fun (_,l) -> add_blacklist_entries l); + load_function = (fun _ (_,l) -> add_blacklist_entries l); + export_function = (fun x -> Some x); + classify_function = (fun (_,o) -> Libobject.Keep o); + subst_function = (fun (_,_,x) -> x) + } + +let _ = declare_summary "Extraction Blacklist" + { freeze_function = (fun () -> !blacklist_table); + unfreeze_function = ((:=) blacklist_table); + init_function = (fun () -> blacklist_table := Stringset.empty); + survive_module = true; + survive_section = true } + +(* Grammar entries. *) + +let extraction_blacklist l = + let l = List.rev_map string_of_id l in + Lib.add_anonymous_leaf (blacklist_extraction l) + +(* Printing part *) + +let print_extraction_blacklist () = + msgnl + (prlist_with_sep fnl str (Stringset.elements !blacklist_table)) + +(* Reset part *) + +let (reset_blacklist,_) = + declare_object + {(default_object "Reset Extraction Blacklist") with + cache_function = (fun (_,_)-> blacklist_table := Stringset.empty); + load_function = (fun _ (_,_)-> blacklist_table := Stringset.empty); + export_function = (fun x -> Some x)} + +let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) (*s Extract Constant/Inductive. *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index fc29e871c..608eb6771 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -141,6 +141,13 @@ val extract_constant_inline : bool -> reference -> string list -> string -> unit val extract_inductive : reference -> string * string list -> unit +(*s Table of blacklisted filenames *) + +val is_blacklisted : string -> bool + +val extraction_blacklist : identifier list -> unit +val reset_extraction_blacklist : unit -> unit +val print_extraction_blacklist : unit -> unit |