X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=716aa04d29f2c6f34e4280cfca3bdf49c2583333;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=8f8a66e098fc9378e73ace85e7c2d1a5d8e93e05;hpb=6fa3a1e91d8a1e647775ca101255633ba265a9f2;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 8f8a66e09..716aa04d2 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -30,23 +30,56 @@ open MatitaTypes let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in Map.fold - (fun domain_item codomain_item acc -> - if not (Map.mem domain_item from.aliases) then - Map.add domain_item codomain_item acc - else - acc) - status.aliases Map.empty + (fun domain_item (description1,_ as codomain_item) acc -> + try + let description2,_ = Map.find domain_item from.aliases in + if description1 <> description2 then + (domain_item,codomain_item)::acc + else + acc + with + Not_found -> + (domain_item,codomain_item)::acc) + status.aliases [] + +let alias_diff = + 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 + let multi_aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) + status.multi_aliases new_aliases in + let new_status = + { status with multi_aliases = multi_aliases ; aliases = aliases} + in + if new_aliases = [] then + new_status + else + 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 -let set_proof_aliases status aliases = - let new_status = {status with aliases = aliases } in - let diff = alias_diff ~from:status new_status in - let moo_content_rev = - CicTextualParser2.EnvironmentP3.to_string diff :: - status.moo_content_rev in - {new_status with moo_content_rev = moo_content_rev} - (** 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) -> @@ -59,19 +92,21 @@ let extract_alias types uri = ) (acc,1) cl)),i+1 ) ([],0) types) -let env_of_list l env = - let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in - DisambiguateTypes.env_of_list l' env +let build_aliases = + List.map + (fun (name,suri) -> + DisambiguateTypes.Id name, + (suri, fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string suri))) let add_aliases_for_inductive_def status types suri = let uri = UriManager.uri_of_string suri in - let aliases = env_of_list (extract_alias types uri) status.aliases in - set_proof_aliases status aliases + 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 name = UriManager.name_of_uri uri in - let new_env = env_of_list [(name,suri)] status.aliases in + let new_env = build_aliases [(name,suri)] in set_proof_aliases status new_env let add_aliases_for_object status suri = @@ -83,9 +118,10 @@ let add_aliases_for_object status suri = | Cic.CurrentProof _ -> assert false let paths_and_uris_of_obj uri status = - let basedir = get_string_option status "basedir" in + 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 @@ -95,55 +131,54 @@ let paths_and_uris_of_obj uri status = let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".body.xml.gz" in let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri + 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 = +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,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = - Cic2acic.acic_object_of_cic_object ~eta_fix:false obj - in + let annobj = Cic2acic.plain_acic_object_of_cic_object obj in (* prepare XML *) let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false - annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter:false + Cic2Xml.print_object + uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri = 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 innertypespath; - Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath) ; - (* now register to the getter *) - Http_getter.register' innertypesuri (path_scheme_of innertypespath); - Http_getter.register' uri (path_scheme_of 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 None,None -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; - Http_getter.register' bodyuri (path_scheme_of xmlbodypath); - [bodyuri,xmlbodypath] + Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + [bodyuri, xmlbodypath] | _-> assert false) -let remove_object_from_disk uri path = - Sys.remove path; - Http_getter.unregister' uri +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 @@ -151,14 +186,32 @@ let add_obj uri obj status = if CicEnvironment.in_library uri then command_error (sprintf "%s already defined" suri) else begin - CicTypeChecker.typecheck_obj uri obj; - MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) - let new_stuff = save_object_to_disk status uri obj in - 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 } + 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 add_obj = + let profiler = HExtlib.profile "add_obj" in + fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status module OrderedUri = struct @@ -166,44 +219,63 @@ struct let compare (u1, _) (u2, _) = UriManager.compare u1 u2 end +module OrderedId = +struct + type t = CicNotation.notation_id + let compare = Pervasives.compare +end + module UriSet = Set.Make (OrderedUri) +module IdSet = Set.Make (OrderedId) -(* returns the uri of objects that were added in the meanwhile... - * status1 ----> status2 - * assumption: objects defined in status2 are a superset of those defined in - * status1 - *) -let delta_status status1 status2 = + (** @return l2 \ l1 *) +let urixstring_list_diff l2 l1 = let module S = UriSet in - let diff l1 l2 = - 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 [] - in - diff status1.objects status2.objects + 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 + 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 remove_coercion uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) let time_travel ~present ~past = - let list_of_objs_to_remove = List.rev (delta_status past present) in - (* List.rev is just for the debugging code, which otherwise may list both - * something.ind and something.ind#xpointer ... (ask Enrico :-) *) + 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 (fun (uri,p) -> - remove_object_from_disk uri p; - remove_coercion uri; - (try - CicEnvironment.remove_obj uri - with CicEnvironment.Object_not_found _ -> - MatitaLog.debug - (sprintf "time_travel removes from cache %s that is not in" - (UriManager.string_of_uri uri))); - let l = MatitaDb.remove_uri uri in - debug_list := UriManager.string_of_uri uri :: !debug_list @ l) - list_of_objs_to_remove; - + List.iter remove_coercion coercions_to_remove; + List.iter + (fun (uri,p) -> + MatitaMisc.safe_remove p; + (try + CicEnvironment.remove_obj uri + with CicEnvironment.Object_not_found _ -> + MatitaLog.debug + (sprintf "time_travel removes from cache %s that is not in" + (UriManager.string_of_uri uri))); + let l = MatitaDb.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 + (* (* this is debug code * idea: debug_list is the list of objects to be removed as computed from the * db, while list_of_objs_to_remove is the same list but computer from the @@ -229,15 +301,17 @@ let time_travel ~present ~past = List.iter MatitaLog.debug l1; MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 + *) +let last_baseuri = ref "" -let remove uri = +let remove ?(verbose=false) uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: - UriManager.annuri_of_uri uri :: + UriManager.univgraphuri_of_uri uri :: (match UriManager.bodyuri_of_uri uri with | None -> [] - | Some u -> [u]) + | Some u -> [u]) in let to_remove = uri :: @@ -247,17 +321,19 @@ let remove uri = List.iter (fun uri -> (try - let path = - let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in - assert (String.sub path 0 7 = "file://"); - String.sub path 7 (String.length path - 7) - in - MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); - remove_object_from_disk uri path; - with - Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri); + (* 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)) + ignore (MatitaDb.remove_uri uri); + CicEnvironment.remove_obj uri) to_remove - -