chore: beta reduce in specialization keys (#11353)

This PR applies beta reduction to specialization keys, allowing us to
reuse specializations in more situations.
This commit is contained in:
Henrik Böving 2025-11-25 13:14:36 +01:00 committed by GitHub
parent 29ac158fcf
commit b6e6094f85
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -238,7 +238,13 @@ def mkKey (params : Array Param) (decls : Array CodeDecl) (body : LetValue) : Co
let key := ToExpr.run do
ToExpr.withParams params do
ToExpr.mkLambdaM params (← ToExpr.abstractM body)
let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key
let pre e := do
-- beta reduce if possible
if e.isHeadBetaTarget then
return .visit e.headBeta
else
return .continue
let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key pre
return normLevelParams key
open Internalize in