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

chore: lower Nat.zero in toMono (#9320)

Browse source 
This currently relies on the encoding pun of Nat.zero as the first
tagged constructor of Nat. Since Nat.succ is lowered to addition, it
makes sense to also lower Nat.zero to a zero literal. This might also
expose more optimization opportunities in the future.
This commit is contained in:
Cameron Zwarich 2025-07-11 16:25:05 -07:00 • committed by GitHub
parent efc101d3b4
commit 46b04c8405
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -92,6 +92,8 @@ 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.zero then
return .lit (.nat 0)
else if declName == ``Nat.succ then
-- This should have been handled in Code.toMono.
unreachable!

2
tests/lean/doubleReset.lean.expected.out
View file

@ -15,7 +15,7 @@
let x_8 : obj := proj[0] x_7;
let x_9 : obj := proj[1] x_7;
let x_18 : obj := reset[2] x_7;
let x_10 : obj := ctor_0[Nat.zero];
let x_10 : obj := 0;
let x_11 : obj := Array.uset ◾ x_4 x_3 x_10 ◾;
let x_12 : obj := reuse x_18 in ctor_0[Prod.mk] x_8 x_9;
let x_13 : obj := reuse x_19 in ctor_0[Prod.mk] x_12 x_1;