From 94ed0c877bd8b776c9fdaf4709a46f6ab2f3c415 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 May 2005 11:40:00 +0000 Subject: [PATCH] added automathic aliases. --- helm/matita/matitaEngine.ml | 26 +++++++++++++++++++++++++- helm/matita/matitaScript.ml | 13 +++++++++++++ 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f1b8f074c..89949cd1d 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -164,7 +164,31 @@ let eval_command status cmd = MatitaSync.add_inductive_def ~uri ~types ~params:[] ~leftno ~ugraph status in - {status with proof_status = No_proof } + let extract_alias types uri = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + ((name, UriManager.string_of_uriref (uri,[i])) + :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) + ) (acc,1) cl))),i+1 + ) ([],0) types) + in + let env_of_list l e = + let module DT = DisambiguateTypes in + let module DTE = DisambiguateTypes.Environment in + List.fold_left ( + fun e (name,uri) -> + DTE.add + (DT.Id name) + (uri,fun _ _ _ -> CicUtil.term_of_uri uri) + e + ) e l + in + let aliases = env_of_list (extract_alias types uri) status.aliases in + let status = {status with proof_status = No_proof } in + { status with aliases = aliases} | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c8fbba9be..58043bbd3 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -85,6 +85,19 @@ let eval_with_engine status user_goal parsed_text st = DisambiguateTypes.Environment.empty | _ -> MatitaSync.alias_diff ~from:status new_status in + (* we remove the defined object since we consider them "automathic aliases" *) + let new_aliases = + let module DTE = DisambiguateTypes.Environment in + let module UM = UriManager in + DTE.fold ( + fun k ((v,_) as value) acc -> + let v = UM.strip_xpointer (UM.uri_of_string v) in + if List.exists (fun (s,_) -> s = v) new_status.objects then + acc + else + DTE.add k value acc + ) new_aliases DTE.empty + in let new_text = if DisambiguateTypes.Environment.is_empty new_aliases then parsed_text -- 2.39.2