Makes the new Proofview.tactic the basic type of Ltac.

On the compilation of Coq, we can see an increase of ~20% compile time on
my completely non-scientific tests. Hopefully this can be fixed.

There are a lot of low hanging fruits, but this is an iso-functionality commit.
With a few exceptions which were not necessary for the compilation of the theories:
- The declarative mode is not yet ported
- The timeout tactical is currently deactivated because it needs some subtle
I/O. The framework is ready to handle it, but I haven't done it yet.
-  For much the same reason, the ltac debugger is unplugged. It will be more
difficult, but will eventually be back.

A few comments:
I occasionnally used a coercion from [unit Proofview.tactic] to the old
[Prooftype.tactic]. It should work smoothely, but loses any backtracking
information: the coerced tactics has at most one success.
- It is used in autorewrite (it shouldn't be a problem there). Autorewrite's
code is fairly old and tricky
- It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes
as we might want to have various success in a "Hint Extern". But it would
require a heavy port of eauto.ml4
- It is used in typeclass eauto, but with a little help from Matthieu, it should
be easy to port the whole thing to the new tactic engine, actually simplifying
the code.
- It is used in fourier. I believe it to be inocuous.
- It is used in firstorder and congruence. I think it's ok. Their code is
somewhat intricate and I'm not sure they would be easy to actually port.
- It is used heavily in Function. And honestly, I have no idea whether it can do
harm or not.

Updates:
(11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based
architecture for Ltac matching (r16533), which avoid painfully and expensively
working around the exception-throwing control flow of the previous API.
(11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730)
rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN
apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma,
rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially
tclREPEAT, causing rewrites to be tried in the side-conditions of conditional
rewrites as well). The new implementation makes Coq faster, but it is
pretty much impossible to tell if it is significant at all.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 18 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 1756f89ce..369107f6c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -42,11 +42,11 @@ let e_assumption gl =
   tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
 
 TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ e_assumption ]
+| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
 END
 
 TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ e_give_exact c ]
+| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
 END
 
 let registered_e_assumption gl =
@@ -58,7 +58,7 @@ let registered_e_assumption gl =
 (************************************************************************)
 
 let one_step l gl =
-  [Tactics.intro]
+  [Proofview.V82.of_tactic Tactics.intro]
   @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
   @ (List.map h_simplest_eapply l)
   @ (List.map assumption (pf_ids_of_hyps gl))
@@ -80,7 +80,7 @@ let prolog_tac l n gl =
     errorlabstrm "Prolog.prolog" (str "Prolog failed.")
 
 TACTIC EXTEND prolog
-| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
+| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ]
 END
 
 open Auto
@@ -100,7 +100,7 @@ let unify_e_resolve flags (c,clenv) gls =
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
     registered_e_assumption ::
-    (tclTHEN Tactics.intro
+    (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
        (function g'->
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
@@ -134,7 +134,7 @@ and e_my_find_search db_list local_db hdc concl =
                tclTHEN (unify_e_resolve st (term,cl))
 		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> h_reduce (Unfold [AllOccurrences,c]) onConcl
-	   | Extern tacast -> conclPattern concl p tacast
+	   | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
        in
        (tac,lazy (pr_autotactic t)))
   in
@@ -241,7 +241,7 @@ module SearchProblem = struct
 	     { depth = s.depth; tacres = res;
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb; prev = ps })
-	  (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
+	  (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")])
       in
       let rec_tacs =
 	let l =
@@ -412,7 +412,7 @@ END
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND new_eauto
@@ -426,19 +426,19 @@ END
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto ~debug:Debug (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto ~debug:Info (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND dfs_eauto
 | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
-    [ gen_eauto (true, make_depth p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ]
 END
 
 let cons a l = a :: l
@@ -472,7 +472,7 @@ let autounfold_tac db cls gl =
 open Extraargs
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> [ autounfold_tac db id ]
+| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> [ Proofview.V82.tactic (autounfold_tac db id) ]
 END
 
 let unfold_head env (ids, csts) c = 
@@ -537,28 +537,30 @@ let autounfold_one db cl gl =
       
 TACTIC EXTEND autounfold_one
 | [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
-    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+    [ Proofview.V82.tactic (autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp))) ]
 | [ "autounfold_one" hintbases(db) ] ->
-    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
+    [ Proofview.V82.tactic (autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None) ]
       END
 
 TACTIC EXTEND autounfoldify
 | [ "autounfoldify" constr(x) ] -> [
+  Proofview.V82.tactic (
     let db = match kind_of_term x with
       | Const c -> Label.to_string (con_label c)
       | _ -> assert false
-    in autounfold ["core";db] onConcl ]
+    in autounfold ["core";db] onConcl 
+  )]
 END
 
 TACTIC EXTEND unify
-| ["unify" constr(x) constr(y) ] -> [ unify x y ]
+| ["unify" constr(x) constr(y) ] -> [ Proofview.V82.tactic (unify x y) ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
-    unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
+    Proofview.V82.tactic (unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y) ]
 END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Proofview.V82.tactic (convert_concl_no_check x DEFAULTcast) ]
 END