From 3b721fe6750a4924f045dd7dd4a18177c636bb4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Mar 2015 13:03:30 -0800 Subject: [PATCH] feat(frontends/lean): add missing 'help' command --- src/frontends/lean/builtin_cmds.cpp | 35 +++++++++++++++++++++++++++++ src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/parser.h | 3 ++- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + tests/lean/run/help_cmd.lean | 5 +++++ 7 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/help_cmd.lean diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 89c9ce7ba..28f04a938 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -643,6 +643,40 @@ environment local_cmd(parser & p) { } } +static environment help_cmd(parser & p) { + flycheck_information info(p.regular_stream()); + if (info.enabled()) { + p.display_information_pos(p.cmd_pos()); + p.regular_stream() << "help result:\n"; + } + if (p.curr_is_token_or_id(get_options_tk())) { + p.next(); + for (auto odecl : get_option_declarations()) { + auto opt = odecl.second; + regular(p.env(), p.ios()) + << " " << opt.get_name() << " (" << opt.kind() << ") " + << opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl; + } + } else if (p.curr_is_token_or_id(get_commands_tk())) { + p.next(); + buffer ns; + cmd_table const & cmds = p.cmds(); + cmds.for_each([&](name const & n, cmd_info const &) { + ns.push_back(n); + }); + std::sort(ns.begin(), ns.end()); + for (name const & n : ns) { + regular(p.env(), p.ios()) + << " " << n << ": " << cmds.find(n)->get_descr() << endl; + }; + } else { + p.regular_stream() + << "help options : describe available options\n" + << "help commands : describe available commands\n"; + } + return p.env(); +} + void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd)); @@ -659,6 +693,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd)); add_cmd(r, cmd_info("find_decl", "find definitions and/or theorems", find_cmd)); add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); + add_cmd(r, cmd_info("help", "brief description of available commands and options", help_cmd)); add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd)); add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9281629e5..d4d61e0bf 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -213,7 +213,7 @@ expr parser::mk_by(expr const & t, pos_info const & pos) { } void parser::updt_options() { - m_verbose = get_verbose(m_ios.get_options()); + m_verbose = get_verbose(m_ios.get_options()); m_show_errors = get_parser_show_errors(m_ios.get_options()); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e861c0dc8..57277301b 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -165,7 +165,6 @@ class parser { tag get_tag(expr e); expr copy_with_new_pos(expr const & e, pos_info p); - 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()); } @@ -231,6 +230,8 @@ public: info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); ~parser(); + cmd_table const & cmds() const { return get_cmd_table(env()); } + void set_cache(definition_cache * c) { m_cache = c; } void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 2f474c839..fe25e3415 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -93,7 +93,7 @@ void init_token_table(token_table & t) { "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[parsing-only]", "[multiple-instances]", "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print", - "end", "namespace", "section", "prelude", + "end", "namespace", "section", "prelude", "help", "import", "inductive", "record", "structure", "module", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 1b691239f..82a3bb4d5 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -58,6 +58,7 @@ static name * g_raw = nullptr; static name * g_true = nullptr; static name * g_false = nullptr; static name * g_options = nullptr; +static name * g_commands = nullptr; static name * g_instances = nullptr; static name * g_classes = nullptr; static name * g_coercions = nullptr; @@ -180,6 +181,7 @@ void initialize_tokens() { g_true = new name("true"); g_false = new name("false"); g_options = new name("options"); + g_commands = new name("commands"); g_instances = new name("instances"); g_classes = new name("classes"); g_coercions = new name("coercions"); @@ -310,6 +312,7 @@ void finalize_tokens() { delete g_true; delete g_false; delete g_options; + delete g_commands; delete g_instances; delete g_classes; delete g_coercions; @@ -426,6 +429,7 @@ name const & get_raw_tk() { return *g_raw; } name const & get_true_tk() { return *g_true; } name const & get_false_tk() { return *g_false; } name const & get_options_tk() { return *g_options; } +name const & get_commands_tk() { return *g_commands; } name const & get_instances_tk() { return *g_instances; } name const & get_classes_tk() { return *g_classes; } name const & get_coercions_tk() { return *g_coercions; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 4fffd620f..f107aa3f9 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -60,6 +60,7 @@ name const & get_raw_tk(); name const & get_true_tk(); name const & get_false_tk(); name const & get_options_tk(); +name const & get_commands_tk(); name const & get_instances_tk(); name const & get_classes_tk(); name const & get_coercions_tk(); diff --git a/tests/lean/run/help_cmd.lean b/tests/lean/run/help_cmd.lean new file mode 100644 index 000000000..40e247fee --- /dev/null +++ b/tests/lean/run/help_cmd.lean @@ -0,0 +1,5 @@ +help options + +help commands + +print options