diff options
-rw-r--r-- | contrib/extraction/extract_env.ml | 17 | ||||
-rw-r--r-- | contrib/extraction/extract_env.mli | 4 | ||||
-rw-r--r-- | contrib/extraction/table.ml | 41 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 5 |
4 files changed, 39 insertions, 28 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 63b12abfb..972c8931c 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 99ce08cd9..7d8bfa9ec 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 529a8e339..b503ba202 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 32aecd613..5c6029e3e 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 |