michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-16 16:56:11 -07:00
parent 73b7a44c84
commit 0779db7ae9
5 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/declaration.cpp
View file

@ -81,8 +81,8 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
}); });
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt); return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
} }
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) { declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx) {
return declaration(new declaration::cell(n, params, t, true, v, true, 0, 0, false)); return declaration(new declaration::cell(n, params, t, true, v, true, 0, mod_idx, false));
} }
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true)); return declaration(new declaration::cell(n, params, t, true));

4
src/kernel/declaration.h
View file

@ -71,7 +71,7 @@ public:
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt); expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque, friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt); unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t); friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
}; };
@ -84,7 +84,7 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true); bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true); bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t); declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
} }

6
src/library/kernel_serializer.cpp
View file

@ -277,7 +277,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
return s; return s;
} }
declaration read_declaration(deserializer & d, unsigned module_idx) { declaration read_declaration(deserializer & d, module_idx midx) {
char k = d.read_char(); char k = d.read_char();
bool has_value = (k & 1) != 0; bool has_value = (k & 1) != 0;
bool is_th_ax = (k & 8) != 0; bool is_th_ax = (k & 8) != 0;
@ -287,12 +287,12 @@ declaration read_declaration(deserializer & d, unsigned module_idx) {
if (has_value) { if (has_value) {
expr v = read_expr(d); expr v = read_expr(d);
if (is_th_ax) { if (is_th_ax) {
return mk_theorem(n, ps, t, v); return mk_theorem(n, ps, t, v, midx);
} else { } else {
unsigned w = d.read_unsigned(); unsigned w = d.read_unsigned();
bool is_opaque = (k & 2) != 0; bool is_opaque = (k & 2) != 0;
bool use_conv_opt = (k & 4) != 0; bool use_conv_opt = (k & 4) != 0;
return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt); return mk_definition(n, ps, t, v, is_opaque, w, midx, use_conv_opt);
} }
} else { } else {
if (is_th_ax) if (is_th_ax)

2
src/library/kernel_serializer.h
View file

@ -28,7 +28,7 @@ struct register_macro_deserializer_fn {
}; };
serializer & operator<<(serializer & s, declaration const & d); serializer & operator<<(serializer & s, declaration const & d);
declaration read_declaration(deserializer & d, unsigned module_idx); declaration read_declaration(deserializer & d, module_idx midx);
typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls; typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls;
serializer & operator<<(serializer & s, inductive_decls const & ds); serializer & operator<<(serializer & s, inductive_decls const & ds);

1
src/library/module.cpp
View file

@ -265,6 +265,7 @@ struct import_modules_fn {
void import_decl(deserializer & d, module_idx midx) { void import_decl(deserializer & d, module_idx midx) {
declaration decl = read_declaration(d, midx); declaration decl = read_declaration(d, midx);
lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
environment env = m_senv.env(); environment env = m_senv.env();
if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
if (!m_keep_proofs && decl.is_theorem()) if (!m_keep_proofs && decl.is_theorem())