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

fix(library/module): module index assignment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-05 23:32:18 -07:00
parent 8e5ac54ae1
commit 9be1a4ab46
2 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/declaration.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include <algorithm> #include <algorithm>
#include <string> #include <string>
#include <limits>
#include "util/rc.h" #include "util/rc.h"
#include "kernel/expr.h" #include "kernel/expr.h"
@ -23,7 +24,8 @@ namespace lean {
*/ */
typedef unsigned module_idx; typedef unsigned module_idx;
/** \brief The main module is the module being currently compiled. We always assigned it the index 0. */ /** \brief The main module is the module being currently compiled. We always assigned it the index 0. */
constexpr unsigned g_main_module_idx = 0; constexpr module_idx g_main_module_idx = 0;
constexpr module_idx g_null_module_idx = std::numeric_limits<unsigned>::max();
/** \brief Environment definitions, theorems, axioms and variable declarations. */ /** \brief Environment definitions, theorems, axioms and variable declarations. */
class declaration { class declaration {

7
src/library/module.cpp
View file

@ -166,6 +166,7 @@ struct import_modules_fn {
std::vector<asynch_update_fn> m_asynch_tasks; std::vector<asynch_update_fn> m_asynch_tasks;
mutex m_delayed_mutex; mutex m_delayed_mutex;
std::vector<delayed_update> m_delayed_tasks; std::vector<delayed_update> m_delayed_tasks;
atomic<unsigned> m_next_module_idx;
atomic<unsigned> m_import_counter; // number of modules to be processed atomic<unsigned> m_import_counter; // number of modules to be processed
atomic<bool> m_all_modules_imported; atomic<bool> m_all_modules_imported;
@ -183,7 +184,7 @@ struct import_modules_fn {
import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios): import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios):
m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios), m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios),
m_import_counter(0), m_all_modules_imported(false) { m_next_module_idx(1), m_import_counter(0), m_all_modules_imported(false) {
if (m_num_threads == 0) if (m_num_threads == 0)
m_num_threads = 1; m_num_threads = 1;
#if !defined(LEAN_MULTI_THREAD) #if !defined(LEAN_MULTI_THREAD)
@ -231,8 +232,7 @@ struct import_modules_fn {
r->m_name = mname; r->m_name = mname;
r->m_fname = fname; r->m_fname = fname;
r->m_counter = imports.size(); r->m_counter = imports.size();
r->m_module_idx = m_import_counter+1; // importate modules have idx > 0, we reserve idx 0 for new module r->m_module_idx = g_null_module_idx;
lean_assert(r->m_module_idx != g_main_module_idx);
m_import_counter++; m_import_counter++;
std::swap(r->m_obj_code, code); std::swap(r->m_obj_code, code);
m_module_info.insert(mname, r); m_module_info.insert(mname, r);
@ -302,6 +302,7 @@ struct import_modules_fn {
} }
void import_module(module_info_ptr const & r) { void import_module(module_info_ptr const & r) {
r->m_module_idx = m_next_module_idx++;
std::string s(r->m_obj_code.data(), r->m_obj_code.size()); std::string s(r->m_obj_code.data(), r->m_obj_code.size());
std::istringstream in(s, std::ios_base::binary); std::istringstream in(s, std::ios_base::binary);
deserializer d(in); deserializer d(in);