X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=0620a6233dcdff5279e11b31e5b3762ad873ce68;hb=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=27fb0baf62db3722a378313847b69e91608cbd90;hpb=2b339969803b2ff9f5442c96a5736626712745f7;p=helm.git diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index 27fb0baf6..0620a6233 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -162,6 +162,11 @@ let time_travel0 (sto,ali) = let time_travel status = time_travel0 status#timestamp;; +let replace status = + let sto,ali = status#timestamp in + storage := sto; local_aliases := ali +;; + type obj = string * Obj.t (* includes are transitively closed; dependencies are only immediate *) type dump = @@ -190,6 +195,16 @@ let dump_obj status obj = status#set_dump {status#dump with objs = obj::status#dump.objs } ;; +let remove_objects ~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 map name = Sys.remove (Filename.concat path name) in + if HExtlib.is_dir path && HExtlib.is_regular (path ^ ".ng") then begin + HLog.warn ("removing contents of baseuri: " ^ uri); + Array.iter map (Sys.readdir path) + end + module type SerializerType = sig type dumpable_status @@ -210,7 +225,7 @@ module type SerializerType = val dependencies_of: baseuri:NUri.uri -> string list end -module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s end) = +module Serializer(D: sig type dumpable_s = private #dumpable_status end) = struct type dumpable_status = D.dumpable_s type 'a register_type = @@ -242,10 +257,12 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status end let serialize ~baseuri status = - let status = D.get status in let ch = open_out (ng_path_of_baseuri baseuri) in Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) []; close_out ch; +(* + remove_objects ~baseuri; (* FG: we remove the old objects before putting the new ones*) +*) List.iter (function | `Obj (uri,obj) -> @@ -260,12 +277,10 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status let require2 ~baseuri ~alias_only status = try - let s = D.get status in let status = - D.set status - (s#set_dump - {s#dump with - includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in + status#set_dump + {status#dump with + includes = baseuri::List.filter ((<>) baseuri) status#dump.includes} in let _dependencies,dump = require0 ~baseuri in List.fold_right (!require1 ~alias_only) dump status with @@ -278,32 +293,28 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = let baseuri = refresh_uri baseuri in - let alias_only = - alias_only || List.mem baseuri (get_transitively_included (D.get status)) - in - (*HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname);*) + if not alias_only && List.mem baseuri (get_transitively_included status) then status + else + (HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname); let status = require2 ~baseuri ~alias_only status in - (*HLog.warn ("done: include " ^ (if alias_only then "alias " else "") ^ fname);*) - status + HLog.warn ("done: include " ^ (if alias_only then "alias " else "") ^ fname); + status) in register#run "include" aux let require ~baseuri ~fname ~alias_only status = - let alias_only = - alias_only || List.mem baseuri (get_transitively_included (D.get status)) in - let status = - if not alias_only then - let s = D.get status in - D.set status - (s#set_dump {s#dump with dependencies = fname::s#dump.dependencies}) - else - status in - let status = require2 ~baseuri ~alias_only status in - let s = D.get status in - D.set status - (s#set_dump - {s#dump with - objs = record_include (baseuri,fname)::s#dump.objs }) + if not alias_only && List.mem baseuri (get_transitively_included status) then status + else + (let status = + if not alias_only then + status#set_dump + {status#dump with dependencies = fname::status#dump.dependencies} + else + status in + let status = require2 ~baseuri ~alias_only status in + status#set_dump + {status#dump with + objs = record_include (baseuri,fname)::status#dump.objs }) end let fetch_obj status uri = @@ -326,10 +337,10 @@ let aliases_of uri = if NUri.eq uri' uri then Some nref else None) !local_aliases ;; -let add_obj status ((u,_,_,_,_) as obj) = - NCicEnvironment.check_and_add_obj status obj; - storage := (`Obj (u,obj))::!storage; - let _,height,_,_,obj = obj in +let add_obj status ((u,_,_,_,_) as orig_obj) = + NCicEnvironment.check_and_add_obj status orig_obj; + storage := (`Obj (u,orig_obj))::!storage; + let _,height,_,_,obj = orig_obj in let references = match obj with NCic.Constant (_,name,None,_,_) -> @@ -361,7 +372,7 @@ let add_obj status ((u,_,_,_,_) as obj) = status#set_timestamp (!storage,!local_aliases) ;; -let add_constraint status u1 u2 = +let add_constraint status ~acyclic u1 u2 = if List.exists (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false) @@ -369,7 +380,7 @@ let add_constraint status u1 u2 = then (*CSC: raise an exception here! *) (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false); - NCicEnvironment.add_lt_constraint u1 u2; + NCicEnvironment.add_lt_constraint ~acyclic u1 u2; storage := (`Constr (u1,u2)) :: !storage; status#set_timestamp (!storage,!local_aliases) ;; @@ -386,4 +397,4 @@ let get_obj status u = raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))) ;; -NCicEnvironment.set_get_obj get_obj;; +NCicEnvironment.set_get_obj get_obj