X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=d54002d60c9c60dabf96ac50bca3808824d054f9;hb=c18631e6e9aad36446af0c126e8616272f44a08a;hp=4e91334170555f6f5c75638e00ced633c4321e4a;hpb=585469505faa97c21687128490828a1aabee94ee;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 4e9133417..d54002d60 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -11,30 +11,198 @@ (* $Id$ *) -exception ObjectNotFound of string Lazy.t +exception LibraryOutOfSync of string Lazy.t +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 add_obj u obj = storage := (u,obj)::!storage;; +let aliases = ref [];; +let cache = ref NUri.UriMap.empty;; + +class status = + object + val timestamp = (time0 : timestamp) + method timestamp = timestamp + method set_timestamp v = {< timestamp = v >} + method set_library_status (o : status) = {< timestamp = o#timestamp >} + end + +let time_travel status = + let sto,ali,cac = status#timestamp in + storage := sto; aliases := ali; cache := cac +;; + +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 magic = 0;; + +let require0 ~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 serialize ~baseuri dump = + let ch = open_out (path_of_baseuri baseuri) in + Marshal.to_channel ch (magic,dump) [Marshal.Closures]; + close_out ch; + List.iter + (fun (uri,obj) -> + let ch = open_out (path_of_baseuri uri) in + Marshal.to_channel ch (magic,obj) []; + close_out ch + ) !storage; + time_travel (new status) +;; + +let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; + +let rec refresh_uri_in_term = + function + NCic.Const (NReference.Ref (u,spec)) -> + NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) + | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t +;; + +let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = + assert (metasenv = []); + assert (subst = []); + uri,height,metasenv,subst, + NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind +;; -let cache = NUri.UriHash.create 313;; +module type Serializer = + sig + type status + type obj + val register: + string -> + ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) + val serialize: baseuri:NUri.uri -> obj list -> unit + val require: baseuri:NUri.uri -> status -> status + end + +module Serializer(S: sig type status end) = + struct + type status = S.status + type obj = string * Obj.t + + let require1 = ref (fun _ -> assert false (* unknown data*)) + let already_registered = ref [] + + let register tag require = + assert (not (List.mem tag !already_registered)); + already_registered := tag :: !already_registered; + require1 := + (fun (tag',data) as x -> + if tag=tag' then + require (Obj.magic data) ~refresh_uri_in_term + else + !require1 x); + (fun x -> tag,Obj.repr x) + + let serialize = serialize + + let require ~baseuri status = + let dump = require0 ~baseuri in + List.fold_right !require1 dump status +end + +let decompile ~baseuri = + Unix.unlink (path_of_baseuri baseuri) + (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *) +;; + +let fetch_obj uri = + let obj = require0 ~baseuri:uri in + refresh_uri_in_obj obj +;; + +let resolve name = + try + HExtlib.filter_map + (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases + with + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) +;; + +let aliases_of uri = + try + HExtlib.filter_map + (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases + with + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) +;; + +let add_obj status u obj = + storage := (u,obj)::!storage; + let _,height,_,_,obj = obj in + let references = + match obj with + NCic.Constant (_,name,None,_,_) -> + [u,name,NReference.reference_of_spec u NReference.Decl] + | NCic.Constant (_,name,Some _,_,_) -> + [u,name,NReference.reference_of_spec u (NReference.Def height)] + | NCic.Fixpoint (is_ind,fl,_) -> + HExtlib.list_mapi + (fun (_,name,recno,_,_) i -> + if is_ind then + u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height)) + else + u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl + | NCic.Inductive (inductive,leftno,il,_) -> + List.flatten + (HExtlib.list_mapi + (fun (_,iname,_,cl) i -> + HExtlib.list_mapi + (fun (_,cname,_) j-> + u,cname, + NReference.reference_of_spec u (NReference.Con (i,j+1,leftno)) + ) cl @ + [u,iname, + NReference.reference_of_spec u + (NReference.Ind (inductive,i,leftno))] + ) il) + in + aliases := references @ !aliases; + status#set_timestamp (!storage,!aliases,!cache) +;; let get_obj u = try List.assq u !storage with Not_found -> - try NUri.UriHash.find cache u - with Not_found -> - (* in the final implementation should get it from disk *) + try fetch_obj u + with Sys_error _ -> + try NUri.UriMap.find u !cache + with Not_found -> 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 + raise (NCicEnvironment.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;; + +NCicEnvironment.set_get_obj get_obj;; +NCicPp.set_get_obj get_obj;;