From 20ab8feeae8971ce1116928552eeed65945ba3e1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Jun 2017 18:17:50 +0200 Subject: [PATCH] feat(init/meta/lean/parser): `pexpr` parser that does not use quoted mode --- library/init/meta/lean/parser.lean | 2 ++ src/frontends/lean/user_notation.cpp | 2 +- src/library/constants.cpp | 8 ++++---- src/library/constants.h | 2 +- src/library/constants.txt | 2 +- src/library/vm/vm_parser.cpp | 15 ++++++++++++++- tests/lean/run/check_constants.lean | 2 +- tests/lean/user_notation.lean | 7 +++---- 8 files changed, 27 insertions(+), 13 deletions(-) diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean index 0fcd76f2f0..61e75b572d 100644 --- a/library/init/meta/lean/parser.lean +++ b/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 diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp index 7ee14c1136..76710892fa 100644 --- a/src/frontends/lean/user_notation.cpp +++ b/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); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index b357111eb6..c02858c377 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 6aa4e04a89..6b3b7eea27 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 104de4dac6..e88dfe93c6 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 0e247d9f43..401cf18c48 100644 --- a/src/library/vm/vm_parser.cpp +++ b/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); } diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 05d2beb1c8..5ce39aa744 100644 --- a/tests/lean/run/check_constants.lean +++ b/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 diff --git a/tests/lean/user_notation.lean b/tests/lean/user_notation.lean index 3398ae2049..95b26cd0db 100644 --- a/tests/lean/user_notation.lean +++ b/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