From 235d5cc96af46d0406bdd28222f56b3ee2bf827e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 15:43:10 +0000 Subject: [PATCH] Invert dependencies between baseuris (files) are now stored in the db. Hence decompilation is now fully correct (???). --- .../components/ng_kernel/nCicLibrary.ml | 127 +++++++++++------- 1 file changed, 79 insertions(+), 48 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 0519e4146..f0f9c99a1 100644 --- 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 = -- 2.39.2