fix(frontends/lean/builtin_cmds): add modifiers/attrs/docstring check…

… to `local` command (#711)

The notation commands are supposed to reject modifiers/attrs/docstrings, but using them via the `local` command circumvents the check. This adds the check for `local` notations.

src/frontends/lean/builtin_cmds.cpp

@@ -414,6 +414,7 @@ static environment local_cmd(parser & p, ast_id & cmd_id, cmd_meta const & meta)
         p.next();
         return local_attribute_cmd(p, cmd_id, meta);
     } else {
+        meta.throw_exception_if_nonempty();
         return local_notation_cmd(p, cmd_id);
     }
 }

src/frontends/lean/cmd_table.h

@@ -24,6 +24,15 @@ struct cmd_meta {
     cmd_meta(decl_attributes const & attrs, decl_modifiers const & mods,
              optional<std::string> const & doc = optional<std::string>()):
         m_attrs(attrs), m_modifiers(mods), m_doc_string(doc) {}
+
+    void throw_exception_if_nonempty() const & {
+        if (m_modifiers)
+            throw exception("command does not accept modifiers");
+        if (m_attrs)
+            throw exception("command does not accept attributes");
+        if (m_doc_string)
+            throw exception("command does not accept doc string");
+    }
 };
 
 typedef std::function<environment(parser&, ast_id &, cmd_meta const &)> command_fn;
@@ -39,12 +48,7 @@ struct cmd_info_tmpl {
         m_name(n), m_descr(d), m_fn(fn), m_skip_token(skip_token) {}
     cmd_info_tmpl(name const & n, char const * d, std::function<environment(parser&, ast_id&)> const & fn, bool skip_token = true):
         cmd_info_tmpl(n, d, [=](parser & p, ast_id & cmd_id, cmd_meta const & meta) {
-            if (meta.m_modifiers)
-                throw exception("command does not accept modifiers");
-            if (meta.m_attrs)
-                throw exception("command does not accept attributes");
-            if (meta.m_doc_string)
-                throw exception("command does not accept doc string");
+            meta.throw_exception_if_nonempty();
             return fn(p, cmd_id);
         }, skip_token) {}
     cmd_info_tmpl() {}

tests/lean/local_notation_meta_bug.lean

@@ -0,0 +1,5 @@
+local infix ` + ` := nat.add
+@[class] local infix ` + ` := nat.add
+noncomputable local infix ` + ` := nat.add
+@[class] noncomputable local infix ` + ` := nat.add
+/-- foo -/ local infix ` + ` := nat.add

tests/lean/local_notation_meta_bug.lean.expected.out

@@ -0,0 +1,4 @@
+local_notation_meta_bug.lean:2:9: error: command does not accept attributes
+local_notation_meta_bug.lean:3:14: error: command does not accept modifiers
+local_notation_meta_bug.lean:4:23: error: command does not accept modifiers
+local_notation_meta_bug.lean:5:11: error: command does not accept doc string