X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=e2e7d1b34054a0448950d75596034a14019cceaa;hb=42fb6dce8110e29ccf233c09e6d6b1d58d9e5fef;hp=87f0cb31b122f8e9f487a4187a947d143559f327;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index 87f0cb31b..e2e7d1b34 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,13 @@ 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; + + if Helm_registry.get_bool "matita.remove_old_objects" then + remove_objects ~baseuri; (* FG: we remove the old objects before putting the new ones*) + List.iter (function | `Obj (uri,obj) -> @@ -260,12 +278,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 @@ -277,35 +293,29 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status let record_include = let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = - 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); + let baseuri = refresh_uri baseuri in + 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 + 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 - includes = baseuri::s#dump.includes; - 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 = @@ -328,10 +338,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,_,_) -> @@ -363,7 +373,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) @@ -371,7 +381,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) ;; @@ -388,4 +398,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