Merge PR#549: Fast path in weak head reduction of applied atoms.

1 files changed, 24 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d7f77eda..cd975ee9a 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)
 
 (********************************************************************)