feat(*): uniform metaclass names, metaclass validation at 'open' command

src/frontends/lean/begin_end_ext.cpp

@@ -78,11 +78,11 @@ bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_
 bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
 
 void initialize_begin_end_ext() {
-    g_class_name = new name("begin_end");
-    g_key        = new std::string("be_pre_tac");
+    g_class_name = new name("begin-end-hints");
+    g_key        = new std::string("bepretac");
     begin_end_ext::initialize();
-    g_begin_end  = new name("begin_end");
-    g_begin_end_element = new name("begin_end_element");
+    g_begin_end  = new name("begin-end");
+    g_begin_end_element = new name("begin-end-element");
     register_annotation(*g_begin_end);
     register_annotation(*g_begin_end_element);
 }

src/frontends/lean/builtin_cmds.cpp

@@ -420,18 +420,25 @@ environment set_option_cmd(parser & p) {
     return update_fingerprint(env, p.get_options().hash());
 }
 
-static name parse_class(parser & p) {
+static name parse_metaclass(parser & p) {
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
+        auto pos = p.pos();
         name n;
-        if (p.curr_is_identifier())
-            n = p.get_name_val();
-        else if (p.curr_is_keyword() || p.curr_is_command())
-            n = p.get_token_info().value();
-        else
-            throw parser_error("invalid 'open' command, identifier or symbol expected", p.pos());
-        p.next();
+        while (!p.curr_is_token(get_rbracket_tk())) {
+            if (p.curr_is_identifier())
+                n = n.append_after(p.get_name_val().to_string().c_str());
+            else if (p.curr_is_keyword() || p.curr_is_command())
+                n = n.append_after(p.get_token_info().value().to_string().c_str());
+            else if (p.curr_is_token(get_sub_tk()))
+                n = n.append_after("-");
+            else
+                throw parser_error("invalid 'open' command, identifier or symbol expected", pos);
+            p.next();
+        }
         p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
+        if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
+            throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
         return n;
     } else {
         return name();
@@ -466,7 +473,7 @@ static environment add_abbrev(parser & p, environment const & env, name const &
 environment open_export_cmd(parser & p, bool open) {
     environment env = p.env();
     while (true) {
-        name cls = parse_class(p);
+        name cls = parse_metaclass(p);
         bool decls = cls.is_anonymous() || cls == get_decls_tk() || cls == get_declarations_tk();
         auto pos   = p.pos();
         name ns    = p.check_id_next("invalid 'open/export' command, identifier expected");

src/frontends/lean/tactic_hint.cpp

@@ -57,7 +57,7 @@ template class scoped_ext<tactic_hint_config>;
 typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
 
 void initialize_tactic_hint() {
-    g_class_name = new name("tactic_hints");
+    g_class_name = new name("tactic-hints");
     g_key        = new std::string("tachint");
     tactic_hint_ext::initialize();
 }

src/library/reducible.cpp

@@ -78,7 +78,7 @@ typedef scoped_ext<reducible_config> reducible_ext;
 static name * g_tmp_prefix = nullptr;
 
 void initialize_reducible() {
-    g_class_name = new name("reduce_hints");
+    g_class_name = new name("reduce-hints");
     g_key        = new std::string("redu");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     reducible_ext::initialize();

src/library/scoped_ext.cpp

@@ -72,6 +72,14 @@ void get_metaclasses(buffer<name> & r) {
     }
 }
 
+bool is_metaclass(name const & n) {
+    for (auto const & t : get_exts()) {
+        if (std::get<0>(t) == n)
+            return true;
+    }
+    return false;
+}
+
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c) {
     environment r = env;
     for (auto const & t : get_exts()) {

src/library/scoped_ext.h

@@ -45,6 +45,9 @@ bool has_open_scopes(environment const & env);
 /** \brief Store in \c r all metaobject classes available in Lean */
 void get_metaclasses(buffer<name> & r);
 
+/** \brief Return true iff \c n is the name of a metaobject class available in Lean */
+bool is_metaclass(name const & n);
+
 /** \brief Add a new namespace (if it does not exist) */
 environment add_namespace(environment const & env, name const & ns);
 

tests/lean/run/class5.lean

@@ -31,7 +31,7 @@ section
 end
 
 section
-  open [notation] algebra
+  open [notations] algebra
   open nat
   -- check mul_struct nat  << This is an error, we opened only the notation from algebra
   variables a b c : nat