From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 30 May 2005 11:40:00 +0000 (+0000)
Subject: added automathic aliases.
X-Git-Tag: PRE_INDEX_1~106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94ed0c877bd8b776c9fdaf4709a46f6ab2f3c415;p=helm.git

added automathic aliases.
---

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