From ebde7756713dbece5b1b367b245ea474eb6d1487 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 23 Dec 2019 17:07:30 +0100 Subject: [PATCH] fix: invoke new parser from old one with maximum precedence --- src/Init/Lean/Elab/Quotation.lean | 2 +- tests/lean/StxQuot.lean | 1 + tests/lean/StxQuot.lean.expected.out | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 0a7242b6bb..b651177a8c 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -390,7 +390,7 @@ let c := Parser.mkParserContextCore env input ""; let c := c.toParserContext env; let s := Parser.mkParserState c.input; let s := s.setPos pos; -let s := (Parser.termParser : Parser.Parser).fn (0 : Nat) c s; +let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn Parser.appPrec c s; let stx := s.stxStack.back; match s.errorMsg with | some errorMsg => diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index d820c20fa3..d59bcc9f5c 100644 --- a/tests/lean/StxQuot.lean +++ b/tests/lean/StxQuot.lean @@ -14,6 +14,7 @@ namespace Syntax #eval run $ let id := Syntax.missing; `($id + 1) end Syntax #eval run `(1 + 1) +#eval run $ `(fun a => a) >>= pure #eval run $ do a ← `(Nat.one); `($a) #eval run $ do a ← `(Nat.one); `(f $a $a) #eval run $ do a ← `(Nat.one); `(f $ f $a 1) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 54144642f1..b39f180573 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -5,6 +5,7 @@ "(Term.add \"+\" (Term.num (numLit \"1\")))" "(Term.add \"+\" (Term.num (numLit \"1\")))" "(Term.add (Term.num (numLit \"1\")) \"+\" (Term.num (numLit \"1\")))" +"(Term.fun \"fun\" (null (Term.id `a.0 (null))) \"=>\" (Term.id `a.0 (null)))" "(Term.id `Nat.one.0 (null))" "(Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.id `Nat.one.0 (null)))" "(Term.dollar\n (Term.id `f.0 (null))\n \"$\"\n (Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.num (numLit \"1\"))))"