X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=96ec76013551e461c898863cd28dd7df17f0af64;hb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;hp=74340421f2c1f117dd268b7e93245fa2464a4d8a;hpb=7703897d2b14dd101c763a4aa6d99b7cc95011d1;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 74340421f..96ec76013 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -83,130 +83,44 @@ let set_proof_aliases status new_aliases = let extract_alias types uri = fst(List.fold_left ( fun (acc,i) (name, _, _, cl) -> - (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None)) - :: + (name, UriManager.uri_of_uriref uri i None) :: (fst(List.fold_left ( fun (acc,j) (name,_) -> - (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i - (Some j))) :: acc) , j+1) + (((name,UriManager.uri_of_uriref uri i + (Some j)) :: acc) , j+1) ) (acc,1) cl)),i+1 ) ([],0) types) let build_aliases = List.map - (fun (name,suri) -> + (fun (name,uri) -> DisambiguateTypes.Id name, - (suri, fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string suri))) + (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) -let add_aliases_for_inductive_def status types suri = - let uri = UriManager.uri_of_string suri in +let add_aliases_for_inductive_def status types uri = let aliases = build_aliases (extract_alias types uri) in set_proof_aliases status aliases -let add_alias_for_constant status suri = - let uri = UriManager.uri_of_string suri in +let add_alias_for_constant status uri = let name = UriManager.name_of_uri uri in - let new_env = build_aliases [(name,suri)] in + let new_env = build_aliases [(name,uri)] in set_proof_aliases status new_env -let add_aliases_for_object status suri = +let add_aliases_for_object status uri = function Cic.InductiveDefinition (types,_,_,_) -> - add_aliases_for_inductive_def status types suri - | Cic.Constant _ -> add_alias_for_constant status suri + add_aliases_for_inductive_def status types uri + | Cic.Constant _ -> add_alias_for_constant status uri | Cic.Variable _ | Cic.CurrentProof _ -> assert false -let paths_and_uris_of_obj uri status = - let basedir = get_string_option status "basedir" ^ "/xml" in - let innertypesuri = UriManager.innertypesuri_of_uri uri in - let bodyuri = UriManager.bodyuri_of_uri uri in - let univgraphuri = UriManager.univgraphuri_of_uri uri in - let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in - let innertypespath = basedir ^ "/" ^ innertypesfilename in - let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".xml.gz" in - let xmlpath = basedir ^ "/" ^ xmlfilename in - let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in - let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri - -let save_object_to_disk status uri obj ugraph univlist = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj = Cic2acic.plain_acic_object_of_cic_object obj in - (* prepare XML *) - let xml, bodyxml = - Cic2Xml.print_object - uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj - in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri = - paths_and_uris_of_obj uri status - in - List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); - (* now write to disk *) - ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath); - CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; - (* we return a list of uri,path we registered/created *) - (uri,xmlpath) :: - (univgraphuri,xmlunivgraphpath) :: - (* now the optional body, both write and register *) - (match bodyxml,bodyuri with - None,None -> [] - | Some bodyxml,Some bodyuri-> - ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath); - [bodyuri, xmlbodypath] - | _-> assert false) - -let typecheck_obj = - let profiler = HExtlib.profile "add_obj.typecheck_obj" in - fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj - -let index_obj = - let profiler = HExtlib.profile "add_obj.index_obj" in - fun ~dbd ~uri -> - profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri - let add_obj uri obj status = - let dbd = MatitaDb.instance () in - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - command_error (sprintf "%s already defined" suri) - else begin - typecheck_obj uri obj; (* 1 *) - let _, ugraph, univlist = - CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in - try - index_obj ~dbd ~uri; (* 2 must be in the env *) - try - let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*) - try - MatitaLog.message (sprintf "%s defined" suri); - let status = add_aliases_for_object status suri obj in - { status with objects = new_stuff @ status.objects; - proof_status = No_proof } - with exc -> - List.iter MatitaMisc.safe_remove (List.map snd new_stuff); (* -3 *) - raise exc - with exc -> - ignore(MatitaDb.remove_uri uri); (* -2 *) - raise exc - with exc -> - CicEnvironment.remove_obj uri; (* -1 *) - raise exc - end + let basedir = Helm_registry.get "matita.basedir" in + let status = + { add_aliases_for_object status uri obj with proof_status = No_proof} + in + LibrarySync.add_obj uri obj basedir; + status let add_obj = let profiler = HExtlib.profile "add_obj" in @@ -250,9 +164,6 @@ let id_list_diff l2 l1 = let diff = S.diff s2 s1 in S.fold (fun uri uris -> uri :: uris) diff [] -let remove_coercion uri = - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) - let time_travel ~present ~past = let objs_to_remove = urixstring_list_diff present.objects past.objects in let coercions_to_remove = uri_list_diff present.coercions past.coercions in @@ -260,17 +171,19 @@ let time_travel ~present ~past = id_list_diff present.notation_ids past.notation_ids in let debug_list = ref [] in - List.iter remove_coercion coercions_to_remove; + List.iter + (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)) + coercions_to_remove; List.iter (fun (uri,p) -> - MatitaMisc.safe_remove p; + HExtlib.safe_remove p; (try CicEnvironment.remove_obj uri with CicEnvironment.Object_not_found _ -> - MatitaLog.debug + HLog.debug (sprintf "time_travel removes from cache %s that is not in" (UriManager.string_of_uri uri))); - let l = MatitaDb.remove_uri uri in + let l = LibraryDb.remove_uri uri in debug_list := UriManager.string_of_uri uri :: !debug_list @ l) objs_to_remove; List.iter CicNotation.remove_notation notation_to_remove @@ -295,44 +208,9 @@ let time_travel ~present ~past = List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2 with | Invalid_argument _ | Exit -> - MatitaLog.debug "It seems you garbaged something..."; - MatitaLog.debug "l1:"; - List.iter MatitaLog.debug l1; - MatitaLog.debug "l2:"; - List.iter MatitaLog.debug l2 + HLog.debug "It seems you garbaged something..."; + HLog.debug "l1:"; + List.iter HLog.debug l1; + HLog.debug "l2:"; + List.iter HLog.debug l2 *) - -let last_baseuri = ref "" - -let remove ?(verbose=false) uri = - let derived_uris_of_uri uri = - UriManager.innertypesuri_of_uri uri :: - UriManager.univgraphuri_of_uri uri :: - (match UriManager.bodyuri_of_uri uri with - | None -> [] - | Some u -> [u]) - in - let to_remove = - uri :: - (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @ - derived_uris_of_uri uri - in - List.iter - (fun uri -> - (try - (* WARNING: non reentrant debugging code *) - if verbose then - let baseuri = UriManager.buri_of_uri uri in - if !last_baseuri <> baseuri then - begin - MatitaLog.debug ("Removing: " ^ baseuri ^ "/*"); - last_baseuri := baseuri - end; - let file = Http_getter.resolve' uri in - MatitaMisc.safe_remove file; - MatitaMisc.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - remove_coercion uri; - ignore (MatitaDb.remove_uri uri); - CicEnvironment.remove_obj uri) - to_remove