From ec59bbe15c830cbac0032d49a218cae55fe8a74a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 16 Oct 2022 16:06:08 -0700
Subject: [PATCH] chore: ensure LCNF pretty printer result supports
 `Format.group`

---
 src/Lean/Compiler/LCNF/PrettyPrinter.lean     |  8 +--
 .../CompilerProvokeFloatLet.lean.expected.out | 48 +++++++-------
 tests/lean/baseIO.lean.expected.out           | 16 ++---
 tests/lean/jpCasesDiscrM.lean.expected.out    | 46 +++++++-------
 tests/lean/jpCasesNary.lean.expected.out      | 62 +++++++++----------
 tests/lean/jpClosureIssue.lean.expected.out   | 12 ++--
 tests/lean/lambdaLiftCache.lean.expected.out  | 16 ++---
 tests/lean/reduceArity.lean.expected.out      | 23 ++++---
 tests/lean/seqToCodeIssue.lean.expected.out   | 12 ++--
 tests/lean/unhygienicCode.lean.expected.out   | 38 ++++++------
 10 files changed, 142 insertions(+), 139 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/PrettyPrinter.lean b/src/Lean/Compiler/LCNF/PrettyPrinter.lean
index 0ed5fd110a..48900164ce 100644
--- a/src/Lean/Compiler/LCNF/PrettyPrinter.lean
+++ b/src/Lean/Compiler/LCNF/PrettyPrinter.lean
@@ -93,11 +93,11 @@ mutual
 
   partial def ppCode (c : Code) : M Format := do
     match c with
-    | .let decl k => return (← ppLetDecl decl) ++ .line ++ (← ppCode k)
-    | .fun decl k => return f!"fun " ++ (← ppFunDecl decl) ++ .line ++ (← ppCode k)
-    | .jp decl k => return f!"jp " ++ (← ppFunDecl decl) ++ .line ++ (← ppCode k)
+    | .let decl k => return (← ppLetDecl decl) ++ ";" ++ .line ++ (← ppCode k)
+    | .fun decl k => return f!"fun " ++ (← ppFunDecl decl) ++ ";" ++ .line ++ (← ppCode k)
+    | .jp decl k => return f!"jp " ++ (← ppFunDecl decl) ++ ";" ++ .line ++ (← ppCode k)
     | .cases c => return f!"cases {← ppFVar c.discr} : {← ppExpr c.resultType}{← prefixJoin .line c.alts ppAlt}"
-    | .return fvarId => ppFVar fvarId
+    | .return fvarId => return f!"return {← ppFVar fvarId}"
     | .jmp fvarId args => return f!"goto {← ppFVar fvarId} {← ppArgs args}"
     | .unreach .. => return "⊥"
 end
diff --git a/tests/lean/CompilerProvokeFloatLet.lean.expected.out b/tests/lean/CompilerProvokeFloatLet.lean.expected.out
index 5895e0e43d..9ce82cfd6f 100644
--- a/tests/lean/CompilerProvokeFloatLet.lean.expected.out
+++ b/tests/lean/CompilerProvokeFloatLet.lean.expected.out
@@ -4,57 +4,57 @@
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 1
 [Compiler.floatLetIn] size: 11
     def provokeFloatLet x y cond : Nat :=
-      let dual := Nat.mul x y
+      let dual := Nat.mul x y;
       cases cond : Nat
       | Bool.false =>
-        let b := Nat.add x y
-        let _x.1 := Nat.add b dual
-        _x.1
+        let b := Nat.add x y;
+        let _x.1 := Nat.add b dual;
+        return _x.1
       | Bool.true =>
         cases dual : Nat
         | Nat.zero =>
-          let a := Nat.pow x y
-          a
+          let a := Nat.pow x y;
+          return a
         | Nat.succ n.2 =>
-          let c := Nat.sub x y
-          c
+          let c := Nat.sub x y;
+          return c
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 0
 [Compiler.floatLetIn] size: 11
     def provokeFloatLet x y cond : Nat :=
-      let dual := Nat.mul x y
+      let dual := Nat.mul x y;
       cases cond : Nat
       | Bool.false =>
-        let b := Nat.add x y
-        let _x.1 := Nat.add b dual
-        _x.1
+        let b := Nat.add x y;
+        let _x.1 := Nat.add b dual;
+        return _x.1
       | Bool.true =>
         cases dual : Nat
         | Nat.zero =>
