aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/extract_env.ml17
-rw-r--r--contrib/extraction/extract_env.mli4
-rw-r--r--contrib/extraction/table.ml41
-rw-r--r--contrib/extraction/table.mli5
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-06 18:29:30 +0000