Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end.

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

src/frontends/lean/lean_parser.cpp

@@ -1277,8 +1277,16 @@ class parser::imp {
         auto id_pos = pos();
         name id = check_identifier_next("invalid set options, identifier (i.e., option name) expected");
         auto decl_it = get_option_declarations().find(id);
-        if (decl_it == get_option_declarations().end())
-            throw parser_error(sstream() << "unknown option '" << id << "', type 'Help Options.' for list of available options", id_pos);
+        if (decl_it == get_option_declarations().end()) {
+            // add "lean" prefix
+            name lean_id = name("lean") + id;
+            decl_it = get_option_declarations().find(lean_id);
+            if (decl_it == get_option_declarations().end()) {
+                throw parser_error(sstream() << "unknown option '" << id << "', type 'Help Options.' for list of available options", id_pos);
+            } else {
+                id = lean_id;
+            }
+        }
         option_kind k = decl_it->second.kind();
         switch (curr()) {
         case scanner::token::Id:

src/tests/util/name.cpp

@@ -117,6 +117,16 @@ static void tst6() {
     lean_assert(!name(name(name(230u), "bla\u2200"), "foo").is_safe_ascii());
 }
 
+static void tst7() {
+    lean_assert(name("foo") + name("bla") == name({"foo", "bla"}));
+    lean_assert(name("foo") + name({"bla", "test"}) == name({"foo", "bla", "test"}));
+    lean_assert(name({"foo", "hello"}) + name({"bla", "test"}) == name({"foo", "hello", "bla", "test"}));
+    lean_assert(name("foo") + (name(10u) + name({"bla", "test"})) == name(name(name(name("foo"), 10u), "bla"), "test"));
+    lean_assert(name() + name({"bla", "test"}) == name({"bla", "test"}));
+    lean_assert(name({"bla", "test"}) + name() == name({"bla", "test"}));
+    lean_assert(name(10u) + name(20u) == name(name(10u), 20u));
+}
+
 int main() {
     tst1();
     tst2();
@@ -124,5 +134,6 @@ int main() {
     tst4();
     tst5();
     tst6();
+    tst7();
     return has_violations() ? 1 : 0;
 }

src/util/name.cpp

@@ -325,6 +325,21 @@ std::ostream & operator<<(std::ostream & out, name const & n) {
     name::imp::display(out, n.m_ptr);
     return out;
 }
-}
 
+name operator+(name const & n1, name const & n2) {
+    if (n2.is_anonymous()) {
+        return n1;
+    } else {
+        name prefix;
+        if (!n2.is_atomic())
+            prefix = n1 + name(n2.m_ptr->m_prefix);
+        else
+            prefix = n1;
+        if (n2.m_ptr->m_is_string)
+            return name(prefix, n2.m_ptr->m_str);
+        else
+            return name(prefix, n2.m_ptr->m_k);
+    }
+}
+}
 void print(lean::name const & n) { std::cout << n << std::endl; }

src/util/name.h

@@ -61,6 +61,8 @@ public:
     /** \brief Return true iff the name contains only safe ASCII chars */
     bool is_safe_ascii() const;
     friend std::ostream & operator<<(std::ostream & out, name const & n);
+    /** \brief Concatenate the two given names. */
+    friend name operator+(name const & n1, name const & n2);
 };
 struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
 struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };