From 0779db7ae9e78f55606b244fce91e003ff98254d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 16:56:11 -0700 Subject: [PATCH] fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions Signed-off-by: Leonardo de Moura --- src/kernel/declaration.cpp | 4 ++-- src/kernel/declaration.h | 4 ++-- src/library/kernel_serializer.cpp | 6 +++--- src/library/kernel_serializer.h | 2 +- src/library/module.cpp | 1 + 5 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 19af64aac..47197cd18 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -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); } -declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) { - return declaration(new declaration::cell(n, params, t, true, v, true, 0, 0, false)); +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, mod_idx, false)); } declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { return declaration(new declaration::cell(n, params, t, true)); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 8feff1e15..62bb30b19 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -71,7 +71,7 @@ public: 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, 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_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); 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); -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_var_decl(name const & n, level_param_names const & params, expr const & t); } diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 4fa9ee405..ed024ffd9 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -277,7 +277,7 @@ serializer & operator<<(serializer & s, declaration const & d) { return s; } -declaration read_declaration(deserializer & d, unsigned module_idx) { +declaration read_declaration(deserializer & d, module_idx midx) { char k = d.read_char(); bool has_value = (k & 1) != 0; bool is_th_ax = (k & 8) != 0; @@ -287,12 +287,12 @@ declaration read_declaration(deserializer & d, unsigned module_idx) { if (has_value) { expr v = read_expr(d); if (is_th_ax) { - return mk_theorem(n, ps, t, v); + return mk_theorem(n, ps, t, v, midx); } else { unsigned w = d.read_unsigned(); bool is_opaque = (k & 2) != 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 { if (is_th_ax) diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h index cfa06f8f6..4ce48eee0 100644 --- a/src/library/kernel_serializer.h +++ b/src/library/kernel_serializer.h @@ -28,7 +28,7 @@ struct register_macro_deserializer_fn { }; 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> inductive_decls; serializer & operator<<(serializer & s, inductive_decls const & ds); diff --git a/src/library/module.cpp b/src/library/module.cpp index 63842df68..0211c54e5 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -265,6 +265,7 @@ struct import_modules_fn { void import_decl(deserializer & d, module_idx midx) { declaration decl = read_declaration(d, midx); + lean_assert(!decl.is_definition() || decl.get_module_idx() == midx); environment env = m_senv.env(); if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { if (!m_keep_proofs && decl.is_theorem())