feat(frontends/lean): reserve notation, closes #95

bin/version

@@ -1 +1 @@
-0.2.1
+0.2.2

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")

src/frontends/lean/notation_cmd.cpp

@@ -67,7 +67,8 @@ using notation::mk_ext_lua_action;
 using notation::transition;
 using notation::action;
 
-static pair<notation_entry, optional<token_entry>> 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<notation_entry, optional<token_entry>> {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     optional<unsigned> prec;
     if (p.curr_is_token(get_colon_tk())) {
@@ -83,34 +84,43 @@ static pair<notation_entry, optional<token_entry>> 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");
+    expr f;
-    auto f_pos = p.pos();
+    if (reserve) {
-    expr f     = p.parse_expr();
+        // reserve notation commands do not have a denotation
-    check_notation_expr(f, f_pos);
+        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<token_entry> & new_tokens) {
+static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve,
-    auto nt = parse_mixfix_notation(p, k, overload);
+                                            buffer<token_entry> & 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<parse_table> const & pt, name const &
     return LEAN_DEFAULT_PRECEDENCE;
 }
 
-static notation_entry parse_notation_core(parser & p, bool overload, buffer<token_entry> & 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<parse_table> find_match(optional<parse_table> 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<parse_table>(at->second);
+        }
+    }
+    return optional<parse_table>();
+}
+
+/** \brief Lift parse_table::find method to optional<parse_table> */
+static optional<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
+    if (pt)
+        return pt->find(tk);
+    else
+        return optional<pair<action, parse_table>>();
+}
+
+static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens) {
     buffer<expr>       locals;
     buffer<transition> ts;
     parser::local_scope scope(p);
     bool is_nud = true;
     optional<parse_table> pt;
+    optional<parse_table> 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, buffer<toke
         parse_notation_local(p, locals);
         is_nud = false;
         pt = get_led_table(p.env());
+        if (!reserve)
+            reserved_pt = get_reserved_led_table(p.env());
     } else {
         pt = get_nud_table(p.env());
+        if (!reserve)
+            reserved_pt = get_reserved_nud_table(p.env());
     }
-    while (!p.curr_is_token(get_assign_tk())) {
+    while ((!reserve && !p.curr_is_token(get_assign_tk())) ||
+           (reserve && !p.curr_is_command() && !p.curr_is_eof())) {
         name tk = parse_quoted_symbol_or_token(p, new_tokens);
-        if (p.curr_is_token_or_id(get_binder_tk())) {
+        if (auto at = find_next(reserved_pt, tk)) {
-            p.next();
+            action const & a = at->first;
-            ts.push_back(transition(tk, mk_binder_action()));
+            reserved_pt      = at->second;
-        } else if (p.curr_is_token_or_id(get_binders_tk())) {
+            switch (a.kind()) {
-            p.next();
+            case notation::action_kind::Skip:
-            ts.push_back(transition(tk, mk_binders_action()));
+                if (!p.curr_is_quoted_symbol() && !p.curr_is_keyword() && !p.curr_is_token(get_assign_tk())) {
-        } else if (p.curr_is_identifier()) {
+                    p.check_token_or_id_next(get_binders_tk(),
-            unsigned default_prec = get_default_prec(pt, tk);
+                                             "invalid notation declaration, quoted-symbol, keyword or `:=` expected "
-            name n   = p.get_name_val();
+                                             "(declaration prefix matches reserved notation)");
-            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())) {
-            ts.push_back(transition(tk, mk_skip_action()));
-        } else {
-            throw parser_error("invalid notation declaration, quoted-symbol, identifier, 'binder', 'binders' expected", p.pos());
-        }
-        if (pt) {
-            // new notation is still compatible with the existing one
-            transition const & new_trans = ts.back();
-            if (auto at = pt->find(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<parse_table>();
                 }
+                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<parse_table>();
+            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
+                throw parser_error("invalid notation declaration, quoted-symbol, identifier, "
-                pt = optional<parse_table>();
+                                   "'binder', 'binders' expected", p.pos());
             }
         }
+        pt = find_match(pt, ts.back());
     }
-    p.next();
+    expr n;
-    if (ts.empty())
+    if (reserve) {
-        throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
+        // reserve notation commands do not have a denotation
-    expr n = parse_notation_expr(p, locals);
+        lean_assert(p.curr_is_command() || p.curr_is_eof());
-    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload);
+        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<token_entry> & new_tokens, bool allow_local) {
+static notation_entry parse_notation(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens,
+                                     bool allow_local) {
     flet<bool> 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<token_entry> & 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<bool> set_allow_local(g_allow_local, in_context(p.env()));
     environment env = p.env();
     buffer<token_entry> 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<bool> 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 notation_cmd(parser & p) {
-static environment postfix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::postfix, overload); }
+    bool overload = !in_context(p.env());
-static environment prefix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::prefix, overload); }
+    bool reserve  = false;
-static environment notation_cmd(parser & p) { return notation_cmd_core(p, !in_context(p.env())); }
+    return notation_cmd_core(p, overload, reserve);
-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 infixl_cmd(parser & p) {
-static environment prefix_cmd(parser & p) { return prefix_cmd_core(p, !in_context(p.env())); }
+    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));
 }
 }

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());

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);

