max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: make implemented_by of casesOn work correctly with hash consing (#8010)

Browse source 
This PR fixes caseOn expressions with an implemented_by to work
correctly with hash consing, even when the elaborator produces terms
that reconstruct the discriminant rather than just reusing a variable.
This commit is contained in:
Cameron Zwarich 2025-04-17 16:32:59 -07:00 • committed by GitHub
parent 7b292090ce
commit d981fa0faf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 33 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Lean/Compiler/LCNF/ToLCNF.lean
View file

@ -8,6 +8,7 @@ import Lean.ProjFns
import Lean.Meta.CtorRecognizer
import Lean.Compiler.BorrowedAnnotation
import Lean.Compiler.CSimpAttr
import Lean.Compiler.ImplementedByAttr
import Lean.Compiler.LCNF.Types
import Lean.Compiler.LCNF.Bind
import Lean.Compiler.LCNF.InferType
@ -567,6 +568,33 @@ where
let result := .fvar auxDecl.fvarId
mkOverApplication result args casesInfo.arity
visitCasesImplementedBy (casesInfo : CasesInfo) (f : Expr) (args : Array Expr) : M Arg := do
let mut args := args
let discr := args[casesInfo.discrPos]!
if discr matches .fvar _ then
let typeName := casesInfo.declName.getPrefix
let .inductInfo indVal ← getConstInfo typeName | unreachable!
args ← args.mapIdxM fun i arg => do
unless casesInfo.altsRange.start <= i && i < casesInfo.altsRange.stop do return arg
let altIdx := i - casesInfo.altsRange.start
let numParams := casesInfo.altNumParams[altIdx]!
let ctorName := indVal.ctors[altIdx]!
-- We simplify `casesOn` arguments that simply reconstruct the discriminant and replace
-- them with the actual discriminant. This is required for hash consing to work correctly,
-- and should eventually be fixed by changing the elaborated term to use the original
-- variable.
Meta.MetaM.run' <| Meta.lambdaBoundedTelescope arg numParams fun paramExprs body => do
let fn := body.getAppFn
let args := body.getAppArgs
let args := args.map fun arg =>
if arg.getAppFn.constName? == some ctorName && arg.getAppArgs == paramExprs then
discr
else
arg
Meta.mkLambdaFVars paramExprs (mkAppN fn args)
visitAppDefaultConst f args
visitCtor (arity : Nat) (e : Expr) : M Arg :=
etaIfUnderApplied e arity do
visitAppDefaultConst e.getAppFn e.getAppArgs
@ -671,7 +699,7 @@ where
visitApp (e : Expr) : M Arg := do
if let some (args, n, t, v, b) := e.letFunAppArgs? then
visitCore <| mkAppN (.letE n t v b (nonDep := true)) args
else if let .const declName _ := CSimp.replaceConstants (← getEnv) e.getAppFn then
else if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then
if declName == ``Quot.lift then
visitQuotLift e
else if declName == ``Quot.mk then
@ -687,7 +715,10 @@ where
else if declName == ``False.rec || declName == ``Empty.rec || declName == ``False.casesOn || declName == ``Empty.casesOn then
visitFalseRec e
else if let some casesInfo ← getCasesInfo? declName then
visitCases casesInfo e
if (getImplementedBy? (← getEnv) declName).isSome then
e.withApp (visitCasesImplementedBy casesInfo)
else
visitCases casesInfo e
else if let some arity ← getCtorArity? declName then
visitCtor arity e
else if isNoConfusion (← getEnv) declName then