Invert dependencies between baseuris (files) are now stored in the db.

Hence decompilation is now fully correct (???).

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 0519e414672057cbbefed2fe1167a6b95a50b803..f0f9c99a1644ad75b8de39d2f3a707dfc000c204 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -13,7 +13,7 @@
 
 exception LibraryOutOfSync of string Lazy.t
 
-let magic = 0;;
+let magic = 1;;
 
 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
 
@@ -60,38 +60,63 @@ let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
 type timestamp =
  (NUri.uri * NCic.obj) list *
  (NUri.uri * string * NReference.reference) list *
- NCic.obj NUri.UriMap.t;;
+ NCic.obj NUri.UriMap.t *
+ NUri.uri list;;
 
-let time0 = [],[],NUri.UriMap.empty;;
+let time0 = [],[],NUri.UriMap.empty,[];;
 let storage = ref [];;
 let local_aliases = ref [];;
+let cache = ref NUri.UriMap.empty;;
+let includes = ref [];;
 
-let set_global_aliases,get_global_aliases =
+let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps =
  let global_aliases = ref [] in
-  let store_db () =
-   let ch = open_out (db_path ()) in
-   Marshal.to_channel ch (magic,!global_aliases) [];
-   close_out ch;
+ let includes_map = ref NUri.UriMap.empty in
+ let store_db () =
+  let ch = open_out (db_path ()) in
+  Marshal.to_channel ch (magic,(!global_aliases,!includes_map)) [];
+  close_out ch in
+ let load_db () =
+  try
+   let ga,im = require_path (db_path ()) in
+   let ga =
+    List.map
+     (fun (uri,name,NReference.Ref (uri2,spec)) ->
+       refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
+     ) ga in
+   let im =
+    NUri.UriMap.fold
+     (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
+     ) im NUri.UriMap.empty
+   in
+    global_aliases := ga;
+    includes_map := im
+  with
+   Sys_error _ -> () in
+ let get_deps u =
+  let get_deps_one_step u =
+    try NUri.UriMap.find u !includes_map with Not_found -> [] in
+  let rec aux res =
+   function
+      [] -> res
+    | he::tl ->
+       if List.mem he res then
+        aux res tl
+       else
+        aux (he::res) (get_deps_one_step he @ tl)
   in
+   aux [] [u]
+ in
+  load_db,
   (fun ga -> global_aliases := ga; store_db ()),
-  (fun () -> !global_aliases)
-;;
-
-let init () =
- try
-  let global_aliases = require_path (db_path ()) in
-  let global_aliases =
-   List.map
-    (fun (uri,name,NReference.Ref (uri2,spec)) ->
-      refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
-    ) global_aliases
-  in
-   set_global_aliases global_aliases
- with
-  Sys_error _ -> ()
+  (fun () -> !global_aliases),
+  (fun u l ->
+    includes_map := NUri.UriMap.add u (l @ get_deps u) !includes_map;
+    store_db ()),
+  get_deps
 ;;
 
-let cache = ref NUri.UriMap.empty;;
+let init = load_db;;
 
 class status =
  object
@@ -104,8 +129,8 @@ class status =
  end
 
 let time_travel status =
- let sto,ali,cac = status#timestamp in
-  storage := sto; local_aliases := ali; cache := cac
+ let sto,ali,cac,inc = status#timestamp in
+  storage := sto; local_aliases := ali; cache := cac; includes := inc
 ;;
 
 let serialize ~baseuri dump =
@@ -119,6 +144,7 @@ let serialize ~baseuri dump =
     close_out ch
   ) !storage;
  set_global_aliases (!local_aliases @ get_global_aliases ());
+ List.iter (fun u -> add_deps u [baseuri]) !includes;
  time_travel (new status)
 ;;
 
@@ -156,32 +182,37 @@ module Serializer(S: sig type status end) =
   let serialize = serialize
 
   let require ~baseuri status =
+   includes := baseuri::!includes;
    let dump = require0 ~baseuri in
     List.fold_right !require1 dump status
 end
 
 let decompile ~baseuri =
- HExtlib.safe_remove (path_of_baseuri baseuri);
- let basepath = path_of_baseuri ~no_suffix:true baseuri in
- try
-  let od = Unix.opendir basepath in
-  let rec aux names =
-   try
-    let name = Unix.readdir od in
-     if name <> "." && name <> ".." then aux (name::names) else aux names
-   with
-    End_of_file -> names in
-  let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
-   Unix.closedir od;
-   List.iter Unix.unlink names;
-   HExtlib.rmdir_descend basepath;
-   set_global_aliases
-    (List.filter
-     (fun (_,_,NReference.Ref (nuri,_)) ->
-       Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
-     ) (get_global_aliases ()))
- with
-  Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
+ let baseuris = get_deps baseuri in
+ List.iter (fun baseuri ->
+  HExtlib.safe_remove (path_of_baseuri baseuri);
+  let basepath = path_of_baseuri ~no_suffix:true baseuri in
+  try
+   let od = Unix.opendir basepath in
+   let rec aux names =
+    try
+     let name = Unix.readdir od in
+      if name <> "." && name <> ".." then aux (name::names) else aux names
+    with
+     End_of_file -> names in
+   let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
+    Unix.closedir od;
+    List.iter Unix.unlink names;
+    HExtlib.rmdir_descend basepath;
+    set_global_aliases
+     (List.filter
+      (fun (_,_,NReference.Ref (nuri,_)) ->
+        Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
+      ) (get_global_aliases ()))
+  with
+   Unix.Unix_error _ -> (* raised by Unix.opendir, we hope :-) *)
+    assert (List.length baseuris = 1)
+ ) baseuris
 ;;
 
 LibraryClean.set_decompile_cb
@@ -241,7 +272,7 @@ let add_obj status u obj =
          ) il)
   in
   local_aliases := references @ !local_aliases;
-  status#set_timestamp (!storage,!local_aliases,!cache)
+  status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;
 
 let get_obj u =