fix: parenthesizer: adjust lbp after parenthesization

src/Init/Lean/PrettyPrinter/Parenthesizer.lean

@@ -264,7 +264,7 @@ adaptReader (fun (ctx : Context) => { ctx with mkParen := some mkParen }) $
   | panic! "visitParenthesizable: visited a term without tokens?!";
 trace! `PrettyPrinter.parenthesize ("...precedences are " ++ fmt rbp ++ " >? " ++ fmt minLbpP ++ ", " ++ fmt trailRbpP ++ " <? " ++ fmt st.firstLbp);
 -- Should we parenthesize?
-trailRbpP ← if rbp > minLbpP || (match trailRbpP, st.firstLbp with some trailRbpP, some firstLbp => trailRbpP < firstLbp | _, _ => false) then do
+when (rbp > minLbpP || match trailRbpP, st.firstLbp with some trailRbpP, some firstLbp => trailRbpP < firstLbp | _, _ => false) $ do {
     -- The recursive `visit` call, by the invariant, has moved to the next node to the left. In order to parenthesize
     -- the original node, we must first move to the right, except if we already were at the left-most child in the first
     -- place.
@@ -281,8 +281,9 @@ trailRbpP ← if rbp > minLbpP || (match trailRbpP, st.firstLbp with some trailR
     stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none);
     goLeft;
     -- after parenthesization, there is no more trailing parser
-    pure (none : Option Nat)
-  else pure trailRbpP;
+    modify (fun st => { st with minLbp := appPrec, firstLbp := appPrec, trailRbp := none })
+};
+{ trailRbp := trailRbpP, .. } ← get;
 -- If we already had a token at this level (`st.firstLbp ≠ none`), keep the trailing parser. Otherwise, use the minimum of
 -- `rbp` and `trailRbpP`.
 let trailRbp := match trailRbpP, st.firstLbp with

tests/lean/run/Reparen.lean

@@ -32,6 +32,10 @@ partial def unparen : Syntax → Syntax
   | _ => stx.modifyArgs $ Array.map unparen
 
 def main (args : List String) : IO Unit := do
+let (debug, f) : Bool × String := match args with
+  | [f, "-d"] => (true, f)
+  | [f]       => (false, f)
+  | _         => panic! "usage: file [-d]";
 initSearchPath none;
 env ← importModules [{module := `Init.Lean.Parser}];
 stx ← Lean.Parser.parseFile env args.head!;
@@ -42,8 +46,7 @@ let cmds := stx.getArgs.extract 1 stx.getArgs.size;
 cmds.forM $ fun cmd => do
   let cmd := unparen cmd;
   (cmd, _) ← IO.runMeta (PrettyPrinter.parenthesizeCommand cmd)
-    -- change to `true` for trace output
-    env { opts := KVMap.insert {} `trace.PrettyPrinter.parenthesize false };
+    env { opts := KVMap.insert {} `trace.PrettyPrinter.parenthesize debug };
   some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
   IO.print s