From aa704399c4d4b8a74f4d6f42e65808c1ceab3b7e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Apr 2017 19:24:00 +0200
Subject: 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.
---
 kernel/reduction.ml | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

(limited to 'kernel')

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)
 
 (********************************************************************)
-- 
cgit v1.2.3