X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=d54002d60c9c60dabf96ac50bca3808824d054f9;hb=c18631e6e9aad36446af0c126e8616272f44a08a;hp=414e5c5de1fad5296fefc5f9fdd8549fbb87ffe6;hpb=f6c887944d48d718f372a57f1609f3d059908aa8;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 414e5c5de..d54002d60 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -11,7 +11,6 @@ (* $Id$ *) -exception ObjectNotFound of string Lazy.t exception LibraryOutOfSync of string Lazy.t type timestamp = @@ -24,7 +23,18 @@ let storage = ref [];; let aliases = ref [];; let cache = ref NUri.UriMap.empty;; -let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;; +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 @@ -57,14 +67,33 @@ let serialize ~baseuri dump = Marshal.to_channel ch (magic,obj) []; close_out ch ) !storage; - time_travel time0 + 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 ;; module type Serializer = sig type status type obj - val register: string -> ('a -> status -> status) -> ('a -> 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 @@ -72,7 +101,7 @@ module type Serializer = module Serializer(S: sig type status end) = struct type status = S.status - type obj = Obj.t + type obj = string * Obj.t let require1 = ref (fun _ -> assert false (* unknown data*)) let already_registered = ref [] @@ -82,14 +111,17 @@ module Serializer(S: sig type status end) = already_registered := tag :: !already_registered; require1 := (fun (tag',data) as x -> - if tag=tag' then Obj.magic require data else Obj.magic !require1 x); - Obj.magic (fun x -> tag,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 (Obj.magic !require1) dump status + List.fold_right !require1 dump status end let decompile ~baseuri = @@ -97,11 +129,9 @@ let decompile ~baseuri = (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *) ;; -(* the miracles of Marshal... *) let fetch_obj uri = let obj = require0 ~baseuri:uri in - (* here we need to refresh the URIs! *) - obj + refresh_uri_in_obj obj ;; let resolve name = @@ -109,7 +139,7 @@ let resolve name = HExtlib.filter_map (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases with - Not_found -> raise (ObjectNotFound (lazy name)) + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) ;; let aliases_of uri = @@ -117,10 +147,10 @@ let aliases_of uri = HExtlib.filter_map (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases with - Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri))) + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) ;; -let add_obj u obj = +let add_obj status u obj = storage := (u,obj)::!storage; let _,height,_,_,obj = obj in let references = @@ -151,7 +181,7 @@ let add_obj u obj = ) il) in aliases := references @ !aliases; - !storage,!aliases,!cache + status#set_timestamp (!storage,!aliases,!cache) ;; let get_obj u = @@ -168,8 +198,11 @@ let get_obj u = 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 () = cache := NUri.UriMap.empty;; + +NCicEnvironment.set_get_obj get_obj;; +NCicPp.set_get_obj get_obj;;