diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 816fa61f42..3359275793 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1399,6 +1399,17 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par let s := mkTrailingResult s iniSz; trailingLoop s +def checkTokenLBPFn : ParserFn := +fun c s => + let left := s.stxStack.back; + let (s, lbp) := currLbp left c s; + if c.rbp < lbp then s + else s.mkUnexpectedError "unexpected token" + +def checkTokenLBP : Parser := +{ info := epsilonInfo, + fn := checkTokenLBPFn } + /-- Implements a recursive precedence parser according to Pratt's algorithm. diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index abe70dc2f4..32e0cd61db 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -124,7 +124,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}" @[builtinTermParser] def uminus := parser! "-" >> termParser 100 def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" -@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec) +@[builtinTermParser] def app := tparser! many1 (namedArgument <|> (checkTokenLBP >> termParser appPrec)) def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort) @[builtinTermParser] def sortApp := tparser! checkIsSort >> levelParser appPrec diff --git a/tests/lean/appParserIssue.lean b/tests/lean/appParserIssue.lean new file mode 100644 index 0000000000..4bbdc9335e --- /dev/null +++ b/tests/lean/appParserIssue.lean @@ -0,0 +1,13 @@ +def f (x : Nat) (g : Nat → Nat) := g x + +new_frontend + +#check f 1 fun x => x -- should fail +#check f 1 (fun x => x) -- should work +#check f 1 $ fun x => x -- should work + +syntax "foo" term:max term:max : term +macro_rules `(foo $x $y) => `(f $x $y) + +#check foo 1 fun x => x -- should fail? +#check foo 1 (fun x => x) -- should work diff --git a/tests/lean/appParserIssue.lean.expected.out b/tests/lean/appParserIssue.lean.expected.out new file mode 100644 index 0000000000..5a4f85f3d4 --- /dev/null +++ b/tests/lean/appParserIssue.lean.expected.out @@ -0,0 +1,6 @@ +f 1 : (Nat → Nat) → Nat +appParserIssue.lean:5:11: error: expected command +f 1 (λ (x : Nat), x) : Nat +f 1 (λ (x : Nat), x) : Nat +f 1 (λ (x : Nat), x) : Nat +f 1 (λ (x : Nat), x) : Nat