feat(frontends/lean/builtin_cmds): add 'set_option' command

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

src/frontends/lean/builtin_cmds.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "util/sstream.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/type_checker.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
@@ -23,6 +24,8 @@ static name g_colon(":");
 static name g_assign(":=");
 static name g_private("[private]");
 static name g_inline("[inline]");
+static name g_true("true");
+static name g_false("false");
 
 static void check_atomic(name const & n) {
     if (!n.is_atomic())
@@ -318,8 +321,48 @@ environment exit_cmd(parser &) {
     throw interrupt_parser();
 }
 
+environment set_option_cmd(parser & p) {
+    auto id_pos = p.pos();
+    name id = p.check_id_next("invalid set option, identifier (i.e., option name) expected");
+    auto decl_it = get_option_declarations().find(id);
+    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();
+    if (k == BoolOption) {
+        if (p.curr_is_token_or_id(g_true))
+            p.set_option(id, true);
+        else if (p.curr_is_token_or_id(g_false))
+            p.set_option(id, false);
+        else
+            throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos());
+        p.next();
+    } else if (k == StringOption) {
+        if (!p.curr_is_string())
+            throw parser_error("invalid option value, given option is not a string", p.pos());
+        p.set_option(id, p.get_str_val());
+        p.next();
+    } else if (k == DoubleOption) {
+        p.set_option(id, p.parse_double());
+    } else if (k == UnsignedOption || k == IntOption) {
+        p.set_option(id, p.parse_small_nat());
+    } else {
+        throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos());
+    }
+    p.updt_options();
+    return p.env();
+}
+
 cmd_table init_cmd_table() {
     cmd_table r;
+    add_cmd(r, cmd_info("set_option",   "set configuration option", set_option_cmd));
     add_cmd(r, cmd_info("exit",         "exit", exit_cmd));
     add_cmd(r, cmd_info("print",        "print a string", print_cmd));
     add_cmd(r, cmd_info("universe",     "declare a global universe level", universe_cmd));

src/frontends/lean/parser.cpp

@@ -357,11 +357,19 @@ unsigned parser::get_small_nat() {
 }
 
 unsigned parser::parse_small_nat() {
+    if (!curr_is_numeral())
+        throw parser_error("(small) natural number expected", pos());
     unsigned r = get_small_nat();
     next();
     return r;
 }
 
+double parser::parse_double() {
+    if (curr() != scanner::token_kind::Decimal)
+        throw parser_error("decimal value expected", pos());
+    return get_num_val().get_double();
+}
+
 static level lift(level l, unsigned k) {
     while (k > 0) {
         k--;

src/frontends/lean/parser.h

@@ -93,8 +93,6 @@ class parser {
     expr copy_with_new_pos(expr const & e, pos_info p);
     expr propagate_levels(expr const & e, levels const & ls);
 
-    void updt_options();
-
     cmd_table const & cmds() const { return get_cmd_table(env()); }
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
@@ -146,6 +144,9 @@ public:
     local_level_decls const & get_local_level_decls() const { return m_local_level_decls; }
     local_expr_decls const & get_local_expr_decls() const { return m_local_decls; }
 
+    void updt_options();
+    template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
+
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
     expr save_pos(expr e, pos_info p);
@@ -192,6 +193,7 @@ public:
     void parse_names(buffer<std::pair<pos_info, name>> & result);
     unsigned get_small_nat();
     unsigned parse_small_nat();
+    double parse_double();
 
     bool parse_local_notation_decl();
 

src/frontends/lean/token_table.cpp

@@ -65,7 +65,8 @@ token_table init_token_table() {
                                "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
-                               "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "#setline", nullptr};
+                               "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option",
+                               "#setline", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/run/t10.lean

@@ -0,0 +1,2 @@
+set_option pp.colors true
+set_option pp.unicode false