-          let a := Nat.pow x y
-          a
+          let a := Nat.pow x y;
+          return a
         | Nat.succ n.2 =>
-          let c := Nat.sub x y
-          c
+          let c := Nat.sub x y;
+          return c
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 0
 [Compiler.floatLetIn] size: 11
     def provokeFloatLet x y cond : Nat :=
-      let dual := Nat.mul x y
+      let dual := Nat.mul x y;
       cases cond : Nat
       | Bool.false =>
-        let b := Nat.add x y
-        let _x.1 := Nat.add b dual
-        _x.1
+        let b := Nat.add x y;
+        let _x.1 := Nat.add b dual;
+        return _x.1
       | Bool.true =>
         cases dual : Nat
         | Nat.zero =>
-          let a := Nat.pow x y
-          a
+          let a := Nat.pow x y;
+          return a
         | Nat.succ n.2 =>
-          let c := Nat.sub x y
-          c
+          let c := Nat.sub x y;
+          return c
diff --git a/tests/lean/baseIO.lean.expected.out b/tests/lean/baseIO.lean.expected.out
index 43d601513c..8ea8c000b0 100644
--- a/tests/lean/baseIO.lean.expected.out
+++ b/tests/lean/baseIO.lean.expected.out
@@ -1,17 +1,17 @@
 [Compiler.saveBase] size: 13
     def test a.1 : EStateM.Result Empty PUnit UInt32 :=
-      let _x.2 := 42
-      let _x.3 := UInt32.ofNat _x.2
-      let _x.4 := @ST.Prim.mkRef _ _ _x.3 a.1
+      let _x.2 := 42;
+      let _x.3 := UInt32.ofNat _x.2;
+      let _x.4 := @ST.Prim.mkRef _ _ _x.3 a.1;
       cases _x.4 : EStateM.Result Empty PUnit UInt32
       | EStateM.Result.ok a.5 a.6 =>
-        let _x.7 := 10
-        let _x.8 := UInt32.ofNat _x.7
-        let _x.9 := @ST.Prim.Ref.set _ _ a.5 _x.8 a.6
+        let _x.7 := 10;
+        let _x.8 := UInt32.ofNat _x.7;
+        let _x.9 := @ST.Prim.Ref.set _ _ a.5 _x.8 a.6;
         cases _x.9 : EStateM.Result Empty PUnit UInt32
         | EStateM.Result.ok a.10 a.11 =>
-          let _x.12 := @ST.Prim.Ref.get _ _ a.5 a.11
-          _x.12
+          let _x.12 := @ST.Prim.Ref.get _ _ a.5 a.11;
+          return _x.12
         | EStateM.Result.error a.13 a.14 =>
           ⊥
       | EStateM.Result.error a.15 a.16 =>
diff --git a/tests/lean/jpCasesDiscrM.lean.expected.out b/tests/lean/jpCasesDiscrM.lean.expected.out
index 2b523c7921..42a8b20eff 100644
--- a/tests/lean/jpCasesDiscrM.lean.expected.out
+++ b/tests/lean/jpCasesDiscrM.lean.expected.out
@@ -2,45 +2,45 @@
     def f1 c a b : Nat :=
       cases c : Nat
       | Bool.false =>
-        let _x.1 := Nat.add a b
-        _x.1
+        let _x.1 := Nat.add a b;
+        return _x.1
       | Bool.true =>
-        let _x.2 := Nat.add a b
-        let _x.3 := Nat.mul b a
-        let _x.4 := Nat.add _x.2 _x.3
-        _x.4
+        let _x.2 := Nat.add a b;
+        let _x.3 := Nat.mul b a;
+        let _x.4 := Nat.add _x.2 _x.3;
+        return _x.4
 [Compiler.saveBase] size: 7
     def f2 c a b : Nat :=
       cases c : Nat
       | Bool.false =>
-        let _x.1 := Nat.add a b
-        _x.1
+        let _x.1 := Nat.add a b;
+        return _x.1
       | Bool.true =>
-        let _x.2 := Nat.add a b
-        let _x.3 := Nat.mul b a
-        let _x.4 := Nat.add _x.2 _x.3
-        _x.4
+        let _x.2 := Nat.add a b;
+        let _x.3 := Nat.mul b a;
+        let _x.4 := Nat.add _x.2 _x.3;
+        return _x.4
 [Compiler.saveBase] size: 22
     def f3 c c' a b : Nat :=
       jp _jp.1 y z : Nat :=
