feat(frontends/lean): local notation 'shadows' global one

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/notation_cmd.cpp

@@ -71,7 +71,7 @@ using notation::mk_skip_action;
 using notation::transition;
 using notation::action;
 
-environment mixfix_cmd(parser & p, mixfix_kind k) {
+static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     optional<unsigned> prec = parse_optional_precedence(p);
     environment env = p.env();
@@ -91,18 +91,18 @@ environment mixfix_cmd(parser & p, mixfix_kind k) {
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
-        return add_led_notation(env, {transition(tks, mk_expr_action(*prec))}, mk_app(f, Var(1), Var(0)));
+        return add_led_notation(env, {transition(tks, mk_expr_action(*prec))}, mk_app(f, Var(1), Var(0)), overload);
     case mixfix_kind::infixr:
-        return add_led_notation(env, {transition(tks, mk_expr_action(*prec-1))}, mk_app(f, Var(1), Var(0)));
+        return add_led_notation(env, {transition(tks, mk_expr_action(*prec-1))}, mk_app(f, Var(1), Var(0)), overload);
     case mixfix_kind::postfix:
-        return add_led_notation(env, {transition(tks, mk_skip_action())}, mk_app(f, Var(0)));
+        return add_led_notation(env, {transition(tks, mk_skip_action())}, mk_app(f, Var(0)), overload);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-environment infixl_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::infixl); }
+environment infixl_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixl, overload); }
-environment infixr_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::infixr); }
+environment infixr_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixr, overload); }
-environment postfix_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::postfix); }
+environment postfix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::postfix, overload); }
 
 static name parse_quoted_symbol(parser & p, environment & env) {
     if (p.curr_is_quoted_symbol()) {
@@ -144,7 +144,7 @@ static void parse_notation_local(parser & p, buffer<expr> & locals) {
     }
 }
 
-action parse_action(parser & p, environment & env, buffer<expr> & locals) {
+static action parse_action(parser & p, environment & env, buffer<expr> & locals) {
     if (p.curr_is_token(g_colon)) {
         p.next();
         if (p.curr_is_numeral()) {
@@ -197,7 +197,7 @@ action parse_action(parser & p, environment & env, buffer<expr> & locals) {
     }
 }
 
-environment notation_cmd(parser & p) {
+environment notation_cmd_core(parser & p, bool overload) {
     environment env = p.env();
     buffer<expr>       locals;
     buffer<transition> ts;
@@ -234,8 +234,8 @@ environment notation_cmd(parser & p) {
         throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
     expr n = parse_notation_expr(p, locals);
     if (is_nud)
-        return add_nud_notation(env, ts.size(), ts.data(), n);
+        return add_nud_notation(env, ts.size(), ts.data(), n, overload);
     else
-        return add_led_notation(env, ts.size(), ts.data(), n);
+        return add_led_notation(env, ts.size(), ts.data(), n, overload);
 }
 }

src/frontends/lean/notation_cmd.h

@@ -9,8 +9,12 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 environment precedence_cmd(parser & p);
-environment notation_cmd(parser & p);
+environment notation_cmd_core(parser & p, bool overload);
-environment infixl_cmd(parser & p);
+environment infixl_cmd_core(parser & p, bool overload);
-environment infixr_cmd(parser & p);
+environment infixr_cmd_core(parser & p, bool overload);
-environment postfix_cmd(parser & p);
+environment postfix_cmd_core(parser & p, bool overload);
+inline environment notation_cmd(parser & p) { return notation_cmd_core(p, true); }
+inline environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
+inline environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
+inline environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
 }

src/frontends/lean/parser.cpp

@@ -532,16 +532,16 @@ void parser::parse_binders_core(buffer<parameter> & r) {
         next();
         if (curr_is_token(g_infix) || curr_is_token(g_infixl)) {
             next();
-            m_env = infixl_cmd(*this);
+            m_env = infixl_cmd_core(*this, false);
         } else if (curr_is_token(g_infixr)) {
             next();
-            m_env = infixr_cmd(*this);
+            m_env = infixr_cmd_core(*this, false);
         } else if (curr_is_token(g_postfix)) {
             next();
-            m_env = postfix_cmd(*this);
+            m_env = postfix_cmd_core(*this, false);
         } else if (curr_is_token(g_notation)) {
             next();
-            m_env = notation_cmd(*this);
+            m_env = notation_cmd_core(*this, false);
         } else {
             parse_binder_block(r, binder_info());
         }

src/frontends/lean/parser_config.cpp

@@ -136,9 +136,10 @@ struct notation_entry {
     bool             m_is_nud;
     list<transition> m_transitions;
     expr             m_expr;
+    bool             m_overload;
     notation_entry():m_is_nud(true) {}
-    notation_entry(bool is_nud, list<transition> const & ts, expr const & e):
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload):
-        m_is_nud(is_nud), m_transitions(ts), m_expr(e) {}
+        m_is_nud(is_nud), m_transitions(ts), m_expr(e), m_overload(overload) {}
 };
 
 struct notation_config {
@@ -148,9 +149,9 @@ struct notation_config {
         buffer<transition> ts;
         to_buffer(e.m_transitions, ts);
         if (e.m_is_nud)
-            s.m_nud = s.m_nud.add(ts.size(), ts.data(), e.m_expr, true);
+            s.m_nud = s.m_nud.add(ts.size(), ts.data(), e.m_expr, e.m_overload);
         else
-            s.m_led = s.m_led.add(ts.size(), ts.data(), e.m_expr, true);
+            s.m_led = s.m_led.add(ts.size(), ts.data(), e.m_expr, e.m_overload);
     }
     static name const & get_class_name() {
         static name g_class_name("notation");
@@ -161,40 +162,40 @@ struct notation_config {
         return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
-        s << e.m_is_nud << e.m_expr;
+        s << e.m_is_nud << e.m_overload << e.m_expr;
         s << length(e.m_transitions);
         for (auto const & t : e.m_transitions)
             s << t;
     }
     static entry read_entry(deserializer & d) {
-        bool is_nud; expr e;
+        bool is_nud, overload; expr e;
-        d >> is_nud >> e;
+        d >> is_nud >> overload >> e;
         unsigned sz;
         d >> 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);
+        return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload);
     }
 };
 
 template class scoped_ext<notation_config>;
 typedef scoped_ext<notation_config> notation_ext;
 
-environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a) {
+environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload) {
-    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(true, to_list(ts, ts+num), a));
+    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(true, to_list(ts, ts+num), a, overload));
 }
 
-environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a) {
+environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload) {
-    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(false, to_list(ts, ts+num), a));
+    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(false, to_list(ts, ts+num), a, overload));
 }
 
-environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a) {
+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);
+    return add_nud_notation(env, ts.size(), ts.begin(), a, overload);
 }
 
-environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a) {
+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);
+    return add_led_notation(env, ts.size(), ts.begin(), a, overload);
 }
 
 parse_table const & get_nud_table(environment const & env) {

src/frontends/lean/parser_config.h

@@ -12,10 +12,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 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);
+environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload = true);
-environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a);
+environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload = true);
-environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a);
+environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
-environment add_led_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,
+                             bool overload = true);
 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);

tests/lean/t13.lean

@@ -0,0 +1,12 @@
+variable A : Type.{1}
+variable f : A → A → A
+variable g : A → A → A
+precedence `+` : 65
+infixl + := f
+infixl + := g
+variable a : A
+variable b : A
+print raw a+b -- + is overloaded
+check fun (h : A → A → A)
+          (infixl + := h), -- Like local declarations, local notation "shadows" global one.
+      a+b

tests/lean/t13.lean.expected.out

@@ -0,0 +1,2 @@
+choice (g a b) (f a b)
+fun (h : A -> A -> A), (h a b) : (A -> A -> A) -> A