src/frontends/lean/parser_config.cpp

@@ -24,22 +24,22 @@ notation_entry replace(notation_entry const & e, std::function<expr(expr const &
     else
         return notation_entry(e.is_nud(),
                               map(e.get_transitions(), [&](transition const & t) { return notation::replace(t, f); }),
-                              f(e.get_expr()),
+                              f(e.get_expr()), e.overload(), e.reserve());
-                              e.overload());
 }
 
 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_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) {
     if (is_numeral())
         new (&m_num) mpz(e.m_num);
     else
         new (&m_transitions) list<transition>(e.m_transitions);
 }
 
-notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload):
+notation_entry::notation_entry(bool is_nud, list<transition> 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<transition>(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;
-
+    // The following two tables are used to implement `reserve notation` commands
-    notation_state() {
+    parse_table      m_reserved_nud;
-        m_nud = get_builtin_nud_table();
+    parse_table      m_reserved_led;
-        m_led = get_builtin_led_table();
+    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<transition> 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<transition> 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<unsigned> 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) {
+                             expr const & a, bool overload, bool reserve) {
-    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload));
+    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) {
+                             expr const & a, bool overload, bool reserve) {
-    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload));
+    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<notation::transition> 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<notation::transition> 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));
 }

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<transition> const & ts, expr const & e, bool overload);
+    notation_entry(bool is_nud, list<transition> 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<notation::transition> const & ts, expr const & a,
                              bool overload = true);
 environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
@@ -69,6 +71,8 @@ environment add_led_notation(environment const & env, std::initializer_list<nota
 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);
+parse_table const & get_reserved_nud_table(environment const & env);
+parse_table const & get_reserved_led_table(environment const & env);
 cmd_table const & get_cmd_table(environment const & env);
 /** \brief Force notation from namespace \c n to shadow any existing notation */
 environment overwrite_notation(environment const & env, name const & n);

src/frontends/lean/token_table.cpp

@@ -84,7 +84,7 @@ void init_token_table(token_table & t) {
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible",
          "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import",
          "inductive", "record", "renaming", "extends", "structure", "module", "universe", "universes",
-         "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
+         "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "include", "omit", "#erase_cache", nullptr};

tests/lean/run/reserve.lean

@@ -0,0 +1,10 @@
+import logic
+
+reserve infix `=?=`:50
+reserve infixr `&&&`:25
+
+notation a `=?=` b := eq a b
+notation a `&&&` b := and a b
+
+set_option pp.notation false
+check λ a b : num, a =?= b &&& b =?= a