added chronometer

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index f1b8f074c4dace915e1a51fefe3b94e9ab74e8d4..0496076e73b26a9968d1eb59b7f9f3e15c4c6029 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -19,9 +19,12 @@ let namer_of names =
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
 let tactic_of_ast = function
-  | TacticAst.Intros (_, _, names) ->
+  | TacticAst.Intros (_, None, names) ->
       (* TODO Zack implement intros length *)
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+  | TacticAst.Intros (_, Some num, names) ->
+      (* TODO Zack implement intros length *)
+      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -113,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
@@ -142,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
@@ -164,7 +197,25 @@ let eval_command status cmd =
         MatitaSync.add_inductive_def
           ~uri ~types ~params:[] ~leftno ~ugraph status
       in
-       {status with proof_status = No_proof }
+      (* aliases for the constructors and types *)
+      let aliases = env_of_list (extract_alias types uri) status.aliases in
+      (* aliases for the eliminations principles *)
+      let aliases = 
+        let base = String.sub suri 0 (String.length suri - 4)  in
+        env_of_list
+        (List.fold_left (
+          fun acc suffix -> 
+            if List.exists (
+              fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
+            ) status.objects then
+              let u = base ^ suffix in
+              (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
+            else
+              acc
+        ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) 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") 
@@ -195,6 +246,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!"