-        let _x.2 := Nat.add y z
-        let _x.3 := Nat.mul z y
-        let _x.4 := Nat.add _x.2 _x.3
-        _x.4
+        let _x.2 := Nat.add y z;
+        let _x.3 := Nat.mul z y;
+        let _x.4 := Nat.add _x.2 _x.3;
+        return _x.4;
       jp _jp.5 y z : Nat :=
-        let _x.6 := Nat.add z y
-        let _x.7 := Nat.add _x.6 y
-        _x.7
+        let _x.6 := Nat.add z y;
+        let _x.7 := Nat.add _x.6 y;
+        return _x.7;
       jp _jp.8 y z d : Nat :=
         cases d : Nat
         | C.c1 =>
           goto _jp.1 y z
         | C.c3 =>
-          let _x.9 := Nat.mul y y
-          let _x.10 := Nat.add _x.9 a
-          _x.10
+          let _x.9 := Nat.mul y y;
+          let _x.10 := Nat.add _x.9 a;
+          return _x.10
         | _ =>
-          goto _jp.5 y z
+          goto _jp.5 y z;
       cases c : Nat
       | C.c1 =>
         goto _jp.1 a b
diff --git a/tests/lean/jpCasesNary.lean.expected.out b/tests/lean/jpCasesNary.lean.expected.out
index b349eca0a4..aa17a6115f 100644
--- a/tests/lean/jpCasesNary.lean.expected.out
+++ b/tests/lean/jpCasesNary.lean.expected.out
@@ -2,41 +2,41 @@
     def f1 c a b : Nat :=
       cases c : Nat
       | Bool.false =>
-        let _x.1 := Nat.add b a
-        let _x.2 := Nat.mul a b
-        let _x.3 := Nat.add _x.1 _x.2
-        _x.3
+        let _x.1 := Nat.add b a;
+        let _x.2 := Nat.mul a b;
+        let _x.3 := Nat.add _x.1 _x.2;
+        return _x.3
       | Bool.true =>
-        let _x.4 := Nat.add b a
-        _x.4
+        let _x.4 := Nat.add b a;
+        return _x.4
 [Compiler.saveBase] size: 7
     def f2 c a b : Nat :=
       cases c : Nat
       | Bool.false =>
-        let _x.1 := Nat.add b a
-        let _x.2 := Nat.mul a b
-        let _x.3 := Nat.add _x.1 _x.2
-        _x.3
+        let _x.1 := Nat.add b a;
+        let _x.2 := Nat.mul a b;
+        let _x.3 := Nat.add _x.1 _x.2;
+        return _x.3
       | Bool.true =>
-        let _x.4 := Nat.add b a
-        _x.4
+        let _x.4 := Nat.add b a;
+        return _x.4
 [Compiler.saveBase] size: 19
     def f3 c c' a b : Nat :=
       jp _jp.1 y z : Nat :=
-        let _x.2 := Nat.add y z
-        let _x.3 := Nat.mul z y
-        let _x.4 := Nat.add _x.2 _x.3
-        _x.4
+        let _x.2 := Nat.add y z;
+        let _x.3 := Nat.mul z y;
+        let _x.4 := Nat.add _x.2 _x.3;
+        return _x.4;
       jp _jp.5 y z : Nat :=
-        let _x.6 := Nat.add z y
-        let _x.7 := Nat.add _x.6 y
-        _x.7
+        let _x.6 := Nat.add z y;
+        let _x.7 := Nat.add _x.6 y;
+        return _x.7;
       jp _jp.8 y d z : Nat :=
         cases d : Nat
         | C.c1 =>
           goto _jp.1 y z
         | _ =>
-          goto _jp.5 y z
+          goto _jp.5 y z;
       cases c : Nat
       | C.c1 =>
         goto _jp.5 a b
@@ -49,24 +49,24 @@
 [Compiler.saveBase] size: 22
     def f4 c c' a b : Nat :=
       jp _jp.1 y z : Nat :=
-        let _x.2 := Nat.add y z
-        let _x.3 := Nat.mul z y
-        let _x.4 := Nat.add _x.2 _x.3
-        _x.4
+        let _x.2 := Nat.add y z;
+        let _x.3 := Nat.mul z y;
+        let _x.4 := Nat.add _x.2 _x.3;
+        return _x.4;
       jp _jp.5 y z : Nat :=
