From 43caef01303b073a7aa3e33bdb9ef6ba49d9dc87 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 13 Jun 2020 11:13:37 +0200
Subject: [PATCH] fix: parenthesizer

---
 src/Lean/PrettyPrinter/Parenthesizer.lean |  4 ++--
 tests/lean/PPRoundtrip.lean               |  2 +-
 tests/lean/PPRoundtrip.lean.expected.out  | 17 ++++++-----------
 3 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 8d2493299a..f72e57ddbb 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -387,6 +387,7 @@ addLbp prec
 def trailingNode.parenthesizer : Parenthesizer | p => do
 stx ← getCur;
 k ← evalName $ p.getArg! 0;
+prec ← evalNat $ p.getArg! 1;
 when (k != stx.getKind) $ do {
   trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
   -- HACK; see `orelse.parenthesizer`
@@ -399,8 +400,7 @@ visitArgs $ do {
   -- parser is calling us; we only need to know its `mkParen`, which we retrieve from the context.
   { mkParen := some mkParen, .. } ← read
     | panic! "trailingNode.parenthesizer called outside of visitParenthesizable call";
-  { minLbp := trailLbp, .. } ← get;
-  visitAntiquot <|> visitParenthesizable mkParen 0 trailLbp;
+  visitAntiquot <|> visitParenthesizable mkParen 0 prec;
   visit p.appArg!
 }
 
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index 7f34849481..1da1f51386 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -49,7 +49,7 @@ def typeAs.{u} (α : Type u) (a : α) := ()
 #eval check `(fun (a : Nat) (b : Bool) => a)
 #eval check `(fun {a b : Nat} => a)
 -- implicit lambdas work as long as the expected type is preserved
-#eval check `(typeAs ({α : Type} → (a : α) → α) (fun a => a))
+#eval check `(typeAs ({α : Type} → (a : α) → α) fun a => a)
 section set_option pp.explicit true
   #eval check `(fun {α : Type} [HasToString α] (a : α) => toString a)
 end
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 5554e4a710..7c81304b56 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -71,18 +71,13 @@
      (Term.arrow (Term.id `α (null)) "→" (Term.id `α (null))))
     (null))
    ")")
-  (Term.paren
-   "("
+  (Term.fun
+   "fun"
    (null
-    (Term.fun
-     "fun"
-     (null
-      (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
-      (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
-     "=>"
-     (Term.id `a (null)))
-    (null))
-   ")")))
+    (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
+    (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
+   "=>"
+   (Term.id `a (null)))))
 (Term.fun
  "fun"
  (null