From 492cb20438ad7254469a8cd1926d4367356baf42 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 17 Jun 2017 18:46:42 +0200 Subject: [PATCH] feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env --- library/init/meta/interactive_base.lean | 35 ++++++++ library/init/meta/lean/parser.lean | 2 + src/frontends/lean/inductive_cmds.cpp | 9 +-- src/frontends/lean/inductive_cmds.h | 13 +++ src/frontends/lean/parser.h | 1 + src/library/vm/vm_option.h | 6 ++ src/library/vm/vm_parser.cpp | 103 ++++++++++++++++++++++++ src/library/vm/vm_parser.h | 2 + 8 files changed, 166 insertions(+), 5 deletions(-) diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean index 70743f486d..aeb8da5e20 100644 --- a/library/init/meta/interactive_base.lean +++ b/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 diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean index 84a198b15a..2a0ecba96a 100644 --- a/library/init/meta/lean/parser.lean +++ b/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 diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 963425b77b..7c4340abd5 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/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() { diff --git a/src/frontends/lean/inductive_cmds.h b/src/frontends/lean/inductive_cmds.h index 7fa1417338..7d06446b03 100644 --- a/src/frontends/lean/inductive_cmds.h +++ b/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 m_intros; +}; + +struct inductive_decl { + buffer m_lp_names; + buffer m_params; + buffer 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); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 088665989e..f3d0f4e984 100644 --- a/src/frontends/lean/parser.h +++ b/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; diff --git a/src/library/vm/vm_option.h b/src/library/vm/vm_option.h index bacf66cd88..4d8f275c3d 100644 --- a/src/library/vm/vm_option.h +++ b/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 +vm_obj to_obj(optional 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); } } diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index d2caabfc4c..b7de3ac266 100644 --- a/src/library/vm/vm_parser.cpp +++ b/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(to_external(o))); + return static_cast(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 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() { diff --git a/src/library/vm/vm_parser.h b/src/library/vm/vm_parser.h index 4e583f984b..6fe548b03d 100644 --- a/src/library/vm/vm_parser.h +++ b/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(); }