feat(frontends/lean/user_notation): more error checking

src/frontends/lean/user_notation.cpp

@@ -20,14 +20,14 @@ static environment add_user_notation(environment const & env, name const & d, un
     auto type = env.get(d).get_type();
     bool is_nud = true;
     name tk;
-    if (is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) {
+    if (is_binding(type) && 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_pexpr_name(), 1)) {
             is_nud = false;
             type = binding_body(type);
         }
     }
-    if (is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) {
+    if (is_binding(type) && 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_tk_name(), 1)) {
             if (auto lit = to_string(app_arg(parser))) {
@@ -41,14 +41,21 @@ static environment add_user_notation(environment const & env, name const & d, un
     }
     if (!tk) {
         throw exception("invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` "
-                                "parameter, optionally preceded by `interactive.parse lean.parser.qexpr` parameter");
+                                "parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter");
     }
+
+    expr t = type;
+    while (is_pi(t)) { t = binding_body(t); }
+    if (!is_app_of(t, get_lean_parser_name(), 1)) {
+        throw exception("invalid user-defined notation, must return type `lean.parser p`");
+    }
+
     expr dummy = mk_true();
     persistence persist = persistent ? persistence::file : persistence::scope;
 
     return add_notation(env, notation_entry(is_nud, {notation::transition(tk, notation::mk_ext_action(
-            [=](parser & p, unsigned num, expr const * args, pos_info const &) -> expr {
-                lean_assert(num == (is_nud ? 0 : 1));
+            [=](parser & p, unsigned num, expr const * args, pos_info const & pos) -> expr {
+                lean_always_assert(num == (is_nud ? 0 : 1));
                 expr parser = mk_constant(d);
                 if (!is_nud)
                     parser = mk_app(parser, mk_pexpr_quote(args[0]));
@@ -67,7 +74,15 @@ static environment add_user_notation(environment const & env, name const & d, un
                     }
                 }
                 parser = p.elaborate("_user_notation", {}, parser).first;
-                return to_expr(run_parser(p, parser));
+                try {
+                    return to_expr(run_parser(p, parser));
+                } catch (formatted_exception const & ex) {
+                    if (ex.get_pos() && *ex.get_pos() >= pos) {
+                        throw;
+                    } else {
+                        throw formatted_exception(some(pos), ex.pp());
+                    }
+                }
             }))}, Var(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true), persist);
 }
 

src/library/constants.cpp

@@ -174,6 +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 = nullptr;
 name const * g_lean_parser_pexpr = nullptr;
 name const * g_lean_parser_tk = nullptr;
 name const * g_left_distrib = nullptr;
@@ -544,6 +545,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 = new name{"lean", "parser"};
     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"};
@@ -915,6 +917,7 @@ void finalize_constants() {
     delete g_is_commutative;
     delete g_is_commutative_comm;
     delete g_ite;
+    delete g_lean_parser;
     delete g_lean_parser_pexpr;
     delete g_lean_parser_tk;
     delete g_left_distrib;
@@ -1285,6 +1288,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_name() { return *g_lean_parser; }
 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; }

src/library/constants.h

@@ -176,6 +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_name();
 name const & get_lean_parser_pexpr_name();
 name const & get_lean_parser_tk_name();
 name const & get_left_distrib_name();

src/library/constants.txt

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

src/library/vm/vm_parser.cpp

@@ -157,9 +157,12 @@ vm_obj vm_parser_with_input(vm_obj const &, vm_obj const & vm_p, vm_obj const &
     std::string input = to_string(vm_input);
     std::istringstream strm(input);
     vm_obj vm_state; pos_info pos;
-    std::tie(vm_state, pos) = s.m_p->with_input<vm_obj>(strm, [&]() {
-        return invoke(vm_p, o);
-    });
+    auto _ = s.m_p->no_error_recovery_scope();
+    TRY;
+        std::tie(vm_state, pos) = s.m_p->with_input<vm_obj>(strm, [&]() {
+            return invoke(vm_p, o);
+        });
+    CATCH;
 
     if (lean_parser::is_result_exception(vm_state)) {
         return vm_state;

tests/lean/run/check_constants.lean

@@ -174,6 +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
 run_cmd script_check_id `lean.parser.pexpr
 run_cmd script_check_id `lean.parser.tk
 run_cmd script_check_id `left_distrib

tests/lean/user_notation.lean

@@ -17,3 +17,9 @@ do n₁ ← ↑(to_expr e₁ >>= eval_expr nat),
    pure $ (n₂+1-n₁).repeat (λ i e, ``(%%e + %%(reflect $ n₁ + i))) ``(0)
 
 #check 1 +⋯+ 10
+
+@[user_notation]
+meta def no_tk (e₁ : parse lean.parser.pexpr) := e₁
+
+@[user_notation]
+meta def no_parser (e₁ : parse $ tk "(") := e₁

tests/lean/user_notation.lean.expected.out

@@ -1,6 +1,6 @@
 2
 0 + (1 + 0) + (1 + 1) + (1 + 2) + (1 + 3) + (1 + 4) + (1 + 5) + (1 + 6) + (1 + 7) + (1 + 8) + (1 + 9) : ℕ
-user_notation.lean:21:0: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.[pq]expr` parameter
+user_notation.lean:21:0: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter
 user_notation.lean:22:9: error: don't know how to synthesize placeholder
 context:
 e₁ : parse lean.parser.pexpr