- Synchronized subst_object with load_object (load_and_subst_objects)

  and set Declare ML Module as a regular substitutive object so that
  Declare ML Module is treated at the right place in the order of 
  appearance of substitutive declarations of a required module.
- Note: The full load/import mechanism for modules is not so clear: 
  the Require part of a Require Import inside a module is set outside 
  the module at module closing but the Import part remains inside (why not
  to put the "special" objects in the module too?); 
  moreover the "substitute" and "keep" objects of a module are
  desynchronised at module closing (is that really harmless/necessary?).
- Treatment of .cmxs targets in coq_makefile and in coqdep.
- Better make clean in coq_makefile generated makefiles.



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

4 files changed, 92 insertions, 80 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 80312cc122..4fc9d10b67 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -152,37 +152,60 @@ let check_subtypes mp sub_mtb =
   in
     ()  (* The constraints are checked and forgot immediately! *) 
 
-let subst_substobjs dir mp (subst,mbids,msid,objs) =
+let compute_subst_objects mp (subst,mbids,msid,objs) =
   match mbids with
-    | [] -> 
+  | [] -> 
+      let subst' = join_alias (map_msid msid mp) subst in
+      Some (join (map_msid msid mp) (join subst' subst), objs)
+  | _ ->
+      None
+
+let subst_substobjs dir mp substobjs =
+  match compute_subst_objects mp substobjs with
+  | Some (subst, objs) ->
 	let prefix = dir,(mp,empty_dirpath) in
-	let subst' = join_alias (map_msid msid mp) subst in
-	let subst = join subst' subst in
-	  Some (subst_objects prefix (join (map_msid msid mp) subst) objs)
-    | _ -> None
+	Some (subst_objects prefix subst objs)
+  | None -> None
+
+(* These functions register the visibility of the module and iterates
+   through its components. They are called by plenty module functions *)
+
+let compute_visibility exists what i dir dirinfo =
+  if exists then 
+    if 
+      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
+      with Not_found -> false 
+    then
+      Nametab.Exactly i
+    else
+      errorlabstrm (what^"_module")
+	(pr_dirpath dir ++ str " should already exist!") 
+  else
+    if Nametab.exists_dir dir then
+      errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+    else
+      Nametab.Until i
 
-(* This function registers the visibility of the module and iterates
-   through its components. It is called by plenty module functions *)
+let do_load_and_subst_module i dir mp substobjs keep =
+  let prefix = (dir,(mp,empty_dirpath)) in
+  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+  let vis = compute_visibility false "load_and_subst" i dir dirinfo in
+  let objects = compute_subst_objects mp substobjs in
+  Nametab.push_dir vis dir dirinfo;
+  modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+  match objects with
+  | Some (subst,seg) ->
+      let seg = load_and_subst_objects (i+1) prefix subst seg in
+      modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+      load_objects (i+1) prefix keep;
+      Some (seg@keep)
+  | None ->
+      None
 
 let do_module exists what iter_objects i dir mp substobjs objects =
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = 
-    if exists then 
-      if 
-	try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-	with Not_found -> false 
-      then
-	Nametab.Exactly i
-      else
-	errorlabstrm (what^"_module") 
-	  (pr_dirpath dir ++ str " should already exist!") 
-    else
-      if Nametab.exists_dir dir then
-	errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
-      else
-	Nametab.Until i
-  in
+  let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
     match objects with
@@ -325,22 +348,7 @@ and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
     try Some (MPmap.find alias !modtab_objects) with
 	Not_found -> None in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = 
-    if exists then 
-      if 
-	try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-	with Not_found -> false 
-      then
-	Nametab.Exactly i
-      else
-	errorlabstrm (what^"_module") 
-	  (pr_dirpath dir ++ str " should already exist!") 
-    else
-      if Nametab.exists_dir dir then
-	errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
-      else
-	Nametab.Until i
-  in
+  let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
     match alias_objects,objects with
@@ -668,8 +676,7 @@ let process_module_bindings argids args =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
     let substobjs = get_modtype_substobjs (Global.env()) mty in
-    let substituted = subst_substobjs dir mp substobjs in
-      do_module false "start" load_objects 1 dir mp substobjs substituted
+    ignore (do_load_and_subst_module 1 dir mp substobjs [])
   in
     List.iter2 process_arg argids args
 
@@ -683,8 +690,7 @@ let intern_args interp_modtype (idl,arg) =
     (fun dir mbid -> 
       Global.add_module_parameter mbid mty;
       let mp = MPbound mbid in
-      let substituted = subst_substobjs dir mp substobjs in
-      do_module false "interp" load_objects 1 dir mp substobjs substituted;
+      ignore (do_load_and_subst_module 1 dir mp substobjs []);
       (mbid,mty))
     dirs mbids
 
@@ -798,25 +804,19 @@ type library_objects =
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let substobjs, objects =
-    try 
-      ignore(Global.lookup_module mp);
-      (* if it's in the environment, the cached objects should be correct *)
-      Dirmap.find dir !library_cache 
-    with
-	Not_found ->
-	  if mp <> Global.import cenv digest then
-	    anomaly "Unexpected disk module name";
-	  let msid,substitute,keep = objs in
-	  let substobjs = empty_subst, [], msid, substitute in
-	  let substituted = subst_substobjs dir mp substobjs in
-	  let objects = Option.map (fun seg -> seg@keep) substituted in
-	  let modobjs = substobjs, objects in
-	    library_cache := Dirmap.add dir modobjs !library_cache;
-	    modobjs
-  in
+  try 
+    ignore(Global.lookup_module mp);
+    (* if it's in the environment, the cached objects should be correct *)
+    let substobjs, objects = Dirmap.find dir !library_cache in
     do_module false "register_library" load_objects 1 dir mp substobjs objects
-
+  with Not_found ->
+    if mp <> Global.import cenv digest then
+      anomaly "Unexpected disk module name";
+    let msid,substitute,keep = objs in
+    let substobjs = empty_subst, [], msid, substitute in
+    let objects = do_load_and_subst_module 1 dir mp substobjs keep in
+    let modobjs = substobjs, objects in
+    library_cache := Dirmap.add dir modobjs !library_cache
 
 let start_library dir = 
   let mp = Global.start_library dir in
diff --git a/library/lib.ml b/library/lib.ml
index 553d353d69..7135a93cc0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -48,6 +48,13 @@ let subst_objects prefix subst seg =
   in
     list_smartmap subst_one seg
 
+let load_and_subst_objects i prefix subst seg =
+  List.rev (List.fold_left (fun seg (id,obj as node) ->
+    let obj' =  subst_object (make_oname prefix id, subst, obj) in
+    let node = if obj == obj' then node else (id, obj') in
+    load_object i (make_oname prefix id, obj');
+    node :: seg) [] seg)
+
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
diff --git a/library/lib.mli b/library/lib.mli
index 3e64a52905..dc8202ed2a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -33,6 +33,7 @@ type lib_objects = (Names.identifier * Libobject.obj) list
 val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
 
 (* [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
diff --git a/library/library.ml b/library/library.ml
index 963b61998a..ab92bb6769 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -323,14 +323,14 @@ let open_libraries export modl =
 (**********************************************************************)
 (* import and export  -  synchronous operations*)
 
-let cache_import (_,(dir,export)) = 
-  open_libraries export [try_find_library dir]
-
-let open_import i (_,(dir,_) as obj) =
+let open_import i (_,(dir,export)) =
   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
+      open_libraries export [try_find_library dir]
+
+let cache_import obj = 
+  open_import 1 obj
 
 let subst_import (_,_,o) = o
 
@@ -509,8 +509,8 @@ let rec_intern_library_from_file idopt f =
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
-(*s [require_library] loads and opens a library. This is a synchronized
-    operation. It is performed as follows:
+(*s [require_library] loads and possibly opens a library. This is a 
+    synchronized operation. It is performed as follows:
 
   preparation phase: (functions require_library* ) the library and its 
     dependencies are read from to disk (using intern_* )
@@ -523,10 +523,6 @@ let rec_intern_library_from_file idopt f =
     the library is loaded in the environment and Nametab, the objects are 
     registered etc, using functions from Declaremods (via load_library, 
     which recursively loads its dependencies)
-
-
-  The [read_library] operation is very similar, but does not "open"
-    the library
 *)
 
 type library_reference = dir_path list * bool option
@@ -539,14 +535,21 @@ let register_library (dir,m) =
     m.library_digest;
   register_loaded_library m
 
-  (* [needed] is the ordered list of libraries not already loaded *)
-let cache_require (_,(needed,modl,export)) =
-  List.iter register_library needed;
+(* Follow the semantics of Anticipate object:
+   - called at module or module type closing when a Require occurs in 
+     the module or module type
+   - not called from a library (i.e. a module identified with a file) *)
+let load_require _ (_,(needed,modl,_)) =
+  List.iter register_library needed
+
+let open_require i (_,(_,modl,export)) =
   Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
     export
 
-let load_require  _ (_,(needed,modl,_)) =
-  List.iter register_library needed
+  (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require o =
+  load_require 1 o;
+  open_require 1 o
 
   (* keeps the require marker for closed section replay but removes
      OS dependent fields from .vo files for cross-platform compatibility *)
@@ -554,10 +557,13 @@ let export_require (_,l,e) = Some ([],l,e)
 
 let discharge_require (_,o) = Some o
 
+(* open_function is never called from here because an Anticipate object *) 
+
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
+       open_function = (fun _ _ -> assert false);
        export_function = export_require;
        discharge_function = discharge_require;
        classify_function = (fun (_,o) -> Anticipate o) }
@@ -565,8 +571,6 @@ let (in_require, out_require) =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-(* read = require without opening *)
-
 let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f