diff options
39 files changed, 506 insertions, 98 deletions
diff --git a/.depend.newcoq b/.depend.newcoq index 455ce85ce..a7299c237 100644 --- a/.depend.newcoq +++ b/.depend.newcoq @@ -60,6 +60,14 @@ newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Notations newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Datatypes.vo newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Specif.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo +newtheories/Init/Notations.vo: newtheories/Init/Notations.v +newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v newtheories/Init/Notations.vo +newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo +newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo +newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo +newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo +newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Datatypes.vo +newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Specif.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo newtheories/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v newtheories/Logic/ProofIrrelevance.vo: newtheories/Logic/ProofIrrelevance.v newtheories/Logic/Hurkens.vo newtheories/Logic/Classical.vo: newtheories/Logic/Classical.v newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Set.vo @@ -263,5 +271,4 @@ newcontrib/correctness/Sorted.vo: newcontrib/correctness/Sorted.v newcontrib/cor newcontrib/correctness/Tuples.vo: newcontrib/correctness/Tuples.v newcontrib/fourier/Fourier_util.vo: newcontrib/fourier/Fourier_util.v newtheories/Reals/Rbase.vo newcontrib/fourier/Fourier.vo: newcontrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo newcontrib/fourier/Fourier_util.vo newcontrib/field/Field.vo newtheories/Reals/DiscrR.vo -newcontrib/interface/Centaur.vo: newcontrib/interface/Centaur.v newcontrib/cc/CC.vo: newcontrib/cc/CC.v newtheories/Logic/Eqdep_dec.vo diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml index 6d96df032..237df88a2 100644 --- a/contrib/correctness/penv.ml +++ b/contrib/correctness/penv.ml @@ -100,6 +100,7 @@ Summary.declare_summary "programs-environment" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } ;; diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index a7ed13863..529a8e339 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -234,6 +234,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_section = true } let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) @@ -269,6 +270,7 @@ 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_section = true } (* Grammar entries. *) @@ -340,6 +342,7 @@ let _ = declare_summary "ML extractions" { freeze_function = (fun () -> !customs); unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap.empty); + survive_module = false; survive_section = true } (* Grammar entries. *) diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index c5ec4df87..437fb0fff 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -53,6 +53,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } let load_addfield _ = () diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 26c76e594..b46d15c4b 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -433,7 +433,7 @@ let load_syntax_action reqid module_name = (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in read_library (dummy_loc,qid); msg (str "opening... "); - Declaremods.import_module (Nametab.locate_module qid); + Declaremods.import_module false (Nametab.locate_module qid); msgnl (str "done" ++ fnl ()); ()) with diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index ac3274ae7..f73cc164b 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -181,6 +181,7 @@ let _ = { Summary.freeze_function = (fun () -> !theories_map); Summary.unfreeze_function = (fun t -> theories_map := t); Summary.init_function = (fun () -> theories_map := Cmap.empty); + Summary.survive_module = false; Summary.survive_section = false } (* declare a new type of object in the environment, "tactic-ring-theory" diff --git a/dev/objects.el b/dev/objects.el index 46ea2dea0..b3a2694d2 100644 --- a/dev/objects.el +++ b/dev/objects.el @@ -1,3 +1,15 @@ +(defun add-survive-module nil + (interactive) + (query-replace-regexp + " +\\([ ]*\\)\\(Summary\.\\)?survive_section" + " +\\1\\2survive_module = false; +\\1\\2survive_section") + ) + +(global-set-key [f2] 'add-survive-module) + ; functions to change old style object declaration to new style (defun repl-open nil diff --git a/interp/reserve.ml b/interp/reserve.ml index d2c84abdf..dc7393c67 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -21,6 +21,7 @@ let _ = { Summary.freeze_function = (fun () -> !reserve_table); Summary.unfreeze_function = (fun r -> reserve_table := r); Summary.init_function = (fun () -> reserve_table := Idmap.empty); + Summary.survive_module = false; Summary.survive_section = false } let declare_reserved_type id t = diff --git a/interp/symbols.ml b/interp/symbols.ml index 3ddb8644f..d1d2d0c84 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -589,4 +589,5 @@ let _ = { freeze_function = freeze; unfreeze_function = unfreeze; init_function = init; + survive_module = false; survive_section = false } diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 69094507d..4b9c32e4f 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -26,6 +26,7 @@ let _ = Summary.declare_summary { Summary.freeze_function = (fun () -> !syntax_table); Summary.unfreeze_function = (fun ft -> syntax_table := ft); Summary.init_function = (fun () -> syntax_table := KNmap.empty); + Summary.survive_module = false; Summary.survive_section = false } let add_syntax_constant kn c = diff --git a/library/declare.ml b/library/declare.ml index 3dc97e0ba..d017b7ea5 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -77,6 +77,7 @@ let _ = Summary.declare_summary "VARIABLE" { Summary.freeze_function = (fun () -> !vartab); Summary.unfreeze_function = (fun ft -> vartab := ft); Summary.init_function = (fun () -> vartab := Idmap.empty); + Summary.survive_module = false; Summary.survive_section = false } let cache_variable ((sp,_),(id,(p,d,mk))) = @@ -128,6 +129,7 @@ let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); Summary.unfreeze_function = (fun ft -> csttab := ft); Summary.init_function = (fun () -> csttab := Spmap.empty); + Summary.survive_module = false; Summary.survive_section = false } let cache_constant ((sp,kn),(cdt,kind)) = diff --git a/library/declaremods.ml b/library/declaremods.ml index 8d7a783fc..305024c3d 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -93,6 +93,7 @@ let _ = Summary.declare_summary "MODULE-INFO" modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ([],None,None)); + Summary.survive_module = false; Summary.survive_section = false } (* auxiliary functions to transform section_path and kernel_name given @@ -300,6 +301,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" Summary.init_function = (fun () -> modtypetab := KNmap.empty; openmodtype_info := []); + Summary.survive_module = false; Summary.survive_section = true } @@ -519,7 +521,7 @@ let end_module id = (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) - Summary.unfreeze_other_summaries fs; + Summary.module_unfreeze_summaries fs; let substituted = subst_substobjs dir mp substobjs in let node = in_module (None,substobjs,substituted) in @@ -545,6 +547,10 @@ let module_objects mp = segment_of_objects prefix objects + +(***********************************************************************) +(* libraries *) + type library_name = dir_path (* The first two will form substitutive_objects, the last one is keep *) @@ -587,7 +593,7 @@ let start_library dir = Lib.add_frozen_state () -let export_library dir = +let end_library dir = let prefix, lib_stack = Lib.end_compilation dir in let cenv = Global.export dir in let msid = msid_of_prefix prefix in @@ -595,38 +601,40 @@ let export_library dir = cenv,(msid,substitute,keep) +(* implementation of Export M and Import M *) -let do_open_export (_,(_,mp)) = -(* for non-substitutive exports: - let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) + +let really_import_module mp = let prefix,objects = MPmap.find mp !modtab_objects in open_objects 1 prefix objects -let classify_export (_,(export,_ as obj)) = + +let cache_import (_,(_,mp)) = +(* for non-substitutive exports: + let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) + really_import_module mp + +let classify_import (_,(export,_ as obj)) = if export then Substitute obj else Dispose -let subst_export (_,subst,(export,mp as obj)) = +let subst_import (_,subst,(export,mp as obj)) = let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') -let (in_export,out_export) = - declare_object {(default_object "EXPORT MODULE") with - cache_function = do_open_export; - open_function = (fun i o -> if i=1 then do_open_export o); - subst_function = subst_export; - classify_function = classify_export } +let (in_import,out_import) = + declare_object {(default_object "IMPORT MODULE") with + cache_function = cache_import; + open_function = (fun i o -> if i=1 then cache_import o); + subst_function = subst_import; + classify_function = classify_import } -let export_module mp = -(* for non-substitutive exports: - let dir = Nametab.dir_of_mp mp in *) - Lib.add_anonymous_leaf (in_export (true,mp)) +let import_module export mp = + Lib.add_anonymous_leaf (in_import (export,mp)) -let import_module mp = - let prefix,objects = MPmap.find mp !modtab_objects in - open_objects 1 prefix objects - +(************************************************************************) +(* module types *) let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in @@ -654,7 +662,7 @@ let end_modtype id = let msid = msid_of_prefix prefix in let mbids = !openmodtype_info in - Summary.unfreeze_other_summaries fs; + Summary.module_unfreeze_summaries fs; let modtypeobjs = empty_subst, mbids, msid, substitute in diff --git a/library/declaremods.mli b/library/declaremods.mli index dfcf9dfc5..94144d625 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -79,20 +79,22 @@ val register_library : val start_library : library_name -> unit -val export_library : +val end_library : library_name -> Safe_typing.compiled_library * library_objects -(* [import_module mp] opens the module [mp] (in a Caml sense). - It modifies Nametab and performs the "open_object" function - for every object of the module. *) +(* [really_import_module mp] opens the module [mp] (in a Caml sense). + It modifies Nametab and performs the "open_object" function for + every object of the module. *) -val import_module : module_path -> unit +val really_import_module : module_path -> unit -(* [export_module mp] is similar, but is run when the module - containing it is imported *) +(* [import_module export mp] is a synchronous version of + [really_import_module]. If [export] is [true], the module is also + opened every time the module containing it is. *) + +val import_module : bool -> module_path -> unit -val export_module : module_path -> unit (*s [fold_all_segments] and [iter_all_segments] iterate over all segments, the modules' segments first and then the current diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 5241bf035..9d940fcd0 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -56,4 +56,5 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = true } diff --git a/library/global.ml b/library/global.ml index 4824f0b2f..8b61c9a4a 100644 --- a/library/global.ml +++ b/library/global.ml @@ -26,10 +26,11 @@ let safe_env () = !global_env let env () = env_of_safe_env !global_env let _ = - declare_global_environment + declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := empty_environment); + survive_module = true; survive_section = false } (* Then we export the functions of [Typing] on that environment. *) diff --git a/library/goptions.ml b/library/goptions.ml index 1b29721c1..111448cf1 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -88,6 +88,7 @@ module MakeTable = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = true } let (add_option,remove_option) = @@ -250,6 +251,7 @@ let declare_option cast uncast {freeze_function = read; unfreeze_function = write; init_function = (fun () -> write default); + survive_module = false; survive_section = true} in fun v -> add_anonymous_leaf (decl_obj v) diff --git a/library/impargs.ml b/library/impargs.ml index 831b34e05..86a93e935 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -539,6 +539,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } (* Remark: flags implicit_args, contextual_implicit_args @@ -569,4 +570,5 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = true } diff --git a/library/lib.ml b/library/lib.ml index 179e51bf8..f456f2410 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -363,6 +363,18 @@ let is_modtype () = with Not_found -> false +(* Returns true if we are inside an opened module *) +let is_module () = + let opened_p = function + | _, OpenedModule _ -> true + | _ -> false + in + try + let _ = find_entry_p opened_p in true + with + Not_found -> false + + (* Returns the most recent OpenedThing node *) let what_is_opened () = find_entry_p is_something_opened diff --git a/library/lib.mli b/library/lib.mli index e16f44af8..d9448f310 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -89,6 +89,7 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool +val is_module : unit -> bool (* Returns the most recent OpenedThing node *) diff --git a/library/library.ml b/library/library.ml index 29fcb61c6..bc7404344 100644 --- a/library/library.ml +++ b/library/library.ml @@ -165,6 +165,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } let find_library s = @@ -222,9 +223,10 @@ let register_open_library export m = (************************************************************************) (*s Opening libraries *) -(*s [open_library s] opens a library. The library [s] and all libraries needed by - [s] are assumed to be already loaded. When opening [s] we recursively open - all the libraries needed by [s] and tagged [exported]. *) +(*s [open_library s] opens a library. The library [s] and all + libraries needed by [s] are assumed to be already loaded. When + opening [s] we recursively open all the libraries needed by [s] + and tagged [exported]. *) let eq_lib_name m1 m2 = m1.library_name = m2.library_name @@ -236,7 +238,7 @@ let open_library export explicit_libs m = or not (library_is_opened m.library_name) then begin register_open_library export m; - Declaremods.import_module (MPfile m.library_name) + Declaremods.really_import_module (MPfile m.library_name) end else if export then @@ -255,6 +257,34 @@ let open_libraries export modl = List.iter (open_library export modl) to_open_list +(**********************************************************************) +(* import and export - synchronous operations*) + +let cache_import (_,(dir,export)) = + open_libraries export [find_library dir] + +let open_import i (_,(dir,_) as obj) = + if i=1 then + (* even if the library is already imported, we re-import it *) + (* if not (library_is_opened dir) then *) + cache_import obj + +let subst_import (_,_,o) = o + +let export_import o = Some o + +let classify_import (_,(_,export as obj)) = + if export then Substitute obj else Dispose + + +let (in_import, out_import) = + declare_object {(default_object "IMPORT LIBRARY") with + cache_function = cache_import; + open_function = open_import; + subst_function = subst_import; + classify_function = classify_import } + + (************************************************************************) (*s Loading from disk to cache (preparation phase) *) @@ -272,6 +302,7 @@ let _ = Summary.unfreeze_function = (fun cu -> compunit_cache := cu); Summary.init_function = (fun () -> compunit_cache := CompilingLibraryMap.empty); + Summary.survive_module = true; Summary.survive_section = true } (*s [load_library s] loads the library [s] from the disk, and [find_library s] @@ -451,7 +482,7 @@ let rec_intern_library_from_file idopt f = which recursively loads its dependencies) - The [read_library] operation is very similar, but has does not "open" + The [read_library] operation is very similar, but does not "open" the library *) @@ -493,12 +524,12 @@ let load_require _ (_,(modl,_)) = let export_require (l,e) = Some (l,e) let (in_require, out_require) = - declare_object {(default_object "REQUIRE") with + declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; export_function = export_require; classify_function = (fun (_,o) -> Anticipate o) } - + let require_library spec qidl export = (* if sections_are_opened () && Options.verbose () then @@ -507,27 +538,30 @@ let require_library spec qidl export = "will be removed at the end of the section"); *) let modrefl = List.map rec_intern_qualified_library qidl in - add_anonymous_leaf (in_require (modrefl,Some export)); - add_frozen_state () + if Lib.is_modtype () || Lib.is_module () then begin + add_anonymous_leaf (in_require (modrefl,None)); + List.iter + (fun dir -> + add_anonymous_leaf (in_import (dir, export))) + modrefl + end + else + add_anonymous_leaf (in_require (modrefl,Some export)); + add_frozen_state () let require_library_from_file spec idopt file export = let modref = rec_intern_library_from_file idopt file in - add_anonymous_leaf (in_require ([modref],Some export)); - add_frozen_state () + if Lib.is_modtype () || Lib.is_module () then begin + add_anonymous_leaf (in_require ([modref],None)); + add_anonymous_leaf (in_import (modref, export)) + end + else + add_anonymous_leaf (in_require ([modref],Some export)); + add_frozen_state () + + +(* read = require without opening *) -let export_library (loc,qid) = - try - match Nametab.locate_module qid with - MPfile dir -> - add_anonymous_leaf (in_require ([dir],Some true)) - | mp -> - export_module mp - with - Not_found -> - user_err_loc - (loc,"export_library", - str ((string_of_qualid qid)^" is not a loaded library")) - let read_library qid = let modref = rec_intern_qualified_library qid in add_anonymous_leaf (in_require ([modref],None)); @@ -539,11 +573,33 @@ let read_library_from_file f = add_anonymous_leaf (in_require ([modref],None)); add_frozen_state () -let reload_library (modrefl, export) = - add_anonymous_leaf (in_require (modrefl,export)); + +(* called at end of section *) + +let reload_library modrefl = + add_anonymous_leaf (in_require modrefl); add_frozen_state () + +(* the function called by Vernacentries.vernac_import *) + +let import_library export (loc,qid) = + try + match Nametab.locate_module qid with + MPfile dir -> + if Lib.is_modtype () || Lib.is_module () || not export then + add_anonymous_leaf (in_import (dir, export)) + else + add_anonymous_leaf (in_require ([dir], Some export)) + | mp -> + import_module export mp + with + Not_found -> + user_err_loc + (loc,"import_library", + str ((string_of_qualid qid)^" is not a module")) + (***********************************************************************) (*s [save_library s] saves the library [m] to the disk. *) @@ -563,7 +619,7 @@ let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list let save_library_to s f = - let cenv, seg = Declaremods.export_library s in + let cenv, seg = Declaremods.end_library s in let md = { md_name = s; md_compiled = cenv; @@ -581,6 +637,7 @@ let save_library_to s f = (*s Pretty-printing of libraries state. *) +(* this function is not used... *) let fmt_libraries_state () = let opened = opened_libraries () and loaded = loaded_libraries () in diff --git a/library/library.mli b/library/library.mli index d69ecef9e..e02cb135c 100644 --- a/library/library.mli +++ b/library/library.mli @@ -15,18 +15,21 @@ open Libnames open Libobject (*i*) -(*s This module is the heart of the library. It provides low level functions to - load, open and save libraries. Modules are saved onto the disk with checksums - (obtained with the [Digest] module), which are checked at loading time to - prevent inconsistencies between files written at various dates. It also - provides a high level function [require] which corresponds to the - vernacular command [Require]. *) +(*s This module is the heart of the library. It provides low level + functions to load, open and save libraries. Libraries are saved + onto the disk with checksums (obtained with the [Digest] module), + which are checked at loading time to prevent inconsistencies + between files written at various dates. It also provides a high + level function [require] which corresponds to the vernacular + command [Require]. *) val read_library : qualid located -> unit val read_library_from_file : System.physical_path -> unit -val export_library : qualid located -> unit +(* [import_library true qid] = [export qid] *) + +val import_library : bool -> qualid located -> unit val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool diff --git a/library/nametab.ml b/library/nametab.ml index 27f56e7b4..c6ab79557 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -524,4 +524,5 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } diff --git a/library/summary.ml b/library/summary.ml index 59560af22..3da261689 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -15,6 +15,7 @@ type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit; + survive_module : bool ; survive_section : bool } let summaries = @@ -29,6 +30,7 @@ let internal_declare_summary sumname sdecl = freeze_function = dyn_freeze; unfreeze_function = dyn_unfreeze; init_function = dyn_init; + survive_module = sdecl.survive_module; survive_section = sdecl.survive_section } in if Hashtbl.mem summaries sumname then @@ -39,11 +41,6 @@ let internal_declare_summary sumname sdecl = let declare_summary sumname decl = internal_declare_summary (sumname^"-SUMMARY") decl -let envsummary = "Global environment SUMMARY" - -let declare_global_environment sdecl = - internal_declare_summary envsummary sdecl - type frozen = Dyn.t Stringmap.t let freeze_summaries () = @@ -53,30 +50,24 @@ let freeze_summaries () = summaries; !m -let unfreeze_summaries fs = - Hashtbl.iter - (fun id decl -> - try decl.unfreeze_function (Stringmap.find id fs) - with Not_found -> decl.init_function()) - summaries -let unfreeze_lost_summaries fs = +let unfreeze_some_summaries p fs = Hashtbl.iter (fun id decl -> try - if not decl.survive_section then + if p decl then decl.unfreeze_function (Stringmap.find id fs) with Not_found -> decl.init_function()) summaries -let unfreeze_other_summaries fs = - Hashtbl.iter - (fun id decl -> - try - if id <> envsummary then - decl.unfreeze_function (Stringmap.find id fs) - with Not_found -> decl.init_function()) - summaries +let unfreeze_summaries = + unfreeze_some_summaries (fun _ -> true) + +let section_unfreeze_summaries = + unfreeze_some_summaries (fun decl -> not decl.survive_section) + +let module_unfreeze_summaries = + unfreeze_some_summaries (fun decl -> not decl.survive_module) let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli index 7ecc5ebf3..23232033a 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -15,17 +15,17 @@ type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit; + survive_module : bool; (* should be false is most cases *) survive_section : bool } val declare_summary : string -> 'a summary_declaration -> unit -val declare_global_environment : 'a summary_declaration -> unit type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit -val unfreeze_lost_summaries : frozen -> unit -val unfreeze_other_summaries : frozen -> unit +val section_unfreeze_summaries : frozen -> unit +val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 03a0da56a..536e292fc 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -203,6 +203,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } (* classe d'un terme *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b0c3df607..03028dcf3 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -172,4 +172,5 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 13fefd306..1e25cc195 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -45,6 +45,7 @@ let _ = { Summary.freeze_function = Conv_oracle.freeze; Summary.unfreeze_function = Conv_oracle.unfreeze; Summary.init_function = Conv_oracle.init; + Summary.survive_module = false; Summary.survive_section = false } let is_evaluable env ref = @@ -141,6 +142,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } diff --git a/tactics/auto.ml b/tactics/auto.ml index c7186e412..4683ce144 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -159,6 +159,7 @@ let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 7febf87ab..a0f0f7226 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -36,6 +36,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } (* Rewriting rules before tactic interpretation *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 252e302c2..fc20b9c76 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -196,6 +196,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } let forward_subst_tactic = diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 3efd23f6a..0ff8ba69a 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -111,6 +111,7 @@ let _ = { Summary.freeze_function = (fun () -> !setoid_table); Summary.unfreeze_function = (fun t -> setoid_table := t); Summary.init_function = (fun () -> setoid_table := Gmap .empty); + Summary.survive_module = false; Summary.survive_section = false } (* Declare a new type of object in the environment : "setoid-theory". *) @@ -163,6 +164,7 @@ let _ = { Summary.freeze_function = (fun () -> !morphism_table); Summary.unfreeze_function = (fun t -> morphism_table := t); Summary.init_function = (fun () -> morphism_table := Gmap .empty); + Summary.survive_module = false; Summary.survive_section = false } (* Declare a new type of object in the environment : "morphism-definition". *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 619d26c61..0f2bf9ca9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -250,6 +250,7 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = false } (* Interpretation of extra generic arguments *) diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f94ed6423..41e8648bc 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,7 +1,10 @@ TrM.A = M.A : Set + OpM.A = M.A : Set + TrM.B = M.B : Set + *** [ OpM.B : Set ] diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v new file mode 100644 index 000000000..b35436247 --- /dev/null +++ b/test-suite/success/import_lib.v @@ -0,0 +1,202 @@ +Definition le_trans:=O. + + +Module Test_Read. + Module M. + Read Module Le. (* Reading without importing *) + + Check Le.le_trans. + + Lemma th0 : le_trans = O. + Reflexivity. + Qed. + End M. + + Check Le.le_trans. + + Lemma th0 : le_trans = O. + Reflexivity. + Qed. + + Import M. + + Lemma th1 : le_trans = O. + Reflexivity. + Qed. +End Test_Read. + + +(****************************************************************) + +Definition le_decide := (S O). (* from Arith/Compare *) +Definition min := O. (* from Arith/Min *) + +Module Test_Require. + + Module M. + Require Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th4 : min = O. + Reflexivity. + Qed. + +End Test_Require. + +(****************************************************************) + +Module Test_Import. + Module M. + Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th4 : min = O. + Reflexivity. + Qed. +End Test_Import. + +(***********************************************************************) + +Module Test_Export. + Module M. + Export Compare. (* Exports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th4 : min = Min.min. + Reflexivity. + Qed. +End Test_Export. + + +(***********************************************************************) + +Module Test_Require_Export. + + Definition mult_sym:=(S O). (* from Arith/Mult *) + Definition plus_sym:=O. (* from Arith/Plus *) + + Module M. + Require Export Mult. (* Exports Plus as well *) + + Lemma th1 : mult_sym = Mult.mult_sym. + Reflexivity. + Qed. + + Lemma th2 : plus_sym = Plus.plus_sym. + Reflexivity. + Qed. + + End M. + + + (* Checks that Mult and Plus are _not_ imported *) + Lemma th1 : mult_sym = (S O). + Reflexivity. + Qed. + + Lemma th2 : plus_sym = O. + Reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : mult_sym = Mult.mult_sym. + Reflexivity. + Qed. + + Lemma th4 : plus_sym = Plus.plus_sym. + Reflexivity. + Qed. + +End Test_Require_Export. diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v new file mode 100644 index 000000000..b4a8af46f --- /dev/null +++ b/test-suite/success/import_mod.v @@ -0,0 +1,75 @@ + +Definition p:=O. +Definition m:=O. + +Module Test_Import. + Module P. + Definition p:=(S O). + End P. + + Module M. + Import P. + Definition m:=p. + End M. + + Module N. + Import M. + + Lemma th0 : p=O. + Reflexivity. + Qed. + + End N. + + + (* M and P should be closed *) + Lemma th1 : m=O /\ p=O. + Split; Reflexivity. + Qed. + + + Import N. + + (* M and P should still be closed *) + Lemma th2 : m=O /\ p=O. + Split; Reflexivity. + Qed. +End Test_Import. + + +(********************************************************************) + + +Module Test_Export. + Module P. + Definition p:=(S O). + End P. + + Module M. + Export P. + Definition m:=p. + End M. + + Module N. + Export M. + + Lemma th0 : p=(S O). + Reflexivity. + Qed. + + End N. + + + (* M and P should be closed *) + Lemma th1 : m=O /\ p=O. + Split; Reflexivity. + Qed. + + + Import N. + + (* M and P should now be opened *) + Lemma th2 : m=(S O) /\ p=(S O). + Split; Reflexivity. + Qed. +End Test_Export. diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index d148a5343..5f2c068fd 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -323,6 +323,6 @@ let close_section _ s = (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls in let ids = last_section_hyps olddir in - Summary.unfreeze_lost_summaries fs; + Summary.section_unfreeze_summaries fs; catch_not_found (List.iter process_operation) (List.rev ops); Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e7402cbc6..f9d927f62 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -86,6 +86,7 @@ let _ = { freeze_function = Esyntax.freeze; unfreeze_function = Esyntax.unfreeze; init_function = Esyntax.init; + survive_module = false; survive_section = false } (* Pretty-printing objects = syntax_entry *) @@ -121,6 +122,7 @@ let _ = { freeze_function = Egrammar.freeze; unfreeze_function = Egrammar.unfreeze; init_function = Egrammar.init; + survive_module = false; survive_section = false } (* Tokens *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index df40b6aa3..56d49d1bf 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -249,6 +249,7 @@ let _ = { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); Summary.init_function = (fun () -> init_ml_modules ()); + Summary.survive_module = false; Summary.survive_section = true } (* Same as restore_ml_modules, but verbosely *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc9b2663e..9d20226b7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -528,11 +528,15 @@ let vernac_require import _ qidl = else raise e -let vernac_import export qidl = - let qidl = List.map qualid_of_reference qidl in - if export then - List.iter Library.export_library qidl - else +let vernac_import export refl = + let import_one ref = + let qid = qualid_of_reference ref in + Library.import_library export qid + in + List.iter import_one refl; + Lib.add_frozen_state () + +(* else let import (loc,qid) = try let mp = Nametab.locate_module qid in @@ -543,7 +547,7 @@ let vernac_import export qidl = str ((string_of_qualid qid)^" is not a module")) in List.iter import qidl; - Lib.add_frozen_state () +*) let vernac_canonical locqid = Recordobj.objdef_declare (Nametab.global locqid) |