diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 87808105f7..eb74505f6b 100644 --- a/library/init/lean/parser/parser.lean +++ b/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 diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 1ac28b5c59..ffe955174d 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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; } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 9d90573878..ef6cbc3b2b 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 56b616fd46..8aa0ee0980 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 5dcfe7df1b..b42c1f920b 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/tests/playground/parser1.lean b/tests/playground/parser1.lean index 1e149b67d8..d7c2b45320 100644 --- a/tests/playground/parser1.lean +++ b/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 :=