From ed4f1ffcd1e53f768fffcbe404c8343cc8ca8608 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 31 May 2005 08:40:54 +0000
Subject: [PATCH] added automathic aliases for qed and definition

---
 helm/matita/matitaEngine.ml | 57 +++++++++++++++++++++++--------------
 1 file changed, 35 insertions(+), 22 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 990276878..eb355f2ea 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -116,6 +116,31 @@ let eval_tactical status tac =
   in
   apply_tactic (tactical_of_ast tac)
 
+(** given a uri and a type list (the contructors types) builds a list of pairs
+ *  (name,uri) that is used to generate authomatic aliases **)
+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)
+
+(** adds a (name,uri) list l to a disambiguation environment e **)
+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
+
 let eval_command status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> set_option status name value
@@ -145,6 +170,11 @@ let eval_command status cmd =
           "type you've declared!");
       MatitaLog.message (sprintf "%s defined" suri);
       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
+      let status = 
+        let name = UriManager.name_of_uri uri in
+        let new_env = env_of_list [(name,suri)] status.aliases in
+        {status with aliases = new_env }
+      in
       {status with proof_status = No_proof }
   | TacticAst.Inductive (loc, dummy_params, types) ->
       (* dummy_params are not real params, it is a list of nothing, and the only
@@ -167,28 +197,6 @@ let eval_command status cmd =
         MatitaSync.add_inductive_def
           ~uri ~types ~params:[] ~leftno ~ugraph status
       in
-      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}
@@ -222,6 +230,11 @@ let eval_command status cmd =
       let body = CicMetaSubst.apply_subst subst body in
       let ty = CicMetaSubst.apply_subst subst ty in
       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
+      let status = 
+        let suri = UriManager.string_of_uri uri in
+        let new_env = env_of_list [(name,suri)] status.aliases in
+        {status with aliases = new_env }
+      in
       {status with proof_status = No_proof}
   | TacticAst.Theorem (_, _, None, _, _) ->
       command_error "The grammas should avoid having unnamed theorems!"
-- 
2.39.2