From b9a546ce449484133ba8e021392a344c8df0609d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 12 Jun 2026 08:28:46 +0200 Subject: [PATCH] Fast path for Reductionops kernel-defined functions. We do not call normalization when the argument is already in head normal form. Note that for some reason the code still relies on the term being evar-expanded, so we do implement this carefully. This fast path seems to be quite important for VM normalization, as most constructors of inductive types already have a type in head normal form. On a micro-benchmark designed to measure VM reification of big first-order terms, this gives a 20% speedup. --- pretyping/vnorm.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 0bc42bea01eb..d40f6e182f98 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -28,7 +28,19 @@ module NamedDecl = Context.Named.Declaration (* Calcul de la forme normal d'un terme *) (*******************************************) -let e_whd_all = Reductionops.clos_whd_flags RedFlags.all +let e_whd_all env sigma t = match EConstr.kind sigma t with +| Sort _ | Meta _ | Ind _ | Construct _ | Prod _| Lambda _ | Fix _ +| CoFix _ | Int _ | Float _ | String _ | Array _ as kind -> + EConstr.of_kind kind (* ensure head evar normalization *) +| App (c, _) as kind -> + begin match EConstr.kind sigma c with + | Ind _ | Construct _ | Meta _ | Int _ | Float _ | String _ | Array _ -> EConstr.of_kind kind + | Sort _ | Rel _ | Var _ | Evar _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ + | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> + Reductionops.clos_whd_flags RedFlags.all env sigma t + end +| Rel _ | Evar _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> + Reductionops.clos_whd_flags RedFlags.all env sigma t let crazy_type = mkSet