From ead4e8998da9d54e7975baadecd894032ac97621 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 19 Dec 2018 14:49:53 +0100 Subject: [PATCH] feat(library/init/lean/elaborator): elaborate constants --- library/init/lean/elaborator.lean | 71 ++++++++++++++++++++-------- src/frontends/lean/vm_elaborator.cpp | 66 +++++++++++++++++++++----- src/runtime/optional.h | 4 ++ 3 files changed, 109 insertions(+), 32 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 89bed1fa03..54268d5da9 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -293,6 +293,47 @@ def to_pexpr : syntax → elaborator_m expr | _ := error stx $ "unexpected node: " ++ to_string k.name) | stx := error stx $ "unexpected: " ++ to_string stx +def old_elab_command (stx : syntax) (cmd : expr) : elaborator_m unit := +do cfg ← read, + st ← get, + match elaborate_command cfg.filename cmd { + univs := st.local_state.univs.entries, + vars := st.local_state.vars.entries, + include_vars := st.local_state.include_vars.to_list, + ..st} with + | except.ok st' := put { + local_state := {st.local_state with + univs := ordered_rbmap.of_list st'.univs, + vars := ordered_rbmap.of_list st'.vars, + include_vars := rbtree.of_list st'.include_vars, + }, + ..st', ..st} + | except.error e := error stx e + +def attrs_to_pexpr (attrs : list (sep_by.elem.view attr_instance.view (option syntax_atom))) : elaborator_m expr := +expr.mk_capp `_ <$> attrs.mmap (λ attr, + expr.mk_capp (mangle_ident attr.item.name) <$> attr.item.args.mmap to_pexpr) + +def decl_modifiers_to_pexpr (mods : decl_modifiers.view) : elaborator_m expr := do + let mdata : kvmap := {}, + let mdata := match mods.doc_comment with + | some {doc := some doc, ..} := mdata.set_string `doc_string doc.val + | _ := mdata, + let mdata := match mods.visibility with + | some (visibility.view.private _) := mdata.set_bool `private tt + | some (visibility.view.protected _) := mdata.set_bool `protected tt + | _ := mdata, + let mdata := mdata.set_bool `noncomputable mods.noncomputable.is_some, + let mdata := mdata.set_bool `meta mods.meta.is_some, + expr.mdata mdata <$> attrs_to_pexpr (match mods.attrs with + | some attrs := attrs.attrs + | none := []) + +def ident_univ_params_to_pexpr (id : ident_univ_params.view) : expr := +expr.const (mangle_ident id.id) $ match id.univ_params with + | some params := params.params.map (level.param ∘ mangle_ident) + | none := [] + /-- Execute `elab` and reset local state (universes, ...) after it has finished. -/ @[specialize] def locally {m : Type → Type} [monad m] [monad_state elaborator_state m] (elab : m unit) : m unit := do @@ -303,8 +344,16 @@ def to_pexpr : syntax → elaborator_m expr def declaration.elaborate : elaborator := locally $ λ stx, do let decl := view «declaration» stx, - -- just test `to_pexpr` for now match decl.inner with + | declaration.inner.view.constant c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do + let mdata := kvmap.set_name {} `command `constant, + mods ← decl_modifiers_to_pexpr decl.modifiers, + let id := ident_univ_params_to_pexpr c.name, + type ← to_pexpr type.type, + old_elab_command stx $ expr.mdata mdata $ expr.mk_capp `_ [mods, id, type] + | declaration.inner.view.constant _ := + error stx "declration.elaborate: unexpected input" + -- just test `to_pexpr` for now | declaration.inner.view.def_like dl@{ val := decl_val.view.simple val, sig := {params := bracketed_binders.view.simple bbs}, ..} := do @@ -508,30 +557,12 @@ def universe.elaborate : elaborator := | none := put {st with local_state := {st.local_state with univs := st.local_state.univs.insert id (level.param id)}} | some _ := error stx $ "a universe named '" ++ to_string id ++ "' has already been declared in this scope" -def old_elab_command (stx : syntax) (cmd : expr) : elaborator_m unit := -do cfg ← read, - st ← get, - match elaborate_command cfg.filename cmd { - univs := st.local_state.univs.entries, - vars := st.local_state.vars.entries, - include_vars := st.local_state.include_vars.to_list, - ..st} with - | except.ok st' := put { - local_state := {st.local_state with - univs := ordered_rbmap.of_list st'.univs, - vars := ordered_rbmap.of_list st'.vars, - include_vars := rbtree.of_list st'.include_vars, - }, - ..st', ..st} - | except.error e := error stx e - def attribute.elaborate : elaborator := λ stx, do let attr := view «attribute» stx, let mdata := kvmap.set_name {} `command `attribute, let mdata := mdata.set_bool `local $ attr.local.is_some, - attrs ← expr.mk_capp `_ <$> attr.attrs.mmap (λ attr, - expr.mk_capp (mangle_ident attr.item.name) <$> attr.item.args.mmap to_pexpr), + attrs ← attrs_to_pexpr attr.attrs, let ids := expr.mk_capp `_ $ attr.ids.map $ λ id, expr.const (mangle_ident id) [], old_elab_command stx $ expr.mdata mdata $ expr.app attrs ids diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index 46a38af033..2b5f5ea328 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -TEMPORARY code for the old runtime +Lean interface to the old elaborator/elaboration parts of the parser */ #include @@ -17,35 +17,72 @@ TEMPORARY code for the old runtime #include "library/vm/vm_nat.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/parser.h" +#include "frontends/lean/decl_cmds.h" namespace lean { +decl_attributes to_decl_attributes(environment const & env, expr const & e, bool local) { + decl_attributes attributes(!local); + buffer args; + get_app_args(e, args); + for (auto const & e : args) + attributes.set_attribute(env, const_name(e)); + return attributes; +} + environment elab_attribute_cmd(environment env, expr const & cmd) { auto const & data = mdata_data(cmd); bool local = *get_bool(data, "local"); - decl_attributes attributes(!local); buffer args, eattrs, eids; get_app_args(mdata_expr(cmd), args); - get_app_args(args[0], eattrs); + auto attributes = to_decl_attributes(env, args[0], local); get_app_args(args[1], eids); - for (auto const & e : eattrs) - attributes.set_attribute(env, const_name(e)); for (auto const & e : eids) env = attributes.apply(env, get_dummy_ios(), const_name(e)); return env; } +cmd_meta to_cmd_meta(environment const & env, expr const & e) { + auto const & data = mdata_data(e); + cmd_meta m(to_decl_attributes(env, mdata_expr(e), false)); + m.m_modifiers.m_is_meta = get_bool(data, "meta").value_or(false); + m.m_modifiers.m_is_mutual = get_bool(data, "mutual").value_or(false); + m.m_modifiers.m_is_noncomputable = get_bool(data, "noncomputable").value_or(false); + m.m_modifiers.m_is_private = get_bool(data, "private").value_or(false); + m.m_modifiers.m_is_protected = get_bool(data, "protected").value_or(false); + if (auto s = get_string(data, "doc_string")) + m.m_doc_string = s->to_std_string(); + return m; +} + +void elab_constant_cmd(parser & p, expr const & cmd) { + buffer args, ls; + get_app_args(mdata_expr(cmd), args); + auto fn = get_app_args(args[1], ls); + buffer ls_buffer; + for (auto const & e : ls) + ls_buffer.push_back(const_name(e)); + p.set_env(elab_var(p, variable_kind::Constant, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd), + optional(), const_name(fn), args[2], ls_buffer)); +} + void elaborate_command(parser & p, expr const & cmd) { auto const & data = mdata_data(cmd); if (auto const & cmd_name = get_name(data, "command")) { if (*cmd_name == "attribute") { p.set_env(elab_attribute_cmd(p.env(), cmd)); return; + } else if (*cmd_name == "constant") { + elab_constant_cmd(p, cmd); + return; } } throw elaborator_exception(cmd, "unexpected input to 'elaborate_command'"); } +/* TEMPORARY code for the old runtime */ + + struct vm_env : public vm_external { environment m_env; @@ -165,11 +202,11 @@ expr to_expr(vm_obj const & o) { case 5: return mk_app(to_expr(cfield(o, 0)), to_expr(cfield(o, 1))); case 6: - return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), - to_binder_info(cfield(o, 3))); + return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)), + to_binder_info(cfield(o, 1))); case 7: - return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), - to_binder_info(cfield(o, 3))); + return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)), + to_binder_info(cfield(o, 1))); case 8: return mk_let(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3))); case 9: { @@ -239,8 +276,9 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v lean_vm_check(dynamic_cast(to_external(vm_e))); auto env = static_cast(to_external(vm_e))->m_env; io_state const & ios = get_dummy_ios(); + auto filename = to_string(vm_filename); std::stringstream in; - parser p(env, ios, in, to_string(vm_filename)); + parser p(env, ios, in, filename); auto s = p.mk_snapshot(); auto ngen = to_name_generator(cfield(vm_st, 1)); auto vm_lds = cfield(vm_st, 2); @@ -270,8 +308,9 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false, parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info {1, 0})); + auto cmd = to_expr(vm_cmd); try { - elaborate_command(p, to_expr(vm_cmd)); + elaborate_command(p, cmd); s = p.mk_snapshot(); auto vm_st2 = mk_vm_constructor(0, { mk_vm_external(new vm_env(env)), @@ -285,7 +324,10 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v }); return mk_vm_constructor(1, vm_st); } catch (exception & e) { - return mk_vm_constructor(0, to_obj(std::string(e.what()))); + message_builder builder(env, ios, filename, get_pos_info_provider()->get_pos_info_or_some(cmd), + message_severity::ERROR); + builder.set_exception(e); + return mk_vm_constructor(0, to_obj(builder.build().get_text())); } } diff --git a/src/runtime/optional.h b/src/runtime/optional.h index 1c1da00b27..6b096511c8 100644 --- a/src/runtime/optional.h +++ b/src/runtime/optional.h @@ -55,6 +55,10 @@ public: T const & value() const { lean_assert(m_some); return m_value; } T & value() { lean_assert(m_some); return m_value; } + T const & value_or(T const & default_value) const { + return m_some ? m_value : default_value; + } + template void emplace(Args&&... args) { if (m_some)