From 1bf43863e65abfeb0ac90ebdf2da93f7a55ba169 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 25 Feb 2026 10:30:23 +0100 Subject: [PATCH] fix: better LCNF pretty printing (#12684) --- src/Lean/Compiler/LCNF/PrettyPrinter.lean | 10 ++++---- tests/lean/4089.lean.expected.out | 18 +++++++------- tests/lean/doubleReset.lean.expected.out | 6 ++--- tests/lean/run/borrowBug.lean | 4 +-- tests/lean/run/compiler_push_proj.lean | 30 +++++++++++------------ tests/lean/run/elim_dead_vars.lean | 2 +- tests/lean/run/simp_cases.lean | 2 +- 7 files changed, 36 insertions(+), 36 deletions(-) diff --git a/src/Lean/Compiler/LCNF/PrettyPrinter.lean b/src/Lean/Compiler/LCNF/PrettyPrinter.lean index b0786d34a4..f924e7ed97 100644 --- a/src/Lean/Compiler/LCNF/PrettyPrinter.lean +++ b/src/Lean/Compiler/LCNF/PrettyPrinter.lean @@ -83,10 +83,10 @@ def ppLetValue (e : LetValue pu) : M Format := do | .proj _ i fvarId _ => return f!"{← ppFVar fvarId} # {i}" | .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}" | .const declName us args _ => return f!"{← ppExpr (.const declName us)}{← ppArgs args}" - | .ctor i args _ => return f!"{i} {← ppArgs args}" + | .ctor i args _ => return f!"{i}{← ppArgs args}" | .fap declName args _ => return f!"{declName}{← ppArgs args}" | .pap declName args _ => return f!"pap {declName}{← ppArgs args}" - | .oproj i fvarId _ => return f!"proj[{i}] {← ppFVar fvarId}" + | .oproj i fvarId _ => return f!"oproj[{i}] {← ppFVar fvarId}" | .uproj i fvarId _ => return f!"uproj[{i}] {← ppFVar fvarId}" | .sproj i offset fvarId _ => return f!"sproj[{i}, {offset}] {← ppFVar fvarId}" | .reset n fvarId _ => return f!"reset[{n}] {← ppFVar fvarId}" @@ -144,11 +144,11 @@ mutual return "⊥" | .sset fvarId i offset y ty k _ => if pp.letVarTypes.get (← getOptions) then - return f!"sset {← ppFVar fvarId} [{i}, {offset}] : {← ppExpr ty} := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k) + return f!"sset {← ppFVar fvarId}[{i}, {offset}] : {← ppExpr ty} := {← ppFVar y};" ++ .line ++ (← ppCode k) else - return f!"sset {← ppFVar fvarId} [{i}, {offset}] := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k) + return f!"sset {← ppFVar fvarId}[{i}, {offset}] := {← ppFVar y};" ++ .line ++ (← ppCode k) | .uset fvarId i y k _ => - return f!"uset {← ppFVar fvarId} [{i}] := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k) + return f!"uset {← ppFVar fvarId}[{i}] := {← ppFVar y};" ++ .line ++ (← ppCode k) | .inc fvarId n _ _ k _ => if n != 1 then return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k) diff --git a/tests/lean/4089.lean.expected.out b/tests/lean/4089.lean.expected.out index 310059f891..b787259685 100644 --- a/tests/lean/4089.lean.expected.out +++ b/tests/lean/4089.lean.expected.out @@ -2,8 +2,8 @@ def f x.1 : obj := cases x.1 : obj | Prod.mk => - let fst.2 := proj[0] x.1; - let snd.3 := proj[1] x.1; + let fst.2 := oproj[0] x.1; + let snd.3 := oproj[1] x.1; let _x.4 := reset[2] x.1; let _x.5 := reuse _x.4 in ctor_0[Prod.mk] snd.3 fst.2; return _x.5 @@ -11,8 +11,8 @@ def Sigma.toProd._redArg x.1 : obj := cases x.1 : obj | Sigma.mk => - let fst.2 := proj[0] x.1; - let snd.3 := proj[1] x.1; + let fst.2 := oproj[0] x.1; + let snd.3 := oproj[1] x.1; let _x.4 := reset[2] x.1; let _x.5 := reuse _x.4 in ctor_0[Prod.mk] fst.2 snd.3; return _x.5 @@ -24,16 +24,16 @@ def foo x.1 : tobj := cases x.1 : tobj | List.nil => - let _x.2 := ctor_0[List.nil] ; + let _x.2 := ctor_0[List.nil]; return _x.2 | List.cons => - let head.3 := proj[0] x.1; + let head.3 := oproj[0] x.1; cases head.3 : tobj | Prod.mk => - let tail.4 := proj[1] x.1; + let tail.4 := oproj[1] x.1; let _x.5 := reset[2] x.1; - let fst.6 := proj[0] head.3; - let snd.7 := proj[1] head.3; + let fst.6 := oproj[0] head.3; + let snd.7 := oproj[1] head.3; let _x.8 := foo tail.4; let _x.9 := reuse _x.5 in ctor_1[List.cons] fst.6 _x.8; return _x.9 diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out index 957032f68b..85de6fd08d 100644 --- a/tests/lean/doubleReset.lean.expected.out +++ b/tests/lean/doubleReset.lean.expected.out @@ -8,12 +8,12 @@ let v := Array.uget ◾ bs i ◾; cases v : obj | Prod.mk => - let fst := proj[0] v; + let fst := oproj[0] v; let _x.2 := reset[2] v; cases fst : obj | Prod.mk => - let fst := proj[0] fst; - let snd := proj[1] fst; + let fst := oproj[0] fst; + let snd := oproj[1] fst; let _x.3 := reset[2] fst; let _x.4 := 0; let bs' := Array.uset ◾ bs i _x.4 ◾; diff --git a/tests/lean/run/borrowBug.lean b/tests/lean/run/borrowBug.lean index 6c5f7a53bd..ed5784c7b5 100644 --- a/tests/lean/run/borrowBug.lean +++ b/tests/lean/run/borrowBug.lean @@ -27,14 +27,14 @@ trace: [Compiler.explicitRc] size: 27 | Bool.false => dec y; let z := g x; - let fst := proj[0] z; + let fst := oproj[0] z; inc fst; dec z; goto _jp.1 fst | Bool.true => dec x; let z := g y; - let fst := proj[0] z; + let fst := oproj[0] z; inc fst; dec z; goto _jp.1 fst diff --git a/tests/lean/run/compiler_push_proj.lean b/tests/lean/run/compiler_push_proj.lean index 489bedaf7b..8f0397e359 100644 --- a/tests/lean/run/compiler_push_proj.lean +++ b/tests/lean/run/compiler_push_proj.lean @@ -9,7 +9,7 @@ trace: [Compiler.pushProj] size: 5 let _x.1 : tagged := 0; return _x.1 | Option.some => - let val.2 : tobj := proj[0] a; + let val.2 : tobj := oproj[0] a; return val.2 -/ #guard_msgs in @@ -32,10 +32,10 @@ trace: [Compiler.pushProj] size: 10 | Option.none => return a | Option.some => - let val.1 : tobj := proj[0] a; - let val.2 : tobj := proj[0] b; + let val.1 : tobj := oproj[0] a; + let val.2 : tobj := oproj[0] b; let _x.3 : tobj := Nat.add val.1 val.2; - let _x.4 : obj := ctor_1[Option.some] _x.3; + let _x.4 : obj := ctor_1[Option.some] _x.3; return _x.4 -/ #guard_msgs in @@ -58,16 +58,16 @@ trace: [Compiler.pushProj] size: 14 | Option.some => cases b : tobj | Option.none => - let val.1 : tobj := proj[0] a; + let val.1 : tobj := oproj[0] a; let _x.2 : tagged := 1; let _x.3 : tobj := Nat.add val.1 _x.2; - let _x.4 : obj := ctor_1[Option.some] _x.3; + let _x.4 : obj := ctor_1[Option.some] _x.3; return _x.4 | Option.some => - let val.5 : tobj := proj[0] a; - let val.6 : tobj := proj[0] b; + let val.5 : tobj := oproj[0] a; + let val.6 : tobj := oproj[0] b; let _x.7 : tobj := Nat.add val.5 val.6; - let _x.8 : obj := ctor_1[Option.some] _x.7; + let _x.8 : obj := ctor_1[Option.some] _x.7; return _x.8 -/ #guard_msgs in @@ -90,21 +90,21 @@ trace: [Compiler.pushProj] size: 18 | Option.some => cases b : tobj | Option.none => - let val.1 : tobj := proj[0] a; + let val.1 : tobj := oproj[0] a; let _x.2 : tagged := 1; let _x.3 : tobj := Nat.add val.1 _x.2; - let _x.4 : obj := ctor_1[Option.some] _x.3; + let _x.4 : obj := ctor_1[Option.some] _x.3; return _x.4 | Option.some => cases c : tobj | Bool.false => - let _x.5 : tagged := ctor_0[Option.none] ; + let _x.5 : tagged := ctor_0[Option.none]; return _x.5 | Bool.true => - let val.6 : tobj := proj[0] a; - let val.7 : tobj := proj[0] b; + let val.6 : tobj := oproj[0] a; + let val.7 : tobj := oproj[0] b; let _x.8 : tobj := Nat.add val.6 val.7; - let _x.9 : obj := ctor_1[Option.some] _x.8; + let _x.9 : obj := ctor_1[Option.some] _x.8; return _x.9 -/ #guard_msgs in diff --git a/tests/lean/run/elim_dead_vars.lean b/tests/lean/run/elim_dead_vars.lean index 674481854d..6ef61148e1 100644 --- a/tests/lean/run/elim_dead_vars.lean +++ b/tests/lean/run/elim_dead_vars.lean @@ -21,7 +21,7 @@ trace: [Compiler.saveMono] size: 5 let _x.1 := 1; return _x.1 | Option.some => - let val.2 := proj[0] x; + let val.2 := oproj[0] x; let _x.3 := 0; return _x.3 [Compiler.elimDeadVars] size: 5 diff --git a/tests/lean/run/simp_cases.lean b/tests/lean/run/simp_cases.lean index 1db7ab4b60..8f5b2f8d16 100644 --- a/tests/lean/run/simp_cases.lean +++ b/tests/lean/run/simp_cases.lean @@ -24,7 +24,7 @@ trace: [Compiler.saveMono] size: 7 return _x.6 [Compiler.simpCase] size: 2 def test f : tobj := - let n.1 := proj[0] f; + let n.1 := oproj[0] f; let _x.2 := aux n.1; return _x.2 -/