From 018ebdd115dca17a80658c971d4abaa5beda0ba9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 9 Jun 2017 21:35:00 +0200 Subject: [PATCH] feat(frontends/lean/user_command): add user-defined commands --- src/frontends/lean/CMakeLists.txt | 3 +- src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/notation_cmd.cpp | 2 +- src/frontends/lean/parser_config.cpp | 19 +++- src/frontends/lean/parser_config.h | 4 +- src/frontends/lean/user_command.cpp | 123 ++++++++++++++++++++++ src/frontends/lean/user_command.h | 12 +++ src/library/vm/vm_parser.cpp | 5 +- src/library/vm/vm_parser.h | 2 +- tests/lean/user_command.lean | 36 +++++++ tests/lean/user_command.lean.expected.out | 11 ++ 11 files changed, 210 insertions(+), 10 deletions(-) create mode 100644 src/frontends/lean/user_command.cpp create mode 100644 src/frontends/lean/user_command.h create mode 100644 tests/lean/user_command.lean create mode 100644 tests/lean/user_command.lean.expected.out diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 0a39b218f1..1362a36868 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -8,4 +8,5 @@ init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp -equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp user_notation.cpp) +equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp +user_notation.cpp user_command.cpp) diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 380117e0cd..76cb291d3e 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include "frontends/lean/interactive.h" #include "frontends/lean/completion.h" #include "frontends/lean/user_notation.h" +#include "frontends/lean/user_command.h" namespace lean { void initialize_frontend_lean_module() { @@ -57,8 +58,10 @@ void initialize_frontend_lean_module() { initialize_interactive(); initialize_completion(); initialize_user_notation(); + initialize_user_command(); } void finalize_frontend_lean_module() { + finalize_user_command(); finalize_user_notation(); finalize_completion(); finalize_interactive(); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index a8ce553270..414087d9f1 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -318,7 +318,7 @@ static unsigned get_precedence(environment const & env, buffer cons std::string token_str = token.to_string(); for (auto const & e : new_tokens) { if (e.m_token == token_str) - return e.m_prec; + return *e.m_prec; } auto prec = get_expr_precedence(get_token_table(env), token_str.c_str()); if (prec) diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index c1b3a03554..e5a91fb19f 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -83,7 +83,11 @@ struct token_config { static name * g_class_name; static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec); + if (e.m_prec) { + s.m_table = add_token(s.m_table, e.m_token.c_str(), *e.m_prec); + } else { + s.m_table = add_command_token(s.m_table, e.m_token.c_str()); + } } static name const & get_class_name() { return *g_class_name; @@ -93,9 +97,9 @@ struct token_config { s << e.m_token.c_str() << e.m_prec; } static entry read_entry(deserializer & d) { - std::string tk = d.read_string(); - unsigned prec = d.read_unsigned(); - return entry(tk, prec); + entry e; + d >> e.m_token >> e.m_prec; + return e; } static optional get_fingerprint(entry const &) { return optional(); @@ -390,6 +394,13 @@ cmd_table const & get_cmd_table(environment const & env) { return get_extension(env).m_cmds; } +environment add_command(environment const & env, name const & n, cmd_info const & info) { + auto env2 = token_ext::register_entry(env, get_dummy_ios(), token_entry(n.to_string())); + cmd_ext ext = get_extension(env2); + ext.m_cmds.insert(n, info); + return env2.update(g_ext->m_ext_id, std::make_shared(ext)); +} + void initialize_parser_config() { token_config::g_class_name = new name("notation"); token_ext::initialize(); diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index a6c4cf84f9..44136b0c1a 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -17,8 +17,9 @@ Author: Leonardo de Moura namespace lean { struct token_entry { std::string m_token; - unsigned m_prec; + optional m_prec; // if none: command token token_entry(std::string const & tk, unsigned prec): m_token(tk), m_prec(prec) {} + token_entry(std::string const & tk): m_token(tk) {} token_entry() : m_prec(0) {} }; inline token_entry mk_token_entry(std::string const & tk, unsigned prec) { return token_entry(tk, prec); } @@ -77,6 +78,7 @@ parse_table const & get_led_table(environment const & env); parse_table const & get_reserved_nud_table(environment const & env); parse_table const & get_reserved_led_table(environment const & env); cmd_table const & get_cmd_table(environment const & env); +environment add_command(environment const & env, name const & n, cmd_info const & info); /** \brief Add \c n as notation for \c e */ environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true, bool parse_only = false); diff --git a/src/frontends/lean/user_command.cpp b/src/frontends/lean/user_command.cpp new file mode 100644 index 0000000000..e3c9c78ffb --- /dev/null +++ b/src/frontends/lean/user_command.cpp @@ -0,0 +1,123 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#include +#include "kernel/abstract.h" +#include "library/constants.h" +#include "library/attribute_manager.h" +#include "library/scoped_ext.h" +#include "library/tactic/elaborator_exception.h" +#include "library/string.h" +#include "library/vm/vm_expr.h" +#include "library/vm/vm_parser.h" +#include "library/quote.h" +#include "library/placeholder.h" +#include "frontends/lean/elaborator.h" + +namespace lean { +static environment add_user_command(environment const & env, name const & d) { + auto type = env.get(d).get_type(); + bool takes_meta_infos = false; + if (is_binding(type) && is_constant(binding_domain(type), {"interactive", "decl_meta_info"})) { + takes_meta_infos = true; + type = binding_body(type); + } + std::string tk; + if (is_binding(type) && is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) { + auto const & parser = app_arg(binding_domain(type)); + if (is_app_of(parser, get_lean_parser_tk_name(), 1)) { + if (auto lit = to_string(app_arg(parser))) { + tk = *lit; + type = binding_body(type); + } else { + throw elaborator_exception(app_arg(parser), + "invalid user-defined command, token must be a name literal"); + } + } + } else { + throw exception("invalid user-defined command, must take `interactive.parse (lean.parser.tk c)` parameter, " + "optionally preceded by `interactive.decl_meta_info` parameter"); + } + + if (!(is_app_of(type, get_lean_parser_name(), 1) && is_constant(app_arg(type), get_unit_name()))) { + throw exception("invalid user-defined command, must return type `lean.parser unit`"); + } + + expr dummy = mk_true(); + + auto run = [=](parser & p, cmd_meta const & meta) { + expr parser = mk_constant(d); + // we don't want to reflect `meta` into an expr, so abstract the parameter and pass it as a vm_obj arg + if (takes_meta_infos) { + parser = mk_app(parser, mk_var(0)); + } + // `parse (tk c)` arg + parser = mk_app(parser, mk_constant(get_unit_star_name())); + for (expr t = type; is_pi(t); t = binding_body(t)) { + expr arg_type = binding_domain(t); + if (is_app_of(arg_type, get_interactive_parse_name())) { + parser = mk_app(parser, parse_interactive_param(p, arg_type)); + } else { + expr e = p.parse_expr(get_max_prec()); + if (!closed(e) || has_local(e)) { + throw elaborator_exception(e, "invalid argument to user-defined command, must be closed term"); + } + parser = mk_app(parser, e); + } + } + buffer args; + if (takes_meta_infos) { + parser = mk_lambda("a", mk_expr_placeholder(), parser); + args.push_back(to_obj(meta)); + } + parser = p.elaborate("_user_command", {}, parser).first; + run_parser(p, parser, args); + return p.env(); + }; + + if (takes_meta_infos) { + return add_command(env, tk, cmd_info(tk, "description", run)); + } else { + return add_command(env, tk, cmd_info(tk, "description", [=](parser & p) { return run(p, {}); })); + } +} + +struct user_command_modification : public modification { + LEAN_MODIFICATION("USR_CMD") + + name m_name; + + user_command_modification() {} + user_command_modification(name const & name) : m_name(name) {} + + void perform(environment & env) const override { + env = add_user_command(env, m_name); + } + + void serialize(serializer & s) const override { + s << m_name; + } + + static std::shared_ptr deserialize(deserializer & d) { + return std::make_shared(read_name(d)); + } +}; +void initialize_user_command() { + user_command_modification::init(); + register_system_attribute(basic_attribute( + "user_command", "user-defined command", + [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { + if (persistent) { + return module::add_and_perform(env, std::make_shared(d)); + } else { + throw exception("[user_command] cannot be used locally"); + } + })); +} +void finalize_user_command() { + user_command_modification::finalize(); +} +} diff --git a/src/frontends/lean/user_command.h b/src/frontends/lean/user_command.h new file mode 100644 index 0000000000..805eff5bf1 --- /dev/null +++ b/src/frontends/lean/user_command.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#pragma once + +namespace lean { +void initialize_user_command(); +void finalize_user_command(); +} diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index b7de3ac266..61756f04b9 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -42,9 +42,10 @@ typedef interaction_monad lean_parser; #define CATCH } catch (break_at_pos_exception const & ex) { throw; }\ catch (exception const & ex) { return lean_parser::mk_exception(ex, s); } -vm_obj run_parser(parser & p, expr const & spec) { +vm_obj run_parser(parser & p, expr const & spec, buffer const & args) { type_context ctx(p.env(), p.get_options()); - return lean_parser::get_result_value(lean_parser::evaluator(ctx, p.get_options())(spec, lean_parser_state {&p})); + auto r = lean_parser::evaluator(ctx, p.get_options())(spec, args, lean_parser_state {&p}); + return lean_parser::get_result_value(r); } expr parse_interactive_param(parser & p, expr const & param_ty) { diff --git a/src/library/vm/vm_parser.h b/src/library/vm/vm_parser.h index 6fe548b03d..e7da1f8a46 100644 --- a/src/library/vm/vm_parser.h +++ b/src/library/vm/vm_parser.h @@ -9,7 +9,7 @@ Author: Sebastian Ullrich #include "frontends/lean/parser.h" namespace lean { -vm_obj run_parser(parser & p, expr const & spec); +vm_obj run_parser(parser & p, expr const & spec, buffer const & args = {}); expr parse_interactive_param(parser & p, expr const & param_ty); vm_obj to_obj(cmd_meta const & meta); diff --git a/tests/lean/user_command.lean b/tests/lean/user_command.lean new file mode 100644 index 0000000000..1e247f8677 --- /dev/null +++ b/tests/lean/user_command.lean @@ -0,0 +1,36 @@ +open lean +open lean.parser +open interactive +open tactic + +-- missing tk +@[user_command] +meta def foo_cmd : parser unit := pure () + +-- wrong return type +@[user_command] +meta def foo_cmd (_ : parse $ tk "foo") : unit := () + +foo + +@[user_command] +meta def foo_cmd (_ : parse $ tk "foo") : parser unit := +trace "foo" + +run_cmd skip + +foo +private foo + +@[user_command] +meta def foo_cmd2 (_ : parse $ tk "foo") : parser unit := +trace "bar" + +foo + +@[user_command] +meta def foo_cmd3 (dmi : decl_meta_info) (_ : parse $ tk "foo") : parser unit := +trace format!"{dmi.modifiers.is_private}" + +foo +private foo diff --git a/tests/lean/user_command.lean.expected.out b/tests/lean/user_command.lean.expected.out new file mode 100644 index 0000000000..b3ea31f733 --- /dev/null +++ b/tests/lean/user_command.lean.expected.out @@ -0,0 +1,11 @@ +user_command.lean:8:5: error: invalid user-defined command, must take `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.decl_meta_info` parameter +user_command.lean:8:5: warning: declaration 'foo_cmd' uses sorry +user_command.lean:14:0: error: unknown identifier 'foo' +user_command.lean:12:5: error: invalid user-defined command, must return type `lean.parser unit` +user_command.lean:12:50: error: function expected at + () +foo +user_command.lean:23:8: error: command does not accept modifiers +bar +ff +tt