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

chore: move Nat.succ lowering from toIR to toMono (#9319)

Browse source 
It makes more sense to do it here, since `cases` on `Nat` is also
lowered in `toMono`.
This commit is contained in:
Cameron Zwarich 2025-07-11 15:49:41 -07:00 • committed by GitHub
parent e2e36087e1
commit efc101d3b4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/IR/ToIR.lean
View file

@ -152,12 +152,6 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
bindErased decl.fvarId
lowerCode k
| some (.joinPoint ..) | none => panic! "unexpected value"
| .const ``Nat.succ _ args =>
let irArgs ← args.mapM lowerArg
let var ← bindVar decl.fvarId
let tmpVar ← newVar
let k := (.vdecl var .object (.fap ``Nat.add #[irArgs[0]!, (.var tmpVar)]) (← lowerCode k))
return .vdecl tmpVar .object (.lit (.num 1)) k
| .const name _ args =>
let irArgs ← args.mapM lowerArg
if let some code ← tryIrDecl? name irArgs then

13
src/Lean/Compiler/LCNF/ToMono.lean
View file

@ -92,6 +92,9 @@ partial def LetValue.toMono (e : LetValue) (resultFVar : FVarId) : ToMonoM LetVa
return args[1]!.toLetValue
else if declName == ``Quot.mk || declName == ``Quot.lcInv then
return args[2]!.toLetValue
else if declName == ``Nat.succ then
-- This should have been handled in Code.toMono.
unreachable!
else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then
if let some info ← hasTrivialStructure? ctorInfo.induct then
args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono resultFVar
@ -316,7 +319,15 @@ partial def trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : ToMo
partial def Code.toMono (code : Code) : ToMonoM Code := do
match code with
| .let decl k => return code.updateLet! (← decl.toMono) (← k.toMono)
| .let decl k =>
match decl.value with
| .const ``Nat.succ _ args =>
let #[arg] := args | unreachable!
let oneDecl ← mkAuxLetDecl (.lit (.nat 1))
let decl ← decl.update decl.type (.const ``Nat.add [] #[arg, .fvar oneDecl.fvarId])
return .let oneDecl (.let decl (← k.toMono))
| _ =>
return code.updateLet! (← decl.toMono) (← k.toMono)
| .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
| .unreach type => return .unreach (← toMonoType type)
| .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono)