module Library

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

8 files changed, 230 insertions, 40 deletions

diff --git a/library/global.ml b/library/global.ml
index d669410b8..d7267a96d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -35,3 +35,5 @@ let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
 let lookup_meta n = lookup_meta n !global_env
 
+let export s = export !global_env s
+let import cenv = global_env := import cenv !global_env
diff --git a/library/global.mli b/library/global.mli
index 4f04d2e51..d21509e32 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -9,6 +9,7 @@ open Sign
 open Evd
 open Constant
 open Inductive
+open Environ
 (*i*)
 
 (* This module defines the global environment of Coq. 
@@ -33,3 +34,5 @@ val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : constr -> mind_specif
 val lookup_meta : int -> constr
 
+val export : string -> compiled_env
+val import : compiled_env -> unit
diff --git a/library/lib.ml b/library/lib.ml
index a8ab156c5..42850bc05 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -20,7 +20,11 @@ type library_entry = section_path * node
 
 
 (* We keep trace of operations in a stack [lib_stk]. 
-   [path_prefix] is the current path of sections (in correct order). *)
+   [path_prefix] is the current path of sections. Sections are stored in 
+   ``correct'' order, the oldest coming first in the list. It may seems 
+   costly, but in practice there is not so many openings and closings of
+   sections, but on the contrary there are many constructions of section
+   paths. *) 
 
 let lib_stk = ref ([] : (section_path * node) list)
 
@@ -122,7 +126,7 @@ let close_section s =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry sp (ClosedSection (s,modp,after));
+  add_entry sp (ClosedSection (s,modp,List.rev after));
   add_frozen_state ();
   pop_path_prefix ()
 
diff --git a/library/lib.mli b/library/lib.mli
index 80f61ef40..a38fb4cef 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -25,7 +25,7 @@ type library_entry = section_path * node
 
 
 (*s Adding operations, and getting the current list of operations (most 
-  recent ones come first). *)
+  recent ones coming first). *)
 
 val add_leaf : identifier -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
@@ -33,7 +33,8 @@ val add_anonymous_leaf : obj -> unit
 val contents_after : section_path option -> library_segment
 
 
-(*s Opening and closing a section. *)
+(*s Opening and closing a section. The boolean in [open_section] indicates
+  a module. *)
 
 val open_section : string -> bool -> section_path
 val close_section : string -> unit
