added automathic aliases.

[helm.git] / helm / matita / matitaEngine.ml

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")