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

fix: invoke new parser from old one with maximum precedence

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-23 17:07:30 +01:00 • committed by Leonardo de Moura
parent 1a7cd0e54d
commit ebde775671
3 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Quotation.lean
View file

@ -390,7 +390,7 @@ let c := Parser.mkParserContextCore env input "<foo>";
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 =>

1
tests/lean/StxQuot.lean
View file

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

1
tests/lean/StxQuot.lean.expected.out
View file

@ -5,6 +5,7 @@
"(Term.add <missing> \"+\" (Term.num (numLit \"1\")))"
"(Term.add <missing> \"+\" (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\"))))"