feat(frontends/lean/user_command): add user-defined commands

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)

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();

src/frontends/lean/notation_cmd.cpp

@@ -318,7 +318,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> 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)

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<unsigned> get_fingerprint(entry const &) {
         return optional<unsigned>();
@@ -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<cmd_ext>(ext));
+}
+
 void initialize_parser_config() {
     token_config::g_class_name = new name("notation");
     token_ext::initialize();

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<unsigned> 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);

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 <string>
+#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<vm_obj> 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<modification const> deserialize(deserializer & d) {
+        return std::make_shared<user_command_modification>(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<user_command_modification>(d));
+                } else {
+                    throw exception("[user_command] cannot be used locally");
+                }
+            }));
+}
+void finalize_user_command() {
+    user_command_modification::finalize();
+}
+}

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();
+}

src/library/vm/vm_parser.cpp

@@ -42,9 +42,10 @@ typedef interaction_monad<lean_parser_state> 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<vm_obj> 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) {

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<vm_obj> const & args = {});
 expr parse_interactive_param(parser & p, expr const & param_ty);
 
 vm_obj to_obj(cmd_meta const & meta);

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

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