- 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

1 files changed, 62 insertions, 62 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 80312cc12..4fc9d10b6 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