From 13b5747713125577e4d52b557f6b367b70f34ca6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Jul 2019 16:00:58 -0700
Subject: [PATCH] fix(library/init/lean/parser/parser): `prattParser`

---
 library/init/lean/parser/parser.lean   | 33 ++++++++++++--------------
 tests/playground/levelparsertest1.lean |  1 +
 tests/playground/termparsertest1.lean  | 20 ++++++++++++++++
 3 files changed, 36 insertions(+), 18 deletions(-)
 create mode 100644 tests/playground/termparsertest1.lean

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 554c462f51..a84f14db17 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -933,30 +933,27 @@ def leadingParser (kind : String) (tables : ParsingTables) : ParserFn leading :=
     let s       := longestMatchFn ps a c s;
     mkResult s iniSz
 
-def trailingParser (kind : String) (tables : ParsingTables) : ParserFn trailing :=
-λ a c s,
-  let iniSz   := s.stackSize;
-  let (s, ps) := indexed tables.trailingTable c s;
-  if ps.isEmpty && tables.trailingParsers.isEmpty then
-    s.mkError ("expected trail of " ++ kind) -- better error message?
-  else
-    let s       := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) a c s;
-    mkResult s iniSz
-
 partial def trailingLoop (kind : String) (tables : ParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState
 | left s :=
   let (s, lbp) := currLbp c s;
   if rbp ≥ lbp then s.pushSyntax left
   else
-    let s    := trailingParser kind tables left c s;
-    if s.hasError then s
+    let iniSz   := s.stackSize;
+    let (s, ps) := indexed tables.trailingTable c s;
+    if ps.isEmpty && tables.trailingParsers.isEmpty then
+      s.pushSyntax left -- no available trail
     else
-      let left := s.stxStack.back;
-      let s    := s.popSyntax;
-      trailingLoop left s
+      let s := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) left c s;
+      if s.hasError then s
+      else
+        let s := mkResult s iniSz;
+        let left := s.stxStack.back;
+        let s    := s.popSyntax;
+        trailingLoop left s
 
 def prattParser (kind : String) (tables : ParsingTables) : ParserFn leading :=
 λ rbp c s,
+  let c := { tokens := tables.tokens, .. c };
   let s := leadingParser kind tables rbp c s;
   if s.hasError then s
   else
@@ -964,18 +961,18 @@ def prattParser (kind : String) (tables : ParsingTables) : ParserFn leading :=
     let s    := s.popSyntax;
     trailingLoop kind tables rbp c left s
 
-def mkParserContext (env : Environment) (input : String) (filename : String) (tokens : Trie TokenConfig) : ParserContext :=
+def mkParserContext (env : Environment) (input : String) (filename : String) : ParserContext :=
 { env      := env,
   input    := input,
   filename := filename,
   fileMap  := input.toFileMap,
-  tokens   := tokens }
+  tokens   := {} }
 
 def mkParserState (input : String) : ParserState :=
 { cache := initCacheForInput input }
 
 def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "<input>") (kind := "<main>") : Except String Syntax :=
-let c := mkParserContext env input fileName tables.tokens;
+let c := mkParserContext env input fileName;
 let s := mkParserState input;
 let s := prattParser kind tables (0 : Nat) c s;
 if s.hasError then
diff --git a/tests/playground/levelparsertest1.lean b/tests/playground/levelparsertest1.lean
index ed7aa173d7..12a726a318 100644
--- a/tests/playground/levelparsertest1.lean
+++ b/tests/playground/levelparsertest1.lean
@@ -11,6 +11,7 @@ IO.println stx
 
 def main (xs : List String) : IO Unit :=
 do
+testParser "max 0 1";
 testParser "(1)";
 testParser "u";
 testParser "(u)";
diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean
new file mode 100644
index 0000000000..290cba19e7
--- /dev/null
+++ b/tests/playground/termparsertest1.lean
@@ -0,0 +1,20 @@
+import init.lean.parser.term
+open Lean
+open Lean.Parser
+
+def testParser (input : String) : IO Unit :=
+do
+env ← mkEmptyEnvironment;
+termPTables ← builtinTermParsingTable.get;
+stx ← IO.ofExcept $ runParser env termPTables input "<input>" "expr";
+IO.println stx
+
+def main (xs : List String) : IO Unit :=
+do
+testParser "x.{u v+1}";
+testParser "x";
+testParser "x.{max u v}";
+testParser "x.{(max u v) 0}";
+testParser "f 0 1";
+testParser "f.{u+1} \"foo\" x";
+pure ()