feat(library/init/lean/parser): universe level parser and bug fixes

library/init/lean/parser/level.lean

@@ -15,20 +15,20 @@ constant builtinLevelParsingTable : IO.Ref ParsingTables := default _
 @[init] def regBuiltinLevelParserAttr : IO Unit :=
 registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
 
-def levelParser (rbp : Nat := 0) : Parser :=
+def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 { fn := λ _, runBuiltinParser "universe level" builtinLevelParsingTable rbp }
 
-/-
-def_parser [builtinLevelParser]
-  paren  := "(":max_prec; levelParser; ")":0
-  hole   := "_":max_prec
-  imax   := "imax"
-  max    := "max"
-  num    := numLit
-  id     := ident
-  addLit := levelParser; "+":65; numLit
-  app    := levelParser; levelParser maxPrec
--/
+namespace Level
+
+@[builtinLevelParser] def paren := parser! symbol "(" maxPrec >> levelParser >> ")"
+@[builtinLevelParser] def max   := parser! "max" >> many1 (levelParser maxPrec)
+@[builtinLevelParser] def imax  := parser! "imax" >> many1 (levelParser maxPrec)
+@[builtinLevelParser] def hole  := parser! "_"
+@[builtinLevelParser] def num   : Parser := numLit
+@[builtinLevelParser] def ident : Parser := ident
+@[builtinLevelParser] def addLit := tparser! pushLeading >> symbol "+" (65:Nat) >> numLit
+
+end Level
 
 end Parser
 end Lean

library/init/lean/parser/parser.lean

@@ -34,6 +34,12 @@ def beq : TokenConfig → TokenConfig → Bool
 instance : HasBeq TokenConfig :=
 ⟨beq⟩
 
+def toStr : TokenConfig → String
+| ⟨val, some lbp⟩ := val ++ ":" ++ toString lbp
+| ⟨val, none⟩     := val
+
+instance : HasToString TokenConfig := ⟨toStr⟩
+
 end TokenConfig
 
 structure TokenCacheEntry :=
@@ -152,6 +158,13 @@ def seq : FirstTokens → FirstTokens → FirstTokens
 | epsilon tks := tks
 | tks     _   := tks
 
+def toStr : FirstTokens → String
+| epsilon      := "epsilon"
+| unknown      := "unknown"
+| (tokens tks) := toString tks
+
+instance : HasToString FirstTokens := ⟨toStr⟩
+
 end FirstTokens
 
 structure ParserInfo :=
@@ -219,10 +232,10 @@ instance hashAndthen {k : ParserKind} : HasAndthen (Parser k) :=
 { info := nodeInfo p.info,
   fn   := nodeFn n p.fn }
 
-@[inline] def leadingNode (n : SyntaxNodeKind) (p : Parser leading) : Parser leading :=
+@[inline] def leadingNode (n : SyntaxNodeKind) (p : Parser leading) : Parser :=
 node n p
 
-@[inline] def trailingNode (n : SyntaxNodeKind) (p : Parser trailing) : Parser trailing :=
+@[inline] def trailingNode (n : SyntaxNodeKind) (p : Parser trailing) : TrailingParser :=
 node n p
 
 @[inline] def orelseFn {k : ParserKind} (p q : ParserFn k) : ParserFn k
@@ -917,7 +930,7 @@ 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 then
+  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;

src/frontends/lean/builtin_exprs.cpp

@@ -890,13 +890,7 @@ expr mk_annotation_with_pos(parser &, name const & a, expr const & e, pos_info c
 }
 
 static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
-    name kind;
-    if (p.curr_is_identifier()) {
-        kind = p.check_id_next("identifier expected");
-        kind = get_namespace(p.env()) + kind;
-    } else {
-        kind = get_curr_declaration_name();
-    }
+    name kind = get_curr_declaration_name();
     expr e = p.parse_expr();
     name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
     expr r = mk_app(mk_constant(n), quote(kind), e);

src/frontends/lean/token_table.cpp

@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          {"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"match", 0}, {"^.", g_max_prec+1}, {"::", 67},
-         {"renaming", 0}, {"extends", 0}, {"parser!", g_max_prec}, {nullptr, 0}};
+         {"renaming", 0}, {"extends", 0}, {"parser!", g_max_prec}, {"tparser!", g_max_prec}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "hide",

tests/playground/levelparsertest1.lean

@@ -0,0 +1,22 @@
+import init.lean.parser.level
+open Lean
+open Lean.Parser
+
+def testParser (input : String) : IO Unit :=
+do
+env ← mkEmptyEnvironment;
+levelPTables ← builtinLevelParsingTable.get;
+stx ← IO.ofExcept $ runParser env levelPTables input;
+IO.println stx
+
+def main (xs : List String) : IO Unit :=
+do
+testParser "(1)";
+testParser "u";
+testParser "(u)";
+testParser "(u+1)";
+testParser "(u+1+2)";
+testParser "(max u v w)";
+testParser "imax u v";
+testParser "(max (u+1) v)";
+pure ()

tests/playground/parser1.lean

@@ -26,15 +26,15 @@ end Foo
 
 def testParser (input : String) : IO Unit :=
 do
-env ← mkEmptyEnvironment,
-testPTables ← builtinTestParsingTable.get,
-stx ← IO.ofExcept $ runParser env testPTables input,
+env ← mkEmptyEnvironment;
+testPTables ← builtinTestParsingTable.get;
+stx ← IO.ofExcept $ runParser env testPTables input;
 IO.println stx
 
 def main (xs : List String) : IO Unit :=
 do
-testParser "(10, hello)",
-testParser "{ hello, 400, \"hello\", (10, hello), /- comment -/ (20, world), { fun x, (10, hello) }, { (30, foo) } }",
+testParser "(10, hello)";
+testParser "{ hello, 400, \"hello\", (10, hello), /- comment -/ (20, world), { fun x, (10, hello) }, { (30, foo) } }";
 -- Following example has syntax error
 testParser
 "{ hello, 400, \"hello\", (10, hello), /- comment -/ (20, world), { fun x, [ (10, hello) }, { (30, foo) } }"