max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean): must set m_gen_code = false for auxiliary declarations of extern declarations

Browse source 
We cannot check the `[extern]` attribute because the auxiliary
declarations are compiled before we even define the main declaration
and set the attribute.
We should consider a better design in the future where we first define
all auxiliary and main definitions, then set the attributes, and then
compile the code.

cc @kha
This commit is contained in:
Leonardo de Moura 2019-02-12 17:49:33 -08:00
parent cd4b8c0c28
commit f41e4dac72
5 changed files with 32 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/decl_attributes.cpp
View file

@ -60,7 +60,7 @@ void decl_attributes::parse_core(parser & p, bool compact) {
if (!is_attribute(p.env(), id))
throw parser_error(sstream() << "unknown attribute [" << id << "]", pos);
auto const & attr = get_attribute(p.env(), id);
auto const & attr = ::lean::get_attribute(p.env(), id);
if (!deleted) {
for (auto const & entry : m_entries) {
if (!entry.deleted() && are_incompatible(*entry.m_attr, attr)) {
@ -104,11 +104,22 @@ void decl_attributes::parse_compact(parser & p) {
void decl_attributes::set_attribute(environment const & env, name const & attr_name, attr_data_ptr data) {
if (!is_attribute(env, attr_name))
throw exception(sstream() << "unknown attribute [" << attr_name << "]");
auto const & attr = get_attribute(env, attr_name);
auto const & attr = ::lean::get_attribute(env, attr_name);
entry e = {&attr, data};
m_entries = append(m_entries, to_list(e));
}
attr_data_ptr decl_attributes::get_attribute(environment const & env, name const & attr_name) const {
if (!is_attribute(env, attr_name))
throw exception(sstream() << "unknown attribute [" << attr_name << "]");
auto const & attr = ::lean::get_attribute(env, attr_name);
for (entry const & e : m_entries) {
if (e.m_attr == &attr)
return e.m_params;
}
return nullptr;
}
environment decl_attributes::apply(environment env, io_state const & ios, name const & d) const {
buffer<entry> entries;
to_buffer(m_entries, entries);

1
src/frontends/lean/decl_attributes.h
View file

@ -28,6 +28,7 @@ private:
public:
decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
void set_attribute(environment const & env, name const & attr_name, attr_data_ptr data = get_default_attr_data());
attr_data_ptr get_attribute(environment const & env, name const & attr_name) const;
/* attributes: zero-or-more [ ... ] */
void parse(parser & p);
/* Parse attributes after `@[` ... ] */

14
src/frontends/lean/decl_util.cpp
View file

@ -407,12 +407,13 @@ struct definition_info {
bool m_is_noncomputable{false};
bool m_is_lemma{false};
bool m_aux_lemmas{false};
bool m_gen_code{true};
unsigned m_next_match_idx{1};
};
MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers) {
declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers, bool is_extern) {
definition_info & info = get_definition_info();
lean_assert(info.m_prefix.is_anonymous());
info.m_prefix = name(); // prefix is used to create local name
@ -426,11 +427,15 @@ declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind ki
info.m_is_noncomputable = modifiers.m_is_noncomputable;
info.m_is_lemma = kind == decl_cmd_kind::Theorem;
info.m_aux_lemmas = kind != decl_cmd_kind::Theorem && !modifiers.m_is_meta;
info.m_next_match_idx = 1;
info.m_gen_code = !is_extern;
info.m_next_match_idx = 1;
}
declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers):
declaration_info_scope(get_namespace(p.env()), kind, modifiers) {}
declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers, bool is_extern):
declaration_info_scope(get_namespace(p.env()), kind, modifiers, is_extern) {}
declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, cmd_meta const & meta):
declaration_info_scope(p, kind, meta.m_modifiers, static_cast<bool>(meta.m_attrs.get_attribute(p.env(), "extern"))) {}
declaration_info_scope::~declaration_info_scope() {
get_definition_info() = definition_info();
@ -450,6 +455,7 @@ equations_header mk_equations_header(names const & ns, names const & actual_ns)
h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
h.m_gen_code = get_definition_info().m_gen_code;
return h;
}

8
src/frontends/lean/decl_util.h
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_attributes.h"
namespace lean {
struct parser;
struct cmd_meta;
class elaborator;
enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var, Abbreviation };
@ -33,9 +34,12 @@ struct decl_modifiers {
It is used to set/restore the thread local information. */
class declaration_info_scope {
declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers);
declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers, bool is_extern);
public:
declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers);
declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers, bool is_extern);
declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers):
declaration_info_scope(p, kind, modifiers, false) {}
declaration_info_scope(parser const & p, decl_cmd_kind kind, cmd_meta const & meta);
~declaration_info_scope();
bool gen_aux_lemmas() const;
};

4
src/frontends/lean/definition_cmds.cpp
View file

@ -278,7 +278,7 @@ static environment elab_defs_core(parser & p, decl_cmd_kind kind, cmd_meta const
}
static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta const & meta) {
declaration_info_scope scope(p, kind, meta.m_modifiers);
declaration_info_scope scope(p, kind, meta);
buffer<name> lp_names;
buffer<expr> fns, params;
/* TODO(Leo): allow a different doc string for each function in a mutual definition. */
@ -612,7 +612,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
buffer<expr> params;
expr fn, val;
auto header_pos = p.pos();
declaration_info_scope scope(p, kind, meta.m_modifiers);
declaration_info_scope scope(p, kind, meta);
environment env = p.env();
private_name_scope prv_scope(meta.m_modifiers.m_is_private, env);
p.set_env(env);