feat: add Meta.Context.canUnfold?

src/Lean/Meta/Basic.lean

@@ -184,6 +184,10 @@ structure Context where
     Remark: in the current implementation, `synthPending` fails if `synthPendingDepth > 0`.
     We will add a configuration option if necessary. -/
   synthPendingDepth : Nat                  := 0
+  /--
+    A predicate to control whether a constant can be unfolded or not at `whnf`.
+    Note that we do not cache results at `whnf` when `canUnfold?` is not `none`. -/
+  canUnfold?        : Option (Config → ConstantInfo → CoreM Bool) := none
 
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 

src/Lean/Meta/GetConst.lean

@@ -7,23 +7,29 @@ import Lean.Meta.GlobalInstances
 
 namespace Lean.Meta
 
-private def getDefInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
+private def canUnfoldDefault (info : ConstantInfo) : MetaM Bool := do
   match (← read).config.transparency with
-  | TransparencyMode.all => return some info
-  | TransparencyMode.default => return some info
+  | TransparencyMode.all => return true
+  | TransparencyMode.default => return true
   | m =>
     if (← isReducible info.name) then
-      return some info
+      return true
     else if m == TransparencyMode.instances && isGlobalInstance (← getEnv) info.name then
-      return some info
+      return true
     else
-      return none
+      return false
+
+def canUnfold (info : ConstantInfo) : MetaM Bool := do
+  if let some f := (← read).canUnfold? then
+    f (← read).config info
+  else
+    canUnfoldDefault info
 
 def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   let env ← getEnv
   match env.find? constName with
   | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
-  | some (info@(ConstantInfo.defnInfo _)) => getDefInfo info
+  | some (info@(ConstantInfo.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some info                             => pure (some info)
   | none                                  => throwUnknownConstant constName
 
@@ -31,7 +37,7 @@ def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
   let env ← getEnv
   match env.find? constName with
   | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
-  | some (info@(ConstantInfo.defnInfo _)) => getDefInfo info
+  | some (info@(ConstantInfo.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some info                             => pure (some info)
   | none                                  => pure none
 

src/Lean/Meta/WHNF.lean

@@ -646,7 +646,7 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
 @[inline] private def useWHNFCache (e : Expr) : MetaM Bool := do
   -- We cache only closed terms without expr metavars.
   -- Potential refinement: cache if `e` is not stuck at a metavariable
-  if e.hasFVar || e.hasExprMVar then
+  if e.hasFVar || e.hasExprMVar || (← read).canUnfold?.isSome then
     return false
   else
     match (← getConfig).transparency with