feat: print more information for LCNF RC ops (#13097)

This PR makes the compiler traces contain more information about the
kind of `inc`/`dec` that are
being conducted (`persistent`, `checked` etc.)

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -154,16 +154,18 @@ mutual
       return f!"oset {← ppFVar fvarId} [{i}] := {← ppArg y};" ++ .line ++ (← ppCode k)
     | .setTag fvarId cidx k _ =>
       return f!"setTag {← ppFVar fvarId} := {cidx};" ++ .line ++ (← ppCode k)
-    | .inc fvarId n _ _ k _ =>
+    | .inc fvarId n check persistent k _ =>
+      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
       if n != 1 then
-        return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"inc[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"inc {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
-    | .dec fvarId n _ _ k _ =>
+        return f!"inc{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+    | .dec fvarId n check persistent k _ =>
+      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
       if n != 1 then
-        return f!"dec[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"dec {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
     | .del fvarId k _ =>
       return f!"del {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
 

tests/elab/borrowBug.lean

@@ -29,14 +29,14 @@ trace: [Compiler.explicitRc] size: 27
         let z := g x;
         let fst := oproj[0] z;
         inc fst;
-        dec z;
+        dec[ref] z;
         goto _jp.1 fst
       | Bool.true =>
         dec x;
         let z := g y;
         let fst := oproj[0] z;
         inc fst;
-        dec z;
+        dec[ref] z;
         goto _jp.1 fst
 [Compiler.explicitRc] size: 2
     def f._boxed x y : tagged :=

tests/elab/compile_borrowed_reset_jp.lean

@@ -27,8 +27,8 @@ trace: [Compiler.explicitRc] size: 17
 [Compiler.explicitRc] size: 4
     def testWithAnnotation._boxed n p q : obj :=
       let res := testWithAnnotation n p q;
-      dec q;
-      dec p;
+      dec[ref] q;
+      dec[ref] p;
       dec n;
       return res
 -/
@@ -55,11 +55,11 @@ trace: [Compiler.explicitRc] size: 20
       let isZero := Nat.decEq n zero;
       cases isZero : obj
       | Bool.true =>
-        dec q;
+        dec[ref] q;
         let _x.6 := 123;
         goto _jp.1 _x.6 p
       | Bool.false =>
-        dec p;
+        dec[ref] p;
         let one := 1;
         let n.7 := Nat.sub n one;
         let _x.8 := Nat.add n.7 one;

tests/elab/compile_recursive_array_access.lean

@@ -17,7 +17,7 @@ trace: [Compiler.explicitRc] size: 19
         cases path : obj
         | List.nil =>
           let x.1 := oproj[0] tree;
-          inc x.1;
+          inc[ref] x.1;
           return x.1
         | _ =>
           let _x.2 := instInhabitedNAryTree.default._closed_0;
@@ -39,7 +39,7 @@ trace: [Compiler.explicitRc] size: 19
     def followPath._boxed tree path : obj :=
       let res := followPath tree path;
       dec path;
-      dec tree;
+      dec[ref] tree;
       return res
 -/
 #guard_msgs in

tests/elab/compiler_push_proj.lean

@@ -61,7 +61,7 @@ trace: [Compiler.pushProj] size: 10
       | Option.some =>
         cases b : tobj
         | Option.none =>
-          inc a;
+          inc[ref] a;
           return a
         | Option.some =>
           let val.1 : tobj := oproj[0] a;
@@ -157,7 +157,7 @@ trace: [Compiler.pushProj] size: 14
         | Option.some =>
           let val.11 : tobj := oproj[0] a;
           inc val.11;
-          dec a;
+          dec[ref] a;
           let val.12 : tobj := oproj[0] b;
           jp resetjp.13 _x.14 isShared.15 : tobj :=
             let _x.16 : tobj := Nat.add val.11 val.12;
@@ -251,14 +251,14 @@ trace: [Compiler.pushProj] size: 18
         | Option.some =>
           cases c : tobj
           | Bool.false =>
-            dec b;
-            dec a;
+            dec[ref] b;
+            dec[ref] a;
             let _x.11 : tagged := ctor_0[Option.none];
             return _x.11
           | Bool.true =>
             let val.12 : tobj := oproj[0] a;
             inc val.12;
-            dec a;
+            dec[ref] a;
             let val.13 : tobj := oproj[0] b;
             jp resetjp.14 _x.15 isShared.16 : tobj :=
               let _x.17 : tobj := Nat.add val.12 val.13;

tests/elab/jpVoidArgs.lean

@@ -52,17 +52,17 @@ trace: [Compiler.saveMono] size: 25
       cases x : tobj
       | Enum.A =>
         let _x.6 := 0;
-        inc y;
+        inc[ref] y;
         let _x.7 := y _x.6 ◾;
         goto _jp.2
       | Enum.B =>
         let _x.8 := 1;
-        inc y;
+        inc[ref] y;
         let _x.9 := y _x.8 ◾;
         goto _jp.2
       | Enum.C =>
         let _x.10 := 2;
-        inc y;
+        inc[ref] y;
         let _x.11 := y _x.10 ◾;
         goto _jp.2
 [Compiler.saveImpure] size: 2

tests/elab/lcnf_borrow_expected_type.lean

@@ -168,7 +168,7 @@ trace: [Compiler.explicitRc] size: 22
 [Compiler.explicitRc] size: 2
     def cascadeDemo._boxed t : tobj :=
       let res := cascadeDemo t;
-      dec t;
+      dec[ref] t;
       return res
 -/
 #guard_msgs in
@@ -183,20 +183,20 @@ def cascadeDemo (t : @&Quad) : Nat :=
 trace: [Compiler.explicitRc] size: 33
     def cascadeDemo' t : tobj :=
       let left := oproj[0] t;
-      inc left;
+      inc[ref] left;
       let right := oproj[1] t;
-      inc right;
-      dec t;
+      inc[ref] right;
+      dec[ref] t;
       let fst := oproj[0] left;
       inc fst;
       let snd := oproj[1] left;
       inc snd;
-      dec left;
+      dec[ref] left;
       let fst := oproj[0] right;
       inc fst;
       let snd := oproj[1] right;
       inc snd;
-      dec right;
+      dec[ref] right;
       let _x.1 := wrap fst;
       let res := List.lengthTR._redArg _x.1;
       dec _x.1;
@@ -238,7 +238,7 @@ trace: [Compiler.explicitRc] size: 15
         dec a;
         let fst := oproj[0] x;
         inc fst;
-        dec x;
+        dec[ref] x;
         return fst
       | Bool.false =>
         let one := 1;

tests/elab/ugetBorrowed.lean

@@ -11,7 +11,7 @@ trace: [Compiler.explicitRc] size: 3
       let i.boxed := unbox i;
       dec i;
       let res := test._redArg xs i.boxed;
-      dec xs;
+      dec[ref] xs;
       let r := box res;
       return r
 [Compiler.explicitRc] size: 1
@@ -23,7 +23,7 @@ trace: [Compiler.explicitRc] size: 3
       let i.boxed := unbox i;
       dec i;
       let res := test xs i.boxed h;
-      dec xs;
+      dec[ref] xs;
       let r := box res;
       return r
 -/