-        let _x.6 := Nat.add z y
-        let _x.7 := Nat.add _x.6 y
-        _x.7
+        let _x.6 := Nat.add z y;
+        let _x.7 := Nat.add _x.6 y;
+        return _x.7;
       jp _jp.8 y z d : Nat :=
         cases d : Nat
         | C.c1 =>
           goto _jp.1 y z
         | C.c3 =>
-          let _x.9 := Nat.mul y y
-          let _x.10 := Nat.add _x.9 a
-          _x.10
+          let _x.9 := Nat.mul y y;
+          let _x.10 := Nat.add _x.9 a;
+          return _x.10
         | _ =>
-          goto _jp.5 y z
+          goto _jp.5 y z;
       cases c : Nat
       | C.c1 =>
         goto _jp.5 a b
diff --git a/tests/lean/jpClosureIssue.lean.expected.out b/tests/lean/jpClosureIssue.lean.expected.out
index 89ae7b990c..b1fdf9c22d 100644
--- a/tests/lean/jpClosureIssue.lean.expected.out
+++ b/tests/lean/jpClosureIssue.lean.expected.out
@@ -2,10 +2,10 @@
     def foo b a.1 : EStateM.Result IO.Error PUnit PUnit :=
       cases b : EStateM.Result IO.Error PUnit PUnit
       | Bool.false =>
-        let _x.2 := 1
-        let _x.3 := print _x.2 a.1
-        _x.3
+        let _x.2 := 1;
+        let _x.3 := print _x.2 a.1;
+        return _x.3
       | Bool.true =>
-        let _x.4 := 0
-        let _x.5 := print _x.4 a.1
-        _x.5
+        let _x.4 := 0;
+        let _x.5 := print _x.4 a.1;
+        return _x.5
diff --git a/tests/lean/lambdaLiftCache.lean.expected.out b/tests/lean/lambdaLiftCache.lean.expected.out
index d7948e8ac7..abbab55b88 100644
--- a/tests/lean/lambdaLiftCache.lean.expected.out
+++ b/tests/lean/lambdaLiftCache.lean.expected.out
@@ -1,14 +1,14 @@
 [Compiler.saveMono] size: 1
     def foo._lam_0 x a.1 : Nat :=
-      let _x.2 := Nat.add a.1 x
-      _x.2
+      let _x.2 := Nat.add a.1 x;
+      return _x.2
 [Compiler.saveMono] size: 2
     def foo x xs : List Nat :=
-      let _f.1 := foo._lam_0 x
-      let _x.2 := List.map._at_.map.spec_0 _f.1 xs
-      _x.2
+      let _f.1 := foo._lam_0 x;
+      let _x.2 := List.map._at_.map.spec_0 _f.1 xs;
+      return _x.2
 [Compiler.saveMono] size: 2
     def boo x xs : List Nat :=
-      let _f.1 := foo._lam_0 x
-      let _x.2 := List.map._at_.map.spec_0 _f.1 xs
-      _x.2
+      let _f.1 := foo._lam_0 x;
+      let _x.2 := List.map._at_.map.spec_0 _f.1 xs;
+      return _x.2
diff --git a/tests/lean/reduceArity.lean.expected.out b/tests/lean/reduceArity.lean.expected.out
index 526c156999..7fce8d6bb8 100644
--- a/tests/lean/reduceArity.lean.expected.out
+++ b/tests/lean/reduceArity.lean.expected.out
@@ -2,16 +2,19 @@
     def g._redArg (n : Nat) (a : ◾) (f : ◾ → ◾) : ◾ :=
       cases n : ◾
       | Nat.zero =>
-        a
+        return a
       | Nat.succ (n.1 : Nat) =>
-        let _x.2 := g._redArg n.1 a f
-        let _x.3 := f _x.2
-        _x.3
-[Compiler.result] size: 1 def g (α : ◾) (n : Nat) (a : ◾) (b : ◾) (f : ◾ → ◾) : ◾ := let _x.1 := g._redArg n a f _x.1
+        let _x.2 := g._redArg n.1 a f;
+        let _x.3 := f _x.2;
+        return _x.3
+[Compiler.result] size: 1
+    def g (α : ◾) (n : Nat) (a : ◾) (b : ◾) (f : ◾ → ◾) : ◾ :=
+      let _x.1 := g._redArg n a f;
+      return _x.1
 [Compiler.result] size: 4
     def h (n : Nat) (a : Nat) : Nat :=
