diff --git a/bin/version b/bin/version index 0c62199f16..ee1372d33a 100644 --- a/bin/version +++ b/bin/version @@ -1 +1 @@ -0.2.1 +0.2.2 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 5290a8e3e8..d983f06a0d 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -12,7 +12,7 @@ "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "universes" - "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" + "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "instance" "class" "section" "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw") diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index ad5c30bc30..f7cc6df3a6 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -67,7 +67,8 @@ using notation::mk_ext_lua_action; using notation::transition; using notation::action; -static pair> parse_mixfix_notation(parser & p, mixfix_kind k, bool overload) { +static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve ) +-> pair> { std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected"); optional prec; if (p.curr_is_token(get_colon_tk())) { @@ -83,34 +84,43 @@ static pair> parse_mixfix_notation(parser } if (!prec) - throw parser_error("invalid notation declaration, precedence was not provided, and it is not set for the given symbol, " + throw parser_error("invalid notation declaration, precedence was not provided, " + "and it is not set for the given symbol, " "solution: use the 'precedence' command", p.pos()); if (k == mixfix_kind::infixr && *prec == 0) throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos()); - p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected"); - auto f_pos = p.pos(); - expr f = p.parse_expr(); - check_notation_expr(f, f_pos); + expr f; + if (reserve) { + // reserve notation commands do not have a denotation + if (p.curr_is_token(get_assign_tk())) + throw parser_error("invalid reserve notation, found `:=`", p.pos()); + } else { + p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected"); + auto f_pos = p.pos(); + f = p.parse_expr(); + check_notation_expr(f, f_pos); + } char const * tks = tk.c_str(); 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), new_token); + mk_app(f, Var(1), Var(0)), overload, reserve), 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), new_token); + mk_app(f, Var(1), Var(0)), overload, reserve), 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), new_token); + mk_app(f, Var(0)), overload, reserve), 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), new_token); + mk_app(f, Var(0)), overload, reserve), new_token); } lean_unreachable(); // LCOV_EXCL_LINE } -static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, buffer & new_tokens) { - auto nt = parse_mixfix_notation(p, k, overload); +static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve, + buffer & new_tokens) { + auto nt = parse_mixfix_notation(p, k, overload, reserve); if (nt.second) new_tokens.push_back(*nt.second); return nt.first; @@ -261,12 +271,33 @@ static unsigned get_default_prec(optional const & pt, name const & return LEAN_DEFAULT_PRECEDENCE; } -static notation_entry parse_notation_core(parser & p, bool overload, buffer & new_tokens) { +/** \brief Given a parsing table a \c pt and transition \c new_trans, if \c new_trans is a + transition in \c pt, then return the successor table */ +static optional find_match(optional const & pt, transition const & new_trans) { + if (pt) { + if (auto at = pt->find(new_trans.get_token())) { + if (new_trans.get_action().is_equal(at->first)) + return optional(at->second); + } + } + return optional(); +} + +/** \brief Lift parse_table::find method to optional */ +static optional> find_next(optional const & pt, name const & tk) { + if (pt) + return pt->find(tk); + else + return optional>(); +} + +static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer & new_tokens) { buffer locals; buffer ts; parser::local_scope scope(p); bool is_nud = true; optional pt; + optional reserved_pt; if (p.curr_is_numeral()) { lean_assert(p.curr_is_numeral()); mpz num = p.get_num_val().get_numerator(); @@ -280,53 +311,96 @@ static notation_entry parse_notation_core(parser & p, bool overload, bufferfind(new_trans.get_token())) { - if (new_trans.get_action().is_equal(at->first)) { - pt = at->second; - } else { - // new notation is not compatible with existing one - pt = optional(); + if (auto at = find_next(reserved_pt, tk)) { + action const & a = at->first; + reserved_pt = at->second; + switch (a.kind()) { + case notation::action_kind::Skip: + if (!p.curr_is_quoted_symbol() && !p.curr_is_keyword() && !p.curr_is_token(get_assign_tk())) { + p.check_token_or_id_next(get_binders_tk(), + "invalid notation declaration, quoted-symbol, keyword or `:=` expected " + "(declaration prefix matches reserved notation)"); } + ts.push_back(transition(tk, a)); + break; + case notation::action_kind::Binder: + p.check_token_or_id_next(get_binders_tk(), + "invalid notation declaration, 'binder' expected " + "(declaration prefix matches reserved notation)"); + ts.push_back(transition(tk, a)); + break; + case notation::action_kind::Binders: + p.check_token_or_id_next(get_binders_tk(), + "invalid notation declaration, 'binders' expected " + "(declaration prefix matches reserved notation)"); + ts.push_back(transition(tk, a)); + break; + case notation::action_kind::Expr: case notation::action_kind::Exprs: case notation::action_kind::ScopedExpr: + case notation::action_kind::Ext: case notation::action_kind::LuaExt: { + name n = p.check_id_next("invalid notation declaration, identifier expected " + "(declaration prefix matches reserved notation)"); + expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant + expr l = mk_local(n, local_type); + p.add_local(l); + locals.push_back(l); + ts.push_back(transition(tk, a)); + break; + }} + if (p.curr_is_token(get_colon_tk())) + throw parser_error("invalid notation declaration, invalid `:` occurrence " + "(declaration prefix matches reserved notation)", p.pos()); + } else { + reserved_pt = optional(); + if (p.curr_is_token_or_id(get_binder_tk())) { + p.next(); + ts.push_back(transition(tk, mk_binder_action())); + } else if (p.curr_is_token_or_id(get_binders_tk())) { + p.next(); + ts.push_back(transition(tk, mk_binders_action())); + } else if (p.curr_is_identifier()) { + unsigned default_prec = get_default_prec(pt, tk); + name n = p.get_name_val(); + p.next(); + action a = parse_action(p, tk, default_prec, locals, new_tokens); + expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant + expr l = mk_local(n, local_type); + p.add_local(l); + locals.push_back(l); + ts.push_back(transition(tk, a)); + } else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || + p.curr_is_token(get_assign_tk()) || p.curr_is_command() || p.curr_is_eof()) { + ts.push_back(transition(tk, mk_skip_action())); } else { - // parse table does not handle this prefix - pt = optional(); + throw parser_error("invalid notation declaration, quoted-symbol, identifier, " + "'binder', 'binders' expected", p.pos()); } } + pt = find_match(pt, ts.back()); } - p.next(); - if (ts.empty()) - throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos()); - expr n = parse_notation_expr(p, locals); - return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload); + expr n; + if (reserve) { + // reserve notation commands do not have a denotation + lean_assert(p.curr_is_command() || p.curr_is_eof()); + expr dummy = mk_Prop(); // any expression without free variables will do + n = dummy; + } else { + lean_assert(p.curr_is_token(get_assign_tk())); + p.next(); + if (ts.empty()) + 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); } bool curr_is_notation_decl(parser & p) { @@ -335,28 +409,35 @@ bool curr_is_notation_decl(parser & p) { p.curr_is_token(get_postfix_tk()) || p.curr_is_token(get_prefix_tk()) || p.curr_is_token(get_notation_tk()); } -notation_entry parse_notation(parser & p, bool overload, buffer & new_tokens, bool allow_local) { +static notation_entry parse_notation(parser & p, bool overload, bool reserve, buffer & new_tokens, + bool allow_local) { flet set_allow_local(g_allow_local, allow_local); if (p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::infixl, overload, new_tokens); + return parse_mixfix_notation(p, mixfix_kind::infixl, overload, reserve, new_tokens); } else if (p.curr_is_token(get_infixr_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::infixr, overload, new_tokens); + return parse_mixfix_notation(p, mixfix_kind::infixr, overload, reserve, new_tokens); } else if (p.curr_is_token(get_postfix_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::postfix, overload, new_tokens); + return parse_mixfix_notation(p, mixfix_kind::postfix, overload, reserve, new_tokens); } else if (p.curr_is_token(get_prefix_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::prefix, overload, new_tokens); + return parse_mixfix_notation(p, mixfix_kind::prefix, overload, reserve, new_tokens); } else if (p.curr_is_token(get_notation_tk())) { p.next(); - return parse_notation_core(p, overload, new_tokens); + return parse_notation_core(p, overload, reserve, new_tokens); } else { - throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', 'postfix' or 'notation' expected", p.pos()); + throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', " + "'postfix' or 'notation' expected", p.pos()); } } +notation_entry parse_notation(parser & p, bool overload, buffer & new_tokens, bool allow_local) { + bool reserve = false; + return parse_notation(p, overload, reserve, new_tokens, allow_local); +} + static char g_reserved_chars[] = {'(', ')', ',', 0}; static void check_token(char const * tk) { @@ -375,7 +456,8 @@ static void check_token(char const * tk) { auto it = g_reserved_chars; while (*it) { if (*tk == *it) - throw exception(sstream() << "invalid token `" << tk << "`, it contains reserved character `" << *it << "`"); + throw exception(sstream() << "invalid token `" << tk + << "`, it contains reserved character `" << *it << "`"); ++it; } ++tk; @@ -393,34 +475,85 @@ static environment add_user_token(environment const & env, char const * val, uns return add_token(env, val, prec); } -static environment notation_cmd_core(parser & p, bool overload) { +static environment notation_cmd_core(parser & p, bool overload, bool reserve) { flet set_allow_local(g_allow_local, in_context(p.env())); environment env = p.env(); buffer new_tokens; - auto ne = parse_notation_core(p, overload, new_tokens); + auto ne = parse_notation_core(p, overload, reserve, new_tokens); for (auto const & te : new_tokens) env = add_user_token(env, te); env = add_notation(env, ne); return env; } -static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) { +static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve) { flet set_allow_local(g_allow_local, in_context(p.env())); - auto nt = parse_mixfix_notation(p, k, overload); + auto nt = parse_mixfix_notation(p, k, overload, reserve); environment env = p.env(); if (nt.second) env = add_user_token(env, *nt.second); env = add_notation(env, nt.first); return env; } -static environment infixl_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixl, overload); } -static environment infixr_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixr, overload); } -static environment postfix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::postfix, overload); } -static environment prefix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::prefix, overload); } -static environment notation_cmd(parser & p) { return notation_cmd_core(p, !in_context(p.env())); } -static environment infixl_cmd(parser & p) { return infixl_cmd_core(p, !in_context(p.env())); } -static environment infixr_cmd(parser & p) { return infixr_cmd_core(p, !in_context(p.env())); } -static environment postfix_cmd(parser & p) { return postfix_cmd_core(p, !in_context(p.env())); } -static environment prefix_cmd(parser & p) { return prefix_cmd_core(p, !in_context(p.env())); } + +static environment notation_cmd(parser & p) { + bool overload = !in_context(p.env()); + bool reserve = false; + return notation_cmd_core(p, overload, reserve); +} + +static environment infixl_cmd(parser & p) { + bool overload = !in_context(p.env()); + bool reserve = false; + return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve); +} + +static environment infixr_cmd(parser & p) { + bool overload = !in_context(p.env()); + bool reserve = false; + return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve); +} + +static environment postfix_cmd(parser & p) { + bool overload = !in_context(p.env()); + bool reserve = false; + return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve); +} + +static environment prefix_cmd(parser & p) { + bool overload = !in_context(p.env()); + bool reserve = false; + return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve); +} + +static environment reserve_cmd(parser & p) { + bool overload = false; + bool reserve = true; + if (in_context(p.env()) || in_section(p.env()) || get_namespace(p.env())) { + throw parser_error("invalid reserve notation, command cannot be used in contexts/sections/namespaces", + p.pos()); + } else if (p.curr_is_token(get_notation_tk())) { + p.next(); + return notation_cmd_core(p, overload, reserve); + } else if (p.curr_is_token(get_infixl_tk())) { + p.next(); + return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve); + } else if (p.curr_is_token(get_infix_tk())) { + p.next(); + return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve); + } else if (p.curr_is_token(get_infixr_tk())) { + p.next(); + return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve); + } else if (p.curr_is_token(get_prefix_tk())) { + p.next(); + return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve); + } else if (p.curr_is_token(get_postfix_tk())) { + p.next(); + return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve); + } else { + throw parser_error("invalid reserve notation, 'infix', 'infixl', 'infixr', 'prefix', " + "'postfix' or 'notation' expected", p.pos()); + } +} static environment precedence_cmd(parser & p) { std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected"); @@ -437,5 +570,6 @@ void register_notation_cmds(cmd_table & r) { add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd)); add_cmd(r, cmd_info("prefix", "declare a new prefix notation", prefix_cmd)); add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd)); + add_cmd(r, cmd_info("reserve", "reserve notation", reserve_cmd)); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 584d41d5c6..6b2caa2c82 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -377,6 +377,12 @@ void parser::check_token_next(name const & tk, char const * msg) { next(); } +void parser::check_token_or_id_next(name const & tk, char const * msg) { + if (!curr_is_token_or_id(tk)) + throw parser_error(msg, pos()); + next(); +} + name parser::check_id_next(char const * msg) { if (!curr_is_identifier()) throw parser_error(msg, pos()); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 991e46df36..cefd3e653e 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -275,6 +275,8 @@ public: bool curr_is_keyword() const { return curr() == scanner::token_kind::Keyword; } /** \brief Return true iff the current token is a keyword */ bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; } + /** \brief Return true iff the current token is EOF */ + bool curr_is_eof() const { return curr() == scanner::token_kind::Eof; } /** \brief Return true iff the current token is a keyword */ bool curr_is_quoted_symbol() const { return curr() == scanner::token_kind::QuotedSymbol; } /** \brief Return true iff the current token is a keyword named \c tk or an identifier named \c tk */ @@ -287,6 +289,7 @@ public: bool curr_is_token(name const & tk) const; /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */ void check_token_next(name const & tk, char const * msg); + void check_token_or_id_next(name const & tk, char const * msg); /** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */ name check_id_next(char const * msg); diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 86de01edcd..32332fa27e 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -24,22 +24,22 @@ notation_entry replace(notation_entry const & e, std::function(e.m_transitions); } -notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload): +notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve): m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD), - m_expr(e), m_overload(overload) { + m_expr(e), m_overload(overload), m_reserve(reserve) { new (&m_transitions) list(ts); m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); }); } @@ -48,7 +48,7 @@ notation_entry::notation_entry(notation_entry const & e, bool overload): 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_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false) { new (&m_num) mpz(val); } @@ -60,7 +60,8 @@ 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()) + if (e1.kind() != e2.kind() || e1.overload() != e2.overload() || e1.get_expr() != e2.get_expr() || + e1.reserve() != e2.reserve()) return false; if (e1.is_numeral()) return e1.get_num() == e2.get_num(); @@ -198,10 +199,14 @@ struct notation_state { parse_table m_led; num_map m_num_map; head_to_entries m_inv_map; - - notation_state() { - m_nud = get_builtin_nud_table(); - m_led = get_builtin_led_table(); + // The following two tables are used to implement `reserve notation` commands + parse_table m_reserved_nud; + parse_table m_reserved_led; + notation_state(): + m_nud(get_builtin_nud_table()), + m_led(get_builtin_led_table()), + m_reserved_nud(true), + m_reserved_led(false) { } }; @@ -218,18 +223,22 @@ struct notation_config { static void add_entry(environment const &, io_state const &, state & s, entry const & e) { buffer ts; switch (e.kind()) { - case notation_entry_kind::NuD: + case notation_entry_kind::NuD: { to_buffer(e.get_transitions(), ts); if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr())) updt_inv_map(s, *idx, e); - s.m_nud = s.m_nud.add(ts.size(), ts.data(), e.get_expr(), e.overload()); + parse_table & nud = e.reserve() ? s.m_reserved_nud : s.m_nud; + nud = nud.add(ts.size(), ts.data(), e.get_expr(), e.overload()); break; - case notation_entry_kind::LeD: + } + case notation_entry_kind::LeD: { to_buffer(e.get_transitions(), ts); if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr())) updt_inv_map(s, *idx, e); - s.m_led = s.m_led.add(ts.size(), ts.data(), e.get_expr(), e.overload()); + parse_table & led = e.reserve() ? s.m_reserved_led : s.m_led; + led = led.add(ts.size(), ts.data(), e.get_expr(), e.overload()); break; + } case notation_entry_kind::Numeral: if (!is_var(e.get_expr())) updt_inv_map(s, head_index(e.get_expr()), e); @@ -254,7 +263,7 @@ struct notation_config { if (e.is_numeral()) { s << e.get_num(); } else { - s << length(e.get_transitions()); + s << e.reserve() << length(e.get_transitions()); for (auto const & t : e.get_transitions()) s << t; } @@ -269,12 +278,13 @@ struct notation_config { return entry(val, e, overload); } else { bool is_nud = k == notation_entry_kind::NuD; + bool reserve; unsigned sz; - d >> sz; + d >> reserve >> sz; 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); + return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve); } } static optional get_fingerprint(entry const &) { @@ -292,23 +302,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) { - return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload)); + expr const & a, bool overload, bool reserve) { + return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve)); } environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, - expr const & a, bool overload) { - return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload)); + expr const & a, bool overload, bool reserve) { + return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve)); } environment add_nud_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload) { - return add_nud_notation(env, ts.size(), ts.begin(), a, overload); + bool reserve = false; + return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve); } environment add_led_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload) { - return add_led_notation(env, ts.size(), ts.begin(), a, overload); + bool reserve = false; + return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve); } parse_table const & get_nud_table(environment const & env) { @@ -319,6 +331,14 @@ parse_table const & get_led_table(environment const & env) { return notation_ext::get_state(env).m_led; } +parse_table const & get_reserved_nud_table(environment const & env) { + return notation_ext::get_state(env).m_reserved_nud; +} + +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)); } diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 1bb13db63b..b94d53a0e1 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -30,10 +30,11 @@ class notation_entry { expr m_expr; bool m_overload; bool m_safe_ascii; + bool m_reserve; public: notation_entry(); notation_entry(notation_entry const & e); - notation_entry(bool is_nud, list const & ts, expr const & e, bool overload); + 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(notation_entry const & e, bool overload); ~notation_entry(); @@ -45,6 +46,7 @@ public: expr const & get_expr() const { return m_expr; } bool overload() const { return m_overload; } bool is_safe_ascii() const { return m_safe_ascii; } + bool reserve() const { return m_reserve; } }; bool operator==(notation_entry const & e1, notation_entry const & e2); inline bool operator!=(notation_entry const & e1, notation_entry const & e2) { @@ -59,9 +61,9 @@ 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 overload = true, bool reserve = false); environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, - bool overload = true); + bool overload = true, bool reserve = false); environment add_nud_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload = true); environment add_led_notation(environment const & env, std::initializer_list const & ts, expr const & a, @@ -69,6 +71,8 @@ environment add_led_notation(environment const & env, std::initializer_list