X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=716aa04d29f2c6f34e4280cfca3bdf49c2583333;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=4005aeb11b4a6a77dc446b67c709fb33da297632;hpb=03be93eb7712b24fa90fcaf7b9b79df99e1f4105;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 4005aeb11..716aa04d2 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -43,10 +43,22 @@ let alias_diff ~from status = status.aliases [] let alias_diff = - let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in - fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status + let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in + fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status let set_proof_aliases status new_aliases = + let commands_of_aliases = + List.map + (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias)) + in + let deps_of_aliases = + HExtlib.filter_map + (function + | GrafiteAst.Ident_alias (_, suri) -> + let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in + Some (GrafiteAst.Dependency buri) + | _ -> None) + in let aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) status.aliases new_aliases in @@ -59,12 +71,15 @@ let set_proof_aliases status new_aliases = if new_aliases = [] then new_status else - add_moo_content - (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases) - new_status + let aliases = + DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases + in + let status = add_moo_content (commands_of_aliases aliases) new_status in + let status = add_moo_metadata (deps_of_aliases aliases) status in + status (** given a uri and a type list (the contructors types) builds a list of pairs - * (name,uri) that is used to generate authomatic aliases **) + * (name,uri) that is used to generate automatic aliases **) let extract_alias types uri = fst(List.fold_left ( fun (acc,i) (name, _, _, cl) -> @@ -125,7 +140,7 @@ let paths_and_uris_of_obj uri status = let save_object_to_disk status uri obj ugraph univlist = let ensure_path_exists path = let dir = Filename.dirname path in - MatitaMisc.mkdir dir + 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 @@ -139,14 +154,13 @@ let save_object_to_disk status uri obj ugraph univlist = paths_and_uris_of_obj uri status in let path_scheme_of path = "file://" ^ path in - List.iter MatitaMisc.mkdir - (List.map Filename.dirname [innertypespath; xmlpath]); + 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) :: (innertypesuri,innertypespath) :: + (uri,xmlpath) :: (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with @@ -158,18 +172,13 @@ let save_object_to_disk status uri obj ugraph univlist = | _-> assert false) let typecheck_obj = - let profiler = CicUtil.profile "add_obj.typecheck_obj" in - fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) 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 = CicUtil.profile "add_obj.index_obj" in + let profiler = HExtlib.profile "add_obj.index_obj" in fun ~dbd ~uri -> - profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri - -let save_object_to_disk = - let profiler = CicUtil.profile "add_obj.save_object_to_disk" in - fun status uri obj ugraph univlist -> - profiler.CicUtil.profile (save_object_to_disk status uri obj ugraph) univlist + profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri let add_obj uri obj status = let dbd = MatitaDb.instance () in @@ -201,8 +210,8 @@ let add_obj uri obj status = end let add_obj = - let profiler = CicUtil.profile "add_obj" in - fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status + let profiler = HExtlib.profile "add_obj" in + fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status module OrderedUri = struct @@ -220,13 +229,20 @@ module UriSet = Set.Make (OrderedUri) module IdSet = Set.Make (OrderedId) (** @return l2 \ l1 *) -let uri_list_diff l2 l1 = +let urixstring_list_diff l2 l1 = let module S = UriSet in let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in let diff = S.diff s2 s1 in S.fold (fun uri uris -> uri :: uris) diff [] +let uri_list_diff l2 l1 = + let module S = UriManager.UriSet in + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + (** @return l2 \ l1 *) let id_list_diff l2 l1 = let module S = IdSet in @@ -239,15 +255,16 @@ let remove_coercion uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) let time_travel ~present ~past = - let objs_to_remove = uri_list_diff present.objects past.objects in + let objs_to_remove = urixstring_list_diff present.objects past.objects in + let coercions_to_remove = uri_list_diff present.coercions past.coercions in let notation_to_remove = 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,p) -> MatitaMisc.safe_remove p; - remove_coercion uri; (try CicEnvironment.remove_obj uri with CicEnvironment.Object_not_found _ -> @@ -286,7 +303,9 @@ let time_travel ~present ~past = List.iter MatitaLog.debug l2 *) -let remove ~verbose uri = +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 :: @@ -302,9 +321,17 @@ let remove ~verbose uri = List.iter (fun uri -> (try + (* WARNING: non reentrant debugging code *) if verbose then - MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); - MatitaMisc.safe_remove (Http_getter.resolve' uri) + 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);