- 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

7 files changed, 113 insertions, 89 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
diff --git a/library/lib.ml b/library/lib.ml
index 553d353d6..7135a93cc 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 3e64a5290..dc8202ed2 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 963b61998..ab92bb676 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
 
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index e2ea8250d..fa5ded938 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -90,7 +90,7 @@ let is_genrule r =
 
 let standard sds sps =
   print "Makefile.config:\n";
-  print "\t$(COQBIN)/coqtop -config > $@\n\n";
+  print "\t$(COQBIN)coqtop -config > $@\n\n";
   print "byte:\n";
   print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
   print "opt:\n";
@@ -115,7 +115,7 @@ let standard sds sps =
     print "\n";
   end;
   print "clean:\n";
-  print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
+  print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
          $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) Makefile.config\n";
   if !some_mlfile then
@@ -147,12 +147,13 @@ let footer_includes () =
 let implicit () =
   let ml_rules () =
     print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
+    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
+    print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
+    print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) -impl \"$<\" > \"$@\"\n\n"
   and v_rule () =
     print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -187,8 +188,8 @@ let variables l =
     print "GALLINA:=$(COQBIN)gallina\n";
     print "COQDOC:=$(COQBIN)coqdoc\n";
     (* Caml executables and relative variables *)
-    printf "CAMLC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlc;
-    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlopt;
+    printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
     printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
     printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
     print "GRAMMARS:=grammar.cma\n";
@@ -345,10 +346,15 @@ let all_target l =
       begin
 	print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
 	print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+	print "CMIFILES:=$(MLFILES:.ml=.cmi)\n";
+	print "CMXFILES:=$(MLFILES:.ml=.cmx)\n";
+	print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n";
+	print "OFILES:=$(MLFILES:.ml=.o)\n";
       end;
     print "\nall: ";
     if !some_vfile then print "$(VOFILES) ";
     if !some_mlfile then print "$(CMOFILES) ";
+    if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) ";
     print_list "\\\n  " other_targets; print "\n";
     if !some_vfile then 
       begin
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 5a31a64d8..529ca0ba5 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -245,7 +245,11 @@ let traite_fichier_Coq verbose f =
 			addQueue deja_vu_ml s;
                	       try
               		 let mldir = Hashtbl.find mlKnown s in
-              		   printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+			 let filename = file_name ([String.uncapitalize s],mldir) in
+              		 if Coq_config.has_natdynlink then
+			   printf " %s.cmo %s.cmxs" filename filename
+			 else
+			   printf " %s.cmo" filename
               	       with Not_found -> ()
 		     end)
 		sl
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 694e60dbc..57c146428 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -309,7 +309,9 @@ let (inMLModule,outMLModule) =
   declare_object {(default_object "ML-MODULE") with
                     load_function = (fun _ -> cache_ml_module_object);
                     cache_function = cache_ml_module_object;
-                    export_function = export_ml_module_object }
+                    export_function = export_ml_module_object;
+                    subst_function = (fun (_,_,o) -> o);
+                    classify_function = (fun (_,o) -> Substitute o) }
 
 let declare_ml_modules l =
   Lib.add_anonymous_leaf (inMLModule {mnames=l})