diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp index bd4c60a14c..07c3f4d3bc 100644 --- a/src/frontends/lean/user_notation.cpp +++ b/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); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index c02858c377..843dc6b304 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 6b3b7eea27..46d2c17c81 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index e88dfe93c6..932146ce92 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 7e7cc1573c..62977635bf 100644 --- a/src/library/vm/vm_parser.cpp +++ b/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(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(strm, [&]() { + return invoke(vm_p, o); + }); + CATCH; if (lean_parser::is_result_exception(vm_state)) { return vm_state; diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 5ce39aa744..194ac66722 100644 --- a/tests/lean/run/check_constants.lean +++ b/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 diff --git a/tests/lean/user_notation.lean b/tests/lean/user_notation.lean index ef6566858b..193ee0cc98 100644 --- a/tests/lean/user_notation.lean +++ b/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₁ diff --git a/tests/lean/user_notation.lean.expected.out b/tests/lean/user_notation.lean.expected.out index 2b5d3b5d76..dc3ffccd8f 100644 --- a/tests/lean/user_notation.lean.expected.out +++ b/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