-      let _x.1 := double
-      let _x.2 := g._redArg n a _x.1
-      let _x.3 := g._redArg a n _x.1
-      let _x.4 := Nat.add _x.2 _x.3
-      _x.4
+      let _x.1 := double;
+      let _x.2 := g._redArg n a _x.1;
+      let _x.3 := g._redArg a n _x.1;
+      let _x.4 := Nat.add _x.2 _x.3;
+      return _x.4
diff --git a/tests/lean/seqToCodeIssue.lean.expected.out b/tests/lean/seqToCodeIssue.lean.expected.out
index 504c4dfa63..12c139450f 100644
--- a/tests/lean/seqToCodeIssue.lean.expected.out
+++ b/tests/lean/seqToCodeIssue.lean.expected.out
@@ -1,17 +1,17 @@
 [Compiler.saveMono] size: 12
     def f b a.1 : EStateM.Result IO.Error PUnit PUnit :=
       jp _jp.2 a _y.3 : EStateM.Result IO.Error PUnit PUnit :=
-        let _x.4 := print a _y.3
+        let _x.4 := print a _y.3;
         cases _x.4 : EStateM.Result IO.Error PUnit PUnit
         | EStateM.Result.ok a.5 a.6 =>
-          let _x.7 := print a a.6
-          _x.7
+          let _x.7 := print a a.6;
+          return _x.7
         | EStateM.Result.error a.8 a.9 =>
-          _x.4
+          return _x.4;
       cases b : EStateM.Result IO.Error PUnit PUnit
       | Bool.false =>
-        let a.10 := 1
+        let a.10 := 1;
         goto _jp.2 a.10 a.1
       | Bool.true =>
-        let a.11 := 0
+        let a.11 := 0;
         goto _jp.2 a.11 a.1
diff --git a/tests/lean/unhygienicCode.lean.expected.out b/tests/lean/unhygienicCode.lean.expected.out
index 25eb1f54d5..55e2d190f6 100644
--- a/tests/lean/unhygienicCode.lean.expected.out
+++ b/tests/lean/unhygienicCode.lean.expected.out
@@ -65,22 +65,22 @@ def foo (x_1 : obj) : obj :=
   let x_9 : obj := Lean.Syntax.node3 x_5 x_6 x_7 x_8 x_4;
   ret x_9[Compiler.result] size: 18
     def foo n : Syntax :=
-      let fst.1 := Syntax.missing
-      let fst.2 := 1
-      let _x.3 := false
-      let fst.4 := SourceInfo.fromRef fst.1 _x.3
-      let _x.5 := "UnhygienicMain"
-      let fst.6 := Name.mkStr1 _x.5
-      let _x.7 := "term_+_"
-      let _x.8 := Name.mkStr1 _x.7
-      let _x.9 := "a"
-      let _x.10 := String.toSubstring' _x.9
-      let _x.11 := Name.mkStr1 _x.9
-      let _x.12 := addMacroScope fst.6 _x.11 fst.2
-      let _x.13 := [] _
-      let _x.14 := Syntax.ident fst.4 _x.10 _x.12 _x.13
-      let _x.15 := "+"
-      let _x.16 := Syntax.atom fst.4 _x.15
-      let _x.17 := Lean.instQuoteNatNumLitKind._elam_0 n
-      let _x.18 := Syntax.node3 fst.4 _x.8 _x.14 _x.16 _x.17
-      _x.18
+      let fst.1 := Syntax.missing;
+      let fst.2 := 1;
+      let _x.3 := false;
+      let fst.4 := SourceInfo.fromRef fst.1 _x.3;
+      let _x.5 := "UnhygienicMain";
+      let fst.6 := Name.mkStr1 _x.5;
+      let _x.7 := "term_+_";
+      let _x.8 := Name.mkStr1 _x.7;
+      let _x.9 := "a";
+      let _x.10 := String.toSubstring' _x.9;
+      let _x.11 := Name.mkStr1 _x.9;
+      let _x.12 := addMacroScope fst.6 _x.11 fst.2;
+      let _x.13 := [] _;
+      let _x.14 := Syntax.ident fst.4 _x.10 _x.12 _x.13;
+      let _x.15 := "+";
+      let _x.16 := Syntax.atom fst.4 _x.15;
+      let _x.17 := Lean.instQuoteNatNumLitKind._elam_0 n;
+      let _x.18 := Syntax.node3 fst.4 _x.8 _x.14 _x.16 _x.17;
+      return _x.18