added automathic aliases.

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index f1b8f074c4dace915e1a51fefe3b94e9ab74e8d4..89949cd1db8099e724f0ba77bb08da13830eb03e 100644 (file)
--- 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 c8fbba9bee8a66c777ff205cb0d351aef5841ff4..58043bbd3d5acb44ab3af00adb206135c8f12f24 100644 (file)
--- 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