From 46b04c840589054199f4b7dc3b4adc3d4c532230 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Fri, 11 Jul 2025 16:25:05 -0700 Subject: [PATCH] chore: lower Nat.zero in toMono (#9320) 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. --- src/Lean/Compiler/LCNF/ToMono.lean | 2 ++ tests/lean/doubleReset.lean.expected.out | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index a6105dadc5..fb0aa38940 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -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! diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out index f341b2caa4..42eefeb59c 100644 --- a/tests/lean/doubleReset.lean.expected.out +++ b/tests/lean/doubleReset.lean.expected.out @@ -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;