diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 5 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 25 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 87 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 9 |
4 files changed, 66 insertions, 60 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index e31b701c..825b3554 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*) +(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*) open Term open Declarations @@ -92,7 +92,8 @@ module Visit : VISIT = struct let needed_kn kn = KNset.mem kn v.kn let needed_con c = Cset.mem c v.con let needed_mp mp = MPset.mem mp v.mp - let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_mp mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) let add_ref = function diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6fd4a3cc..6982ffc6 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*) +(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*) (*i*) open Util @@ -31,10 +31,6 @@ open Mlutil exception I of inductive_info -(* A set of all inductive currently being computed, - to avoid loops in [extract_inductive] *) -let internal_call = ref KNset.empty - (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : constant list) @@ -303,13 +299,15 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) and extract_ind env kn = (* kn is supposed to be in long form *) - try - if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *) - else if visible_kn kn then lookup_ind kn (* Standard situation. *) - else raise Not_found (* Never trust the table for a internal kn. *) + let mib = Environ.lookup_mind kn env in + try + (* For a same kn, we can get various bodies due to module substitutions. + We hence check that the mib has not changed from recording + time to retrieving time. Ideally we should also check the env. *) + let (mib0,ml_ind) = lookup_ind kn in + if not (mib = mib0) then raise Not_found; + ml_ind with Not_found -> - internal_call := KNset.add kn !internal_call; - let mib = Environ.lookup_mind kn env in (* First, if this inductive is aliased via a Module, *) (* we process the original inductive. *) option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; @@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_types = t }) mib.mind_packets in - add_ind kn + add_ind kn mib {ind_info = Standard; ind_nparams = npar; ind_packets = packets; @@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ind_packets = packets; ind_equiv = mib.mind_equiv} in - add_ind kn i; - internal_call := KNset.remove kn !internal_call; + add_ind kn mib i; i (*s [extract_type_cons] extracts the type of an inductive 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) -> diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 66662138..c9a4e8da 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*) +(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*) open Names open Libnames open Miniml +open Declarations val id_of_global : global_reference -> identifier @@ -27,11 +28,11 @@ val error_unknown_module : qualid -> 'a val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_unqualified_name : string -> string -> 'a val error_MPfile_as_mod : dir_path -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit +val check_loaded_modfile : module_path -> unit (*s utilities concerning [module_path]. *) @@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl val add_type : constant -> ml_schema -> unit val lookup_type : constant -> ml_schema -val add_ind : kernel_name -> ml_ind -> unit -val lookup_ind : kernel_name -> ml_ind +val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool |