feat(frontends/lean/builtin_exprs): minor improvement

library/init/lean/parser/parser.lean

@@ -219,6 +219,12 @@ 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 :=
+node n p
+
+@[inline] def trailingNode (n : SyntaxNodeKind) (p : Parser trailing) : Parser trailing :=
+node n p
+
 @[inline] def orelseFn {k : ParserKind} (p q : ParserFn k) : ParserFn k
 | a c s :=
   let iniSz  := s.stackSize in

src/frontends/lean/builtin_exprs.cpp

@@ -889,7 +889,7 @@ expr mk_annotation_with_pos(parser &, name const & a, expr const & e, pos_info c
     return save_pos(r, pos);
 }
 
-static expr parse_parser(parser & p, unsigned, expr const *, pos_info const & pos) {
+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");
@@ -898,10 +898,19 @@ static expr parse_parser(parser & p, unsigned, expr const *, pos_info const & po
         kind = get_curr_declaration_name();
     }
     expr e = p.parse_expr();
-    expr r = mk_app(mk_constant(get_lean_parser_node_name()), quote(kind), e);
+    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);
     return save_pos(r, pos);
 }
 
+static expr parse_lparser(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_parser(p, true, pos);
+}
+
+static expr parse_tparser(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_parser(p, false, pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -936,7 +945,8 @@ parse_table init_nud_table() {
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
     r = r.add({transition("match", mk_ext_action(parse_match))}, x0);
     r = r.add({transition("do", mk_ext_action(parse_do_expr))}, x0);
-    r = r.add({transition("parser!", mk_ext_action(parse_parser))}, x0);
+    r = r.add({transition("parser!", mk_ext_action(parse_lparser))}, x0);
+    r = r.add({transition("tparser!", mk_ext_action(parse_tparser))}, x0);
     return r;
 }
 

src/library/constants.cpp

@@ -114,7 +114,8 @@ name const * g_lean_name = nullptr;
 name const * g_lean_name_anonymous = nullptr;
 name const * g_lean_name_mk_numeral = nullptr;
 name const * g_lean_name_mk_string = nullptr;
-name const * g_lean_parser_node = nullptr;
+name const * g_lean_parser_leading_node = nullptr;
+name const * g_lean_parser_trailing_node = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_succ = nullptr;
 name const * g_nat_zero = nullptr;
@@ -295,7 +296,8 @@ void initialize_constants() {
     g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
     g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"};
     g_lean_name_mk_string = new name{"Lean", "Name", "mkString"};
-    g_lean_parser_node = new name{"Lean", "Parser", "node"};
+    g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
+    g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
     g_nat = new name{"Nat"};
     g_nat_succ = new name{"Nat", "succ"};
     g_nat_zero = new name{"Nat", "zero"};
@@ -477,7 +479,8 @@ void finalize_constants() {
     delete g_lean_name_anonymous;
     delete g_lean_name_mk_numeral;
     delete g_lean_name_mk_string;
-    delete g_lean_parser_node;
+    delete g_lean_parser_leading_node;
+    delete g_lean_parser_trailing_node;
     delete g_nat;
     delete g_nat_succ;
     delete g_nat_zero;
@@ -658,7 +661,8 @@ name const & get_lean_name_name() { return *g_lean_name; }
 name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
 name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; }
 name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; }
-name const & get_lean_parser_node_name() { return *g_lean_parser_node; }
+name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
+name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_succ_name() { return *g_nat_succ; }
 name const & get_nat_zero_name() { return *g_nat_zero; }

src/library/constants.h

@@ -116,7 +116,8 @@ name const & get_lean_name_name();
 name const & get_lean_name_anonymous_name();
 name const & get_lean_name_mk_numeral_name();
 name const & get_lean_name_mk_string_name();
-name const & get_lean_parser_node_name();
+name const & get_lean_parser_leading_node_name();
+name const & get_lean_parser_trailing_node_name();
 name const & get_nat_name();
 name const & get_nat_succ_name();
 name const & get_nat_zero_name();

src/library/constants.txt

@@ -109,7 +109,8 @@ Lean.Name
 Lean.Name.anonymous
 Lean.Name.mkNumeral
 Lean.Name.mkString
-Lean.Parser.node
+Lean.Parser.leadingNode
+Lean.Parser.trailingNode
 Nat
 Nat.succ
 Nat.zero

tests/playground/parser1.lean

@@ -4,13 +4,13 @@ open Lean.Parser
 
 namespace Foo
 
-@[builtinTestParser] def pairParser : Parser :=
+@[builtinTestParser] def pairParser :=
 parser! "(" >> numLit >> "," >> ident >> ")"
 
-@[builtinTestParser] def pairsParser : Parser :=
+@[builtinTestParser] def pairsParser :=
 parser! "{" >> sepBy1 testParser "," >> "}"
 
-@[builtinTestParser] def functionParser : Parser :=
+@[builtinTestParser] def functionParser :=
 parser! "fun" >> ident >> "," >> testParser
 
 @[builtinTestParser] def identParser : Parser :=