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

fix(msvc): change previous MSVC workaround to change the code less

Browse source
This commit is contained in:
Nuno Lopes 2018-02-01 16:04:04 +00:00 • committed by Leonardo de Moura
parent 9c756e24d3
commit d01e2d7ae8
4 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/vm_compiler.cpp
View file

@ -344,9 +344,9 @@ public:
};
buffer<name> extern_names(environment const & env, buffer<procedure> const & procs) {
used_defs live_names(env, [&] (used_defs & live_names, declaration const & d) {
used_defs live_names{env, [&] (declaration const & d) {
live_names.names_in_decl(d);
});
}};
for (auto p : procs) {
live_names.names_in_preprocessed_body(p.m_code);

8
src/library/native_compiler/native_compiler.cpp
View file

@ -359,7 +359,7 @@ void native_compile_module(environment const & env, buffer<declaration> decls) {
// Compute the live set of names, we attach a callback that will be
// invoked for every declaration encountered.
used_defs used_names(env, [&] (used_defs & used_names, declaration const & d) {
used_defs used_names{env, [&] (declaration const & d) {
buffer<procedure> procs;
// The the name is an internal decl we should not add it to the live set.
if (is_internal_decl(d)) {
@ -379,7 +379,7 @@ void native_compile_module(environment const & env, buffer<declaration> decls) {
all_procs.push_back(pair);
}
}
});
}};
// We then loop over the set of procs produced by preprocessing the
// main function, we transitively collect all names.
@ -416,7 +416,7 @@ void native_compile_binary(environment const & env, declaration const & d) {
// Compute the live set of names, we attach a callback that will be
// invoked for every declaration encountered.
used_defs used_names(env, [&] (used_defs & used_names, declaration const & d) {
used_defs used_names{env, [&] (declaration const & d) {
buffer<procedure> procs;
if (is_internal_decl(d)) {
return;
@ -432,7 +432,7 @@ void native_compile_binary(environment const & env, declaration const & d) {
all_procs.push_back(pair);
}
}
});
}};
// We then loop over the set of procs produced by preprocessing the
// main function, we transitively collect all names.

4
src/library/native_compiler/used_defs.cpp
View file

@ -17,7 +17,7 @@ Author: Jared Roesch
#include "library/native_compiler/used_defs.h"
namespace lean {
used_defs::used_defs(environment const & env, std::function<void(used_defs &, declaration const &)> action) : m_env(env) {
used_defs::used_defs(environment const & env, std::function<void(declaration const &)> action) : m_env(env) {
this->m_used_names = name_set();
this->m_names_to_process = std::vector<name>();
this->m_action = action;
@ -40,7 +40,7 @@ void used_defs::empty_stack() {
// Is a definition and not a synthetic compiler name.
auto d = this->m_env.find(n);
if (d && d.value().is_definition()) {
m_action(*this, d.value());
m_action(d.value());
}
}
}

4
src/library/native_compiler/used_defs.h
View file

@ -20,9 +20,9 @@ struct used_defs {
name_set m_used_names;
std::vector<name> m_names_to_process;
environment const & m_env;
std::function<void(used_defs &, declaration const &)> m_action;
std::function<void(declaration const &)> m_action;
used_defs(environment const & env, std::function<void(used_defs &, declaration const &)>);
used_defs(environment const & env, std::function<void(declaration const &)>);
void names_in_decl(declaration const & d);
void names_in_expr(expr const & e);
void names_in_preprocessed_body(expr const & e);