Fast path in weak head reduction of applied atoms.

Instead of calling the whole reduction machirery, we check before reducing that
a term is an applied atom, i.e. inductive, constructor, evar or meta. In that
case, the abstract machine acts as the identity but needs to destruct and
reconstruct the whole term, which can be very costly.

This fixes part of bug #5421: vm_compute is very slow at doing nothing, where
recomputation of the type of a big inductive was incredibly expensive.

1 files changed, 24 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d7f77edae..cd975ee9a9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -107,7 +107,15 @@ let pure_stack lfts stk =
 (****************************************************************************)
 
 let whd_betaiota env t =
-  whd_val (create_clos_infos betaiota env) (inject t)
+  match kind_of_term t with
+    | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+       Prod _|Lambda _|Fix _|CoFix _) -> t
+    | App (c, _) ->
+      begin match kind_of_term c with
+      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
+      | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+      end
+    | _ -> whd_val (create_clos_infos betaiota env) (inject t)
 
 let nf_betaiota env t =
   norm_val (create_clos_infos betaiota env) (inject t)
@@ -116,18 +124,33 @@ let whd_betaiotazeta env x =
   match kind_of_term x with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
+    | App (c, _) ->
+      begin match kind_of_term c with
+      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
+      | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+      end
     | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
 
 let whd_all env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
+    | App (c, _) ->
+      begin match kind_of_term c with
+      | Ind _ | Construct _ | Evar _ | Meta _ -> t
+      | _ -> whd_val (create_clos_infos all env) (inject t)
+      end
     | _ -> whd_val (create_clos_infos all env) (inject t)
 
 let whd_allnolet env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
+    | App (c, _) ->
+      begin match kind_of_term c with
+      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
+      | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+      end
     | _ -> whd_val (create_clos_infos allnolet env) (inject t)
 
 (********************************************************************)