feat(init/meta/lean/parser): pexpr parser that does not use quoted mode

library/init/meta/lean/parser.lean

@@ -25,6 +25,8 @@ namespace parser
 meta constant ident : parser name
 /-- Check that the next token is `tk` and consume it. `tk` must be a registered token. -/
 meta constant tk (tk : string) : parser unit
+/-- Parse an unelaborated expression using the given right-binding power. -/
+protected meta constant pexpr (rbp := std.prec.max) : parser pexpr
 /-- Parse an unelaborated expression using the given right-binding power. The expression
     may contain antiquotations (`%%e`). -/
 meta constant qexpr (rbp := std.prec.max) : parser pexpr

src/frontends/lean/user_notation.cpp

@@ -21,7 +21,7 @@ static environment add_user_notation(environment const & env, name const & d, un
     name tk;
     if (is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) {
         auto const & parser = app_arg(binding_domain(type));
-        if (is_app_of(parser, get_lean_parser_qexpr_name(), 1)) {
+        if (is_app_of(parser, get_lean_parser_pexpr_name(), 1)) {
             is_nud = false;
             type = binding_body(type);
         }

src/library/constants.cpp

@@ -174,7 +174,7 @@ name const * g_is_associative_assoc = nullptr;
 name const * g_is_commutative = nullptr;
 name const * g_is_commutative_comm = nullptr;
 name const * g_ite = nullptr;
-name const * g_lean_parser_qexpr = nullptr;
+name const * g_lean_parser_pexpr = nullptr;
 name const * g_lean_parser_tk = nullptr;
 name const * g_left_distrib = nullptr;
 name const * g_left_comm = nullptr;
@@ -544,7 +544,7 @@ void initialize_constants() {
     g_is_commutative = new name{"is_commutative"};
     g_is_commutative_comm = new name{"is_commutative", "comm"};
     g_ite = new name{"ite"};
-    g_lean_parser_qexpr = new name{"lean", "parser", "qexpr"};
+    g_lean_parser_pexpr = new name{"lean", "parser", "pexpr"};
     g_lean_parser_tk = new name{"lean", "parser", "tk"};
     g_left_distrib = new name{"left_distrib"};
     g_left_comm = new name{"left_comm"};
@@ -915,7 +915,7 @@ void finalize_constants() {
     delete g_is_commutative;
     delete g_is_commutative_comm;
     delete g_ite;
-    delete g_lean_parser_qexpr;
+    delete g_lean_parser_pexpr;
     delete g_lean_parser_tk;
     delete g_left_distrib;
     delete g_left_comm;
@@ -1285,7 +1285,7 @@ name const & get_is_associative_assoc_name() { return *g_is_associative_assoc; }
 name const & get_is_commutative_name() { return *g_is_commutative; }
 name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; }
 name const & get_ite_name() { return *g_ite; }
-name const & get_lean_parser_qexpr_name() { return *g_lean_parser_qexpr; }
+name const & get_lean_parser_pexpr_name() { return *g_lean_parser_pexpr; }
 name const & get_lean_parser_tk_name() { return *g_lean_parser_tk; }
 name const & get_left_distrib_name() { return *g_left_distrib; }
 name const & get_left_comm_name() { return *g_left_comm; }

src/library/constants.h

@@ -176,7 +176,7 @@ name const & get_is_associative_assoc_name();
 name const & get_is_commutative_name();
 name const & get_is_commutative_comm_name();
 name const & get_ite_name();
-name const & get_lean_parser_qexpr_name();
+name const & get_lean_parser_pexpr_name();
 name const & get_lean_parser_tk_name();
 name const & get_left_distrib_name();
 name const & get_left_comm_name();

src/library/constants.txt

@@ -169,7 +169,7 @@ is_associative.assoc
 is_commutative
 is_commutative.comm
 ite
-lean.parser.qexpr
+lean.parser.pexpr
 lean.parser.tk
 left_distrib
 left_comm

src/library/vm/vm_parser.cpp

@@ -95,6 +95,18 @@ vm_obj vm_parser_tk(vm_obj const & vm_tk, vm_obj const & o) {
     CATCH;
 }
 
+vm_obj vm_parser_pexpr(vm_obj const & vm_rbp, vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    TRY;
+        auto rbp = to_unsigned(vm_rbp);
+        if (auto e = s.m_p->maybe_parse_expr(rbp)) {
+            return lean_parser::mk_success(to_obj(*e), s);
+        } else {
+            throw parser_error(sstream() << "expression expected", s.m_p->pos());
+        }
+    CATCH;
+}
+
 vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
     TRY;
@@ -130,7 +142,8 @@ void initialize_vm_parser() {
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),     vm_parser_state_cur_pos);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),             vm_parser_ident);
     DECLARE_VM_BUILTIN(get_lean_parser_tk_name(),                     vm_parser_tk);
-    DECLARE_VM_BUILTIN(get_lean_parser_qexpr_name(),                  vm_parser_qexpr);
+    DECLARE_VM_BUILTIN(get_lean_parser_pexpr_name(),                  vm_parser_pexpr);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),             vm_parser_qexpr);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "skip_info"}),         vm_parser_skip_info);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos);
 }

tests/lean/run/check_constants.lean

@@ -174,7 +174,7 @@ run_cmd script_check_id `is_associative.assoc
 run_cmd script_check_id `is_commutative
 run_cmd script_check_id `is_commutative.comm
 run_cmd script_check_id `ite
-run_cmd script_check_id `lean.parser.qexpr
+run_cmd script_check_id `lean.parser.pexpr
 run_cmd script_check_id `lean.parser.tk
 run_cmd script_check_id `left_distrib
 run_cmd script_check_id `left_comm

tests/lean/user_notation.lean

@@ -4,11 +4,10 @@ open tactic
 
 reserve prefix `unquote! `:100
 @[user_notation]
-meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse qexpr) : tactic pexpr :=
 to_expr e >>= eval_expr pexpr
+meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse lean.parser.pexpr) : parser pexpr :=
 
-meta def e := ``(1 + 1)
-#eval unquote! e
+#eval unquote! ``(1 + 1)
 
 private meta def parse_format : string → string → ℕ × pexpr
 | acc [] := (0, pexpr.of_expr (reflect acc))
@@ -29,8 +28,8 @@ pure $ n.repeat (λ _ e, expr.lam `_ binder_info.default pexpr.mk_placeholder e)
 
 reserve infix ` +⋯+ `:65
 @[user_notation]
-meta def upto_notation (e₁ : parse qexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : tactic pexpr :=
 do n₁ ← to_expr e₁ >>= eval_expr nat,
+meta def upto_notation (e₁ : parse lean.parser.pexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : parser pexpr :=
    pure $ (n₂+1-n₁).repeat (λ i e, ``(%%e + %%(reflect $ n₁ + i))) ``(0)
 
 #check 1 +⋯+ 10