(* $Id$ *)
exception ObjectNotFound of string Lazy.t
+exception LibraryOutOfSync of string Lazy.t
-let storage = ref [];;
+type timestamp =
+ (NUri.uri * NCic.obj) list *
+ (NUri.uri * string * NReference.reference) list *
+ NCic.obj NUri.UriMap.t;;
+let time0 = [],[],NUri.UriMap.empty;;
+let storage = ref [];;
let aliases = ref [];;
+let cache = ref NUri.UriMap.empty;;
+
+let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
let resolve name =
try
(NReference.Ind (inductive,i,leftno))]
) il)
in
- aliases := references @ !aliases
+ aliases := references @ !aliases;
+ !storage,!aliases,!cache
;;
-let cache = NUri.UriHash.create 313;;
-
let get_obj u =
try List.assq u !storage
with Not_found ->
- try NUri.UriHash.find cache u
+ try NUri.UriMap.find u !cache
with Not_found ->
(* in the final implementation should get it from disk *)
let ouri = NCic2OCic.ouri_of_nuri u in
try
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
let l = OCic2NCic.convert_obj ouri o in
- List.iter (fun (u,_,_,_,_ as o) ->
- (* prerr_endline ("+"^NUri.string_of_uri u); *)
- NUri.UriHash.add cache u o) l;
+ List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
HExtlib.list_last l
with CicEnvironment.Object_not_found u ->
raise (ObjectNotFound
(lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
;;
-let clear_cache () = NUri.UriHash.clear cache;;
+let clear_cache () = cache := NUri.UriMap.empty;;
+
+let magic = 0;;
+
+let path_of_baseuri baseuri =
+ let uri = NUri.string_of_uri baseuri in
+ let path = String.sub uri 4 (String.length uri - 4) in
+ let path = Helm_registry.get "matita.basedir" ^ path in
+ let dirname = Filename.dirname path in
+ HExtlib.mkdir dirname;
+ path ^ ".ng"
+;;
+
+let serialize ~baseuri dump =
+ let ch = open_out (path_of_baseuri baseuri) in
+ Marshal.to_channel ch (magic,dump) [Marshal.Closures];
+ close_out ch
+;;
+
+let require ~baseuri =
+ let ch = open_in (path_of_baseuri baseuri) in
+ let mmagic,dump = Marshal.from_channel ch in
+ close_in ch;
+ if mmagic <> magic then
+ raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
+ else
+ dump
+;;
+
+let decompile ~baseuri =
+ Unix.unlink (path_of_baseuri baseuri)
+;;