Correction du bug 335 et Export/Require Export dans un module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 172 insertions, 89 deletions

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