From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 15:06:49 +0000 (+0000) Subject: Great speed-up in alias_diff (about 3x). X-Git-Tag: LAST_BEFORE_NEW~94 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e64a1cf254620a3397bceabee53f2726a06ee0e7;p=helm.git Great speed-up in alias_diff (about 3x). NOTE: alias_diff is still quite slow (e.g. 2.4s in the processing of factorization.ma). This function really deserves to be got rid of. (Moreover, this is possible and not that difficult) --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index e47e11d1b..7521cb49f 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -90,6 +90,11 @@ TODO - riattaccare hbugs (brrr...) -> Zack GUI LOGICA + - la funzione alias_diff e' lentissima (anche se CSC l'ha accellerata di + un fattore 3x) e puo' essere evitata: chi vuole aggiungere alias (la + disambiguazione, il comando "alias" e l'add_obj) deve indicare + esplicitamente quali sono i nuovi alias, evitando cosi' la diff per + scoprirlo - matitac deve fallire quando matita vuole aggiungere un alias! - default equality e famiglia non e' undo-aware - nuovo pretty-printer testuale: non stampa usando la notazione diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 4d549fade..6662b7d6e 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -30,22 +30,22 @@ 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 "accusato" 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 diff = alias_diff ~from:status new_status in