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, 32 insertions, 22 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 92b27c3e8..0cf4d3bb4 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -109,6 +109,7 @@ open Pattern
 open Patternops
 open Matching
 open Tacmach
+open Proofview.Notations
 (*i*)
 
 (*s First, we need to access some Coq constants
@@ -219,14 +220,16 @@ let compute_rhs bodyi index_of_f =
 
 (*s Now the function [compute_ivs] itself *)
 
-let compute_ivs gl f cs =
+let compute_ivs f cs =
   let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
-        begin match decomp_term body3 with
+	Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv ->
+        Goal.return
+          begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
               let n_lhs_rhs = ref []
               and v_lhs = ref (None : constr option)
@@ -245,8 +248,7 @@ let compute_ivs gl f cs =
            (* Then we test if the RHS is the RHS for variables *)
                    else begin match decompose_app bodyi with
                      | vmf, [_; _; a3; a4 ]
-                         when isRel a3 && isRel a4 &&
-			   pf_conv_x gl vmf
+                         when isRel a3 && isRel a4 && is_conv vmf
                            (Lazy.force coq_varmap_find)->
                              v_lhs := Some (compute_lhs
                                               (snd (List.hd args3))
@@ -389,7 +391,10 @@ module Constrhash = Hashtbl.Make
   [ivs : inversion_scheme]\\
   [lc: constr list]\\
   [gl: goal sigma]\\ *)
-let quote_terms ivs lc gl =
+let quote_terms ivs lc =
+  (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in
+     [Coqlib.check_required_library]. *)
+  Goal.return () >- fun () ->
   Coqlib.check_required_library ["Coq";"quote";"Quote"];
   let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
@@ -436,36 +441,41 @@ let quote_terms ivs lc gl =
     auxl ivs.normal_lhs_rhs
   in
   let lp = List.map aux lc in
-  (lp, (btree_of_array (Array.of_list (List.rev !varlist))
-          ivs.return_type ))
+  Goal.return begin
+    (lp, (btree_of_array (Array.of_list (List.rev !varlist))
+            ivs.return_type ))
+  end
 
 (*s actually we could "quote" a list of terms instead of a single
   term. Ring for example needs that, but Ring doesn't use Quote
   yet. *)
 
-let quote f lid gl =
-  let f = pf_global gl f in
-  let cl = List.map (pf_global gl) lid in
-  let ivs = compute_ivs gl f cl in
-  let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with
+let quote f lid =
+  Tacmach.New.pf_global f >>- fun f ->
+  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
+  compute_ivs f cl >>- fun ivs ->
+  Goal.concl >>- fun concl ->
+  quote_terms ivs [concl] >>- fun quoted_terms ->
+  let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
-
-let gen_quote cont c f lid gl =
-  let f = pf_global gl f in
-  let cl = List.map (pf_global gl) lid in
-  let ivs = compute_ivs gl f cl in
-  let (p, vm) = match quote_terms ivs [c] gl with
+    | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
+    | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+
+let gen_quote cont c f lid =
+  Tacmach.New.pf_global f >>- fun f ->
+  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
+  compute_ivs f cl >>- fun ivs ->
+  quote_terms ivs [c] >>- fun quoted_terms ->
+  let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> cont (mkApp (f, [| p |])) gl
-    | Some _ -> cont (mkApp (f, [| vm; p |])) gl
+    | None -> cont (mkApp (f, [| p |]))
+    | Some _ -> cont (mkApp (f, [| vm; p |]))
 
 (*i