feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function

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

src/frontends/lean/builtin_cmds.cpp

@@ -173,7 +173,12 @@ environment using_cmd(parser & p) {
     while (true) {
         name cls = parse_class(p);
         bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations;
+        auto pos   = p.pos();
         name ns    = p.check_id_next("invalid 'using' command, identifier expected");
+        optional<name> real_ns = to_valid_namespace_name(env, ns);
+        if (!real_ns)
+            throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos);
+        ns = *real_ns;
         env = using_namespace(env, p.ios(), ns, cls);
         if (decls) {
             // Remark: we currently to not allow renaming and hiding of universe levels

src/library/scoped_ext.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <memory>
+#include <string>
 #include "library/scoped_ext.h"
 #include "library/kernel_bindings.h"
 
@@ -25,7 +26,8 @@ void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn p
 }
 
 struct scope_mng_ext : public environment_extension {
-    list<name> m_namespaces;
+    name_set   m_namespace_set; // all namespaces registered in the system
+    list<name> m_namespaces; // stack of namespaces/sections
     list<bool> m_in_section;
 };
 
@@ -61,12 +63,30 @@ environment using_namespace(environment const & env, io_state const & ios, name
     return r;
 }
 
+optional<name> to_valid_namespace_name(environment const & env, name const & n) {
+    scope_mng_ext const & ext = get_extension(env);
+    if (ext.m_namespace_set.contains(n))
+        return optional<name>(n);
+    for (auto const & ns : ext.m_namespaces) {
+        name r = ns + n;
+        if (ext.m_namespace_set.contains(r))
+            return optional<name>(r);
+    }
+    return optional<name>();
+}
+
+static std::string g_new_namespace_key("nspace");
 environment push_scope(environment const & env, io_state const & ios, name const & n) {
     if (!n.is_anonymous() && in_section(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
     bool in_section = n.is_anonymous();
     name new_n = get_namespace(env) + n;
     scope_mng_ext ext = get_extension(env);
+    bool save_ns = false;
+    if (!ext.m_namespace_set.contains(new_n)) {
+        save_ns  = true;
+        ext.m_namespace_set.insert(new_n);
+    }
     ext.m_namespaces = list<name>(new_n, ext.m_namespaces);
     ext.m_in_section = list<bool>(n.is_anonymous(), ext.m_in_section);
     environment r = update(env, ext);
@@ -75,9 +95,24 @@ environment push_scope(environment const & env, io_state const & ios, name const
     }
     if (!n.is_anonymous())
         r = using_namespace(r, ios, n);
+    if (save_ns)
+        r = module::add(r, g_new_namespace_key, [=](serializer & s) { s << new_n; });
     return r;
 }
 
+static void namespace_reader(deserializer & d, module_idx, shared_environment &,
+                             std::function<void(asynch_update_fn const &)> &,
+                             std::function<void(delayed_update_fn const &)> & add_delayed_update) {
+    name n;
+    d >> n;
+    add_delayed_update([=](environment const & env, io_state const &) -> environment {
+            scope_mng_ext ext = get_extension(env);
+            ext.m_namespace_set.insert(n);
+            return update(env, ext);
+        });
+}
+register_module_object_reader_fn g_namespace_reader(g_new_namespace_key, namespace_reader);
+
 environment pop_scope(environment const & env) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))

src/library/scoped_ext.h

@@ -30,6 +30,17 @@ environment pop_scope(environment const & env);
 name const & get_namespace(environment const & env);
 bool in_section(environment const & env);
 
+/** \brief Check if \c n may be a reference to a namespace, if it is return it.
+    The procedure checks if \c n is a registered namespace, if it is not, it tries
+    to prefix \c n with each prefix in the current scope. Example: suppose the scope is:
+       namespace foo
+         namespace bla
+           namespace boo
+              ...
+    Then, the procedure tries n, 'foo.bla.boo'+n, 'foo.bla'+n, 'foo'+n.
+*/
+optional<name> to_valid_namespace_name(environment const & env, name const & n);
+
 void open_scoped_ext(lua_State * L);
 
 /**

tests/lean/run/algebra1.lean

@@ -86,7 +86,7 @@ namespace monoid
   definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s)
   := monoid_struct_rec (fun mul id a i, a) s
 
-  using algebra.semigroup -- Fix: allow user to write just semigroup
+  using semigroup
   definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A
   := mk_semigroup_struct (mul s) (assoc s)