From: Claudio Sacerdoti Coen Date: Fri, 23 Sep 2005 09:51:21 +0000 (+0000) Subject: The new_aliases argument of the functions alias_diff and set_proof_aliases X-Git-Tag: LAST_BEFORE_NEW~48 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=675c9cf70d8537d70675b5520ca708fe75c67aed;p=helm.git The new_aliases argument of the functions alias_diff and set_proof_aliases used to be a whole environment. It is now just the diff! Much more efficient! --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0cab549b1..644b492fa 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -170,7 +170,7 @@ let disambiguate_term status_ref term = ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in status_ref := status; cic @@ -189,7 +189,7 @@ let disambiguate_lazy_term status_ref term = ~universe:(Some status.multi_aliases) ~context ~metasenv term) in let status = MatitaTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in status_ref := status; cic, metasenv, ugraph) @@ -652,7 +652,7 @@ let disambiguate_obj status obj = | Intermediate _ -> assert false in let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in status, cic let disambiguate_command status = function @@ -757,37 +757,30 @@ let eval_command opts status cmd = | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion | GrafiteAst.Alias (loc, spec) -> - let aliases = + let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Id id) - (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) - status.aliases + [DisambiguateTypes.Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symb,instance)) - (DisambiguateChoices.lookup_symbol_by_dsc symb desc) - status.aliases + [DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc] | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases + [DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc] in - MatitaSync.set_proof_aliases status aliases + MatitaSync.set_proof_aliases status diff | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status' = add_moo_content [stm] status in - let aliases' = - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symbol, 0)) - (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) - status.aliases + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] in - MatitaSync.set_proof_aliases status' aliases' + MatitaSync.set_proof_aliases status' diff | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status | GrafiteAst.Obj (loc,obj) -> let ext,name = diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index a4f805bfb..c58e0fa39 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -110,16 +110,15 @@ let eval_with_engine guistuff status user_goal parsed_text st = match ex with | TA.Command (_, TA.Alias _) | TA.Command (_, TA.Include _) - | TA.Command (_, TA.Interpretation _) -> - DisambiguateTypes.Environment.empty + | TA.Command (_, TA.Interpretation _) -> [] | _ -> MatitaSync.alias_diff ~from:status new_status in (* we remove the defined object since we consider them "automatic aliases" *) let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - DTE.fold ( - fun k ((v,_) as value) (initial_space,status,acc) -> + List.fold_left ( + fun (initial_space,status,acc) (k,((v,_) as value)) -> let b = try let v = UM.strip_xpointer (UM.uri_of_string v) in @@ -133,12 +132,14 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space = if initial_space = "" then "\n" else initial_space in initial_space ^ - DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty) in let new_status = - MatitaSync.set_proof_aliases status (DTE.add k value status.aliases) + MatitaSync.set_proof_aliases status [k,value] in "\n",new_status,((new_status, new_text)::acc) - ) new_aliases (initial_space,status,[]) in + ) (initial_space,status,[]) new_aliases in let parsed_text = initial_space ^ parsed_text in let res = List.rev new_status_and_text_list_rev @ new_status_and_text_list' @ diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 5f1f5b6c2..3351725db 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -34,29 +34,39 @@ let alias_diff ~from status = try let description2,_ = Map.find domain_item from.aliases in if description1 <> description2 then - Map.add domain_item codomain_item acc + (domain_item,codomain_item)::acc else acc with Not_found -> - Map.add domain_item codomain_item acc) - status.aliases Map.empty + (domain_item,codomain_item)::acc) + 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 set_proof_aliases status aliases = - let new_status = { status with aliases = aliases } in - let diff = alias_diff ~from:status new_status in +let set_proof_aliases status new_aliases = + let aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) + status.aliases new_aliases in 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 + 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 - add_moo_content (DisambiguatePp.commands_of_environment diff) new_status + add_moo_content + (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases) + new_status + +let compute_diff_and_set_proof_aliases status aliases = + let new_status = { status with aliases = aliases } in + let diff = alias_diff ~from:status new_status in + set_proof_aliases status diff (** given a uri and a type list (the contructors types) builds a list of pairs * (name,uri) that is used to generate authomatic aliases **) @@ -72,19 +82,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 = diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 492bc8c3b..2175a23dc 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -33,11 +33,17 @@ val time_travel: * that the second one can only have more aliases than the first one * @return the list of aliases that should be added to aliases of from in * order to be equal to aliases of the second argument *) -val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> - DisambiguateTypes.environment +val alias_diff: + from:MatitaTypes.status -> MatitaTypes.status -> + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list (** set the proof aliases enriching the moo_content *) val set_proof_aliases : + MatitaTypes.status -> + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> + MatitaTypes.status + +val compute_diff_and_set_proof_aliases : MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter