X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=5f1f5b6c29e676ac84cb49ac7595f9df3c9ee7e4;hb=73e63e535940a068e660d3688a3c8ebfa1930561;hp=2547bbdfc1cbab499f2053dbf9326d476ab962a4;hpb=d83fc9accd4ba44a6296eb707b2f62900380f00a;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 2547bbdfc..5f1f5b6c2 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -30,32 +30,33 @@ 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 - begin - try - let description1 = fst(Map.find domain_item from.aliases) in - let description2 = fst(Map.find domain_item status.aliases) in - if description1 <> description2 then - Map.add domain_item codomain_item acc - else - acc - with Not_found -> acc - end) + (fun domain_item (description1,_ as codomain_item) acc -> + try + let description2,_ = Map.find domain_item from.aliases in + if description1 <> description2 then + Map.add domain_item codomain_item acc + else + acc + with + Not_found -> + Map.add domain_item codomain_item acc) status.aliases Map.empty +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 set_proof_aliases status aliases = - let new_status = {status with aliases = aliases } in + let new_status = { status with aliases = aliases } in let diff = alias_diff ~from:status new_status in - let textual_diff = - if DisambiguateTypes.Environment.is_empty diff then - "" - else - DisambiguatePp.pp_environment diff ^ "\n" in - let moo_content_rev = textual_diff :: status.moo_content_rev in - {new_status with moo_content_rev = moo_content_rev} + let multi_aliases = + DisambiguateTypes.Environment.fold DisambiguateTypes.Environment.cons + diff status.multi_aliases in + let new_status = { new_status with multi_aliases = multi_aliases } in + if DisambiguateTypes.Environment.is_empty diff then + new_status + else + add_moo_content (DisambiguatePp.commands_of_environment diff) new_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 **) @@ -115,17 +116,11 @@ let save_object_to_disk status uri obj = MatitaMisc.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 = paths_and_uris_of_obj uri status @@ -134,12 +129,10 @@ let save_object_to_disk status uri obj = List.iter MatitaMisc.mkdir (List.map Filename.dirname [innertypespath; 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) ; (* we return a list of uri,path we registered/created *) - (uri,xmlpath) :: (innertypesuri,innertypespath) :: + (uri,xmlpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with None,None -> [] @@ -149,20 +142,50 @@ let save_object_to_disk status uri obj = [bodyuri, xmlbodypath] | _-> 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 index_obj = + let profiler = CicUtil.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 -> + profiler.CicUtil.profile (save_object_to_disk status uri) obj + 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 - 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 *) + try + index_obj ~dbd ~uri; (* 2 must be in the env *) + try + let new_stuff = save_object_to_disk status uri obj 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 = CicUtil.profile "add_obj" in + fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status module OrderedUri = struct @@ -266,5 +289,6 @@ let remove ~verbose uri = MatitaMisc.safe_remove (Http_getter.resolve' uri) 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