fix(frontends/lean): bugs in notation management

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

src/frontends/lean/class.cpp

@@ -30,7 +30,9 @@ struct class_state {
     }
     void add_instance(name const & c, name const & i) {
         auto it = m_instances.find(c);
-        if (!it) throw exception(sstream() << "invalid instance, unknown class '" << c << "'");
+        if (!it)
+            m_instances.insert(c, list<name>(i));
+        else
             m_instances.insert(c, cons(i, filter(*it, [&](name const & i1) { return i1 != i; })));
     }
 };

src/frontends/lean/parse_table.cpp

@@ -131,6 +131,24 @@ bool action::is_compatible(action const & a) const {
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
+void action::display(std::ostream & out) const {
+    switch (kind()) {
+    case action_kind::Skip:    out << "skip"; break;
+    case action_kind::Binder:  out << "binder"; break;
+    case action_kind::Binders: out << "binders"; break;
+    case action_kind::Ext:     out << "ext"; break;
+    case action_kind::LuaExt:  out << "luaext"; break;
+    case action_kind::Expr:    out << rbp(); break;
+    case action_kind::Exprs:
+        out << "(fold" << (is_fold_right() ? "r" : "l") << " "
+            << rbp() << " " << get_rec() << " " << get_initial() << ")";
+        break;
+    case action_kind::ScopedExpr:
+        out << "(scoped " << rbp() << " " << get_rec() << ")";
+        break;
+    }
+}
+
 
 void action_cell::dealloc() {
     switch (m_kind) {
@@ -287,6 +305,25 @@ parse_table parse_table::merge(parse_table const & s, bool overload) const {
 
 bool parse_table::is_nud() const { return m_ptr->m_nud; }
 
+void parse_table::display(std::ostream & out) const {
+    for_each([&](unsigned num, transition const * ts, list<expr> const & es) {
+            for (unsigned i = 0; i < num; i++) {
+                if (i > 0) out << " ";
+                out << "`" << ts[i].get_token() << "`:";
+                ts[i].get_action().display(out);
+            }
+            out << " :=";
+            if (length(es) == 1) {
+                out << " " << head(es) << "\n";
+            } else {
+                out << "\n";
+                for (auto e : es) {
+                    out << "  | " << e << "\n";
+                }
+            }
+        });
+}
+
 typedef action notation_action;
 DECL_UDATA(notation_action)
 

src/frontends/lean/parse_table.h

@@ -77,6 +77,7 @@ public:
     std::string const & get_lua_fn() const;
 
     bool is_compatible(action const & a) const;
+    void display(std::ostream & out) const;
 };
 
 action mk_skip_action();
@@ -125,6 +126,8 @@ public:
     optional<std::pair<action, parse_table>> find(name const & tk) const;
     list<expr> const & is_accepting() const;
     void for_each(std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const;
+
+    void display(std::ostream & out) const;
 };
 }
 typedef notation::parse_table parse_table;

src/frontends/lean/parser_config.cpp

@@ -196,14 +196,23 @@ environment add_led_notation(environment const & env, std::initializer_list<nota
 }
 
 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;
+    bool found = false;
+    if (auto it = token_ext::get_entries(r, n)) {
+        found = true;
+        for (token_entry e : *it) {
+            r = add_token(r, e);
+        }
+    }
+    if (auto it = notation_ext::get_entries(env, n)) {
+        found = true;
         for (notation_entry e : *it) {
             e.m_overload = false;
             r = add_notation(r, e);
         }
+    }
+    if (!found)
+        throw exception(sstream() << "unknown namespace '" << n << "'");
     return r;
 }
 

src/frontends/lean/token_table.cpp

@@ -45,6 +45,16 @@ void for_each(token_table const & s, std::function<void(char const *, token_info
             fn(str.data(), info);
         });
 }
+void display(std::ostream & out, token_table const & s) {
+    for_each(s, [&](char const * token, token_info const & info) {
+            out << "`" << token << "`:" << info.precedence();
+            if (info.is_command())
+                out << " [command]";
+            if (info.value() != info.token())
+                out << " " << info.value();
+            out << "\n";
+        });
+}
 
 static char const * g_lambda_unicode = "\u03BB";
 static char const * g_pi_unicode     = "\u03A0";

src/frontends/lean/token_table.h

@@ -43,6 +43,7 @@ token_table add_command_token(token_table const & s, char const * token, char co
 token_table add_token(token_table const & s, char const * token, unsigned prec = 0);
 token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = 0);
 void for_each(token_table const & s, std::function<void(char const *, token_info const&)> const & fn);
+void display(std::ostream & out, token_table const & s);
 token_table const * find(token_table const & s, char c);
 optional<unsigned> get_precedence(token_table const & s, char const * token);
 token_info const * value_of(token_table const & s);

tests/lean/run/class5.lean

@@ -0,0 +1,58 @@
+import standard
+
+namespace algebra
+  inductive mul_struct (A : Type) : Type :=
+  | mk_mul_struct : (A → A → A) → mul_struct A
+
+  class mul_struct
+
+  definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
+  := mul_struct_rec (λ f, f) s a b
+
+  infixl `*`:75 := mul
+end
+
+namespace nat
+  inductive nat : Type :=
+  | zero : nat
+  | succ : nat → nat
+
+  variable mul : nat → nat → nat
+  variable add : nat → nat → nat
+
+  definition mul_struct [instance] : algebra.mul_struct nat
+  := algebra.mk_mul_struct mul
+end
+
+section
+  using algebra
+  using nat
+  variables a b c : nat
+  check a * b * c
+end
+
+section
+  using [notation] algebra
+  using nat
+  -- check mul_struct nat  << This is an error, we are using only the notation from algebra
+  variables a b c : nat
+  check a * b * c
+end
+
+section
+  using nat
+  -- check mul_struct nat  << This is an error, we are using only the notation from algebra
+  variables a b c : nat
+  check #algebra a*b*c
+end
+
+section
+  using nat
+
+  definition add_struct [instance] : algebra.mul_struct nat
+  := algebra.mk_mul_struct add
+
+  variables a b c : nat
+  check #algebra a*b*c  -- << is using add instead of mul
+end
+

tests/lean/run/e10.lean

@@ -40,3 +40,7 @@ section
   print raw i + n
   check n + m
 end
+
+
+variables a b : nat.nat
+check #nat a + b