From 77e1260ed2573e3f06564924048c2f68690eaade Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Jun 2020 14:34:58 -0700
Subject: [PATCH] chore: simplify `checkPrec`

---
 src/Lean/Parser/Parser.lean                      | 14 ++++++--------
 src/Lean/Parser/Term.lean                        |  2 +-
 tests/compiler/termparsertest1.lean.expected.out |  2 +-
 3 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index 132d62dc36..47ae7a64de 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -1082,17 +1082,15 @@ let asciiSym := asciiSym.trim;
 { info := unicodeSymbolInfo sym asciiSym,
   fn   := unicodeSymbolFn sym asciiSym }
 
-/- Succeeds if prec <= upper -/
-def checkPrecFn (upper : Nat) (errorMsg : String) : ParserFn :=
+/- Succeeds if `c.prec <= prec` -/
+def checkPrecFn (prec : Nat) : ParserFn :=
 fun c s =>
-  if c.prec <= upper then s
-  else s.mkUnexpectedError errorMsg
+  if c.prec <= prec then s
+  else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term"
 
-private def precErrorMsg := "unexpected token at this precedence level; consider parenthesizing the term"
-
-@[inline] def checkPrec (upper : Nat) (errorMsg : String := precErrorMsg) : Parser :=
+@[inline] def checkPrec (prec : Nat) : Parser :=
 { info := epsilonInfo,
-  fn   := checkPrecFn upper errorMsg }
+  fn   := checkPrecFn prec }
 
 /- Version of `leadingNode` which uses `checkPrec` -/
 @[inline] def leadingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index cff7263762..124a6624cf 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -91,7 +91,7 @@ def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >>
 def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
 def instBinder := parser! "[" >> optIdent >> termParser >> "]"
 def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
-@[builtinTermParser] def depArrow := parser! [appPrec] bracketedBinder true >> checkPrec 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
+@[builtinTermParser] def depArrow := parser! [appPrec] bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
 def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser! [leadPrec] unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
 
diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index a2cc8ad864..e2a1445913 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -525,7 +525,7 @@ f 20
 max a b
 (Term.app (Term.id `max (null)) (null (Term.id `a (null)) (Term.id `b (null))))
 f {x : a} -> b
-failed as expected, error: <input>:1:10 expected parentheses around dependent arrow
+failed as expected, error: <input>:1:10 unexpected token at this precedence level; consider parenthesizing the term
 (x := 20)
 failed as expected, error: <input>:1:3 expected ')' or ':'
 let x 10; x