Safe_typing+Libary: use some arrays instead of lists in vo structures

 Very little space saved this way, but it would hurt either...

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

4 files changed, 29 insertions, 28 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 03a18280a..eb4016f5f 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -42,8 +42,8 @@ type library_disk = {
   md_name : compilation_unit_name;
   md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
   md_objects : library_objects;
-  md_deps : (compilation_unit_name * Digest.t) list;
-  md_imports : compilation_unit_name list }
+  md_deps : (compilation_unit_name * Digest.t) array;
+  md_imports : compilation_unit_name array }
 
 (************************************************************************)
 (*s Modules on disk contain the following informations (after the magic
@@ -56,7 +56,7 @@ type library_t = {
   library_name : compilation_unit_name;
   library_filename : CUnix.physical_path;
   library_compiled : Safe_typing.compiled_library;
-  library_deps : (compilation_unit_name * Digest.t) list;
+  library_deps : (compilation_unit_name * Digest.t) array;
   library_digest : Digest.t }
 
 module LibraryOrdered =
@@ -330,8 +330,9 @@ let rec intern_library seen (dir, f) needed =
     let m = intern_from_file (dir,f) in
     let seen' = LibrarySet.add dir seen in
     let deps =
-      List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in
-    (dir,m) :: List.fold_right (intern_library seen') deps needed
+      Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps
+    in
+    (dir,m) :: Array.fold_right (intern_library seen') deps needed
 
 (* Compute the reflexive transitive dependency closure *)
 let rec fold_deps seen ff (dir,f) (s,acc) =
@@ -339,9 +340,9 @@ let rec fold_deps seen ff (dir,f) (s,acc) =
   if LibrarySet.mem dir s then (s,acc)
   else
     let deps = get_deps (dir,f) in
-    let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
+    let deps = Array.map (fun (d,_) -> try_locate_absolute_library d) deps in
     let seen' = LibrarySet.add dir seen in
-    let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in
+    let (s',acc') = Array.fold_right (fold_deps seen' ff) deps (s,acc) in
     (LibrarySet.add dir s', ff dir acc')
 
 and fold_deps_list seen ff modl needed =
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 5a190de7f..5cbcc00f5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -57,13 +57,13 @@ let check_imports f caller env needed =
     with Not_found ->
       error ("Reference to unknown module " ^ (DirPath.to_string dp))
   in
-  List.iter check needed
+  Array.iter check needed
 
 
 type compiled_library =
     DirPath.t *
     module_body *
-    (DirPath.t * Digest.t) list *
+    (DirPath.t * Digest.t) array *
     engagement option
 
  (* Store the body of modules' opaque constants inside a table.  
@@ -168,7 +168,7 @@ end = struct
 end
 
 open Validate
-let val_deps = val_list (val_tuple ~name:"dep"[|val_dp;no_val|])
+let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|])
 let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
 
 (* This function should append a certificate to the .vo file.
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a11dfe91a..20ca16476 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -630,7 +630,7 @@ let set_engagement c senv =
 type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
-  comp_deps : library_info list;
+  comp_deps : library_info array;
   comp_enga : engagement option;
   comp_natsymbs : Nativecode.symbol array
 }
@@ -715,7 +715,7 @@ let export senv dir =
   let lib = {
     comp_name = dir;
     comp_mod = mb;
-    comp_deps = senv.imports;
+    comp_deps = Array.of_list senv.imports;
     comp_enga = engagement senv.env;
     comp_natsymbs = values }
   in
@@ -732,7 +732,7 @@ let check_imports senv needed =
     with Not_found ->
       error ("Reference to unknown module "^(DirPath.to_string id)^".")
   in
-  List.iter check needed
+  Array.iter check needed
 
 
 
diff --git a/library/library.ml b/library/library.ml
index dc0981497..b7a2f8149 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Libnames
 open Nameops
-open Safe_typing
 open Libobject
 open Lib
 
@@ -25,20 +24,20 @@ type compilation_unit_name = DirPath.t
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : LightenLibrary.lightened_compiled_library;
+  md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
   md_objects : Declaremods.library_objects;
-  md_deps : (compilation_unit_name * Digest.t) list;
-  md_imports : compilation_unit_name list }
+  md_deps : (compilation_unit_name * Digest.t) array;
+  md_imports : compilation_unit_name array }
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [libraries_table]. *)
 
 type library_t = {
   library_name : compilation_unit_name;
-  library_compiled : compiled_library;
+  library_compiled : Safe_typing.compiled_library;
   library_objects : Declaremods.library_objects;
-  library_deps : (compilation_unit_name * Digest.t) list;
-  library_imports : compilation_unit_name list;
+  library_deps : (compilation_unit_name * Digest.t) array;
+  library_imports : compilation_unit_name array;
   library_digest : Digest.t }
 
 module LibraryOrdered = DirPath
@@ -186,7 +185,7 @@ let open_libraries export modl =
     List.fold_left
       (fun l m ->
          let subimport =
-           List.fold_left
+           Array.fold_left
              (fun l m -> remember_last_of_each l (try_find_library m))
              l m.library_imports
          in remember_last_of_each subimport m)
@@ -295,7 +294,8 @@ let try_locate_qualified_library (loc,qid) =
 
 let mk_library md table digest =
   let md_compiled =
-    LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled
+    Safe_typing.LightenLibrary.load ~load_proof:!Flags.load_proofs
+      table md.md_compiled
   in {
     library_name     = md.md_name;
     library_compiled = md_compiled;
@@ -310,7 +310,7 @@ let fetch_opaque_table (f,pos,digest) =
     let ch = System.with_magic_number_check raw_intern_library f in
     let () = seek_in ch pos in
     if not (String.equal (System.marshal_in f ch) digest) then failwith "File changed!";
-    let table = (System.marshal_in f ch : LightenLibrary.table) in
+    let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
     let () = close_in ch in
     table
   with e when Errors.noncritical e ->
@@ -346,7 +346,7 @@ let rec intern_library needed (dir, f) =
   m, intern_library_deps needed dir m
 
 and intern_library_deps needed dir m =
-  (dir,m)::List.fold_left (intern_mandatory_library dir) needed m.library_deps
+  (dir,m)::Array.fold_left (intern_mandatory_library dir) needed m.library_deps
 
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
@@ -550,14 +550,14 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 let save_library_to dir f =
   let cenv, seg, ast = Declaremods.end_library dir in
-  let cenv, table = LightenLibrary.save cenv in
+  let cenv, table = Safe_typing.LightenLibrary.save cenv in
   let md = {
     md_name = dir;
     md_compiled = cenv;
     md_objects = seg;
-    md_deps = current_deps ();
-    md_imports = current_reexports () } in
-  if List.mem_assoc dir md.md_deps then
+    md_deps = Array.of_list (current_deps ());
+    md_imports = Array.of_list (current_reexports ()) } in
+  if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then
     error_recursively_dependent_library dir;
   let (f',ch) = raw_extern_library f in
   try