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.ml87
1 files changed, 47 insertions, 40 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b1a3cb31..6d39faee 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 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Names
open Term
@@ -60,7 +60,6 @@ let at_toplevel mp =
let visible_kn kn = at_toplevel (base_mp (modpath kn))
let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
(*S The main tables: constants, inductives, records, ... *)
(*s Constants tables. *)
@@ -77,9 +76,9 @@ let lookup_type kn = Cmap.find kn !types
(*s Inductives table. *)
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
let init_inductives () = inductives := KNmap.empty
-let add_ind kn m = inductives := KNmap.add kn m !inductives
+let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
@@ -124,11 +123,24 @@ let reset_tables () =
let id_of_global = function
| ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
- | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
- | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
+ | 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 = pr_id (id_of_global r)
+let pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (id_of_global r)
+
+(* idem, but with qualification, and only for constants. *)
+
+let pr_long_global r =
+ try Printer.pr_global r
+ with _ -> match r with
+ | ConstRef kn ->
+ let mp,_,l = repr_con kn in
+ str ((string_of_mp mp)^"."^(string_of_label l))
+ | _ -> assert false
(*S Warning and Error messages. *)
@@ -150,13 +162,13 @@ let warning_log_ax r =
spc () ++ str "may lead to incorrect or non-terminating ML terms.")
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 -> ()
+ if Lib.is_modtype () then
+ err (str "You can't do that within a Module Type." ++ fnl () ++
+ str "Close it and try again.")
+ else if Lib.is_module () then
+ msg_warning
+ (str "Extraction inside an opened module is experimental.\n" ++
+ str "In case of problem, close it first.\n")
let check_inside_section () =
if Lib.sections_are_opened () then
@@ -164,10 +176,10 @@ let check_inside_section () =
str "Close it and try again.")
let error_constant r =
- err (Printer.pr_global r ++ str " is not a constant.")
+ err (pr_global r ++ str " is not a constant.")
let error_inductive r =
- err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+ err (pr_global r ++ spc () ++ str "is not an inductive type.")
let error_nb_cons () =
err (str "Not the right number of constructors.")
@@ -187,23 +199,23 @@ let error_scheme () =
err (str "No Scheme modular extraction available yet.")
let error_not_visible r =
- err (Printer.pr_global r ++ str " is not directly visible.\n" ++
+ err (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_unqualified_name s1 s2 =
- err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
- "in ML from another name sharing the same basename.\n" ^
- "Please do some renaming.\n"))
-
let error_MPfile_as_mod d =
err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
"Extraction cannot currently deal with this situation.\n"))
let error_record r =
- err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+ err (str "Record " ++ 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
+ err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+ | _ -> ()
+
(*S The Extraction auxiliary commands *)
(*s Extraction AutoInline *)
@@ -310,7 +322,7 @@ let _ = declare_summary "Extraction Lang"
{ freeze_function = (fun () -> !lang_ref);
unfreeze_function = ((:=) lang_ref);
init_function = (fun () -> lang_ref := Ocaml);
- survive_module = false;
+ survive_module = true;
survive_section = true }
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
@@ -342,28 +354,21 @@ let (inline_extraction,_) =
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
export_function = (fun x -> Some x);
classify_function = (fun (_,o) -> Substitute o);
- (*CSC: The following substitution may istantiate a realized parameter.
- The right solution would be to make the substitution erase the
- realizer from the table. However, this is not allowed by Coq.
- In this particular case, though, keeping the realizer is place seems
- to be harmless since the current code looks for a realizer only
- when the constant is a parameter. However, if this behaviour changes
- subtle bugs can happear in the future. *)
subst_function =
- (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))}
+ (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+ }
let _ = declare_summary "Extraction Inline"
{ freeze_function = (fun () -> !inline_table);
unfreeze_function = ((:=) inline_table);
init_function = (fun () -> inline_table := empty_inline_table);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extraction_inline b l =
check_inside_section ();
- check_inside_module ();
let refs = List.map Nametab.global l in
List.iter
(fun r -> match r with
@@ -380,11 +385,11 @@ let print_extraction_inline () =
(str "Extraction Inline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
str "Extraction NoInline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ()))
(* Reset part *)
@@ -423,20 +428,23 @@ let (in_customs,_) =
{(default_object "ML extractions") with
cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
- export_function = (fun x -> Some x)}
+ export_function = (fun x -> Some x);
+ classify_function = (fun (_,o) -> Substitute o);
+ subst_function =
+ (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+ }
let _ = declare_summary "ML extractions"
{ freeze_function = (fun () -> !customs);
unfreeze_function = ((:=) customs);
init_function = (fun () -> customs := Refmap.empty);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extract_constant_inline inline r ids s =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| ConstRef kn ->
@@ -455,7 +463,6 @@ let extract_constant_inline inline r ids s =
let extract_inductive r (s,l) =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| IndRef ((kn,i) as ip) ->
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-04 15:14:43 +0000