feat(frontends/lean): allow user to assign priorities to notation declarations

src/frontends/lean/builtin_cmds.cpp

@@ -134,7 +134,7 @@ static bool print_parse_table(parser & p, parse_table const & t, bool nud, buffe
     os = os.update(get_pp_preterm_name(), true);
     ios.set_options(os);
     optional<token_table> tt(get_token_table(p.env()));
-    t.for_each([&](unsigned num, notation::transition const * ts, list<expr> const & overloads) {
+    t.for_each([&](unsigned num, notation::transition const * ts, list<pair<unsigned, expr>> const & overloads) {
             if (uses_some_token(num, ts, tokens)) {
                 found = true;
                 io_state_stream out = regular(p.env(), ios);

src/frontends/lean/notation_cmd.cpp

@@ -118,7 +118,8 @@ static token_entry mk_token_entry(std::string const & tk, unsigned prec, notatio
     return mk_token_entry(tk, prec, grp != notation_entry_group::Tactic);
 }
 
-static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only)
+static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only,
+                                  unsigned priority)
 -> pair<notation_entry, optional<token_entry>> {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     char const * tks = tk.c_str();
@@ -210,16 +211,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
         switch (k) {
         case mixfix_kind::infixl:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, grp, parse_only), new_token);
+                                          dummy, overload, priority, grp, parse_only), new_token);
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, grp, parse_only), new_token);
+                                          dummy, overload, priority, grp, parse_only), new_token);
         case mixfix_kind::postfix:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                          dummy, overload, grp, parse_only), new_token);
+                                          dummy, overload, priority, grp, parse_only), new_token);
         case mixfix_kind::prefix:
             return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, grp, parse_only), new_token);
+                                          dummy, overload, priority, grp, parse_only), new_token);
         }
     } else {
         p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
@@ -231,25 +232,25 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
 #if defined(__GNUC__) && !defined(__CLANG__)
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, priority, grp, parse_only), new_token);
 #endif
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, priority, grp, 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, grp, parse_only), new_token);
+                                          mk_app(f, Var(0)), overload, priority, grp, 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, grp, parse_only), new_token);
+                                          mk_app(f, Var(0)), overload, priority, grp, parse_only), new_token);
         }
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp,
-                                            buffer<token_entry> & new_tokens, bool parse_only) {
+                                            buffer<token_entry> & new_tokens, bool parse_only, unsigned priority) {
-    auto nt = parse_mixfix_notation(p, k, overload, grp, parse_only);
+    auto nt = parse_mixfix_notation(p, k, overload, grp, parse_only, priority);
     if (nt.second)
         new_tokens.push_back(*nt.second);
     return nt.first;
@@ -438,7 +439,8 @@ static unsigned parse_binders_rbp(parser & p) {
     }
 }
 
