X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=cc13dde6e306959c18ba48d0a64f4a992c1e7012;hb=c7a74f0ef29118fc97c1a6283f4249a0ed4b0ba1;hp=a5ecefad8fb0dcd18ee4879f8dbfb95ebcdd5e35;hpb=e48acbc0d00717ce8f12412673ece4e4ee0e9642;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index a5ecefad8..cc13dde6e 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -11,19 +11,187 @@ (* $Id$ *) -exception ObjectNotFound of string Lazy.t +exception LibraryOutOfSync of string Lazy.t -let cache = NUri.UriHash.create 313;; +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 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 time0 +;; + +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 +;; + +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 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; + !storage,!aliases,!cache +;; let get_obj u = - try NUri.UriHash.find cache u - with Not_found -> - (* in the final implementation should get it from disk *) - let ouri = NUri.ouri_of_nuri u in - 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; - HExtlib.list_last l + try List.assq u !storage + with Not_found -> + 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) -> cache:= NUri.UriMap.add u o !cache) l; + HExtlib.list_last l + with CicEnvironment.Object_not_found u -> + raise (NCicEnvironment.ObjectNotFound + (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u)))) ;; + +let clear_cache () = cache := NUri.UriMap.empty;; + +NCicEnvironment.set_get_obj get_obj;; +NCicPp.set_get_obj get_obj;;