From 85d0521d484dd6cd4757ba7bed5175c426c1d9bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Nov 2014 21:34:05 -0800 Subject: [PATCH] feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305 --- library/type.lean | 4 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/notation_cmd.cpp | 35 +++++++++++----- src/frontends/lean/parser_config.cpp | 49 ++++++++++++----------- src/frontends/lean/parser_config.h | 16 ++++---- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + tests/lean/parsing_only.lean | 9 +++++ tests/lean/parsing_only.lean.expected.out | 3 ++ 10 files changed, 80 insertions(+), 45 deletions(-) create mode 100644 tests/lean/parsing_only.lean create mode 100644 tests/lean/parsing_only.lean.expected.out diff --git a/library/type.lean b/library/type.lean index 52b45248d..bc25cc320 100644 --- a/library/type.lean +++ b/library/type.lean @@ -3,8 +3,8 @@ -- Authors: Leonardo de Moura notation `Prop` := Type.{0} -notation `Type'` := Type.{_+1} -notation `Type₊` := Type.{_+1} +notation [parsing-only] `Type'` := Type.{_+1} +notation [parsing-only] `Type₊` := Type.{_+1} notation `Type₁` := Type.{1} notation `Type₂` := Type.{2} notation `Type₃` := Type.{3} diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 830494b44..35078460d 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -115,7 +115,7 @@ ;; place holder (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers - (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" + (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]" "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face) (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 82b05e367..4727acb63 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -78,8 +78,21 @@ void check_not_forbidden(char const * tk) { } } +struct notation_modifiers { + bool m_parse_only; + notation_modifiers():m_parse_only(false) {} + void parse(parser & p) { + if (p.curr_is_token(get_parsing_only_tk())) { + p.next(); + m_parse_only = true; + } + } +}; + static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve) -> pair> { + notation_modifiers mod; + mod.parse(p); std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected"); char const * tks = tk.c_str(); check_not_forbidden(tks); @@ -156,16 +169,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool switch (k) { case mixfix_kind::infixl: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - dummy, overload, reserve), new_token); + dummy, overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::infixr: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))), - dummy, overload, reserve), new_token); + dummy, overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::postfix: return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), - dummy, overload, reserve), new_token); + dummy, overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::prefix: return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), - dummy, overload, reserve), new_token); + dummy, overload, reserve, mod.m_parse_only), new_token); } } else { p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected"); @@ -175,16 +188,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool switch (k) { case mixfix_kind::infixl: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(1), Var(0)), overload, reserve), new_token); + mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::infixr: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))), - mk_app(f, Var(1), Var(0)), overload, reserve), new_token); + mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::postfix: return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), - mk_app(f, Var(0)), overload, reserve), new_token); + mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token); case mixfix_kind::prefix: return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(0)), overload, reserve), new_token); + mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token); } } lean_unreachable(); // LCOV_EXCL_LINE @@ -372,6 +385,8 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv bool is_nud = true; optional pt; optional reserved_pt; + notation_modifiers mod; + mod.parse(p); if (p.curr_is_numeral()) { lean_assert(p.curr_is_numeral()); mpz num = p.get_num_val().get_numerator(); @@ -380,7 +395,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv auto e_pos = p.pos(); expr e = p.parse_expr(); check_notation_expr(e, e_pos); - return notation_entry(num, e, overload); + return notation_entry(num, e, overload, mod.m_parse_only); } else if (p.curr_is_identifier()) { parse_notation_local(p, locals); is_nud = false; @@ -474,7 +489,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos()); n = parse_notation_expr(p, locals); } - return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve); + return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, mod.m_parse_only); } bool curr_is_notation_decl(parser & p) { diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 32332fa27..f56b1e681 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -20,26 +20,26 @@ using notation::action_kind; notation_entry replace(notation_entry const & e, std::function const & f) { if (e.is_numeral()) - return notation_entry(e.get_num(), f(e.get_expr()), e.overload()); + return notation_entry(e.get_num(), f(e.get_expr()), e.overload(), e.parse_only()); else return notation_entry(e.is_nud(), map(e.get_transitions(), [&](transition const & t) { return notation::replace(t, f); }), - f(e.get_expr()), e.overload(), e.reserve()); + f(e.get_expr()), e.overload(), e.reserve(), e.parse_only()); } notation_entry::notation_entry():m_kind(notation_entry_kind::NuD) {} notation_entry::notation_entry(notation_entry const & e): m_kind(e.m_kind), m_expr(e.m_expr), m_overload(e.m_overload), - m_safe_ascii(e.m_safe_ascii), m_reserve(e.m_reserve) { + m_safe_ascii(e.m_safe_ascii), m_reserve(e.m_reserve), m_parse_only(e.m_parse_only) { if (is_numeral()) new (&m_num) mpz(e.m_num); else new (&m_transitions) list(e.m_transitions); } -notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve): +notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve, bool parse_only): m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD), - m_expr(e), m_overload(overload), m_reserve(reserve) { + m_expr(e), m_overload(overload), m_reserve(reserve), m_parse_only(parse_only) { new (&m_transitions) list(ts); m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); }); } @@ -47,8 +47,8 @@ notation_entry::notation_entry(notation_entry const & e, bool overload): notation_entry(e) { m_overload = overload; } -notation_entry::notation_entry(mpz const & val, expr const & e, bool overload): - m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false) { +notation_entry::notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only): + m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false), m_parse_only(parse_only) { new (&m_num) mpz(val); } @@ -61,7 +61,7 @@ notation_entry::~notation_entry() { bool operator==(notation_entry const & e1, notation_entry const & e2) { if (e1.kind() != e2.kind() || e1.overload() != e2.overload() || e1.get_expr() != e2.get_expr() || - e1.reserve() != e2.reserve()) + e1.reserve() != e2.reserve() || e1.parse_only() != e2.parse_only()) return false; if (e1.is_numeral()) return e1.get_num() == e2.get_num(); @@ -217,7 +217,8 @@ struct notation_config { static std::string * g_key; static void updt_inv_map(state & s, head_index const & idx, entry const & e) { - s.m_inv_map.insert(idx, e); + if (!e.parse_only()) + s.m_inv_map.insert(idx, e); } static void add_entry(environment const &, io_state const &, state & s, entry const & e) { @@ -259,7 +260,7 @@ struct notation_config { return *g_key; } static void write_entry(serializer & s, entry const & e) { - s << static_cast(e.kind()) << e.overload() << e.get_expr(); + s << static_cast(e.kind()) << e.overload() << e.parse_only() << e.get_expr(); if (e.is_numeral()) { s << e.get_num(); } else { @@ -270,12 +271,12 @@ struct notation_config { } static entry read_entry(deserializer & d) { notation_entry_kind k = static_cast(d.read_char()); - bool overload; expr e; - d >> overload >> e; + bool overload, parse_only; expr e; + d >> overload >> parse_only >> e; if (k == notation_entry_kind::Numeral) { mpz val; d >> val; - return entry(val, e, overload); + return entry(val, e, overload, parse_only); } else { bool is_nud = k == notation_entry_kind::NuD; bool reserve; @@ -284,7 +285,7 @@ struct notation_config { buffer ts; for (unsigned i = 0; i < sz; i++) ts.push_back(read_transition(d)); - return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve); + return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve, parse_only); } } static optional get_fingerprint(entry const &) { @@ -302,25 +303,25 @@ environment add_notation(environment const & env, notation_entry const & e) { } environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, - expr const & a, bool overload, bool reserve) { - return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve)); + expr const & a, bool overload, bool reserve, bool parse_only) { + return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve, parse_only)); } environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, - expr const & a, bool overload, bool reserve) { - return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve)); + expr const & a, bool overload, bool reserve, bool parse_only) { + return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve, parse_only)); } environment add_nud_notation(environment const & env, std::initializer_list const & ts, - expr const & a, bool overload) { + expr const & a, bool overload, bool parse_only) { bool reserve = false; - return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve); + return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only); } environment add_led_notation(environment const & env, std::initializer_list const & ts, - expr const & a, bool overload) { + expr const & a, bool overload, bool parse_only) { bool reserve = false; - return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve); + return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only); } parse_table const & get_nud_table(environment const & env) { @@ -339,8 +340,8 @@ parse_table const & get_reserved_led_table(environment const & env) { return notation_ext::get_state(env).m_reserved_led; } -environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload) { - return add_notation(env, notation_entry(n, e, overload)); +environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload, bool parse_only) { + return add_notation(env, notation_entry(n, e, overload, parse_only)); } list get_mpz_notation(environment const & env, mpz const & n) { diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index b94d53a0e..883edd0eb 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -31,11 +31,12 @@ class notation_entry { bool m_overload; bool m_safe_ascii; bool m_reserve; + bool m_parse_only; public: notation_entry(); notation_entry(notation_entry const & e); - notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve); - notation_entry(mpz const & val, expr const & e, bool overload); + notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve, bool parse_only); + notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only); notation_entry(notation_entry const & e, bool overload); ~notation_entry(); notation_entry_kind kind() const { return m_kind; } @@ -47,6 +48,7 @@ public: bool overload() const { return m_overload; } bool is_safe_ascii() const { return m_safe_ascii; } bool reserve() const { return m_reserve; } + bool parse_only() const { return m_parse_only; } }; bool operator==(notation_entry const & e1, notation_entry const & e2); inline bool operator!=(notation_entry const & e1, notation_entry const & e2) { @@ -61,13 +63,13 @@ environment add_notation(environment const & env, notation_entry const & e); environment add_token(environment const & env, char const * val, unsigned prec); environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, - bool overload = true, bool reserve = false); + bool overload = true, bool reserve = false, bool parse_only = false); environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, - bool overload = true, bool reserve = false); + bool overload = true, bool reserve = false, bool parse_only = false); environment add_nud_notation(environment const & env, std::initializer_list const & ts, expr const & a, - bool overload = true); + bool overload = true, bool parse_only = false); environment add_led_notation(environment const & env, std::initializer_list const & ts, expr const & a, - bool overload = true); + bool overload = true, bool parse_only = false); token_table const & get_token_table(environment const & env); parse_table const & get_nud_table(environment const & env); parse_table const & get_led_table(environment const & env); @@ -78,7 +80,7 @@ cmd_table const & get_cmd_table(environment const & env); environment overwrite_notation(environment const & env, name const & n); /** \brief Add \c n as notation for \c e */ -environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true); +environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true, bool parse_only = false); /** \brief Return the additional interpretations for \c n in the current environment. \remark It does not include the default one based on the \c num inductive datatype. diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 057728574..66bd0caf6 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -81,7 +81,7 @@ void init_token_table(token_table & t) { char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion", "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", - "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible", + "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible", "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import", "inductive", "record", "structure", "module", "universe", "universes", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index c41670ccd..1d379c278 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -74,6 +74,7 @@ static name * g_instance = nullptr; static name * g_priority = nullptr; static name * g_coercion = nullptr; static name * g_reducible = nullptr; +static name * g_parsing_only = nullptr; static name * g_with = nullptr; static name * g_class = nullptr; static name * g_prev = nullptr; @@ -161,6 +162,7 @@ void initialize_tokens() { g_priority = new name("[priority"); g_coercion = new name("[coercion]"); g_reducible = new name("[reducible]"); + g_parsing_only = new name("[parsing-only]"); g_with = new name("with"); g_class = new name("[class]"); g_prev = new name("prev"); @@ -212,6 +214,7 @@ void finalize_tokens() { delete g_priority; delete g_coercion; delete g_reducible; + delete g_parsing_only; delete g_in; delete g_assign; delete g_visible; @@ -336,6 +339,7 @@ name const & get_instance_tk() { return *g_instance; } name const & get_priority_tk() { return *g_priority; } name const & get_coercion_tk() { return *g_coercion; } name const & get_reducible_tk() { return *g_reducible; } +name const & get_parsing_only_tk() { return *g_parsing_only; } name const & get_class_tk() { return *g_class; } name const & get_with_tk() { return *g_with; } name const & get_prev_tk() { return *g_prev; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 469468f7d..f79d9b8a6 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -76,6 +76,7 @@ name const & get_instance_tk(); name const & get_priority_tk(); name const & get_coercion_tk(); name const & get_reducible_tk(); +name const & get_parsing_only_tk(); name const & get_class_tk(); name const & get_with_tk(); name const & get_prev_tk(); diff --git a/tests/lean/parsing_only.lean b/tests/lean/parsing_only.lean new file mode 100644 index 000000000..b15253be2 --- /dev/null +++ b/tests/lean/parsing_only.lean @@ -0,0 +1,9 @@ +import logic + +constant f : num → num +constant g : num → num +notation a `+++` := f a +notation [parsing-only] a `***` := g a +check 10 +++ +check 10 *** +check Type.{8} -- Type₊ should not be used diff --git a/tests/lean/parsing_only.lean.expected.out b/tests/lean/parsing_only.lean.expected.out new file mode 100644 index 000000000..2df76179f --- /dev/null +++ b/tests/lean/parsing_only.lean.expected.out @@ -0,0 +1,3 @@ +10 +++ : num +g 10 : num +Type : Type