summaryrefslogtreecommitdiff
path: root/contrib/extraction/table.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/table.ml')
-rw-r--r--contrib/extraction/table.ml158
1 files changed, 117 insertions, 41 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 10f669e1..c675a744 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml 11262 2008-07-24 20:59:29Z letouzey $ i*)
+(*i $Id: table.ml 11844 2009-01-22 16:45:06Z letouzey $ i*)
open Names
open Term
@@ -52,7 +52,7 @@ let is_modfile = function
| MPfile _ -> true
| _ -> false
-let string_of_modfile = function
+let raw_string_of_modfile = function
| MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
| _ -> assert false
@@ -76,24 +76,15 @@ let rec prefixes_mp mp = match mp with
| MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
| _ -> MPset.singleton mp
-let rec get_nth_label_mp n mp = match mp with
- | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
+let rec get_nth_label_mp n = function
+ | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
| _ -> failwith "get_nth_label: not enough MPdot"
-let get_nth_label n r =
- if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r)
-
-let rec common_prefix prefixes_mp1 mp2 =
- if MPset.mem mp2 prefixes_mp1 then mp2
- else match mp2 with
- | MPdot (mp,_) -> common_prefix prefixes_mp1 mp
- | _ -> raise Not_found
-
let common_prefix_from_list mp0 mpl =
- let prefixes_mp0 = prefixes_mp mp0 in
+ let prefixes = prefixes_mp mp0 in
let rec f = function
| [] -> raise Not_found
- | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+ | mp :: l -> if MPset.mem mp prefixes then mp else f l
in f mpl
let rec parse_labels ll = function
@@ -185,39 +176,39 @@ let modular_ref = ref false
let set_modular b = modular_ref := b
let modular () = !modular_ref
-(*s Tables synchronization. *)
-
-let reset_tables () =
- init_terms (); init_types (); init_inductives (); init_recursors ();
- init_projs (); init_axioms ()
-
(*s Printing. *)
(* The following functions work even on objects not in [Global.env ()].
WARNING: for inductive objects, an extract_inductive must have been
done before. *)
-let id_of_global = function
+let safe_id_of_global = function
| ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
| IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
| ConstructRef ((kn,i),j) ->
(snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
| _ -> assert false
-let pr_global r =
- try Printer.pr_global r
- with _ -> pr_id (id_of_global r)
+let safe_pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (safe_id_of_global r)
(* idem, but with qualification, and only for constants. *)
-let pr_long_global r =
- try Printer.pr_global r
+let safe_pr_long_global r =
+ try Printer.pr_global r
with _ -> match r with
- | ConstRef kn ->
- let mp,_,l = repr_con kn in
+ | ConstRef kn ->
+ let mp,_,l = repr_con kn in
str ((string_of_mp mp)^"."^(string_of_label l))
| _ -> assert false
+let pr_long_mp mp =
+ let lid = repr_dirpath (Nametab.dir_of_mp mp) in
+ str (String.concat "." (List.map string_of_id (List.rev lid)))
+
+let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+
(*S Warning and Error messages. *)
let err s = errorlabstrm "Extraction" s
@@ -229,7 +220,7 @@ let warning_axioms () =
let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
msg_warning
(str ("The following "^s^" must be realized in the extracted code:")
- ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms)
+ ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
++ str "." ++ fnl ())
end;
let log_axioms = Refset.elements !log_axioms in
@@ -239,15 +230,27 @@ let warning_axioms () =
in
msg_warning
(str ("The following logical "^s^" encountered:") ++
- hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++
+ hov 1
+ (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
+ ++
str "Having invalid logical axiom in the environment when extracting" ++
spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
fnl ())
end
+let warning_both_mod_and_cst q mp r =
+ msg_warning
+ (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
+ str "do you mean module " ++
+ pr_long_mp mp ++
+ str " or object " ++
+ pr_long_global r ++ str " ?" ++ fnl () ++
+ str "First choice is assumed, for the second one please use " ++
+ str "fully qualified name." ++ fnl ())
+
let error_axiom_scheme r i =
err (str "The type scheme axiom " ++ spc () ++
- pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+ safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
str " type variable(s).")
let check_inside_module () =
@@ -265,10 +268,10 @@ let check_inside_section () =
str "Close it and try again.")
let error_constant r =
- err (pr_global r ++ str " is not a constant.")
+ err (safe_pr_global r ++ str " is not a constant.")
let error_inductive r =
- err (pr_global r ++ spc () ++ str "is not an inductive type.")
+ err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
let error_nb_cons () =
err (str "Not the right number of constructors.")
@@ -284,21 +287,21 @@ let error_scheme () =
err (str "No Scheme modular extraction available yet.")
let error_not_visible r =
- err (pr_global r ++ str " is not directly visible.\n" ++
+ err (safe_pr_global r ++ str " is not directly visible.\n" ++
str "For example, it may be inside an applied functor." ++
str "Use Recursive Extraction to get the whole environment.")
let error_MPfile_as_mod mp b =
let s1 = if b then "asked" else "required" in
let s2 = if b then "extract some objects of this module or\n" else "" in
- err (str ("Extraction of file "^(string_of_modfile mp)^
+ err (str ("Extraction of file "^(raw_string_of_modfile mp)^
".v as a module is "^s1^".\n"^
"Monolithic Extraction cannot deal with this situation.\n"^
"Please "^s2^"use (Recursive) Extraction Library instead.\n"))
-let error_record r =
- err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
- str "To help extraction, please use an explicit name.")
+let error_record r =
+ err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
+ fnl () ++ str "To help extraction, please use an explicit name.")
let check_loaded_modfile mp = match base_mp mp with
| MPfile dp -> if not (Library.library_is_loaded dp) then
@@ -481,11 +484,11 @@ let print_extraction_inline () =
(str "Extraction Inline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
+ (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
str "Extraction NoInline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ()))
+ (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
(* Reset part *)
@@ -498,6 +501,73 @@ 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 Idset.empty
+
+let modfile_ids = ref []
+let modfile_mps = ref MPmap.empty
+
+let reset_modfile () =
+ modfile_ids := Idset.elements !blacklist_table;
+ modfile_mps := MPmap.empty
+
+let string_of_modfile mp =
+ try MPmap.find mp !modfile_mps
+ with Not_found ->
+ let id = id_of_string (raw_string_of_modfile mp) in
+ let id' = next_ident_away id !modfile_ids in
+ let s' = string_of_id id' in
+ modfile_ids := id' :: !modfile_ids;
+ modfile_mps := MPmap.add mp s' !modfile_mps;
+ s'
+
+let add_blacklist_entries l =
+ blacklist_table :=
+ List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
+ 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 := Idset.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 pr_id (Idset.elements !blacklist_table))
+
+(* Reset part *)
+
+let (reset_blacklist,_) =
+ declare_object
+ {(default_object "Reset Extraction Blacklist") with
+ cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
+ load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
+ export_function = (fun x -> Some x)}
+
+let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
(*s Extract Constant/Inductive. *)
@@ -575,3 +645,9 @@ let extract_inductive r (s,l) =
| _ -> error_inductive g
+
+(*s Tables synchronization. *)
+
+let reset_tables () =
+ init_terms (); init_types (); init_inductives (); init_recursors ();
+ init_projs (); init_axioms (); reset_modfile ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 22:32:25 +0000