max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: simplify checkPrec

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-10 14:34:58 -07:00
parent a677c18683
commit 77e1260ed2
3 changed files with 8 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Parser/Parser.lean
View file

@ -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 :=

2
src/Lean/Parser/Term.lean
View file

@ -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

2
tests/compiler/termparsertest1.lean.expected.out
View file

@ -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