diff --git a/library/libobject.ml b/library/libobject.ml
index f5e610704..1096ac43a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -5,15 +5,17 @@ open Util
 open Names
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
 type dynamic_object_declaration = {
-  dyn_load_function : obj -> unit;
   dyn_cache_function : section_path * obj -> unit;
+  dyn_load_function : obj -> unit;
+  dyn_open_function : obj -> unit;
   dyn_specification_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
@@ -23,41 +25,39 @@ let cache_tab =
 
 let declare_object (na,odecl) =
   let (infun,outfun) = Dyn.create na in
-  let loader lobj =
-    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the loadfun"
-  and cacher (spopt,lobj) =
+  let cacher (spopt,lobj) =
     if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the cachefun"
+  and loader lobj =
+    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+  and opener lobj =
+    if Dyn.tag lobj = na then odecl.open_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the openfun"
   and spec_extractor lobj = 
     infun(odecl.specification_function (outfun lobj))
   in 
-  Hashtbl.add cache_tab na { dyn_load_function = loader;
-                             dyn_cache_function = cacher;
+  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
+			     dyn_load_function = loader;
+                             dyn_open_function = opener;
                              dyn_specification_function = spec_extractor };
   (infun,outfun)
 
-
-let load_object lobj =
+let apply_dyn_fun f lobj =
   let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_load_function lobj
-  with Not_found ->
-    anomaly ("Cannot find loadfun for an object with tag "^tag)
+  try
+    let dodecl = Hashtbl.find cache_tab tag in f dodecl
+  with Not_found -> 
+    anomaly ("Cannot find library functions for an object with tag "^tag)
 
-let cache_object (spopt,lobj) =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_cache_function(spopt,lobj)
-  with Not_found ->
-    anomaly ("Cannot find cachefun for an object with tag "^tag)
+let cache_object ((_,lobj) as node) =
+  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
+
+let load_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj
+
+let open_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj
 
 let extract_object_specification lobj =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in
-    dodecl.dyn_specification_function lobj
-  with Not_found ->
-    anomaly ("Cannot find specification extractor for an object with tag "^tag)
+  apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 967e4c410..7ddac57b2 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -5,20 +5,23 @@
 open Names
 (*i*)
 
-(* [Libobject] declares persistent objects given with three methods:
+(* [Libobject] declares persistent objects, given with three methods:
+   - a caching function specifying how to add the object in the current
+     scope of theory modules;
    - a loading function, specifying what to do when the object is loaded
      from the disk;
-   - a caching function specifying how to import the object in the current
-     scope of theory modules;
+   - an opening function, specifying what to do when the module containing
+     the object is opened;
    - a specification function, to extract its specification when writing
      the specification of a module to the disk (.vi) *)
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
-(*s given the object-name, the "loading" function, the "caching" function, 
+(*s Given the object-name, the "loading" function, the "caching" function, 
    and the "specification" function, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
@@ -30,8 +33,7 @@ val declare_object :
 
 val object_tag : obj -> string
 
-val load_object : obj -> unit
-
 val cache_object : (section_path * obj) -> unit
-
+val load_object : obj -> unit
+val open_object : obj -> unit
 val extract_object_specification : obj -> obj
diff --git a/library/library.ml b/library/library.ml
new file mode 100644
index 000000000..7de5a845d
--- /dev/null
+++ b/library/library.ml
@@ -0,0 +1,150 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Environ
+open Libobject
+open Lib
+
+(* Modules on disk contain the following informations (after the magic 
+   number, and before the digest). *)
+
+type module_disk = { 
+  md_name : string;
+  md_compiled_env : compiled_env;
+  md_declarations : library_segment;
+  md_deps : (string * Digest.t * bool) list }
+
+(* Modules loaded in memory contain the following informations. They are
+   kept in the hash table [modules_table]. *)
+
+type module_t = {
+  module_name : string;
+  module_compiled_env : compiled_env;
+  module_declarations : library_segment;
+  mutable module_opened : bool;
+  mutable module_exported : bool;
+  module_deps : (string * Digest.t * bool) list;
+  module_digest : Digest.t }
+
+let modules_table =
+  (Hashtbl.create 17 : (string, module_t) Hashtbl.t)
+
+let find_module s =
+  try
+    Hashtbl.find modules_table s
+  with Not_found ->
+    error ("Unknown module " ^ s)
+
+let module_is_loaded s =
+  try let _ = Hashtbl.find modules_table s in true with Not_found -> false
+
+let module_is_opened s =
+  (find_module s).module_opened
+
+let vo_magic_number = 0700
+
+let (raw_extern_module, raw_intern_module) =
+  System.raw_extern_intern vo_magic_number ".vo"
+
+let segment_iter f =
+  let rec apply = function
+    | _,Leaf obj -> f obj
+    | _,ClosedSection (_,_,mseg) -> iter mseg
+    | _,OpenedSection _ -> assert false
+    | _,FrozenState _ -> ()
+  and iter seg =
+    List.iter apply seg
+  in
+  iter
+
+
+(* [open_module s] opens a module which is assumed to be already loaded. *)
+
+let open_module s =
+  let m = find_module s in
+  if not m.module_opened then begin
+    segment_iter open_object m.module_declarations;
+    m.module_opened <- true
+  end
+
+
+(* [load_module s] loads the module [s] from the disk, and [find_module s]
+   returns the module of name [s], loading it if necessary. 
+   The boolean [doexp] specifies if we open the modules which are declared
+   exported in the dependencies (usually it is [true] at the highest level;
+   it is always [false] in recursive loadings). *)
+
+let load_objects s =
+  let m = find_module s in
+  segment_iter load_object m.module_declarations
+
+let rec load_module_from doexp s f =
+  let (fname,ch) = raw_intern_module f in
+  let md = input_value ch in
+  let digest = input_value ch in
+  close_in ch;
+  let m = { module_name = md.md_name;
+	    module_compiled_env = md.md_compiled_env;
+	    module_declarations = md.md_declarations;
+	    module_opened = false;
+	    module_exported = false;
+	    module_deps = md.md_deps;
+	    module_digest = digest } in
+  if s <> md.md_name then
+    error ("The file " ^ fname ^ " does not contain module " ^ s);
+  List.iter (load_mandatory_module doexp s) m.module_deps;
+  Hashtbl.add modules_table s m;
+  m
+
+and load_mandatory_module doexp caller (s,d,export) =
+  let m = find_module false s s in
+  if d <> m.module_digest then
+    error ("module "^caller^" makes inconsistent assumptions over module "^s);
+  if doexp && export then open_module s
+
+and find_module doexp s f =
+  try Hashtbl.find modules_table s with Not_found -> load_module_from doexp s f
+
+
+let load_module s = function
+  | None -> let _ = load_module_from true s s in ()
+  | Some f -> let _ = load_module_from true s f in ()
+
+
+(* [require_module] loads and opens a module. *)
+
+let require_module spec name fileopt export =
+  let file = match fileopt with
+    | None -> name
+    | Some f -> f in
+  let m = load_module_from true name file in
+  open_module name;
+  if export then m.module_exported <- true
+
+
+(* [save_module s] saves the module [m] to the disk. *)
+
+let current_imports () =
+  let l = ref [] in
+  Hashtbl.iter 
+    (fun _ m -> l := (m.module_name, m.module_digest, m.module_exported) :: !l)
+    modules_table;
+  !l
+
+let save_module_to s f =
+  let seg = contents_after None in
+  let md = { 
+    md_name = s;
+    md_compiled_env = Global.export s;
+    md_declarations = seg;
+    md_deps = current_imports () } in
+  let (_,ch) = raw_extern_module f in
+  output_value ch md;
+  flush ch;
+  let di = Digest.file f in
+  output_value ch di;
+  close_out ch
+
+
diff --git a/library/library.mli b/library/library.mli
new file mode 100644
index 000000000..2c54aec2e
--- /dev/null
+++ b/library/library.mli
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+(* This module is the heart of the library. It provides low level functions to
+   load, open and save modules. 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]. *)
+
+val load_module : string -> string option -> unit
+val open_module : string -> unit
+
+val module_is_loaded : string -> bool
+val module_is_opened : string -> bool
+
+(*s Require. The command [require_module spec m file export] loads and opens
+  a module [m]. [file] specifies the filename, if not [None]. [spec]
+  specifies to look for a specification ([true]) or for an implementation
+  ([false]), if not [None]. And [export] specifies if the module must be 
+  exported. *)
+
+val require_module : bool option -> string -> string option -> bool -> unit
+
+(*s [save_module_to s f] saves the current environment as a module [s]
+  in the file [f]. *)
+
+val save_module_to : string -> string -> unit