feat(frontends/lean): add notation overwrite

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

src/frontends/lean/builtin_exprs.cpp

@@ -224,6 +224,12 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &
     return parse_calc(p);
 }
 
+static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
+    name n = p.check_id_next("invalid '#' local notation, identifier expected");
+    environment env = overwrite_notation(p.env(), n);
+    return p.parse_scoped_expr(0, nullptr, env);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -240,6 +246,7 @@ parse_table init_nud_table() {
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
+    r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     return r;
 }
 

src/frontends/lean/parser.cpp

@@ -901,15 +901,11 @@ expr parser::parse_expr(unsigned rbp) {
 }
 
 expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp) {
-    if (num_params == 0) {
-        return parse_expr(rbp);
-    } else {
-        local_scope scope(*this);
-        m_env = lenv;
-        for (unsigned i = 0; i < num_params; i++)
-            add_local(ps[i].m_local, ps[i].m_bi);
-        return parse_expr(rbp);
-    }
+    local_scope scope(*this);
+    m_env = lenv;
+    for (unsigned i = 0; i < num_params; i++)
+        add_local(ps[i].m_local, ps[i].m_bi);
+    return parse_expr(rbp);
 }
 
 expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p) {

src/frontends/lean/parser_config.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include "util/sstream.h"
 #include "library/scoped_ext.h"
 #include "library/kernel_serializer.h"
 #include "frontends/lean/parser_config.h"
@@ -195,6 +196,18 @@ environment add_led_notation(environment const & env, std::initializer_list<nota
     return add_led_notation(env, ts.size(), ts.begin(), a, overload);
 }
 
+environment overwrite_notation(environment const & env, name const & n) {
+    auto it = notation_ext::get_entries(env, n);
+    if (!it)
+        throw exception(sstream() << "unknown namespace '" << n << "'");
+    environment r = env;
+    for (notation_entry e : *it) {
+        e.m_overload = false;
+        r = add_notation(r, e);
+    }
+    return r;
+}
+
 parse_table const & get_nud_table(environment const & env) {
     return notation_ext::get_state(env).m_nud;
 }

src/frontends/lean/parser_config.h

@@ -44,4 +44,6 @@ parse_table const & get_nud_table(environment const & env);
 parse_table const & get_led_table(environment const & env);
 cmd_table const & get_cmd_table(environment const & env);
 tactic_cmd_table const & get_tactic_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

@@ -57,7 +57,7 @@ token_table init_token_table() {
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
-         {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
+         {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 

src/library/scoped_ext.h

@@ -174,6 +174,9 @@ public:
     static state const & get_state(environment const & env) {
         return get(env).m_state;
     }
+    static list<entry> const * get_entries(environment const & env, name const & n) {
+        return get(env).m_entries.find(n);
+    }
 };
 
 template<typename Config>

tests/lean/run/local_using.lean

@@ -0,0 +1,24 @@
+variable N : Type.{1}
+precedence `+`:65
+
+namespace foo
+  variable a : N
+  variable f : N → N → N
+  infix + := f
+end
+
+namespace bla
+  variable b : N
+  variable f : N → N → N
+  infix + := f
+end
+
+variable g : N → N → N
+
+using foo
+using bla
+print raw a + b -- + is overloaded, it creates a choice
+print raw #foo a + b   -- + is not overloaded, we are parsing inside #foo
+print raw g (#foo a + b) (#bla a + b) -- mixing both
+
+