feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env

library/init/meta/interactive_base.lean

@@ -140,6 +140,41 @@ meta def param_desc : expr → tactic format
 | e := if is_constant e ∧ (const_name e).components.ilast = `itactic
   then return $ to_fmt "{ tactic }"
   else paren <$> pp e
+
+
+meta constant decl_attributes : Type
+
+meta constant decl_attributes.apply : decl_attributes → name → parser unit
+
+meta structure decl_modifiers :=
+(is_private       : bool)
+(is_protected     : bool)
+(is_meta          : bool)
+(is_mutual        : bool)
+(is_noncomputable : bool)
+
+meta structure decl_meta_info :=
+(attrs      : decl_attributes)
+(modifiers  : decl_modifiers)
+(doc_string : option string)
+
+
+meta structure single_inductive_decl :=
+(attrs  : decl_attributes)
+(sig    : expr)
+(intros : list expr)
+
+meta def single_inductive_decl.name (d : single_inductive_decl) : name :=
+d.sig.app_fn.const_name
+
+meta structure inductive_decl :=
+(u_names     : list name)
+(params      : list expr)
+(decls       : list single_inductive_decl)
+
+/-- Parses and elaborates a single or multiple mutual inductive declarations (without the `inductive` keyword), depending on `is_mutual` -/
+meta constant inductive_decl.parse : decl_meta_info → parser inductive_decl
+
 end interactive
 
 section macros

library/init/meta/lean/parser.lean

@@ -23,6 +23,8 @@ open interaction_monad.result
 namespace parser
 variable {α : Type}
 
+meta constant set_env : environment → parser unit
+
 /-- Make sure the next token is an identifier, consume it, and
     produce the quoted name `t, where t is the identifier. -/
 meta constant ident : parser name

src/frontends/lean/inductive_cmds.cpp

@@ -569,6 +569,7 @@ class inductive_cmd_fn {
         declaration_name_scope nscope;
         expr ind = parse_single_header(m_p, nscope, m_lp_names, params);
         m_explicit_levels = !m_lp_names.empty();
+        m_mut_attrs.push_back({});
 
         ind = mk_local(get_namespace(m_p.env()) + mlocal_name(ind), mlocal_name(ind), mlocal_type(ind), local_info(ind));
 
@@ -661,11 +662,9 @@ public:
             if (m_meta_info.m_doc_string)
                 m_env = add_doc_string(m_env, mlocal_name(ind), *m_meta_info.m_doc_string);
         }