-static notation_entry parse_notation_core(parser & p, bool overload, notation_entry_group grp, buffer<token_entry> & new_tokens, bool parse_only) {
+static notation_entry parse_notation_core(parser & p, bool overload, notation_entry_group grp, buffer<token_entry> & new_tokens, bool parse_only,
+                                          unsigned priority) {
     buffer<expr>       locals;
     buffer<transition> ts;
     parser::local_scope scope(p);
@@ -555,7 +557,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
             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, grp, parse_only);
+    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, priority, grp, parse_only);
 }
 
 bool curr_is_notation_decl(parser & p) {
@@ -566,23 +568,24 @@ bool curr_is_notation_decl(parser & p) {
 
 static notation_entry parse_notation(parser & p, bool overload, notation_entry_group grp, buffer<token_entry> & new_tokens,
                                      bool allow_local) {
-    bool parse_only = false;
+    bool parse_only   = false;
+    unsigned priority = LEAN_DEFAULT_NOTATION_PRIORITY;
     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, grp, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::infixl, overload, grp, new_tokens, parse_only, priority);
     } else if (p.curr_is_token(get_infixr_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::infixr, overload, grp, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::infixr, overload, grp, new_tokens, parse_only, priority);
     } else if (p.curr_is_token(get_postfix_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::postfix, overload, grp, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::postfix, overload, grp, new_tokens, parse_only, priority);
     } else if (p.curr_is_token(get_prefix_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::prefix, overload, grp, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::prefix, overload, grp, new_tokens, parse_only, priority);
     } else if (p.curr_is_token(get_notation_tk())) {
         p.next();
-        return parse_notation_core(p, overload, grp, new_tokens, parse_only);
+        return parse_notation_core(p, overload, grp, new_tokens, parse_only, priority);
     } else {
         throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', "
                            "'postfix' or 'notation' expected", p.pos());
@@ -632,13 +635,16 @@ static environment add_user_token(environment const & env, char const * val, uns
 }
 
 struct notation_modifiers {
-    bool m_parse_only;
+    bool     m_parse_only;
-    notation_modifiers():m_parse_only(false) {}
+    unsigned m_priority;
+    notation_modifiers():m_parse_only(false), m_priority(LEAN_DEFAULT_NOTATION_PRIORITY) {}
     void parse(parser & p) {
         while (true) {
             if (p.curr_is_token(get_parsing_only_tk())) {
                 p.next();
                 m_parse_only = true;
+            } else if (auto prio = parse_priority(p)) {
+                m_priority = *prio;
             } else {
                 return;
             }
@@ -652,7 +658,7 @@ static environment notation_cmd_core(parser & p, bool overload, notation_entry_g
     flet<bool> set_allow_local(g_allow_local, !persistent);
     environment env = p.env();
     buffer<token_entry> new_tokens;
-    auto ne = parse_notation_core(p, overload, grp, new_tokens, mods.m_parse_only);
+    auto ne = parse_notation_core(p, overload, grp, new_tokens, mods.m_parse_only, mods.m_priority);
     for (auto const & te : new_tokens)
         env = add_user_token(env, te, persistent);
     env = add_notation(env, ne, persistent);
@@ -663,7 +669,7 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, notation
     notation_modifiers mods;
     mods.parse(p);
     flet<bool> set_allow_local(g_allow_local, !persistent);
-    auto nt = parse_mixfix_notation(p, k, overload, grp, mods.m_parse_only);
+    auto nt = parse_mixfix_notation(p, k, overload, grp, mods.m_parse_only, mods.m_priority);
     environment env = p.env();
     if (nt.second)
         env = add_user_token(env, *nt.second, persistent);

src/frontends/lean/parse_table.cpp

@@ -302,7 +302,7 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
 
 struct parse_table::cell {
     bool                                m_nud;
-    list<expr>                          m_accept;
+    list<pair<unsigned, expr>>          m_accept;
     name_map<pair<action, parse_table>> m_children;
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc() { delete this; }
@@ -325,7 +325,7 @@ optional<pair<action, parse_table>> parse_table::find(name const & tk) const {
         return optional<pair<action, parse_table>>();
 }
 
-list<expr> const & parse_table::is_accepting() const {
+list<pair<unsigned, expr>> const & parse_table::is_accepting() const {
     return m_ptr->m_accept;
 }
 
@@ -357,13 +357,26 @@ static void validate_transitions(bool nud, unsigned num, transition const * ts,
         throw exception("invalid notation declaration, expression template has more free variables than arguments");
 }
 
-parse_table parse_table::add_core(unsigned num, transition const * ts, expr const & a, bool overload) const {
+static list<pair<unsigned, expr>> insert(list<pair<unsigned, expr>> const & l, unsigned priority, expr const & a) {
+    if (!l) {
+        return to_list(mk_pair(priority, a));
+    } else if (priority <= head(l).first) {
+        return cons(mk_pair(priority, a), l);
+    } else {
+        return cons(head(l), insert(tail(l), priority, a));
+    }
+}
+
+parse_table parse_table::add_core(unsigned num, transition const * ts, expr const & a,
+                                  unsigned priority, bool overload) const {
     parse_table r(new cell(*m_ptr));
     if (num == 0) {
-        if (!overload)
+        if (!overload) {
-            r.m_ptr->m_accept = to_list(a);
+            r.m_ptr->m_accept = to_list(mk_pair(priority, a));
-        else
+        } else {
-            r.m_ptr->m_accept = cons(a, remove(r.m_ptr->m_accept, a));
+            auto new_accept   = filter(r.m_ptr->m_accept, [&](pair<unsigned, expr> const & p) { return p.second != a; });
+            r.m_ptr->m_accept = insert(new_accept, priority, a);
+        }
     } else {
         auto * it = r.m_ptr->m_children.find(ts->get_token());
         parse_table new_child;
@@ -371,12 +384,12 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
             action const & act        = it->first;
             parse_table const & child = it->second;
             if (act.is_equal(ts->get_action())) {
-                new_child = child.add_core(num-1, ts+1, a, overload);
+                new_child = child.add_core(num-1, ts+1, a, priority, overload);
             } else {
-                new_child = parse_table().add_core(num-1, ts+1, a, overload);
+                new_child = parse_table().add_core(num-1, ts+1, a, priority, overload);
             }
         } else {
-            new_child = parse_table().add_core(num-1, ts+1, a, overload);
+            new_child = parse_table().add_core(num-1, ts+1, a, priority, overload);
         }
         r.m_ptr->m_children.insert(ts->get_token(), mk_pair(ts->get_action(), new_child));
     }
@@ -445,14 +458,15 @@ optional<head_index> get_head_index(unsigned num, transition const * ts, expr co
     return optional<head_index>();
 }
 
-parse_table parse_table::add(unsigned num, transition const * ts, expr const & a, bool overload) const {
+parse_table parse_table::add(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload) const {
     expr new_a = annotate_macro_subterms(a);
     validate_transitions(is_nud(), num, ts, new_a);
-    return add_core(num, ts, new_a, overload);
+    return add_core(num, ts, new_a, priority, overload);
 }
 
 void parse_table::for_each(buffer<transition> & ts,
-                           std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const {
+                           std::function<void(unsigned, transition const *,
+                                              list<pair<unsigned, expr>> const &)> const & fn) const {
     if (!is_nil(m_ptr->m_accept))
         fn(ts.size(), ts.data(), m_ptr->m_accept);
     m_ptr->m_children.for_each([&](name const & k, pair<action, parse_table> const & p) {
@@ -462,7 +476,8 @@ void parse_table::for_each(buffer<transition> & ts,
         });
 }
 
-void parse_table::for_each(std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const {
+void parse_table::for_each(std::function<void(unsigned, transition const *,
+                                              list<pair<unsigned, expr>> const &)> const & fn) const {
     buffer<transition> tmp;
     for_each(tmp, fn);
 }
@@ -471,16 +486,17 @@ parse_table parse_table::merge(parse_table const & s, bool overload) const {
     if (is_nud() != s.is_nud())
         throw exception("invalid parse table merge, tables have different kinds");
     parse_table r(*this);
-    s.for_each([&](unsigned num, transition const * ts, list<expr> const & accept) {
+    s.for_each([&](unsigned num, transition const * ts, list<pair<unsigned, expr>> const & accept) {
-            for (expr const & a : accept)
+            for (pair<unsigned, expr> const & p : accept) {
-                r = r.add(num, ts, a, overload);
+                r = r.add(num, ts, p.second, p.first, overload);
+            }
         });
     return r;
 }
 
 bool parse_table::is_nud() const { return m_ptr->m_nud; }
 
-void display(io_state_stream & out, unsigned num, transition const * ts, list<expr> const & es, bool nud,
+void display(io_state_stream & out, unsigned num, transition const * ts, list<pair<unsigned, expr>> const & es, bool nud,
              optional<token_table> const & tt) {
     if (!nud)
         out << "_ ";
@@ -505,21 +521,24 @@ void display(io_state_stream & out, unsigned num, transition const * ts, list<ex
     }
     out << " :=";
     if (length(es) == 1) {
-        out << " " << head(es) << "\n";
+        out << " " << head(es).second << "\n";
     } else {
-        buffer<expr> tmp;
+        buffer<pair<unsigned, expr>> tmp;
         to_buffer(es, tmp);
         out << "\n";
         unsigned i = tmp.size();
         while (i > 0) {
             --i;
-            out << "  | " << tmp[i] << "\n";
+            out << "  | ";
+            if (tmp[i].first != LEAN_DEFAULT_NOTATION_PRIORITY)
+                out << "[priority " << tmp[i].first << "] ";
+            out << tmp[i].second << "\n";
         }
     }
 }
 
 void parse_table::display(io_state_stream & out, optional<token_table> const & tt) const {
-    for_each([&](unsigned num, transition const * ts, list<expr> const & es) {
+    for_each([&](unsigned num, transition const * ts, list<pair<unsigned, expr>> const & es) {
             ::lean::notation::display(out, num, ts, es, is_nud(), tt);
         });
 }
@@ -683,7 +702,8 @@ static int add(lua_State * L) {
         }
     }
     bool overload = (nargs <= 3) || lua_toboolean(L, 4);
-    return push_parse_table(L, to_parse_table(L, 1).add(ts.size(), ts.data(), to_expr(L, 3), overload));
+    return push_parse_table(L, to_parse_table(L, 1).add(ts.size(), ts.data(), to_expr(L, 3), LEAN_DEFAULT_NOTATION_PRIORITY,
+                                                        overload));
 }
 
 static int merge(lua_State * L) {
@@ -703,34 +723,6 @@ static int find(lua_State * L) {
     }
 }
 
-static int is_accepting(lua_State * L) {
-    list<expr> const & l = to_parse_table(L, 1).is_accepting();
-    if (is_nil(l))
-        return push_nil(L);
-    else
-        return push_list_expr(L, l);
-}
-
-static int for_each(lua_State * L) {
-    parse_table const & t = to_parse_table(L, 1);
-    luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
-    t.for_each([&](unsigned num, transition const * ts, list<expr> const & as) {
-            lua_pushvalue(L, 2);
-            lua_newtable(L);
-            for (unsigned i = 0; i < num; i++) {
-                lua_newtable(L);
-                push_name(L, ts[i].get_token());
-                lua_rawseti(L, -2, 1);
-                push_notation_action(L, ts[i].get_action());
-                lua_rawseti(L, -2, 2);
-                lua_rawseti(L, -2, i+1);
-            }
-            push_list_expr(L, as);
-            pcall(L, 2, 0, 0);
-        });
-    return 0;
-}
-
 static int is_nud(lua_State * L) {
     return push_boolean(L, to_parse_table(L, 1).is_nud());
 }
@@ -740,8 +732,6 @@ static const struct luaL_Reg parse_table_m[] = {
     {"add",              safe_function<add>},
     {"merge",            safe_function<merge>},
     {"find",             safe_function<find>},
-    {"is_accepting",     safe_function<is_accepting>},
-    {"for_each",         safe_function<for_each>},
     {"is_nud",           safe_function<is_nud>},
     {0, 0}
 };

src/frontends/lean/parse_table.h

@@ -14,6 +14,10 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/parser_pos_provider.h"
 
+#ifndef LEAN_DEFAULT_NOTATION_PRIORITY
+#define LEAN_DEFAULT_NOTATION_PRIORITY 1000
+#endif
+
 namespace lean {
 class parser;
 class io_state_stream;
@@ -125,7 +129,7 @@ inline bool operator!=(transition const & t1, transition const & t2) {
 /** \brief Apply \c f to expressions embedded in the given transition */
 transition replace(transition const & t, std::function<expr(expr const &)> const & f);
 
-void display(io_state_stream & out, unsigned num, transition const * ts, list<expr> const & es, bool nud,
+void display(io_state_stream & out, unsigned num, transition const * ts, list<pair<unsigned, expr>> const & es, bool nud,
              optional<token_table> const & tt);
 
 /**
@@ -136,8 +140,9 @@ class parse_table {
     struct cell;
     cell * m_ptr;
     explicit parse_table(cell * c);
-    parse_table add_core(unsigned num, transition const * ts, expr const & a, bool overload) const;
+    parse_table add_core(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload) const;
-    void for_each(buffer<transition> & ts, std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const;
+    void for_each(buffer<transition> & ts, std::function<void(unsigned, transition const *,
+                                                              list<pair<unsigned, expr>> const &)> const & fn) const;
 public:
     parse_table(bool nud = true);
     parse_table(parse_table const & s);
@@ -147,14 +152,14 @@ public:
     parse_table & operator=(parse_table&& n);
 
     bool is_nud() const;
-    parse_table add(unsigned num, transition const * ts, expr const & a, bool overload) const;
+    parse_table add(unsigned num, transition const * ts, expr const & a, unsigned priority, bool overload) const;
     parse_table add(std::initializer_list<transition> const & ts, expr const & a) const {
-        return add(ts.size(), ts.begin(), a, true);
+        return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true);
     }
     parse_table merge(parse_table const & s, bool overload) const;
     optional<pair<action, parse_table>> find(name const & tk) const;
-    list<expr> const & is_accepting() const;
+    list<pair<unsigned, expr>> const & is_accepting() const;
-    void for_each(std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const;
+    void for_each(std::function<void(unsigned, transition const *, list<pair<unsigned, expr>> const &)> const & fn) const;
 
     void display(io_state_stream & out, optional<token_table> const & tk) const;
 };

src/frontends/lean/parser.cpp

@@ -1122,7 +1122,7 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
 
         t = r->second;
     }
-    list<expr> const & as = t.is_accepting();
+    list<pair<unsigned, expr>> const & as = t.is_accepting();
     save_overload_notation(as, p);
     if (is_nil(as)) {
         if (p == pos())
@@ -1131,8 +1131,8 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
             throw parser_error(sstream() << "invalid expression starting at " << p.first << ":" << p.second, pos());
     }
     buffer<expr> cs;
-    for (expr const & a : as) {
+    for (pair<unsigned, expr> const & a : as) {
-        expr r = copy_with_new_pos(a, p);
+        expr r = copy_with_new_pos(a.second, p);
         if (args.empty()) {
             // Notation does not have arguments. Thus, the info-manager should treat is as a single thing.
             r = mk_notation_info(r, r.get_tag());
@@ -1913,7 +1913,12 @@ void parser::save_overload_notation(list<expr> const & as, pos_info const & p) {
         return;
     m_info_manager->add_overload_notation_info(p.first, p.second, as);
 }
-
+void parser::save_overload_notation(list<pair<unsigned, expr>> const & as, pos_info const & p) {
+    if (!m_info_manager || length(as) <= 1)
+        return;
+    list<expr> new_as = map2<expr>(as, [](pair<unsigned, expr> const & p) { return p.second; });
+    save_overload_notation(new_as, p);
+}
 void parser::save_identifier_info(pos_info const & p, name const & full_id) {
     if (!m_info_manager)
         return;

src/frontends/lean/parser.h

@@ -224,6 +224,7 @@ class parser {
     void save_snapshot();
     void save_overload(expr const & e);
     void save_overload_notation(list<expr> const & as, pos_info const & p);
+    void save_overload_notation(list<pair<unsigned, expr>> const & as, pos_info const & p);
     void save_type_info(expr const & e);
     void save_pre_info_data();
     void save_identifier_info(pos_info const & p, name const & full_id);

src/frontends/lean/parser_config.cpp

@@ -25,13 +25,14 @@ 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()), e.overload(), e.group(), e.parse_only());
+                              f(e.get_expr()), e.overload(), e.priority(), e.group(), 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_group(e.m_group), m_parse_only(e.m_parse_only) {
+    m_safe_ascii(e.m_safe_ascii), m_group(e.m_group), m_parse_only(e.m_parse_only),
+    m_priority(e.m_priority) {
     if (is_numeral())
         new (&m_num) mpz(e.m_num);
     else
@@ -39,9 +40,9 @@ notation_entry::notation_entry(notation_entry const & e):
 }
 
 notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload,
-                               notation_entry_group g, bool parse_only):
+                               unsigned priority, notation_entry_group g, bool parse_only):
     m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD),
-    m_expr(e), m_overload(overload), m_group(g), m_parse_only(parse_only) {
+    m_expr(e), m_overload(overload), m_group(g), m_parse_only(parse_only), m_priority(priority) {
     new (&m_transitions) list<transition>(ts);
     m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); });
 }
@@ -273,7 +274,7 @@ struct notation_config {
             if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr()))
                 updt_inv_map(s, *idx, e);
             parse_table & nud = s.nud(e.group());
-            nud = nud.add(ts.size(), ts.data(), e.get_expr(), e.overload());
+            nud = nud.add(ts.size(), ts.data(), e.get_expr(), e.priority(), e.overload());
             break;
         }
         case notation_entry_kind::LeD: {
@@ -281,7 +282,7 @@ struct notation_config {
             if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr()))
                 updt_inv_map(s, *idx, e);
             parse_table & led = s.led(e.group());
-            led = led.add(ts.size(), ts.data(), e.get_expr(), e.overload());
+            led = led.add(ts.size(), ts.data(), e.get_expr(), e.priority(), e.overload());
             break;
         }
         case notation_entry_kind::Numeral:
@@ -311,6 +312,7 @@ struct notation_config {
             s << static_cast<char>(e.group()) << length(e.get_transitions());
             for (auto const & t : e.get_transitions())
                 s << t;
+            s << e.priority();
         }
     }
     static entry read_entry(deserializer & d) {
@@ -329,7 +331,9 @@ struct notation_config {
             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, g, parse_only);
+            unsigned priority;
+            d >> priority;
+            return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, priority, g, parse_only);
         }
     }
     static optional<unsigned> get_fingerprint(entry const &) {

src/frontends/lean/parser_config.h

@@ -35,10 +35,12 @@ class notation_entry {
     bool                 m_safe_ascii;
     notation_entry_group m_group;
     bool                 m_parse_only;
+    unsigned             m_priority;
 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_group g, bool parse_only);
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, unsigned priority,
+                   notation_entry_group g, 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();
@@ -52,6 +54,7 @@ public:
     bool is_safe_ascii() const { return m_safe_ascii; }
     notation_entry_group group() const { return m_group; }
     bool reserve() const { return group() == notation_entry_group::Reserve; }
+    unsigned priority() const { return m_priority; }
     bool parse_only() const { return m_parse_only; }
 };
 bool operator==(notation_entry const & e1, notation_entry const & e2);

tests/lean/run/notation_priority.lean

@@ -0,0 +1,27 @@
+constant f : nat → nat → nat
+constant g : nat → nat → nat
+
+
+infix [priority 10] + := f
+infix [priority 20] + := g
+
+variables a b : nat
+
+example : a + b = g a b := rfl
+infix [priority 5] + := g
+example : a + b = f a b := rfl
+infix [priority 15] + := g
+example : a + b = g a b := rfl
+
+infix [priority default+1] + := f
+infix + := g
+example : a + b = f a b := rfl
+infix [priority default+2] + := g
+example : a + b = g a b := rfl
+
+infix + := f
+infix + := g
+example : a + b = f a b := rfl
+
+infix [priority default+1] + := g
+example : a + b = g a b := rfl