Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.

The interpretation of arguments of tactic notations were normalizing the goal
beforehand, which incurred an important time penalty. We now do this argumentwise
which allows to save time in frequent cases, notably tactic arguments.

1 files changed, 46 insertions, 10 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 54adbd937f..5ecc46d670 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1219,34 +1219,53 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg)
         end
       | _ as tag -> (** Special treatment. TODO: use generic handler  *)
-        Ftactic.nf_enter begin fun gl ->
-          let sigma = Proofview.Goal.sigma gl in
-          let env = Proofview.Goal.env gl in
           match tag with
           | IntOrVarArgType ->
+            Ftactic.enter begin fun _ ->
               Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))
+            end
           | IdentArgType ->
+            Ftactic.enter begin fun gl ->
+              let sigma = Proofview.Goal.sigma gl in
+              let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
               Ftactic.return (value_of_ident (interp_ident ist env sigma
                                                (out_gen (glbwit wit_ident) x)))
+            end
           | VarArgType ->
+            Ftactic.enter begin fun gl ->
+              let sigma = Proofview.Goal.sigma gl in
+              let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
               Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x))
-          | GenArgType -> f (out_gen (glbwit wit_genarg) x)
+            end
+          | GenArgType ->
+            Ftactic.enter begin fun _ ->
+              f (out_gen (glbwit wit_genarg) x)
+            end
           | ConstrArgType ->
+            Ftactic.nf_enter begin fun gl ->
               let (sigma,v) =
                 Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl
               in
               Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
+            end
           | OpenConstrArgType ->
+            Ftactic.nf_enter begin fun gl ->
               let (sigma,v) =
                 Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in
               Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
+            end
           | ConstrMayEvalArgType ->
+            Ftactic.nf_enter begin fun gl ->
+              let sigma = Proofview.Goal.sigma gl in
+              let env = Proofview.Goal.env gl in
               let (sigma,c_interp) =
                 interp_constr_may_eval ist env sigma
                   (out_gen (glbwit wit_constr_may_eval) x)
               in
               Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
+            end
           | ListArgType ConstrArgType ->
+            Ftactic.nf_enter begin fun gl ->
               let wit = glbwit (wit_list wit_constr) in
               let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
                 Evd.MonadR.List.map_right
@@ -1255,22 +1274,34 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                   (project gl)
               end gl in
               Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp))
+            end
           | ListArgType VarArgType ->
+            Ftactic.enter begin fun gl ->
+              let sigma = Proofview.Goal.sigma gl in
+              let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
               let wit = glbwit (wit_list wit_var) in
               Ftactic.return (
                 let ans = List.map (mk_hyp_value ist env sigma) (out_gen wit x) in
                 in_gen (topwit (wit_list wit_genarg)) ans
               )
+            end
           | ListArgType IntOrVarArgType ->
+            Ftactic.enter begin fun _ ->
               let wit = glbwit (wit_list wit_int_or_var) in
               let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
+            end
           | ListArgType IdentArgType ->
+            Ftactic.enter begin fun gl ->
+              let sigma = Proofview.Goal.sigma gl in
+              let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
               let wit = glbwit (wit_list wit_ident) in
               let mk_ident x = value_of_ident (interp_ident ist env sigma x) in
               let ans = List.map mk_ident (out_gen wit x) in
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
+            end
           | ListArgType t  ->
+            Ftactic.enter begin fun gl ->
               let open Ftactic in
               let list_unpacker wit l =
                 let map x =
@@ -1281,17 +1312,22 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                 Ftactic.return (in_gen (topwit (wit_list wit)) l)
               in
               list_unpack { list_unpacker } x
+            end
           | ExtraArgType _ ->
               (** Special treatment of tactics *)
-              if has_type x (glbwit wit_tactic) then
+            if has_type x (glbwit wit_tactic) then
+              Ftactic.enter begin fun _ ->
                 let tac = out_gen (glbwit wit_tactic) x in
                 val_interp ist tac
-              else
-                let goal = Proofview.Goal.goal gl in
-                let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
-                Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v)
+              end
+            else
+              Ftactic.nf_enter begin fun gl ->
+                let sigma = Proofview.Goal.sigma gl in
+                  let goal = Proofview.Goal.goal gl in
+                  let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
+                  Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v)
+              end
           | _ -> assert false
-        end
       in
       let (>>=) = Ftactic.bind in
       let interp_vars =