-        if (!m_mut_attrs.empty()) {
-            lean_assert(new_inds.size() == m_mut_attrs.size());
-            for (unsigned i = 0; i < new_inds.size(); ++i)
-                m_env = m_mut_attrs[i].apply(m_env, m_p.ios(), mlocal_name(new_inds[i]));
-        }
+        lean_assert(new_inds.size() == m_mut_attrs.size());
+        for (unsigned i = 0; i < new_inds.size(); ++i)
+            m_env = m_mut_attrs[i].apply(m_env, m_p.ios(), mlocal_name(new_inds[i]));
     }
 
     environment inductive_cmd() {

src/frontends/lean/inductive_cmds.h

@@ -8,6 +8,19 @@ Author: Daniel Selsam
 #include "frontends/lean/cmd_table.h"
 #include "frontends/lean/decl_attributes.h"
 namespace lean {
+struct single_inductive_decl {
+    decl_attributes m_attrs;
+    expr            m_expr;
+    buffer<expr>    m_intros;
+};
+
+struct inductive_decl {
+    buffer<name>                  m_lp_names;
+    buffer<expr>                  m_params;
+    buffer<single_inductive_decl> m_decls;
+};
+
+inductive_decl parse_inductive_decl(parser & p, cmd_meta const & meta);
 environment inductive_cmd(parser & p, cmd_meta const & meta);
 environment coinductive_cmd(parser & p, cmd_meta const & meta);
 

src/frontends/lean/parser.h

@@ -212,6 +212,7 @@ public:
     cmd_table const & cmds() const { return get_cmd_table(env()); }
 
     environment const & env() const { return m_env; }
+    void set_env(environment const & env) { m_env = env; }
     io_state const & ios() const { return m_ios; }
 
     message_builder mk_message(pos_info const & p, message_severity severity) const;

src/library/vm/vm_option.h

@@ -10,6 +10,12 @@ Author: Leonardo de Moura
 namespace lean {
 inline vm_obj mk_vm_none() { return mk_vm_simple(0); }
 inline vm_obj mk_vm_some(vm_obj const & a) { return mk_vm_constructor(1, 1, &a); }
+
+template<typename T>
+vm_obj to_obj(optional<T> const & o) {
+    return o ? mk_vm_some(to_obj(*o)) : mk_vm_none();
+}
+
 inline bool is_none(vm_obj const & o) { return is_simple(o); }
 inline vm_obj get_some_value(vm_obj const & o) { lean_assert(!is_none(o)); return cfield(o, 0); }
 }

src/library/vm/vm_parser.cpp

@@ -25,6 +25,7 @@ Author: Sebastian Ullrich
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/inductive_cmds.h"
 #include "util/utf8.h"
 
 namespace lean {
@@ -76,6 +77,72 @@ expr parse_interactive_param(parser & p, expr const & param_ty) {
     }
 }
 
+struct vm_decl_attributes : public vm_external {
+    decl_attributes m_val;
+    vm_decl_attributes(decl_attributes const & v):m_val(v) {}
+    virtual ~vm_decl_attributes() {}
+    virtual void dealloc() override { this->~vm_decl_attributes(); get_vm_allocator().deallocate(sizeof(vm_decl_attributes), this); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_decl_attributes(m_val); }
+    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_decl_attributes))) vm_decl_attributes(m_val); }
+};
+
+static decl_attributes const & to_decl_attributes(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_decl_attributes*>(to_external(o)));
+    return static_cast<vm_decl_attributes*>(to_external(o))->m_val;
+}
+
+static vm_obj to_obj(decl_attributes const & n) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_decl_attributes))) vm_decl_attributes(n));
+}
+
+static vm_obj to_obj(decl_modifiers const & mods) {
+    return mk_vm_constructor(0, {
+            mk_vm_bool(mods.m_is_private),
+            mk_vm_bool(mods.m_is_protected),
+            mk_vm_bool(mods.m_is_meta),
+            mk_vm_bool(mods.m_is_mutual),
+            mk_vm_bool(mods.m_is_noncomputable),
+    });
+}
+
+vm_obj to_obj(cmd_meta const & meta) {
+    return mk_vm_constructor(0, {
+            to_obj(meta.m_attrs),
+            to_obj(meta.m_modifiers),
+            to_obj(meta.m_doc_string)
+    });
+}
+
+decl_modifiers to_decl_modifiers(vm_obj const & o) {
+    lean_always_assert(cidx(o) == 0);
+    decl_modifiers mods;
+    if (to_bool(cfield(o, 0))) {
+        mods.m_is_private = true;
+    }
+    if (to_bool(cfield(o, 1))) {
+        mods.m_is_protected = true;
+    }
+    if (to_bool(cfield(o, 2))) {
+        mods.m_is_meta = true;
+    }
+    if (to_bool(cfield(o, 3))) {
+        mods.m_is_mutual = true;
+    }
+    if (to_bool(cfield(o, 4))) {
+        mods.m_is_noncomputable = true;
+    }
+    return mods;
+}
+
+cmd_meta to_cmd_meta(vm_obj const & o) {
+    lean_always_assert(cidx(o) == 0);
+    optional<std::string> doc_string;
+    if (!is_none(cfield(o, 2))) {
+        doc_string = some(to_string(get_some_value(cfield(o, 2))));
+    }
+    return {to_decl_attributes(cfield(o, 0)), to_decl_modifiers(cfield(o, 1)), doc_string};
+}
+
 vm_obj vm_parser_state_env(vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
     return to_obj(s.m_p->env());
@@ -91,6 +158,12 @@ vm_obj vm_parser_state_cur_pos(vm_obj const & o) {
     return to_obj(s.m_p->pos());
 }
 
+vm_obj vm_parser_set_env(vm_obj const & vm_env, vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    s.m_p->set_env(to_env(vm_env));
+    return lean_parser::mk_success(s);
+}
+
 vm_obj vm_parser_ident(vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
     TRY;
@@ -189,17 +262,47 @@ vm_obj vm_parser_with_input(vm_obj const &, vm_obj const & vm_p, vm_obj const &
     return lean_parser::mk_result(vm_res, lean_parser::get_result_state(vm_state));
 }
 
+static vm_obj interactive_decl_attributes_apply(vm_obj const & vm_attrs, vm_obj const & vm_n, vm_obj const & vm_s) {
+    auto s = lean_parser::to_state(vm_s);
+    TRY;
+        auto env = to_decl_attributes(vm_attrs).apply(s.m_p->env(), get_dummy_ios(), to_name(vm_n));
+        s.m_p->set_env(env);
+        return lean_parser::mk_success({s.m_p});
+    CATCH;
+}
+
+static vm_obj to_obj(single_inductive_decl const & d) {
+    return mk_vm_constructor(0, {to_obj(d.m_attrs), to_obj(d.m_expr), to_obj(d.m_intros)});
+}
+
+static vm_obj to_obj(inductive_decl const & d) {
+    return mk_vm_constructor(0, {to_obj(d.m_lp_names), to_obj(d.m_params),
+                                 to_vm_list(to_list(d.m_decls), [](single_inductive_decl const & d) { return to_obj(d); })});
+}
+
+static vm_obj interactive_inductive_decl_parse(vm_obj const & vm_meta, vm_obj const & vm_s) {
+    auto s = lean_parser::to_state(vm_s);
+    TRY;
+        auto decl = parse_inductive_decl(*s.m_p, to_cmd_meta(vm_meta));
+        return lean_parser::mk_success(to_obj(decl), s);
+    CATCH;
+}
+
 void initialize_vm_parser() {
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "env"}),         vm_parser_state_env);
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "options"}),     vm_parser_state_options);
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),     vm_parser_state_cur_pos);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),             vm_parser_ident);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "set_env"}),           vm_parser_set_env);
     DECLARE_VM_BUILTIN(get_lean_parser_tk_name(),                     vm_parser_tk);
     DECLARE_VM_BUILTIN(get_lean_parser_pexpr_name(),                  vm_parser_pexpr);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),             vm_parser_qexpr);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "skip_info"}),         vm_parser_skip_info);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "with_input"}),        vm_parser_with_input);
+
+    DECLARE_VM_BUILTIN(name({"interactive", "decl_attributes", "apply"}), interactive_decl_attributes_apply);
+    DECLARE_VM_BUILTIN(name({"interactive", "inductive_decl", "parse"}),  interactive_inductive_decl_parse);
 }
 
 void finalize_vm_parser() {

src/library/vm/vm_parser.h

@@ -12,6 +12,8 @@ namespace lean {
 vm_obj run_parser(parser & p, expr const & spec);
 expr parse_interactive_param(parser & p, expr const & param_ty);
 
+vm_obj to_obj(cmd_meta const & meta);
+
 void initialize_vm_parser();
 void finalize_vm_parser();
 }